awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.WellFounded
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_1 : ∀ (i : ι), WellFounded (s i)
inst_1 : DecidableEq ι
i_1 i : ι
h : ∀ (y : ι), (rᶜ ⊓ fun (x1 x2 : ι) ↦ x1 ≠ x2) y i → Acc (rᶜ ⊓ fun (x1 x2 : ι) ↦ x1 ≠ x2) y
ih :
  ∀ (y : ι),
    (rᶜ ⊓ fun (x1 x2 : ι) ↦ x1 ≠ x2) y i →
      ∀ (a : α y), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) y a)
a_1 a : α i
ha :
  ∀ (y : α i),
    s i y a → (fun (x : α i) ↦ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i x)) y
x : Π₀ (i : ι), α i
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = (single (β := α) i a : (a : ι) → α a) j
hs : s i ((x : (a : ι) → α a) i) (Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ α x) ⋯ a)
pos :
  ∀ (j : ι) (hj : j ∈ x.support (β := α)),
    Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
pos₁ :
  ∀ (j : ι) (hj : j ∈ x.support (β := α)),
    (∀ (y : ι), (rᶜ ⊓ fun (x1 x2 : ι) ↦ x1 ≠ x2) y j → Acc (rᶜ ⊓ fun (x1 x2 : ι) ↦ x1 ≠ x2) y) →
      ∀
        (ih :
          ∀ (y : ι),
            (rᶜ ⊓ fun (x1 x2 : ι) ↦ x1 ≠ x2) y j →
              ∀ (a : α y), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) y a))
        (a a : α j)
        (ha :
          ∀ (y : α j),
            s j y a → (fun (x : α j) ↦ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j x)) y)
        (hr : ∀ (j_1 : ι), r j_1 j → (x : (a : ι) → α a) j_1 = (single (β := α) j a : (a : ι) → α a) j_1)
        (hs : s j ((x : (a : ι) → α a) j) (Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ α x) ⋯ a)),
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
pos₂ pos₃ :
  ∀ (j : ι) (hj : j ∈ x.support (β := α)) (hij : j ≠ i),
    Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
pos₄ :
  ∀ (j : ι) (hj : j ∈ x.support (β := α)) (hij : j ≠ i) (h : r j i),
    Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
neg neg₁ :
  ∀ (j : ι) (hj : j ∈ x.support (β := α)) (hij : j ≠ i) (h : ¬r j i),
    Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
classical
    refine Lex.acc_of_single hbot x fun j hj ↦ ?_
    obtain rfl | hij := eq_or_ne j i
    · exact ha _ hs
    by_cases h : r j i
    · rw [hr j h, single_eq_of_ne hij, single_zero]
      exact Lex.acc_zero hbot
    · exact ih _ ⟨h, hij⟩ _

Premises used: DFinsupp.Lex.acc_zero, DFinsupp.single_zero, rfl
-- Module: Mathlib.Data.DFinsupp.WellFounded
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_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
h : ∀ i ∈ x.support (β := α), Acc (rᶜ ⊓ fun (x1 x2 : ι) ↦ x1 ≠ x2) i
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
Lex.acc_of_single hbot x fun i hi => Lex.acc_single hbot hs (h i hi) _

Premises used: DFinsupp.Lex.acc_single, DFinsupp.Lex.acc_of_single, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.WellFounded
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 (x1 x2 : ι) ↦ x1 ≠ x2)
x : Π₀ (i : ι), α i
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
Lex.acc hbot hs x fun i _ => hr.apply i

Premises used: WellFounded.apply, DFinsupp.Lex.acc
-- Module: Mathlib.Data.DFinsupp.WellFounded
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 (x1 x2 : ι) ↦ x1 ≠ x2)
x : Π₀ (i : ι), α i
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
exact Lex.acc hbot hs x fun i _ => hr.apply i

Premises used: WellFounded.apply, DFinsupp.Lex.acc
-- Module: Mathlib.Data.DFinsupp.WellFounded
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 (x1 x2 : ι) ↦ x1 ≠ x2)
x : Π₀ (i : ι), α i
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
classical exact Lex.acc hbot hs x fun i _ => hr.apply i
-- Module: Mathlib.Data.DFinsupp.WellFounded
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_1 : Std.Trichotomous r
hr : WellFounded (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r)
⊢ WellFounded (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s)

Tactic:
Lex.wellFounded hbot hs <| Subrelation.wf
    (fun {i j} h ↦ Not.imp_symm (@Std.Trichotomous.trichotomous ι r _ i j h.left) h.right) hr

Premises used: DFinsupp.Lex.wellFounded, Not.imp_symm, And.right, Subrelation.wf, And.left, Std.Trichotomous.trichotomous
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LT ι
inst_1 : Std.Trichotomous fun (x1 x2 : ι) ↦ x1 < x2
hι : WellFoundedGT ι
inst_2 : (i : ι) → AddMonoid (α i)
inst_3 : (i : ι) → PartialOrder (α i)
inst_4 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
hα : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
⊢ WellFoundedLT (Lex (Π₀ (i : ι), α i))

Tactic:
⟨Lex.wellFounded' (fun _ _ => not_lt_zero) (fun i => (hα i).wf) hι.wf⟩

Premises used: IsWellFounded.mk, IsWellFounded.wf, DFinsupp.Lex.wellFounded', not_lt_zero
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LT ι
inst_1 : Std.Trichotomous fun (x1 x2 : ι) ↦ x1 < x2
inst_2 : WellFoundedLT ι
inst_3 : (i : ι) → AddMonoid (α i)
inst_4 : (i : ι) → PartialOrder (α i)
inst_5 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_6 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
⊢ WellFoundedLT (Colex (Π₀ (i : ι), α i))

Tactic:
Lex.wellFoundedLT (ι := ιᵒᵈ)

Premises used: Colex, DFinsupp.Lex.wellFoundedLT, OrderDual
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : IsStrictTotalOrder ι r
inst_1 : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
inl : ∀ (h : IsEmpty ((i : ι) → α i)), WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)
inr : ∀ (x : (i : ι) → α i), WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)
⊢ WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)

Tactic:
obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : IsStrictTotalOrder ι r
inst_1 : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
h : IsEmpty ((i : ι) → α i)
⊢ WellFounded (α := (i : ι) → α i) WellFoundedRelation.rel

Tactic:
emptyWf.wf

Premises used: WellFoundedRelation.wf
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : IsStrictTotalOrder ι r
inst_1 : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
h : IsEmpty ((i : ι) → α i)
⊢ WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)

Tactic:
convert! emptyWf.wf

Premises used: WellFoundedRelation.wf
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : IsStrictTotalOrder ι r
inst_1 : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := ⋯.min (r := s i) ⊤ ⋯ }
inr : ∀ (this : Fintype ι), WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)
⊢ WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : IsStrictTotalOrder ι r
inst_1 : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this_1 : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := ⋯.min (r := s i) ⊤ ⋯ }
this : Fintype ι
⊢ WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)

Tactic:
InvImage.wf equivFunOnFintype.symm (Lex.wellFounded' (fun i a => ?_) hs ?_)

Premises used: Pi.Lex, DFinsupp.equivFunOnFintype, DFinsupp.Lex.wellFounded', InvImage.wf, Equiv.symm, DFinsupp.Lex, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : IsStrictTotalOrder ι r
inst_1 : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this_1 : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := ⋯.min (r := s i) ⊤ ⋯ }
this : Fintype ι
inr : ∀ (i : ι) (a : α i), ¬s i a 0
inr₁ : WellFounded (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r)
⊢ WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)

Tactic:
refine InvImage.wf equivFunOnFintype.symm (Lex.wellFounded' (fun i a => ?_) hs ?_)

Premises used: DFinsupp.equivFunOnFintype, DFinsupp.Lex.wellFounded', InvImage.wf, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : IsStrictTotalOrder ι r
inst_1 : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this_1 : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := ⋯.min (r := s i) ⊤ ⋯ }
this : Fintype ι
i : ι
a : α i
⊢ ¬s i a 0

Tactic:
(hs i).not_lt_min ⊤ trivial

Premises used: trivial, WellFounded.not_lt_min, Top.top
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : IsStrictTotalOrder ι r
inst_1 : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this_1 : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := ⋯.min (r := s i) ⊤ ⋯ }
this : Fintype ι
⊢ WellFounded (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r)

Tactic:
Finite.wellFounded_of_trans_of_irrefl (Function.swap r)

Premises used: Function.swap, Finite.wellFounded_of_trans_of_irrefl
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : IsStrictTotalOrder ι r
inst_1 : Finite ι
hs : ∀ (i : ι), WellFounded (s i)
x : (i : ι) → α i
this_1 : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := ⋯.min (r := s i) ⊤ ⋯ }
this : Fintype ι
i : ι
a : α i
⊢ ¬s i a 0

Tactic:
exacts [(hs i).not_lt_min ⊤ trivial, Finite.wellFounded_of_trans_of_irrefl (Function.swap r)]

Premises used: trivial, Function.swap, WellFounded.not_lt_min, Top.top, Finite.wellFounded_of_trans_of_irrefl
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : LinearOrder ι
inst_1 : Finite ι
inst_2 : (i : ι) → LT (α i)
hwf : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
⊢ WellFoundedLT (Lex ((i : ι) → α i))

Tactic:
⟨Pi.Lex.wellFounded (· < ·) fun i => (hwf i).1⟩

Premises used: IsWellFounded.mk, IsWellFounded.wf, LT.lt, Pi.Lex.wellFounded
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : LinearOrder ι
inst_1 : Finite ι
inst_2 : (i : ι) → LT (α i)
inst_3 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
⊢ WellFoundedLT (Colex ((i : ι) → α i))

Tactic:
Pi.Lex.wellFoundedLT (ι := ιᵒᵈ)

Premises used: Colex, Pi.Lex.wellFoundedLT, OrderDual
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α_1 : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α_1 i → α_1 i → Prop
α : Type u_3
inst : LinearOrder ι
inst_1 : Finite ι
inst_2 : LT α
inst_3 : WellFoundedLT α
⊢ WellFoundedLT (Lex (ι → α))

Tactic:
Pi.Lex.wellFoundedLT

Premises used: Pi.Lex.wellFoundedLT
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : IsStrictTotalOrder ι r
inst_1 : Finite ι
inst_2 : (i : ι) → Zero (α i)
hs : ∀ (i : ι), WellFounded (s i)
⊢ WellFounded (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s)

Tactic:
have := Fintype.ofFinite ι
  InvImage.wf equivFunOnFintype (Pi.Lex.wellFounded r hs)

Premises used: Fintype.ofFinite, InvImage, DFinsupp.equivFunOnFintype, InvImage.wf, DFinsupp.Lex, DFunLike.coe, Pi.Lex.wellFounded
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : LinearOrder ι
inst_1 : Finite ι
inst_2 : (i : ι) → Zero (α i)
inst_3 : (i : ι) → LT (α i)
hwf : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
⊢ WellFoundedLT (Lex (Π₀ (i : ι), α i))

Tactic:
⟨DFinsupp.Lex.wellFounded_of_finite (· < ·) fun i => (hwf i).1⟩

Premises used: IsWellFounded.mk, IsWellFounded.wf, LT.lt, DFinsupp.Lex.wellFounded_of_finite
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : LinearOrder ι
inst_1 : Finite ι
inst_2 : (i : ι) → Zero (α i)
inst_3 : (i : ι) → LT (α i)
hwf : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
⊢ WellFoundedLT (Colex (Π₀ (i : ι), α i))

Tactic:
DFinsupp.Lex.wellFoundedLT_of_finite (ι := ιᵒᵈ)

Premises used: Colex, DFinsupp.Lex.wellFoundedLT_of_finite, OrderDual
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
⊢ WellFounded (α := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)

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

Premises used: IsWellFounded.wf, DFinsupp.Lex.wellFounded'
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
refine_1 : ∀ ⦃i : ι⦄ ⦃a : β i⦄, ¬a < 0
refine_2 :
  WellFounded.{u_1 + 1} (α := ι)
    (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel))
⊢ WellFounded (α := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)

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

Premises used: IsWellFounded.wf, DFinsupp.Lex.wellFounded'
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
i : ι
a_1 : β i
a : α i
⊢ ¬LT.lt (α := β i) (Quot.mk (⇑(AntisymmRel.setoid (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2) : α i → α i → Prop) a) 0

Tactic:
apply hbot
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
⊢ WellFounded fun (y x : ι) ↦ WellOrderingRel y x

Tactic:
IsWellFounded.wf

Premises used: IsWellFounded.wf
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
⊢ WellFounded fun (y x : ι) ↦ WellOrderingRel y x

Tactic:
exact IsWellFounded.wf

Premises used: IsWellFounded.wf
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
⊢ WellFounded (α := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)

Tactic:
have : WellFounded (DFinsupp.Lex (Function.swap <| @WellOrderingRel ι)
        (fun _ ↦ (· < ·) : (i : ι) → β i → β i → Prop)) := by
      refine Lex.wellFounded' ?_ (fun i ↦ IsWellFounded.wf) ?_
      · rintro i ⟨a⟩
        apply hbot
      · simp +unfoldPartialApp only [Function.swap]
        exact IsWellFounded.wf
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
this :
  WellFounded (α := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)
⊢ WellFounded fun (x1 x2 : Π₀ (i : ι), α i) ↦ x1 < x2

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

Premises used: DFinsupp.mapRange, Subrelation.wf, InvImage.wf, rfl
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
this :
  WellFounded (α := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)
refine :
  ∀ {x_1 y : Π₀ (i : ι), α i} (h : x_1 < y),
    InvImage (β := Π₀ (i : ι), β i)
      (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
        x1 < x2)
      (mapRange (β₁ := α) (β₂ := β) e ⋯) x_1 y
⊢ WellFounded fun (x1 x2 : Π₀ (i : ι), α i) ↦ x1 < x2

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

Premises used: DFinsupp.mapRange, Subrelation.wf, InvImage.wf, rfl
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
this :
  WellFounded (α := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)
x_1 y : Π₀ (i : ι), α i
h : x_1 < y
obtain :
  ∀ (i : ι)
    (he :
      ∀ (j : ι),
        Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel j i →
          (x_1 : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x_1 : (a : ι) → α a) j)
    (hl : (x_1 : (a : ι) → α a) i < (y : (a : ι) → α a) i),
    InvImage (β := Π₀ (i : ι), β i)
      (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
        x1 < x2)
      (mapRange (β₁ := α) (β₂ := β) e ⋯) x_1 y
⊢ InvImage (β := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)
    (mapRange (β₁ := α) (β₂ := β) e ⋯) x_1 y

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

Premises used: Function.swap, DFinsupp.lex_lt_of_lt_of_preorder, WellOrderingRel
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
this :
  WellFounded (α := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)
x_1 y : Π₀ (i : ι), α i
h : x_1 < y
i : ι
he :
  ∀ (j : ι),
    Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel j i →
      (x_1 : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x_1 : (a : ι) → α a) j
hl : (x_1 : (a : ι) → α a) i < (y : (a : ι) → α a) i
⊢ InvImage (β := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)
    (mapRange (β₁ := α) (β₂ := β) e ⋯) x_1 y

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

Premises used: Quot.sound, InvImage, Pi.Lex, And.intro, Exists.intro, DFinsupp.Lex
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Preorder (α i)
inst_2 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : (i : ι) → Type u_2 := fun (i : ι) ↦ Antisymmetrization (α i) fun (x1 x2 : α i) ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun (i : ι) ↦ toAntisymmetrization fun (x1 x2 : α i) ↦ x1 ≤ x2
x : (i : ι) → Zero (β i) := fun (i : ι) ↦ { zero := e i 0 }
this :
  WellFounded (α := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)
x_1 y : Π₀ (i : ι), α i
h : x_1 < y
i : ι
he :
  ∀ (j : ι),
    Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel j i →
      (x_1 : (a : ι) → α a) j ≤ (y : (a : ι) → α a) j ∧ (y : (a : ι) → α a) j ≤ (x_1 : (a : ι) → α a) j
hl : (x_1 : (a : ι) → α a) i < (y : (a : ι) → α a) i
⊢ InvImage (β := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)
    (mapRange (β₁ := α) (β₂ := β) e ⋯) x_1 y

Tactic:
exact ⟨i, fun j hj ↦ Quot.sound (he j hj), hl⟩
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : (i : ι) → AddMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_3 : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
⊢ WellFoundedLT (Π₀ (i : ι), α i)

Tactic:
DFinsupp.wellFoundedLT fun _ _ => not_lt_zero

Premises used: DFinsupp.wellFoundedLT, not_lt_zero