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 : ∀ (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)

Tactic:
fun a => WellFounded.induction (hs i)
    (C := fun x ↦ Acc (DFinsupp.Lex r s) (single i x)) a fun a ha ↦ ?_

Premises used: WellFounded.induction
-- 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 ι
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)
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
⊢ ∀ (a : α i), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i a)

Tactic:
refine fun a => WellFounded.induction (hs i)
    (C := fun x ↦ Acc (DFinsupp.Lex r s) (single i x)) a fun a ha ↦ ?_

Premises used: WellFounded.induction
-- 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 ι
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

Tactic:
Acc.intro _ fun x ↦ ?_

Premises used: Acc.intro
-- 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 ι
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
intro : ∀ (x : Π₀ (i : ι), α i), DFinsupp.Lex (α := α) r s x (single (β := α) i a) → Acc (DFinsupp.Lex (α := α) r s) x
⊢ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i a)

Tactic:
refine Acc.intro _ fun x ↦ ?_

Premises used: Acc.intro
-- 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
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)
⊢ 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

Premises used: DFinsupp.single_apply
-- 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
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
neg : ∀ (hik : ¬i = k) (hs : s k ((x : (a : ι) → α a) k) 0), Acc (DFinsupp.Lex (α := α) r s) x
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
split_ifs at hs with hik
-- 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
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) 0
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
(hbot hs).elim

Premises used: False.elim
-- 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
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) 0
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
exact (hbot hs).elim

Premises used: False.elim
-- 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
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)
⊢ ∀ (j : ι), r j i → (x : (a : ι) → α a) j = (single (β := α) i a : (a : ι) → α a) j

Tactic:
subst hik
-- 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
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
⊢ s i ((x : (a : ι) → α a) i) (Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ α x) ⋯ a)

Tactic:
subst hik
-- 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)
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
Lex.acc_of_single hbot x fun j hj ↦ ?_

Premises used: DFinsupp.Lex.acc_of_single
-- 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))
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
refine Lex.acc_of_single hbot x fun j hj ↦ ?_

Premises used: DFinsupp.Lex.acc_of_single
-- 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)
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))
pos₁ :
  ∀ (hij : 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))

Tactic:
obtain rfl | hij := eq_or_ne j i

Premises used: eq_or_ne, 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_1 : ∀ (i : ι), WellFounded (s i)
inst_1 : DecidableEq ι
i : ι
x : Π₀ (i : ι), α i
j : ι
hj : j ∈ x.support (β := α)
h : ∀ (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_1 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))

Tactic:
ha _ hs
-- 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 : ι
x : Π₀ (i : ι), α i
j : ι
hj : j ∈ x.support (β := α)
h : ∀ (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_1 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))

Tactic:
exact ha _ hs
-- 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)
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))
neg : ∀ (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))

Tactic:
by_cases h : r j 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_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
pos : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) 0
⊢ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) j ((x : (a : ι) → α a) j))

Tactic:
rw [hr j h, single_eq_of_ne hij, single_zero]

Premises used: DFinsupp.single_eq_of_ne, DFinsupp.single_zero
-- 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_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) 0

Tactic:
Lex.acc_zero hbot

Premises used: DFinsupp.Lex.acc_zero
-- 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_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) 0

Tactic:
exact Lex.acc_zero hbot

Premises used: DFinsupp.Lex.acc_zero
-- 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_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))

Tactic:
ih _ ⟨h, hij⟩ _

Premises used: And.intro
-- 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_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))

Tactic:
exact ih _ ⟨h, hij⟩ _

Premises used: And.intro