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
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
j : ι
neg :
  (if r j i ∧ j ∈ p then (x₁ : (a : ι) → α a) j else if r j i then (x₂ : (a : ι) → α a) j else (x : (a : ι) → α a) j) =
    (x : (a : ι) → α a) j
⊢ (x₁.piecewise (β := α) (x₂.piecewise (β := α) x {j : ι | r j i}) {j : ι | r j i ∧ j ∈ p} : (a : ι) → α a) j =
    (x : (a : ι) → α a) j

Tactic:
simp only [piecewise_apply, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, DFinsupp.piecewise_apply
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
j : ι
pos : ∀ (h₁ : r j i ∧ j ∈ p), (x₁ : (a : ι) → α a) j = (x : (a : ι) → α a) j
pos₁ : ∀ (h₁ : ¬(r j i ∧ j ∈ p)) (h₂ : r j i), (x₂ : (a : ι) → α a) j = (x : (a : ι) → α a) j
neg : ∀ (h₁ : ¬(r j i ∧ j ∈ p)) (h₂ : ¬r j i), (x : (a : ι) → α a) j = (x : (a : ι) → α a) j
⊢ (if r j i ∧ j ∈ p then (x₁ : (a : ι) → α a) j else if r j i then (x₂ : (a : ι) → α a) j else (x : (a : ι) → α a) j) =
    (x : (a : ι) → α a) j

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : ¬r j i
⊢ (x : (a : ι) → α a) j = (x : (a : ι) → α a) j

Tactic:
rfl
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : ¬r j i
⊢ (x : (a : ι) → α a) j = (x : (a : ι) → α a) j

Tactic:
try rfl
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
j : ι
h₁ : r j i ∧ j ∈ p
pos : (x₁ : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
pos₁ pos₂ : (x₁ : (a : ι) → α a) j = (x₁ : (a : ι) → α a) j
⊢ (x₁ : (a : ι) → α a) j = (x : (a : ι) → α a) j

Tactic:
rw [hr j h₁.1, if_pos h₁.2]

Premises used: if_pos, And.right, And.left
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
pos : j ∉ p
⊢ (x₂ : (a : ι) → α a) j = (x : (a : ι) → α a) j

Tactic:
rw [hr j h₂, if_neg]

Premises used: if_neg
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → (x : (a : ι) → α a) j = if j ∈ p then (x₁ : (a : ι) → α a) j else (x₂ : (a : ι) → α a) j
hp : i ∉ p
hs : s i ((x : (a : ι) → α a) i) ((x₂ : (a : ι) → α a) i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ j ∉ p

Tactic:
simpa [h₂] using h₁
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
hu : Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) i x)
⊢ Acc (DFinsupp.Lex (α := α) r s)
    (piecewise (β := α) ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.1
      ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.2
      ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).1)

Tactic:
@Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{ i }, _⟩
        (InvImage.accessible snd <| hs.prod_gameAdd hu)

Premises used: InvImage.accessible, DFinsupp.lex_fibration, Acc.of_fibration, Prod.snd, Acc.prod_gameAdd
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
hu : Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) i x)
h :
  piecewise (β := α) ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.1
      ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.2
      ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).1 =
    x
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
convert! ←
      @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{ i }, _⟩
        (InvImage.accessible snd <| hs.prod_gameAdd hu)

Premises used: InvImage.accessible, DFinsupp.lex_fibration, Acc.of_fibration, Prod.snd, Acc.prod_gameAdd
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
hu : Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) i x)
⊢ piecewise (β := α) (single (β := α) i ((x : (a : ι) → α a) i)) (erase (β := α) i x) {i} = x

Tactic:
piecewise_single_erase x i

Premises used: DFinsupp.piecewise_single_erase
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
hu : Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) i x)
⊢ piecewise (β := α) ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.1
      ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.2
      ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).1 =
    x

Tactic:
convert! piecewise_single_erase x i

Premises used: DFinsupp.piecewise_single_erase
-- Module: Mathlib.Data.DFinsupp.WellFounded
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst_1 : DecidableEq ι
x : Π₀ (i : ι), α i
i : ι
hs : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
hu : Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) i x)
h :
  piecewise (β := α) ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.1
      ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).2.2
      ({i}, single (β := α) i ((x : (a : ι) → α a) i), erase (β := α) i x).1 =
    x
⊢ Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
classical
    convert! ←
      @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{ i }, _⟩
        (InvImage.accessible snd <| hs.prod_gameAdd hu)
    convert! piecewise_single_erase x i

Premises used: DFinsupp.piecewise_single_erase
-- 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
⊢ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) 0

Tactic:
Acc.intro 0 fun _ ⟨_, _, h⟩ => (hbot h).elim

Premises used: False.elim, _private.0.DFinsupp.Lex.acc_zero.match_1, Acc, OfNat.ofNat, DFinsupp.Lex, 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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
generalize :
  ∀ (t : Finset ι) (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
⊢ (∀ i ∈ x.support (β := α),
      Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
generalize ht : x.support = t

Premises used: DFinsupp.support
-- 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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
t : Finset ι
ht : x.support (β := α) = t
revert :
  ∀ (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
⊢ (∀ i ∈ t, Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
    Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
revert x
-- 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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : x.support (β := α) = ∅
empty :
  (∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((0 : (a : ι) → α a) i))) →
    Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) 0
⊢ (∀ (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:
rw [support_eq_empty.1 ht]

Premises used: DFinsupp.support_eq_empty, Iff.mp
-- 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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : x.support (β := α) = ∅
⊢ (∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((0 : (a : ι) → α a) i))) →
    Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) 0

Tactic:
fun _ => 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
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
x : Π₀ (i : ι), α i
ht : x.support (β := α) = ∅
⊢ (∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((0 : (a : ι) → α a) i))) →
    Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) 0

Tactic:
exact fun _ => 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
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),
    (∀ i ∈ insert b t,
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
fun x ht h => Lex.acc_of_single_erase b (h b <| t.mem_insert_self b) ?_

Premises used: Finset.mem_insert_self, DFinsupp.Lex.acc_of_single_erase
-- 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
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
insert :
  ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = Insert.insert b t)
    (h :
      ∀ i ∈ Insert.insert b t,
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))),
    Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) b x)
⊢ ∀ (x : Π₀ (i : ι), α i) (ht : x.support (β := α) = Insert.insert b t),
    (∀ i ∈ Insert.insert b t,
        Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))) →
      Acc (DFinsupp.Lex (α := α) r s) x

Tactic:
refine fun x ht h => Lex.acc_of_single_erase b (h b <| t.mem_insert_self b) ?_

Premises used: DFinsupp.Lex.acc_of_single_erase
-- 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
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))
rw : x.support (β := α).erase b = t
rw₁ : (insert b t).erase b = t
rw₂ rw₃ : t = t
⊢ (erase (β := α) b x).support (β := α) = t

Tactic:
rw [support_erase, ht, Finset.erase_insert hb]

Premises used: DFinsupp.support_erase, Finset.erase_insert
-- 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
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.insert b t
h :
  ∀ i ∈ Insert.insert b t,
    Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
insert :
  ∀ (a : ι) (ha : a ∈ t),
    Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) a ((erase (β := α) b x : (a : ι) → α a) a))
⊢ Acc (DFinsupp.Lex (α := α) r s) (erase (β := α) b x)

Tactic:
refine ih _ (by rw [support_erase, ht, Finset.erase_insert hb]) fun a ha => ?_
-- 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
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.insert b t
h :
  ∀ i ∈ Insert.insert b t,
    Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i ((x : (a : ι) → α a) i))
a : ι
ha : a ∈ t
insert : Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) a ((x : (a : ι) → α a) a))
⊢ Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) a ((erase (β := α) b x : (a : ι) → α a) a))

Tactic:
rw [erase_ne (ha.ne_of_notMem hb)]

Premises used: Membership.mem.ne_of_notMem, DFinsupp.erase_ne
-- 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
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 ((x : (a : ι) → α a) a))

Tactic:
h a (Finset.mem_insert_of_mem ha)

Premises used: Finset.mem_insert_of_mem
-- 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
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 ((x : (a : ι) → α a) a))

Tactic:
exact h a (Finset.mem_insert_of_mem ha)

Premises used: Finset.mem_insert_of_mem
-- 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
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
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.insert b t),
    (∀ i ∈ Insert.insert b 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 (β := α) = t),
    (∀ i ∈ 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)

Premises used: DFinsupp.Lex.acc_zero, Insert.insert
-- 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
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
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.insert b t),
    (∀ i ∈ Insert.insert b 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 (β := α) = t),
    (∀ i ∈ 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)

Premises used: DFinsupp.Lex.acc_zero, Insert.insert
-- 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 : ι
hi : Acc (rᶜ ⊓ fun (x1 x2 : ι) ↦ x1 ≠ x2) i
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)
⊢ ∀ (a : α i), Acc (α := Π₀ (i : ι), α i) (DFinsupp.Lex (α := α) r s) (single (β := α) i a)

Tactic:
induction hi with | _ i _ ih