awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
f : (i : ι) → β i
s : Multiset ι
H : ∀ (i : ι), i ∈ s ∨ f i = 0
h :
  ∀ (i : ι) (s : Multiset ι)
    (ih :
      ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
        p
          (mk' (β := fun (i : ι) ↦ β i) f
            (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H))))
    (f : (i : ι) → β i) (H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))

Tactic:
induction s using Multiset.induction_on generalizing f with
  | empty =>
    have : f = 0 := funext fun i => (H i).resolve_left (Multiset.notMem_zero _)
    subst this
    exact h0
  | cons i s ih => ?_
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
dsimp :
  p
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i_1 : ι), i_1 ∈ s ∨ (if i_1 = i then 0 else f i_1) = 0) (i ::ₘ s)
          ⋯)))
⊢ p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))

Tactic:
dsimp only [erase, Trunc.map, Trunc.bind, Trunc.liftOn, Trunc.lift_mk,
      Function.comp, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Trunc.map, Trunc.bind, Function.comp, DFinsupp.erase, Trunc.lift_mk, Trunc.liftOn
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
⊢ ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0

Tactic:
grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
have :
  ∀ (H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
        (Trunc.mk
          (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i_1 : ι), i_1 ∈ s ∨ (if i_1 = i then 0 else f i_1) = 0) (i ::ₘ s)
            ⋯)))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i_1 : ι), i_1 ∈ s ∨ (if i_1 = i then 0 else f i_1) = 0) (i ::ₘ s)
          ⋯)))

Tactic:
have H2 : ∀ j, j ∈ s ∨ ite (j = i) 0 (f j) = 0 := by grind
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0
⊢ ∀ (aux : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0),
    Eq (α := Π₀ (i : ι), β i)
      (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
        (Trunc.mk
          (Subtype.mk (p := fun (s : Multiset ι) ↦
            ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) (i ::ₘ s)
            aux)))
      (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
        (Trunc.mk
          (Subtype.mk (p := fun (s : Multiset ι) ↦
            ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) s H2)))

Tactic:
have H3 : ∀ aux, (⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨i ::ₘ s, aux⟩⟩ : Π₀ i, β i) =
        ⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨s, H2⟩⟩ :=
      fun _ ↦ ext fun _ => rfl
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0
H3 :
  ∀ (aux : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0),
    Eq (α := Π₀ (i : ι), β i)
      (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
        (Trunc.mk
          (Subtype.mk (p := fun (s : Multiset ι) ↦
            ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) (i ::ₘ s)
            aux)))
      (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
        (Trunc.mk
          (Subtype.mk (p := fun (s : Multiset ι) ↦
            ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) s H2)))
rw :
  p
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦
          ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) s H2)))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i_1 : ι), i_1 ∈ s ∨ (if i_1 = i then 0 else f i_1) = 0) (i ::ₘ s)
          ⋯)))

Tactic:
rw [H3]
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0
H3 :
  ∀ (aux : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0),
    Eq (α := Π₀ (i : ι), β i)
      (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
        (Trunc.mk
          (Subtype.mk (p := fun (s : Multiset ι) ↦
            ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) (i ::ₘ s)
            aux)))
      (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
        (Trunc.mk
          (Subtype.mk (p := fun (s : Multiset ι) ↦
            ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) s H2)))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) (fun (j : ι) ↦ if j = i then 0 else f j)
      (Trunc.mk
        (Subtype.mk (p := fun (s : Multiset ι) ↦
          ∀ (i_1 : ι), i_1 ∈ s ∨ Eq.{v + 1} (α := β i_1) ((fun (j : ι) ↦ if j = i then 0 else f j) i_1) 0) s H2)))

Tactic:
apply ih
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
h :
  ∀
    (H2 :
      p
        (erase (β := β) i
          (mk' (β := fun (i : ι) ↦ β i) f
            (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))

Tactic:
have H2 : p (erase i ⟨f, Trunc.mk ⟨i ::ₘ s, H⟩⟩) := by
    dsimp only [erase, Trunc.map, Trunc.bind, Trunc.liftOn, Trunc.lift_mk,
      Function.comp, Subtype.coe_mk]
    have H2 : ∀ j, j ∈ s ∨ ite (j = i) 0 (f j) = 0 := by grind
    have H3 : ∀ aux, (⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨i ::ₘ s, aux⟩⟩ : Π₀ i, β i) =
        ⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨s, H2⟩⟩ :=
      fun _ ↦ ext fun _ => rfl
    rw [H3]
    apply ih
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
⊢ HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))

Tactic:
have H3 : single i _ + _ = (⟨f, Trunc.mk ⟨i ::ₘ s, H⟩⟩ : Π₀ i, β i) := single_add_erase _ _
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
h :
  p
    (HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
⊢ p
    (mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))

Tactic:
rw [← H3]
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
h :
  p
    (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
⊢ p
    (HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))

Tactic:
change p (single i (f i) + _)

Premises used: DFinsupp.single, HAdd.hAdd
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
h :
  ∀ (h : f i = 0),
    p
      (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
        (erase (β := β) i
          (mk' (β := fun (i : ι) ↦ β i) f
            (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
h₁ :
  ∀ (h : ¬f i = 0),
    p
      (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
        (erase (β := β) i
          (mk' (β := fun (i : ι) ↦ β i) f
            (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))
⊢ p
    (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))

Tactic:
rcases Classical.em (f i = 0) with h | h

Premises used: Classical.em, OfNat.ofNat, Eq
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
h : f i = 0
h₁ :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
⊢ p
    (HAdd.hAdd (α := Π₀ (i : ι), β i) (single (β := β) i (f i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))))

Tactic:
rw [h, single_zero, zero_add]

Premises used: zero_add, DFinsupp.single_zero
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
h : f i = 0
⊢ p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))

Tactic:
H2
-- Module: Mathlib.Data.DFinsupp.Defs
Goal:
ι : Type u
β : ι → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), (f : (a : ι) → β a) i = 0 → b ≠ 0 → p f → p (single (β := β) i b + f)
i : ι
s : Multiset ι
ih :
  ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0),
    p
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) s H)))
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 :
  p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))
H3 :
  HAdd.hAdd (α := Π₀ (i : ι), β i)
      (single (β := β) i
        ((mk' (β := fun (i : ι) ↦ β i) f
              (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)) :
            (a : ι) → β a)
          i))
      (erase (β := β) i
        (mk' (β := fun (i : ι) ↦ β i) f
          (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H)))) =
    mk' (β := fun (i : ι) ↦ β i) f
      (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))
h : f i = 0
⊢ p
    (erase (β := β) i
      (mk' (β := fun (i : ι) ↦ β i) f
        (Trunc.mk (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f i = 0) (i ::ₘ s) H))))

Tactic:
exact H2