[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
⊢ Fibration (InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd) (DFinsupp.Lex r s) fun x =>
    piecewise x.snd.fst x.snd.snd x.fst
[PROOFSTEP]
rintro ⟨p, x₁, x₂⟩ x ⟨i, hr, hs⟩
[GOAL]
case mk.mk.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = ↑((fun x => piecewise x.snd.fst x.snd.snd x.fst) (p, x₁, x₂)) j
hs : s i (↑x i) (↑((fun x => piecewise x.snd.fst x.snd.snd x.fst) (p, x₁, x₂)) i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x => piecewise x.snd.fst x.snd.snd x.fst) a' = x
[PROOFSTEP]
simp_rw [piecewise_apply] at hs hr
[GOAL]
case mk.mk.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hs : s i (↑x i) (if i ∈ p then ↑x₁ i else ↑x₂ i)
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x => piecewise x.snd.fst x.snd.snd x.fst) a' = x
[PROOFSTEP]
split_ifs at hs  with hp
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x => piecewise x.snd.fst x.snd.snd x.fst) a' = x
[PROOFSTEP]
refine ⟨⟨{j | r j i → j ∈ p}, piecewise x₁ x {j | r j i}, x₂⟩, .fst ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩
[GOAL]
case pos.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
hj : r j i
⊢ ↑(piecewise x₁ x {j | r j i}) j = ↑x₁ j
[PROOFSTEP]
simp only [piecewise_apply, Set.mem_setOf_eq]
[GOAL]
case pos.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
⊢ (fun {i} => s i) (↑(piecewise x₁ x {j | r j i}) i) (↑x₁ i)
[PROOFSTEP]
simp only [piecewise_apply, Set.mem_setOf_eq]
[GOAL]
case pos.refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
⊢ (fun x => piecewise x.snd.fst x.snd.snd x.fst) ({j | r j i → j ∈ p}, piecewise x₁ x {j | r j i}, x₂) = x
[PROOFSTEP]
simp only [piecewise_apply, Set.mem_setOf_eq]
[GOAL]
case pos.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
hj : r j i
⊢ (if r j i then ↑x₁ j else ↑x j) = ↑x₁ j
[PROOFSTEP]
simp only [if_pos hj]
[GOAL]
case pos.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
⊢ s i (if r i i then ↑x₁ i else ↑x i) (↑x₁ i)
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
hi : r i i
⊢ s i (↑x₁ i) (↑x₁ i)
[PROOFSTEP]
rwa [hr i hi, if_pos hp] at hs
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
hi : ¬r i i
⊢ s i (↑x i) (↑x₁ i)
[PROOFSTEP]
assumption
[GOAL]
case pos.refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
⊢ piecewise (piecewise x₁ x {j | r j i}) x₂ {j | r j i → j ∈ p} = x
[PROOFSTEP]
ext1 j
[GOAL]
case pos.refine_3.h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
⊢ ↑(piecewise (piecewise x₁ x {j | r j i}) x₂ {j | r j i → j ∈ p}) j = ↑x j
[PROOFSTEP]
simp only [piecewise_apply, Set.mem_setOf_eq]
[GOAL]
case pos.refine_3.h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
⊢ (if r j i → j ∈ p then if r j i then ↑x₁ j else ↑x j else ↑x₂ j) = ↑x j
[PROOFSTEP]
split_ifs with h₁ h₂
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
h₁ : r j i → j ∈ p
h₂ : r j i
⊢ ↑x₁ j = ↑x j
[PROOFSTEP]
try rfl
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
h₁ : r j i → j ∈ p
h₂ : r j i
⊢ ↑x₁ j = ↑x j
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
h₁ : r j i → j ∈ p
h₂ : ¬r j i
⊢ ↑x j = ↑x j
[PROOFSTEP]
try rfl
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
h₁ : r j i → j ∈ p
h₂ : ¬r j i
⊢ ↑x j = ↑x j
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
h₁ : ¬(r j i → j ∈ p)
⊢ ↑x₂ j = ↑x j
[PROOFSTEP]
try rfl
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
h₁ : ¬(r j i → j ∈ p)
⊢ ↑x₂ j = ↑x j
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
h₁ : r j i → j ∈ p
h₂ : r j i
⊢ ↑x₁ j = ↑x j
[PROOFSTEP]
rw [hr j h₂, if_pos (h₁ h₂)]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
h₁ : ¬(r j i → j ∈ p)
⊢ ↑x₂ j = ↑x j
[PROOFSTEP]
rw [not_imp] at h₁
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : i ∈ p
hs : s i (↑x i) (↑x₁ i)
j : ι
h₁ : r j i ∧ ¬j ∈ p
⊢ ↑x₂ j = ↑x j
[PROOFSTEP]
rw [hr j h₁.1, if_neg h₁.2]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x => piecewise x.snd.fst x.snd.snd x.fst) a' = x
[PROOFSTEP]
refine ⟨⟨{j | r j i ∧ j ∈ p}, x₁, piecewise x₂ x {j | r j i}⟩, .snd ⟨i, fun j hj ↦ ?_, ?_⟩, ?_⟩
[GOAL]
case neg.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
hj : r j i
⊢ ↑(piecewise x₂ x {j | r j i}) j = ↑x₂ j
[PROOFSTEP]
simp only [piecewise_apply, Set.mem_setOf_eq]
[GOAL]
case neg.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
⊢ (fun {i} => s i) (↑(piecewise x₂ x {j | r j i}) i) (↑x₂ i)
[PROOFSTEP]
simp only [piecewise_apply, Set.mem_setOf_eq]
[GOAL]
case neg.refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
⊢ (fun x => piecewise x.snd.fst x.snd.snd x.fst) ({j | r j i ∧ j ∈ p}, x₁, piecewise x₂ x {j | r j i}) = x
[PROOFSTEP]
simp only [piecewise_apply, Set.mem_setOf_eq]
[GOAL]
case neg.refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
hj : r j i
⊢ (if r j i then ↑x₂ j else ↑x j) = ↑x₂ j
[PROOFSTEP]
exact if_pos hj
[GOAL]
case neg.refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
⊢ s i (if r i i then ↑x₂ i else ↑x i) (↑x₂ i)
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
hi : r i i
⊢ s i (↑x₂ i) (↑x₂ i)
[PROOFSTEP]
rwa [hr i hi, if_neg hp] at hs
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
hi : ¬r i i
⊢ s i (↑x i) (↑x₂ i)
[PROOFSTEP]
assumption
[GOAL]
case neg.refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
⊢ piecewise x₁ (piecewise x₂ x {j | r j i}) {j | r j i ∧ j ∈ p} = x
[PROOFSTEP]
ext1 j
[GOAL]
case neg.refine_3.h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
⊢ ↑(piecewise x₁ (piecewise x₂ x {j | r j i}) {j | r j i ∧ j ∈ p}) j = ↑x j
[PROOFSTEP]
simp only [piecewise_apply, Set.mem_setOf_eq]
[GOAL]
case neg.refine_3.h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
⊢ (if r j i ∧ j ∈ p then ↑x₁ j else if r j i then ↑x₂ j else ↑x j) = ↑x j
[PROOFSTEP]
split_ifs with h₁ h₂
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
h₁ : r j i ∧ j ∈ p
⊢ ↑x₁ j = ↑x j
[PROOFSTEP]
try rfl
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
h₁ : r j i ∧ j ∈ p
⊢ ↑x₁ j = ↑x j
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ ↑x₂ j = ↑x j
[PROOFSTEP]
try rfl
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ ↑x₂ j = ↑x j
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : ¬r j i
⊢ ↑x j = ↑x j
[PROOFSTEP]
try rfl
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : ¬r j i
⊢ ↑x j = ↑x j
[PROOFSTEP]
rfl
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
h₁ : r j i ∧ j ∈ p
⊢ ↑x₁ j = ↑x j
[PROOFSTEP]
rw [hr j h₁.1, if_pos h₁.2]
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ ↑x₂ j = ↑x j
[PROOFSTEP]
rw [hr j h₂, if_neg]
[GOAL]
case pos.hnc
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → ↑x j = if j ∈ p then ↑x₁ j else ↑x₂ j
hp : ¬i ∈ p
hs : s i (↑x i) (↑x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ ¬j ∈ p
[PROOFSTEP]
simpa [h₂] using h₁
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (↑x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
classical
convert ← @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{ i }, _⟩ (InvImage.accessible snd <| hs.prod_gameAdd hu)
convert piecewise_single_erase x i
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (↑x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
convert ← @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{ i }, _⟩ (InvImage.accessible snd <| hs.prod_gameAdd hu)
[GOAL]
case h.e'_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (DFinsupp.Lex r s) (single i (↑x i))
hu : Acc (DFinsupp.Lex r s) (erase i x)
⊢ piecewise ({i}, single i (↑x i), erase i x).snd.fst ({i}, single i (↑x i), erase i x).snd.snd
      ({i}, single i (↑x i), erase i x).fst =
    x
[PROOFSTEP]
convert piecewise_single_erase x i
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
⊢ (∀ (i : ι), i ∈ support x → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
generalize ht : x.support = t
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
t : Finset ι
ht : support x = t
⊢ (∀ (i : ι), i ∈ t → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
revert x
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
t : Finset ι
⊢ ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
classical
induction' t using Finset.induction with b t hb ih
· intro x ht
  rw [support_eq_empty.1 ht]
  exact fun _ => Lex.acc_zero hbot
refine' fun x ht h => Lex.acc_of_single_erase b (h b <| t.mem_insert_self b) _
refine' ih _ (by rw [support_erase, ht, Finset.erase_insert hb]) fun a ha => _
rw [erase_ne (ha.ne_of_not_mem hb)]
exact h a (Finset.mem_insert_of_mem ha)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
t : Finset ι
⊢ ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
induction' t using Finset.induction with b t hb ih
[GOAL]
case empty
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ ∀ (x : Π₀ (i : ι), α i),
    support x = ∅ → (∀ (i : ι), i ∈ ∅ → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
intro x ht
[GOAL]
case empty
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : support x = ∅
⊢ (∀ (i : ι), i ∈ ∅ → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
rw [support_eq_empty.1 ht]
[GOAL]
case empty
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : support x = ∅
⊢ (∀ (i : ι), i ∈ ∅ → Acc (DFinsupp.Lex r s) (single i (↑0 i))) → Acc (DFinsupp.Lex r s) 0
[PROOFSTEP]
exact fun _ => Lex.acc_zero hbot
[GOAL]
case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
⊢ ∀ (x : Π₀ (i : ι), α i),
    support x = insert b t →
      (∀ (i : ι), i ∈ insert b t → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
refine' fun x ht h => Lex.acc_of_single_erase b (h b <| t.mem_insert_self b) _
[GOAL]
case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (DFinsupp.Lex r s) (single i (↑x i))
⊢ Acc (DFinsupp.Lex r s) (erase b x)
[PROOFSTEP]
refine' ih _ (by rw [support_erase, ht, Finset.erase_insert hb]) fun a ha => _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (DFinsupp.Lex r s) (single i (↑x i))
⊢ support (erase b x) = t
[PROOFSTEP]
rw [support_erase, ht, Finset.erase_insert hb]
[GOAL]
case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (DFinsupp.Lex r s) (single i (↑x i))
a : ι
ha : a ∈ t
⊢ Acc (DFinsupp.Lex r s) (single a (↑(erase b x) a))
[PROOFSTEP]
rw [erase_ne (ha.ne_of_not_mem hb)]
[GOAL]
case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : ¬b ∈ t
ih :
  ∀ (x : Π₀ (i : ι), α i),
    support x = t → (∀ (i : ι), i ∈ t → Acc (DFinsupp.Lex r s) (single i (↑x i))) → Acc (DFinsupp.Lex r s) x
x : Π₀ (i : ι), α i
ht : support x = insert b t
h : ∀ (i : ι), i ∈ insert b t → Acc (DFinsupp.Lex r s) (single i (↑x i))
a : ι
ha : a ∈ t
⊢ Acc (DFinsupp.Lex r s) (single a (↑x a))
[PROOFSTEP]
exact h a (Finset.mem_insert_of_mem ha)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i : ι
hi : Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) i
⊢ ∀ (a : α i), Acc (DFinsupp.Lex r s) (single i a)
[PROOFSTEP]
induction' hi with i _ ih
[GOAL]
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
⊢ ∀ (a : α i), Acc (DFinsupp.Lex r s) (single i a)
[PROOFSTEP]
refine fun a => WellFounded.induction (hs i) (C := fun x ↦ Acc (DFinsupp.Lex r s) (single i x)) a fun a ha ↦ ?_
[GOAL]
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
⊢ (fun x => Acc (DFinsupp.Lex r s) (single i x)) a
[PROOFSTEP]
refine Acc.intro _ fun x ↦ ?_
[GOAL]
case intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
⊢ DFinsupp.Lex r s x (single i a) → Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
rintro ⟨k, hr, hs⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hs : s k (↑x k) (↑(single i a) k)
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
rw [single_apply] at hs
[GOAL]
case intro.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hs : s k (↑x k) (if h : i = k then Eq.recOn h a else 0)
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
split_ifs at hs  with hik
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : i = k
hs : s k (↑x k) (Eq.recOn hik a)
⊢ Acc (DFinsupp.Lex r s) x
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : ¬i = k
hs : s k (↑x k) 0
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
swap
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : ¬i = k
hs : s k (↑x k) 0
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
exact (hbot hs).elim
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
k : ι
hr : ∀ (j : ι), r j k → ↑x j = ↑(single i a) j
hik : i = k
hs : s k (↑x k) (Eq.recOn hik a)
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
subst hik
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
classical
refine Lex.acc_of_single hbot x fun j hj ↦ ?_
obtain rfl | hij := eq_or_ne i j
· exact ha _ hs
by_cases r j i
· rw [hr j h, single_eq_of_ne hij, single_zero]
  exact Lex.acc_zero hbot
· exact ih _ ⟨h, hij.symm⟩ _
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
refine Lex.acc_of_single hbot x fun j hj ↦ ?_
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
⊢ Acc (DFinsupp.Lex r fun i a => s i a) (single j (↑x j))
[PROOFSTEP]
obtain rfl | hij := eq_or_ne i j
[GOAL]
case pos.inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
hj : i ∈ support x
⊢ Acc (DFinsupp.Lex r fun i a => s i a) (single i (↑x i))
[PROOFSTEP]
exact ha _ hs
[GOAL]
case pos.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
⊢ Acc (DFinsupp.Lex r fun i a => s i a) (single j (↑x j))
[PROOFSTEP]
by_cases r j i
[GOAL]
case pos.inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
⊢ Acc (DFinsupp.Lex r fun i a => s i a) (single j (↑x j))
[PROOFSTEP]
by_cases r j i
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
h : r j i
⊢ Acc (DFinsupp.Lex r fun i a => s i a) (single j (↑x j))
[PROOFSTEP]
rw [hr j h, single_eq_of_ne hij, single_zero]
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
h : r j i
⊢ Acc (DFinsupp.Lex r fun i a => s i a) 0
[PROOFSTEP]
exact Lex.acc_zero hbot
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs✝ : ∀ (i : ι), WellFounded (s i)
inst✝ : DecidableEq ι
i✝ i : ι
h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y
ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)
a✝ a : α i
ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → ↑x j = ↑(single i a) j
hs : s i (↑x i) (Eq.recOn (_ : i = i) a)
j : ι
hj : j ∈ support x
hij : i ≠ j
h : ¬r j i
⊢ Acc (DFinsupp.Lex r fun i a => s i a) (single j (↑x j))
[PROOFSTEP]
exact ih _ ⟨h, hij.symm⟩ _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
hr : WellFounded (rᶜ ⊓ fun x x_1 => x ≠ x_1)
x : Π₀ (i : ι), α i
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
classical exact Lex.acc hbot hs x fun i _ => hr.apply i
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
hr : WellFounded (rᶜ ⊓ fun x x_1 => x ≠ x_1)
x : Π₀ (i : ι), α i
⊢ Acc (DFinsupp.Lex r s) x
[PROOFSTEP]
exact Lex.acc hbot hs x fun i _ => hr.apply i
[GOAL]
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
⊢ WellFounded (Pi.Lex r fun {i} => s i)
[PROOFSTEP]
obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
h : IsEmpty ((i : ι) → α i)
⊢ WellFounded (Pi.Lex r fun {i} => s i)
[PROOFSTEP]
convert emptyWf.wf
[GOAL]
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
⊢ WellFounded (Pi.Lex r fun {i} => s i)
[PROOFSTEP]
letI : ∀ i, Zero (α i) := fun i => ⟨(hs i).min ⊤ ⟨x i, trivial⟩⟩
[GOAL]
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
⊢ WellFounded (Pi.Lex r fun {i} => s i)
[PROOFSTEP]
haveI := IsTrans.swap r
[GOAL]
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝ : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this : IsTrans ι (Function.swap r)
⊢ WellFounded (Pi.Lex r fun {i} => s i)
[PROOFSTEP]
haveI := IsIrrefl.swap r
[GOAL]
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝¹ : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝ : IsTrans ι (Function.swap r)
this : IsIrrefl ι (Function.swap r)
⊢ WellFounded (Pi.Lex r fun {i} => s i)
[PROOFSTEP]
haveI := Fintype.ofFinite ι
[GOAL]
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝² : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝¹ : IsTrans ι (Function.swap r)
this✝ : IsIrrefl ι (Function.swap r)
this : Fintype ι
⊢ WellFounded (Pi.Lex r fun {i} => s i)
[PROOFSTEP]
refine' InvImage.wf equivFunOnFintype.symm (Lex.wellFounded' (fun i a => _) hs _)
[GOAL]
case inr.intro.refine'_1
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝² : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝¹ : IsTrans ι (Function.swap r)
this✝ : IsIrrefl ι (Function.swap r)
this : Fintype ι
i : ι
a : α i
⊢ ¬s i a 0
case inr.intro.refine'_2
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : IsStrictTotalOrder ι r
inst✝ : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this✝² : (i : ι) → Zero (α i) := fun i => { zero := WellFounded.min (_ : WellFounded (s i)) ⊤ (_ : ∃ x, x ∈ ⊤) }
this✝¹ : IsTrans ι (Function.swap r)
this✝ : IsIrrefl ι (Function.swap r)
this : Fintype ι
⊢ WellFounded (Function.swap fun j i => r j i)
[PROOFSTEP]
exacts [(hs i).not_lt_min ⊤ _ trivial, Finite.wellFounded_of_trans_of_irrefl (Function.swap r)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
set β := fun i ↦ Antisymmetrization (α i) (· ≤ ·)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
set e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization (· ≤ ·)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
let _ : ∀ i, Zero (β i) := fun i ↦ ⟨e i 0⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
have : WellFounded (DFinsupp.Lex (Function.swap <| @WellOrderingRel ι) (fun _ ↦ (· < ·) : (i : ι) → β i → β i → Prop))
[GOAL]
case this
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
⊢ WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)
[PROOFSTEP]
have := IsTrichotomous.swap (@WellOrderingRel ι)
[GOAL]
case this
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
⊢ WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)
[PROOFSTEP]
refine Lex.wellFounded' ?_ (fun i ↦ IsWellFounded.wf) ?_
[GOAL]
case this.refine_1
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
⊢ ∀ ⦃i : ι⦄ ⦃a : β i⦄, ¬a < 0
[PROOFSTEP]
rintro i ⟨a⟩
[GOAL]
case this.refine_1.mk
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
i : ι
a✝ : β i
a : α i
⊢ ¬Quot.mk Setoid.r a < 0
[PROOFSTEP]
apply hbot
[GOAL]
case this.refine_2
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
⊢ WellFounded (Function.swap (Function.swap WellOrderingRel))
[PROOFSTEP]
simp only [Function.swap]
[GOAL]
case this.refine_2
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
⊢ WellFounded fun y x => WellOrderingRel y x
[PROOFSTEP]
exact IsWellFounded.wf
[GOAL]
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
refine Subrelation.wf (fun h => ?_) <| InvImage.wf (mapRange (fun i ↦ e i) fun _ ↦ rfl) this
[GOAL]
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝¹ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)
x✝ y✝ : Π₀ (i : ι), α i
h : x✝ < y✝
⊢ InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)
    (mapRange (fun i => e i) (_ : ∀ (x : ι), (fun i => e i) x 0 = (fun i => e i) x 0)) x✝ y✝
[PROOFSTEP]
have := IsStrictOrder.swap (@WellOrderingRel ι)
[GOAL]
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝¹ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this✝ : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)
x✝ y✝ : Π₀ (i : ι), α i
h : x✝ < y✝
this : IsStrictOrder ι (Function.swap WellOrderingRel)
⊢ InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)
    (mapRange (fun i => e i) (_ : ∀ (x : ι), (fun i => e i) x 0 = (fun i => e i) x 0)) x✝ y✝
[PROOFSTEP]
obtain ⟨i, he, hl⟩ := lex_lt_of_lt_of_preorder (Function.swap WellOrderingRel) h
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1
x✝¹ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this✝ : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)
x✝ y✝ : Π₀ (i : ι), α i
h : x✝ < y✝
this : IsStrictOrder ι (Function.swap WellOrderingRel)
i : ι
he : ∀ (j : ι), Function.swap WellOrderingRel j i → ↑x✝ j ≤ ↑y✝ j ∧ ↑y✝ j ≤ ↑x✝ j
hl : ↑x✝ i < ↑y✝ i
⊢ InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)
    (mapRange (fun i => e i) (_ : ∀ (x : ι), (fun i => e i) x 0 = (fun i => e i) x 0)) x✝ y✝
[PROOFSTEP]
exact ⟨i, fun j hj ↦ Quot.sound (he j hj), hl⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)
[GOAL]
case inl
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
h : IsEmpty ((i : ι) → α i)
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
convert emptyWf.wf
[GOAL]
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
x : (i : ι) → α i
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
letI : ∀ i, Zero (α i) := fun i => ⟨(hw i).wf.min ⊤ ⟨x i, trivial⟩⟩
[GOAL]
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
x : (i : ι) → α i
this : (i : ι) → Zero (α i) :=
  fun i => { zero := WellFounded.min (_ : WellFounded fun x x_1 => x < x_1) ⊤ (_ : ∃ x, x ∈ ⊤) }
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
haveI := Fintype.ofFinite ι
[GOAL]
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
x : (i : ι) → α i
this✝ : (i : ι) → Zero (α i) :=
  fun i => { zero := WellFounded.min (_ : WellFounded fun x x_1 => x < x_1) ⊤ (_ : ∃ x, x ∈ ⊤) }
this : Fintype ι
⊢ WellFounded fun x x_1 => x < x_1
[PROOFSTEP]
refine' InvImage.wf equivFunOnFintype.symm (DFinsupp.wellFoundedLT fun i a => _).wf
[GOAL]
case inr.intro
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝¹ : Finite ι
inst✝ : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT (α i)
x : (i : ι) → α i
this✝ : (i : ι) → Zero (α i) :=
  fun i => { zero := WellFounded.min (_ : WellFounded fun x x_1 => x < x_1) ⊤ (_ : ∃ x, x ∈ ⊤) }
this : Fintype ι
i : ι
a : α i
⊢ ¬a < 0
[PROOFSTEP]
exact (hw i).wf.not_lt_min ⊤ _ trivial


[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f✝ g✝ f g : Π₀ (a : α), N a
a : α
⊢ a ∈ neLocus f g ↔ ↑f a ≠ ↑g a
[PROOFSTEP]
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff, and_iff_right_iff_imp] using Ne.ne_or_ne _
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f✝ g✝ f g : Π₀ (a : α), N a
h : f = g
⊢ neLocus f f = ∅
[PROOFSTEP]
simp only [neLocus, Ne.def, eq_self_iff_true, not_true, Finset.filter_False]
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
⊢ neLocus f g = neLocus g f
[PROOFSTEP]
simp_rw [neLocus, Finset.union_comm, ne_comm]
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
⊢ neLocus f 0 = support f
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
a✝ : α
⊢ a✝ ∈ neLocus f 0 ↔ a✝ ∈ support f
[PROOFSTEP]
rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
a : α
⊢ a ∈ neLocus (mapRange F F0 f) (mapRange F F0 g) → a ∈ neLocus f g
[PROOFSTEP]
simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg (F a)
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a f g
⊢ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) = neLocus g₁ g₂
[PROOFSTEP]
ext a
[GOAL]
case a
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a f g
a : α
⊢ a ∈ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) ↔ a ∈ neLocus g₁ g₂
[PROOFSTEP]
simpa only [mem_neLocus] using (hF a _).ne_iff
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (M a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective fun f => F a f g
⊢ neLocus (zipWith F F0 f₁ g) (zipWith F F0 f₂ g) = neLocus f₁ f₂
[PROOFSTEP]
ext a
[GOAL]
case a
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (M a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective fun f => F a f g
a : α
⊢ a ∈ neLocus (zipWith F F0 f₁ g) (zipWith F F0 f₂ g) ↔ a ∈ neLocus f₁ f₂
[PROOFSTEP]
simpa only [mem_neLocus] using (hF a _).ne_iff
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
hF : ∀ (a : α), Function.Injective (F a)
⊢ neLocus (mapRange F F0 f) (mapRange F F0 g) = neLocus f g
[PROOFSTEP]
ext a
[GOAL]
case a
α : Type u_1
N : α → Type u_2
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
hF : ∀ (a : α), Function.Injective (F a)
a : α
⊢ a ∈ neLocus (mapRange F F0 f) (mapRange F F0 g) ↔ a ∈ neLocus f g
[PROOFSTEP]
simpa only [mem_neLocus] using (hF a).ne_iff
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a
⊢ neLocus (-f) g = neLocus f (-g)
[PROOFSTEP]
rw [← neLocus_neg_neg, neg_neg]
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a
⊢ neLocus f g = support (f - g)
[PROOFSTEP]
rw [← @neLocus_add_right α N _ _ _ _ _ (-g), add_right_neg, neLocus_zero_right, sub_eq_add_neg]
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a
⊢ neLocus (f - g₁) (f - g₂) = neLocus g₁ g₂
[PROOFSTEP]
simp only [sub_eq_add_neg, @neLocus_add_left α N _ _ _, neLocus_neg_neg]
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a
⊢ neLocus (f₁ - g) (f₂ - g) = neLocus f₁ f₂
[PROOFSTEP]
simpa only [sub_eq_add_neg] using @neLocus_add_right α N _ _ _ _ _ _
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a
⊢ neLocus f (f + g) = support g
[PROOFSTEP]
rw [← neLocus_zero_left, ← @neLocus_add_left α N _ _ _ f 0 g, add_zero]
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a
⊢ neLocus (f + g) f = support g
[PROOFSTEP]
rw [neLocus_comm, neLocus_self_add_right]
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a
⊢ neLocus f (f - g) = support g
[PROOFSTEP]
rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
[GOAL]
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a
⊢ neLocus (f - g) f = support g
[PROOFSTEP]
rw [neLocus_comm, neLocus_self_sub_right]


[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (α i)
s✝ : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ Function.Injective fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)
[PROOFSTEP]
refine' (mk_injective _).comp fun f g h => _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (α i)
s✝ : Finset ι
f✝ : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
f g : (a : ι) → a ∈ s → α a
h : (fun i => f ↑i (_ : ↑i ∈ ↑s)) = fun i => g ↑i (_ : ↑i ∈ ↑s)
⊢ f = g
[PROOFSTEP]
ext i hi
[GOAL]
case h.h
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (α i)
s✝ : Finset ι
f✝ : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
f g : (a : ι) → a ∈ s → α a
h : (fun i => f ↑i (_ : ↑i ∈ ↑s)) = fun i => g ↑i (_ : ↑i ∈ ↑s)
i : ι
hi : i ∈ s
⊢ f i hi = g i hi
[PROOFSTEP]
convert congr_fun h ⟨i, hi⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ f ∈ dfinsupp s t ↔ support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
[PROOFSTEP]
refine' mem_map.trans ⟨_, _⟩
[GOAL]
case refine'_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (∃ a,
      a ∈ pi s t ∧
        ↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
            a =
          f) →
    support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
[PROOFSTEP]
rintro ⟨f, hf, rfl⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → (fun i => α i) a
hf : f ∈ pi s t
⊢ support
        (↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
              inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
          f) ⊆
      s ∧
    ∀ (i : ι),
      i ∈ s →
        ↑(↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                    inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
                f)
            i ∈
          t i
[PROOFSTEP]
rw [Function.Embedding.coeFn_mk]
  -- porting note: added to avoid heartbeat timeout
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → (fun i => α i) a
hf : f ∈ pi s t
⊢ support (DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) ⊆ s ∧
    ∀ (i : ι), i ∈ s → ↑(DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i ∈ t i
[PROOFSTEP]
refine' ⟨support_mk_subset, fun i hi => _⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → (fun i => α i) a
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i ∈ t i
[PROOFSTEP]
convert mem_pi.1 hf i hi
[GOAL]
case h.e'_4
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
f : (a : ι) → a ∈ s → (fun i => α i) a
hf : f ∈ pi s t
i : ι
hi : i ∈ s
⊢ ↑(DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s)) i = f i hi
[PROOFSTEP]
exact mk_of_mem hi
[GOAL]
case refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
⊢ (support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i) →
    ∃ a,
      a ∈ pi s t ∧
        ↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
                inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
            a =
          f
[PROOFSTEP]
refine' fun h => ⟨fun i _ => f i, mem_pi.2 h.2, _⟩
[GOAL]
case refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
⊢ (↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
          inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
      fun i x => ↑f i) =
    f
[PROOFSTEP]
ext i
[GOAL]
case refine'_2.h
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ ↑(↑{ toFun := fun f => DFinsupp.mk s fun i => f ↑i (_ : ↑i ∈ ↑s),
              inj' := (_ : Function.Injective (DFinsupp.mk s ∘ fun f i => f ↑i (_ : ↑i ∈ ↑s))) }
          fun i x => ↑f i)
      i =
    ↑f i
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2.h
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
h : support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i
i : ι
⊢ (if i ∈ s then ↑f i else 0) = ↑f i
[PROOFSTEP]
exact ite_eq_left_iff.2 fun hi => (not_mem_support_iff.1 fun H => hi <| h.1 H).symm
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
⊢ f ∈ dfinsupp s ↑t ↔ ∀ (i : ι), ↑f i ∈ ↑t i
[PROOFSTEP]
refine'
  mem_dfinsupp_iff.trans
    (forall_and.symm.trans <|
      forall_congr' fun i =>
        ⟨fun h => _, fun h => ⟨fun hi => ht <| mem_support_iff.2 fun H => mem_support_iff.1 hi _, fun _ => h⟩⟩)
[GOAL]
case refine'_1
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
by_cases hi : i ∈ s
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : i ∈ s
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
exact h.2 hi
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ ↑f i ∈ ↑t i
[PROOFSTEP]
rw [not_mem_support_iff.1 (mt h.1 hi), not_mem_support_iff.1 (not_mem_mono ht hi)]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : (i ∈ support f → i ∈ s) ∧ (i ∈ s → ↑f i ∈ ↑t i)
hi : ¬i ∈ s
⊢ 0 ∈ 0
[PROOFSTEP]
exact zero_mem_zero
[GOAL]
case refine'_2
ι : Type u_1
α : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (α i)
s : Finset ι
f : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
inst✝ : (i : ι) → DecidableEq (α i)
t : Π₀ (i : ι), Finset (α i)
ht : support t ⊆ s
i : ι
h : ↑f i ∈ ↑t i
hi : i ∈ support f
H : ↑t i = 0
⊢ ↑f i = 0
[PROOFSTEP]
rwa [H, mem_zero] at h
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ toFun f i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ toFun g i = 0 }
i : ι
h : ¬i ∈ ↑fs + ↑gs
⊢ (fun i => Icc (↑f i) (↑g i)) i = 0
[PROOFSTEP]
have hf : f i = 0 :=
  (fs.prop i).resolve_left (Multiset.not_mem_mono (Multiset.Le.subset <| Multiset.le_add_right _ _) h)
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ toFun f i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ toFun g i = 0 }
i : ι
h : ¬i ∈ ↑fs + ↑gs
hf : ↑f i = 0
⊢ (fun i => Icc (↑f i) (↑g i)) i = 0
[PROOFSTEP]
have hg : g i = 0 :=
  (gs.prop i).resolve_left
    (Multiset.not_mem_mono (Multiset.Le.subset <| Multiset.le_add_left _ _) h)
      -- porting note: was rw, but was rewriting under lambda, so changed to simp_rw
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ toFun f i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ toFun g i = 0 }
i : ι
h : ¬i ∈ ↑fs + ↑gs
hf : ↑f i = 0
hg : ↑g i = 0
⊢ (fun i => Icc (↑f i) (↑g i)) i = 0
[PROOFSTEP]
simp_rw [hf, hg]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f✝ g✝ : Π₀ (i : ι), α i
i✝ : ι
a : α i✝
f g : Π₀ (i : ι), α i
fs : { s // ∀ (i : ι), i ∈ s ∨ toFun f i = 0 }
gs : { s // ∀ (i : ι), i ∈ s ∨ toFun g i = 0 }
i : ι
h : ¬i ∈ ↑fs + ↑gs
hf : ↑f i = 0
hg : ↑g i = 0
⊢ Icc 0 0 = 0
[PROOFSTEP]
exact Icc_self _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
i : ι
a : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
⊢ support (rangeIcc f g) ⊆ support f ∪ support g
[PROOFSTEP]
refine' fun x hx => _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
i : ι
a : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ support (rangeIcc f g)
⊢ x ∈ support f ∪ support g
[PROOFSTEP]
by_contra h
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
i : ι
a : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ support (rangeIcc f g)
h : ¬x ∈ support f ∪ support g
⊢ False
[PROOFSTEP]
refine' not_mem_support_iff.2 _ hx
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
i : ι
a : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ support (rangeIcc f g)
h : ¬x ∈ support f ∪ support g
⊢ ↑(rangeIcc f g) x = 0
[PROOFSTEP]
rw [rangeIcc_apply, not_mem_support_iff.1 (not_mem_mono (subset_union_left _ _) h),
  not_mem_support_iff.1 (not_mem_mono (subset_union_right _ _) h)]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → Zero (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
i : ι
a : α i
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
x : ι
hx : x ∈ support (rangeIcc f g)
h : ¬x ∈ support f ∪ support g
⊢ Icc 0 0 = 0
[PROOFSTEP]
exact Icc_self _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ card (pi f) = prod f fun i => ↑(card (↑f i))
[PROOFSTEP]
rw [pi, card_dfinsupp]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ ∏ i in support f, card (↑f i) = prod f fun i => ↑(card (↑f i))
[PROOFSTEP]
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.nat_apply, Nat.cast_id]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
i : ι
x✝ : i ∈ support f
⊢ card (↑f i) = (fun i => ↑(card (↑f i))) i (↑f i)
[PROOFSTEP]
simp only [Pi.nat_apply, Nat.cast_id]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ x ∈ (fun f g => dfinsupp (support f ∪ support g) ↑(rangeIcc f g)) f g ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
refine' (mem_dfinsupp_iff_of_support_subset <| support_rangeIcc_subset).trans _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ (∀ (i : ι), ↑x i ∈ ↑(rangeIcc f g) i) ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
simp_rw [mem_rangeIcc_apply_iff, forall_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g x : Π₀ (i : ι), α i
⊢ ((∀ (x_1 : ι), ↑f x_1 ≤ ↑x x_1) ∧ ∀ (x_1 : ι), ↑x x_1 ≤ ↑g x_1) ↔ f ≤ x ∧ x ≤ g
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (Ico f g) = ∏ i in support f ∪ support g, card (Icc (↑f i) (↑g i)) - 1
[PROOFSTEP]
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (Ioc f g) = ∏ i in support f ∪ support g, card (Icc (↑f i) (↑g i)) - 1
[PROOFSTEP]
rw [card_Ioc_eq_card_Icc_sub_one, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (Ioo f g) = ∏ i in support f ∪ support g, card (Icc (↑f i) (↑g i)) - 2
[PROOFSTEP]
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (uIcc f g) = ∏ i in support f ∪ support g, card (uIcc (↑f i) (↑g i))
[PROOFSTEP]
rw [← support_inf_union_support_sup]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → Lattice (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ card (uIcc f g) = ∏ i in support (f ⊓ g) ∪ support (f ⊔ g), card (uIcc (↑f i) (↑g i))
[PROOFSTEP]
exact card_Icc _ _
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ card (Iic f) = ∏ i in support f, card (Iic (↑f i))
[PROOFSTEP]
simp_rw [Iic_eq_Icc, card_Icc, DFinsupp.bot_eq_zero, support_zero, empty_union, zero_apply, bot_eq_zero]
[GOAL]
ι : Type u_1
α : ι → Type u_2
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ card (Iio f) = ∏ i in support f, card (Iic (↑f i)) - 1
[PROOFSTEP]
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]


[GOAL]
⊢ SuccOrder (Fin 0)
[PROOFSTEP]
constructor
[GOAL]
case le_succ
⊢ ∀ (a : Fin 0), a ≤ ?succ a
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case le_succ
⊢ ∀ (a : Fin 0), a ≤ ?succ a
[PROOFSTEP]
assumption
[GOAL]
case le_succ
⊢ ∀ (a : Fin 0), a ≤ ?succ a
[PROOFSTEP]
intro a
[GOAL]
case le_succ
a : Fin 0
⊢ a ≤ ?succ a
[PROOFSTEP]
exact elim0 a
[GOAL]
case max_of_succ_le
⊢ ∀ {a : Fin 0}, ?succ a ≤ a → IsMax a
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case max_of_succ_le
⊢ ∀ {a : Fin 0}, ?succ a ≤ a → IsMax a
[PROOFSTEP]
assumption
[GOAL]
case max_of_succ_le
⊢ ∀ {a : Fin 0}, ?succ a ≤ a → IsMax a
[PROOFSTEP]
intro a
[GOAL]
case max_of_succ_le
a : Fin 0
⊢ ?succ a ≤ a → IsMax a
[PROOFSTEP]
exact elim0 a
[GOAL]
case succ_le_of_lt
⊢ ∀ {a b : Fin 0}, a < b → ?succ a ≤ b
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case succ_le_of_lt
⊢ ∀ {a b : Fin 0}, a < b → ?succ a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case succ_le_of_lt
⊢ ∀ {a b : Fin 0}, a < b → ?succ a ≤ b
[PROOFSTEP]
intro a
[GOAL]
case succ_le_of_lt
a : Fin 0
⊢ ∀ {b : Fin 0}, a < b → ?succ a ≤ b
[PROOFSTEP]
exact elim0 a
[GOAL]
case le_of_lt_succ
⊢ ∀ {a b : Fin 0}, a < ?succ b → a ≤ b
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case le_of_lt_succ
⊢ ∀ {a b : Fin 0}, a < ?succ b → a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case le_of_lt_succ
⊢ ∀ {a b : Fin 0}, a < ?succ b → a ≤ b
[PROOFSTEP]
intro a
[GOAL]
case le_of_lt_succ
a : Fin 0
⊢ ∀ {b : Fin 0}, a < ?succ b → a ≤ b
[PROOFSTEP]
exact elim0 a
[GOAL]
case succ
⊢ Fin 0 → Fin 0
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case succ
⊢ Fin 0 → Fin 0
[PROOFSTEP]
assumption
[GOAL]
case succ
⊢ Fin 0 → Fin 0
[PROOFSTEP]
intro a
[GOAL]
case succ
a : Fin 0
⊢ Fin 0
[PROOFSTEP]
exact elim0 a
[GOAL]
n : ℕ
⊢ ∀ {a : Fin (n + 1)}, ¬IsMax a → ∀ (b : Fin (n + 1)), a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
[PROOFSTEP]
intro a ha b
[GOAL]
n : ℕ
a : Fin (n + 1)
ha : ¬IsMax a
b : Fin (n + 1)
⊢ a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
[PROOFSTEP]
rw [isMax_iff_eq_top, eq_top_iff, not_le, top_eq_last] at ha
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMax a
ha : a < last n
b : Fin (n + 1)
⊢ a < b ↔ (fun i => if i < last n then i + 1 else i) a ≤ b
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMax a
ha : a < last n
b : Fin (n + 1)
⊢ a < b ↔ (if a < last n then a + 1 else a) ≤ b
[PROOFSTEP]
rw [if_pos ha, lt_iff_val_lt_val, le_iff_val_le_val, val_add_one_of_lt ha]
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMax a
ha : a < last n
b : Fin (n + 1)
⊢ ↑a < ↑b ↔ ↑a + 1 ≤ ↑b
[PROOFSTEP]
exact Nat.lt_iff_add_one_le
[GOAL]
n : ℕ
⊢ ∀ (a : Fin (n + 1)), IsMax a → (fun i => if i < last n then i + 1 else i) a = a
[PROOFSTEP]
intro a ha
[GOAL]
n : ℕ
a : Fin (n + 1)
ha : IsMax a
⊢ (fun i => if i < last n then i + 1 else i) a = a
[PROOFSTEP]
rw [isMax_iff_eq_top, top_eq_last] at ha
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : IsMax a
ha : a = last n
⊢ (fun i => if i < last n then i + 1 else i) a = a
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : IsMax a
ha : a = last n
⊢ (if a < last n then a + 1 else a) = a
[PROOFSTEP]
rw [if_neg ha.not_lt]
[GOAL]
⊢ PredOrder (Fin 0)
[PROOFSTEP]
constructor
[GOAL]
case pred_le
⊢ ∀ (a : Fin 0), ?pred a ≤ a
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case pred_le
⊢ ∀ (a : Fin 0), ?pred a ≤ a
[PROOFSTEP]
assumption
[GOAL]
case pred_le
⊢ ∀ (a : Fin 0), ?pred a ≤ a
[PROOFSTEP]
intro a
[GOAL]
case pred_le
a : Fin 0
⊢ ?pred a ≤ a
[PROOFSTEP]
exact elim0 a
[GOAL]
case min_of_le_pred
⊢ ∀ {a : Fin 0}, a ≤ ?pred a → IsMin a
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case min_of_le_pred
⊢ ∀ {a : Fin 0}, a ≤ ?pred a → IsMin a
[PROOFSTEP]
assumption
[GOAL]
case min_of_le_pred
⊢ ∀ {a : Fin 0}, a ≤ ?pred a → IsMin a
[PROOFSTEP]
intro a
[GOAL]
case min_of_le_pred
a : Fin 0
⊢ a ≤ ?pred a → IsMin a
[PROOFSTEP]
exact elim0 a
[GOAL]
case le_pred_of_lt
⊢ ∀ {a b : Fin 0}, a < b → a ≤ ?pred b
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case le_pred_of_lt
⊢ ∀ {a b : Fin 0}, a < b → a ≤ ?pred b
[PROOFSTEP]
assumption
[GOAL]
case le_pred_of_lt
⊢ ∀ {a b : Fin 0}, a < b → a ≤ ?pred b
[PROOFSTEP]
intro a
[GOAL]
case le_pred_of_lt
a : Fin 0
⊢ ∀ {b : Fin 0}, a < b → a ≤ ?pred b
[PROOFSTEP]
exact elim0 a
[GOAL]
case le_of_pred_lt
⊢ ∀ {a b : Fin 0}, ?pred a < b → a ≤ b
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case le_of_pred_lt
⊢ ∀ {a b : Fin 0}, ?pred a < b → a ≤ b
[PROOFSTEP]
assumption
[GOAL]
case le_of_pred_lt
⊢ ∀ {a b : Fin 0}, ?pred a < b → a ≤ b
[PROOFSTEP]
intro a
[GOAL]
case le_of_pred_lt
a : Fin 0
⊢ ∀ {b : Fin 0}, ?pred a < b → a ≤ b
[PROOFSTEP]
exact elim0 a
[GOAL]
case pred
⊢ Fin 0 → Fin 0
[PROOFSTEP]
first
| assumption
| intro a; exact elim0 a
[GOAL]
case pred
⊢ Fin 0 → Fin 0
[PROOFSTEP]
assumption
[GOAL]
case pred
⊢ Fin 0 → Fin 0
[PROOFSTEP]
intro a
[GOAL]
case pred
a : Fin 0
⊢ Fin 0
[PROOFSTEP]
exact elim0 a
[GOAL]
n : ℕ
⊢ ∀ {a : Fin (n + 1)}, ¬IsMin a → ∀ (b : Fin (n + 1)), b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
[PROOFSTEP]
intro a ha b
[GOAL]
n : ℕ
a : Fin (n + 1)
ha : ¬IsMin a
b : Fin (n + 1)
⊢ b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
[PROOFSTEP]
rw [isMin_iff_eq_bot, eq_bot_iff, not_le, bot_eq_zero] at ha
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMin a
ha : 0 < a
b : Fin (n + 1)
⊢ b ≤ (fun x => if x = 0 then 0 else x - 1) a ↔ b < a
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMin a
ha : 0 < a
b : Fin (n + 1)
⊢ (b ≤ if a = 0 then 0 else a - 1) ↔ b < a
[PROOFSTEP]
rw [if_neg ha.ne', lt_iff_val_lt_val, le_iff_val_le_val, coe_sub_one, if_neg ha.ne', le_tsub_iff_right, Iff.comm]
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMin a
ha : 0 < a
b : Fin (n + 1)
⊢ ↑b < ↑a ↔ ↑b + 1 ≤ ↑a
n : ℕ a : Fin (n + 1) ha✝ : ¬IsMin a ha : 0 < a b : Fin (n + 1) ⊢ 1 ≤ ↑a
[PROOFSTEP]
exact Nat.lt_iff_add_one_le
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : ¬IsMin a
ha : 0 < a
b : Fin (n + 1)
⊢ 1 ≤ ↑a
[PROOFSTEP]
exact ha
[GOAL]
n : ℕ
⊢ ∀ (a : Fin (n + 1)), IsMin a → (fun x => if x = 0 then 0 else x - 1) a = a
[PROOFSTEP]
intro a ha
[GOAL]
n : ℕ
a : Fin (n + 1)
ha : IsMin a
⊢ (fun x => if x = 0 then 0 else x - 1) a = a
[PROOFSTEP]
rw [isMin_iff_eq_bot, bot_eq_zero] at ha
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : IsMin a
ha : a = 0
⊢ (fun x => if x = 0 then 0 else x - 1) a = a
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
a : Fin (n + 1)
ha✝ : IsMin a
ha : a = 0
⊢ (if a = 0 then 0 else a - 1) = a
[PROOFSTEP]
rwa [if_pos ha, eq_comm]