-- Mathlib/Data/DFinsupp/WellFounded.lean
theorem DFinsupp.wellFoundedLT [∀ i, Zero (α i)] [∀ i, Preorder (α i)]
    [∀ i, WellFoundedLT (α i)] (hbot : ∀ ⦃i⦄ ⦃a : α i⦄, ¬a < 0) : WellFoundedLT (Π₀ i, α i) :=
  ⟨by
    set β := fun i ↦ Antisymmetrization (α i) (· ≤ ·)
    set e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization (· ≤ ·)
    let _ : ∀ i, Zero (β i) := fun i ↦ ⟨e i 0⟩
    have : WellFounded (DFinsupp.Lex (Function.swap <| @WellOrderingRel ι)
        (fun _ ↦ (· < ·) : (i : ι) → β i → β i → Prop))

Proof state:
case refine_2
ι : Type u_1
α : ι → Type u_2
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 x1 x2 => x1 ≤ x2
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x1 x2 => x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
⊢ WellFounded fun y x => WellOrderingRel y x

Tactic:
exact IsWellFounded.wf

Result:
no goals

Proof state:
case refine_2
ι : Type u_1
α : ι → Type u_2
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 x1 x2 => x1 ≤ x2
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x1 x2 => x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
⊢ WellFounded (Function.swap (Function.swap WellOrderingRel))

Tactic:
simp +unfoldPartialApp only [Function.swap]

Result:
case refine_2
ι : Type u_1
α : ι → Type u_2
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 x1 x2 => x1 ≤ x2
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x1 x2 => x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
⊢ WellFounded fun y x => WellOrderingRel y x

Proof state:
case refine_1
ι : Type u_1
α : ι → Type u_2
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 x1 x2 => x1 ≤ x2
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x1 x2 => x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
⊢ ∀ ⦃i : ι⦄ ⦃a : β i⦄, ¬a < 0

Tactic:
rintro i ⟨a⟩

Result:
case refine_1.mk
ι : Type u_1
α : ι → Type u_2
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 x1 x2 => x1 ≤ x2
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x1 x2 => x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
i : ι
a✝ : β i
a : α i
⊢ ¬Quot.mk (⇑(AntisymmRel.setoid (α i) fun x1 x2 => x1 ≤ x2)) a < 0

Proof state:
ι : Type u_1
α : ι → Type u_2
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 x1 x2 => x1 ≤ x2
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x1 x2 => x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
⊢ WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2)

Tactic:
have := IsTrichotomous.swap (@WellOrderingRel ι)

Result:
ι : Type u_1
α : ι → Type u_2
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 x1 x2 => x1 ≤ x2
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x1 x2 => x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
this : IsTrichotomous ι (Function.swap WellOrderingRel)
⊢ WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2)

Proof state:
ι : Type u_1
α : ι → Type u_2
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 x1 x2 => x1 ≤ x2
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x1 x2 => x1 ≤ x2
⊢ WellFounded fun x1 x2 => x1 < x2

Tactic:
let _ : ∀ i, Zero (β i) := fun i ↦ ⟨e i 0⟩

Result:
ι : Type u_1
α : ι → Type u_2
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 x1 x2 => x1 ≤ x2
e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x1 x2 => x1 ≤ x2
x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }
⊢ WellFounded fun x1 x2 => x1 < x2