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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
    (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
x : Π₀ (i : ι), α i
ht : x.support (β := α) = insert b t
h : ∀ i ∈ insert b t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
⊢ Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) b x)
have insert : ∀ (a : ι) (ha : a ∈ t),
  Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) a ((erase (β := α) b x : (a : ι) → α a) a))
Tactic: refine ih _ (by rw [support_erase, ht, Finset.erase_insert hb]) fun a ha => ?_
-- 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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
    (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
x : Π₀ (i : ι), α i
ht : x.support (β := α) = insert b t
h : ∀ i ∈ insert b t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
a : ι
ha : a ∈ t
⊢ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) a ((erase (β := α) b x : (a : ι) → α a) a))
have insert : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) a ((x : (a : ι) → α a) a))
Tactic: rw [erase_ne (ha.ne_of_notMem hb)]
-- 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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
t : Finset ι
⊢ ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
    (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
have empty : ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = ∅),
  (∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x
Tactic: induction t using Finset.induction with
    | empty =>
      intro x ht
      rw [support_eq_empty.1 ht]
      exact fun _ => Lex.acc_zero hbot
    | insert b t hb ih =>
      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_notMem hb)]
      exact h a (Finset.mem_insert_of_mem ha)
Cleared hypotheses: t
-- 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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
t : Finset ι
empty :
  ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = ∅),
    (∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
⊢ ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
    (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
have insert : ∀ (b : ι) (t : Finset ι) (hb : b ∉ t)
  (ih :
    ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
      (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
        Acc (DFinsupp.Lex (α := α) r s) x)
  (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = insert b t),
  (∀ i ∈ insert b t,
      Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x
Tactic: induction t using Finset.induction with
    | empty =>
      intro x ht
      rw [support_eq_empty.1 ht]
      exact fun _ => Lex.acc_zero hbot
    | insert b t hb ih =>
      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_notMem hb)]
      exact h a (Finset.mem_insert_of_mem ha)
Cleared hypotheses: t
-- 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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
t : Finset ι
⊢ ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
    (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
have empty : ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = ∅),
  (∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x
Tactic: classical
    induction t using Finset.induction with
    | empty =>
      intro x ht
      rw [support_eq_empty.1 ht]
      exact fun _ => Lex.acc_zero hbot
    | insert b t hb ih =>
      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_notMem hb)]
      exact h a (Finset.mem_insert_of_mem ha)
Cleared hypotheses: t
-- 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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
t : Finset ι
empty :
  ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = ∅),
    (∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
⊢ ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
    (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x
have insert : ∀ (b : ι) (t : Finset ι) (hb : b ∉ t)
  (ih :
    ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = t),
      (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
        Acc (DFinsupp.Lex (α := α) r s) x)
  (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = insert b t),
  (∀ i ∈ insert b t,
      Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x
Tactic: classical
    induction t using Finset.induction with
    | empty =>
      intro x ht
      rw [support_eq_empty.1 ht]
      exact fun _ => Lex.acc_zero hbot
    | insert b t hb ih =>
      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_notMem hb)]
      exact h a (Finset.mem_insert_of_mem ha)
Cleared hypotheses: t
-- 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 : ∀ (i : ι), WellFounded (s i)
inst_1 : DecidableEq ι
i : ι
hi : Acc (rᶜ ⊓ fun (x1 x2 : ι) ↦ x1 ≠ x2) i
⊢ ∀ (a : α i), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i a)
have intro : ∀ (i : ι),
  (∀ (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 : α i), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i a)
Tactic: induction hi with | _ i _ ih
Cleared hypotheses: hi
-- 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 : ∀ (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 : α i), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i a)
have intro : ∀ (a a : α i)
  (ha :
    ∀ (y : α i),
      s i y a → (fun (x : α i) ↦ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i x)) y),
  (fun (x : α i) ↦ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i x)) a
Tactic: refine fun a => WellFounded.induction (hs i)
    (C := fun x ↦ Acc (DFinsupp.Lex r s) (single i x)) a fun a ha ↦ ?_
-- 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 : ∀ (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
⊢ (fun (x : α i) ↦ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i x)) a
have intro : ∀ (x : Π₀ (i : ι), α i), DFinsupp.Lex (α := α) r s x (single (β := α) i a) → Acc (DFinsupp.Lex (α := α) r s) x
Tactic: refine Acc.intro _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (hypothesis)
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
k : ι
hr : ∀ (j : ι), r j k → (x : (a : ι) → α a) j = (single (β := α) i a : (a : ι) → α a) j
hs : s k ((x : (a : ι) → α a) k) ((single (β := α) i a : (a : ι) → α a) k)
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have hs₁ : s k ((x : (a : ι) → α a) k) (if h : i = k then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ α x) h a else 0)
Tactic: rw [single_apply] at hs
Cleared hypotheses: 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
k : ι
hr : ∀ (j : ι), r j k → (x : (a : ι) → α a) j = (single (β := α) i a : (a : ι) → α a) j
hs : s k ((x : (a : ι) → α a) k) (if h : i = k then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ α x) h a else 0)
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have pos : ∀ (hik : i = k) (hs : s k ((x : (a : ι) → α a) k) (Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ α x) hik a)),
  Acc (DFinsupp.Lex (α := α) r s) x
Tactic: split_ifs at hs with hik
Cleared hypotheses: 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
k : ι
hr : ∀ (j : ι), r j k → (x : (a : ι) → α a) j = (single (β := α) i a : (a : ι) → α a) j
hs : s k ((x : (a : ι) → α a) k) (if h : i = k then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ α x) h a else 0)
pos :
  ∀ (hik : i = k) (hs : s k ((x : (a : ι) → α a) k) (Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ α x) hik a)),
    Acc (DFinsupp.Lex (α := α) r s) x
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have neg : ∀ (hik : ¬i = k) (hs : s k ((x : (a : ι) → α a) k) 0), Acc (DFinsupp.Lex (α := α) r s) x
Tactic: split_ifs at hs with hik
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (hypothesis)
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
k : ι
hr : ∀ (j : ι), r j k → (x : (a : ι) → α a) j = (single (β := α) i a : (a : ι) → α a) j
hik : i = k
hs : s k ((x : (a : ι) → α a) k) (Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ α x) hik a)
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have hr₁ : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = (single (β := α) i a : (a : ι) → α a) j
Tactic: subst hik
Cleared hypotheses: k, hr, hik, hs
-- Lean 4 proof step from Mathlib.Data.DFinsupp.WellFounded (hypothesis)
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
k : ι
hr : ∀ (j : ι), r j k → (x : (a : ι) → α a) j = (single (β := α) i a : (a : ι) → α a) j
hik : i = k
hs : s k ((x : (a : ι) → α a) k) (Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ α x) hik a)
hr₁ : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = (single (β := α) i a : (a : ι) → α a) j
⊢ Acc (DFinsupp.Lex (α := α) r s) x
have hs₁ : s i ((x : (a : ι) → α a) i) (Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ α x) sorry a)
Tactic: subst hik
Cleared hypotheses: k, hr, hik, 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)
⊢ 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: refine Lex.acc_of_single hbot x fun j hj ↦ ?_
-- 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)
j : ι
hj : j ∈ x.support (β := α)
⊢ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
have pos : (∀ (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: obtain rfl | hij := eq_or_ne j i
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)
j : ι
hj : j ∈ x.support (β := α)
pos :
  (∀ (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 (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
have pos₁ : ∀ (hij : j ≠ i), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
Tactic: obtain rfl | hij := eq_or_ne j i
-- 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)
j : ι
hj : j ∈ x.support (β := α)
hij : j ≠ i
⊢ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
have pos : ∀ (h : r j i), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
Tactic: by_cases h : r j i
-- 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)
j : ι
hj : j ∈ x.support (β := α)
hij : j ≠ i
pos : ∀ (h : r j i), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
⊢ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
have neg : ∀ (h : ¬r j i), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))
Tactic: by_cases h : r j i