awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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_1 : ∀ (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)
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))
have pos : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) 0
Tactic: rw [hr j h, single_eq_of_ne hij, single_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have pos : ∀ (j : ι) (hj : j ∈ x.support (β := α)),
  Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
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⟩ _
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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))
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have 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) sorry a)),
      Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
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⟩ _
Cleared hypotheses: i, h, ih, a_1, a, ha, hr, hs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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))
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have pos₂ : ∀ (j : ι) (hj : j ∈ x.support (β := α)) (hij : j ≠ i),
  Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
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⟩ _
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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))
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have 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))
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⟩ _
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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))
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have 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))
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⟩ _
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
⊢ WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)
have inl : ∀ (h : IsEmpty ((i : ι) → α i)), WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)
Tactic: obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
⊢ WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)
have inr : ∀ (x : (i : ι) → α i), WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)
Tactic: obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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) ⊤ ⋯ }
⊢ WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)
have inr : ∀ (this : Fintype ι), WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
have inr : ∀ (i : ι) (a : α i), ¬s i a 0
Tactic: refine InvImage.wf equivFunOnFintype.symm (Lex.wellFounded' (fun i a => ?_) hs ?_)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
⊢ WellFounded (α := (i : ι) → α i) (Pi.Lex (β := α) r fun {i : ι} ↦ s i)
have inr₁ : WellFounded (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) r)
Tactic: refine InvImage.wf equivFunOnFintype.symm (Lex.wellFounded' (fun i a => ?_) hs ?_)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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)
have refine_1 : ∀ ⦃i : ι⦄ ⦃a : β i⦄, ¬a < 0
Tactic: refine Lex.wellFounded' ?_ (fun i ↦ IsWellFounded.wf) ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
⊢ WellFounded (α := Π₀ (i : ι), β i)
    (DFinsupp.Lex (α := β) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel) fun (x : ι) (x1 x2 : β x) ↦
      x1 < x2)
have refine_2 : WellFounded.{u_1 + 1} (α := ι)
  (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) (Function.swap (φ := fun (a a_1 : ι) ↦ Prop) WellOrderingRel))
Tactic: refine Lex.wellFounded' ?_ (fun i ↦ IsWellFounded.wf) ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (hypothesis)
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 (x1 x2 : Π₀ (i : ι), α i) ↦ x1 < x2
have this : 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
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
have 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 sorry) x_1 y
Tactic: refine Subrelation.wf (fun h => ?_) <| InvImage.wf (mapRange e fun _ ↦ rfl) this
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
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
⊢ 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
have 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 sorry) x_1 y
Tactic: obtain ⟨i, he, hl⟩ := lex_lt_of_lt_of_preorder (Function.swap WellOrderingRel) h
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
⊢ WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
have inl : ∀ (h : IsEmpty ((i : ι) → α i)), WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
Tactic: obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
inl : ∀ (h : IsEmpty ((i : ι) → α i)), WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
⊢ WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
have inr : ∀ (x : (i : ι) → α i), WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
Tactic: obtain h | ⟨⟨x⟩⟩ := isEmpty_or_nonempty (∀ i, α i)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
x : (i : ι) → α i
this : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := WellFounded.min (r := fun (x1 x2 : α i) ↦ x1 < x2) ⋯ ⊤ ⋯ }
⊢ WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
have inr : ∀ (this : Fintype ι), WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
hw : ∀ (i : ι), WellFoundedLT.{u_2} (α i)
x : (i : ι) → α i
this_1 : (i : ι) → Zero (α i) := fun (i : ι) ↦ { zero := WellFounded.min (r := fun (x1 x2 : α i) ↦ x1 < x2) ⋯ ⊤ ⋯ }
this : Fintype ι
⊢ WellFounded fun (x1 x2 : (i : ι) → α i) ↦ x1 < x2
have inr : ∀ (i : ι) (a : α i), ¬a < 0
Tactic: refine InvImage.wf equivFunOnFintype.symm (DFinsupp.wellFoundedLT fun i a => ?_).wf
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
R : Type u_1
r : R
s : ℝ≥0
inst : SMul R ℝ≥0
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0 ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
⊢ (↑(r • s) : ℝ≥0∞) = r • (↑s : ℝ≥0∞)
have rw : (↑(r • s) : ℝ≥0∞) = HSMul.hSMul (β := ℝ≥0) r 1 • (↑s : ℝ≥0∞)
Tactic: rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc,
    one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
R : Type u_1
r : R
s : ℝ≥0
inst : SMul R ℝ≥0
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0 ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
rw : (↑(r • s) : ℝ≥0∞) = HSMul.hSMul (β := ℝ≥0) r 1 • (↑s : ℝ≥0∞)
⊢ (↑(r • s) : ℝ≥0∞) = r • (↑s : ℝ≥0∞)
have rw₁ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) • (↑s : ℝ≥0∞)
Tactic: rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc,
    one_mul]
-- Lean 4 proof step from Mathlib.Data.ENNReal.Action (goal)
Goal:
R : Type u_1
r : R
s : ℝ≥0
inst : SMul R ℝ≥0
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0 ℝ≥0
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
rw : (↑(r • s) : ℝ≥0∞) = HSMul.hSMul (β := ℝ≥0) r 1 • (↑s : ℝ≥0∞)
rw₁ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) • (↑s : ℝ≥0∞)
⊢ (↑(r • s) : ℝ≥0∞) = r • (↑s : ℝ≥0∞)
have rw₂ : (↑(r • s) : ℝ≥0∞) = (↑(HSMul.hSMul (β := ℝ≥0) r 1) : ℝ≥0∞) * (↑s : ℝ≥0∞)
Tactic: rw [← smul_one_smul ℝ≥0 r (s : ℝ≥0∞), smul_def, smul_eq_mul, ← ENNReal.coe_mul, smul_mul_assoc,
    one_mul]