-- 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:
ι : 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)

Tactic:
refine Lex.wellFounded' ?_ (fun i ↦ IsWellFounded.wf) ?_

Result:
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

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))

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 }
this : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2)
x✝ y✝ : Π₀ (i : ι), α i
h : x✝ < y✝
⊢ InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2) (mapRange e ⋯) x✝ y✝

Tactic:
have := IsStrictOrder.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✝ : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2)
x✝ y✝ : Π₀ (i : ι), α i
h : x✝ < y✝
this : IsStrictOrder ι (Function.swap WellOrderingRel)
⊢ InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2) (mapRange e ⋯) x✝ y✝

Proof state:
case intro.intro
ι : 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✝ : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2)
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 x1 x2 => x1 < x2) (mapRange e ⋯) x✝ y✝

Tactic:
exact ⟨i, fun j hj ↦ Quot.sound (he j hj), hl⟩

Result:
no goals

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 }
this : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2)
⊢ WellFounded fun x1 x2 => x1 < x2

Tactic:
refine Subrelation.wf (fun h => ?_) <| InvImage.wf (mapRange e fun _ ↦ rfl) this

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 : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2)
x✝ y✝ : Π₀ (i : ι), α i
h : x✝ < y✝
⊢ InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2) (mapRange e ⋯) x✝ y✝

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 }
this✝ : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2)
x✝ y✝ : Π₀ (i : ι), α i
h : x✝ < y✝
this : IsStrictOrder ι (Function.swap WellOrderingRel)
⊢ InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2) (mapRange e ⋯) x✝ y✝

Tactic:
obtain ⟨i, he, hl⟩ := lex_lt_of_lt_of_preorder (Function.swap WellOrderingRel) h

Result:
case intro.intro
ι : 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✝ : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 => x1 < x2)
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 x1 x2 => x1 < x2) (mapRange e ⋯) x✝ y✝

Proof state:
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

Tactic:
apply hbot

Result:
no goals