[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
