-- Mathlib/Data/DFinsupp/Defs.lean
theorem induction {p : (Π₀ i, β i) → Prop} (f : Π₀ i, β i) (h0 : p 0)
    (ha : ∀ (i b) (f : Π₀ i, β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)) : p f

Proof state:
case mk'.h.mk.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f 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 { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (single i (f i) + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Tactic:
rw [h, single_zero, zero_add]

Result:
case mk'.h.mk.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f 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 { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Proof state:
case mk'.h.mk.cons
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f 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 { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
⊢ p
    (single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

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

Result:
case mk'.h.mk.cons
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f 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 { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
⊢ p (single i (f i) + erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f 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 { toFun := f, support' := Trunc.mk ⟨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 ∨ (fun j => if j = i then 0 else f j) i_1 = 0),
    { toFun := fun j => if j = i then 0 else f j, support' := Trunc.mk ⟨i ::ₘ s, aux⟩ } =
      { toFun := fun j => if j = i then 0 else f j, support' := Trunc.mk ⟨s, H2⟩ }
⊢ p { toFun := fun j => if j = i then 0 else f j, support' := Trunc.mk ⟨i ::ₘ s, ⋯⟩ }

Tactic:
rw [H3]

Result:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f 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 { toFun := f, support' := Trunc.mk ⟨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 ∨ (fun j => if j = i then 0 else f j) i_1 = 0),
    { toFun := fun j => if j = i then 0 else f j, support' := Trunc.mk ⟨i ::ₘ s, aux⟩ } =
      { toFun := fun j => if j = i then 0 else f j, support' := Trunc.mk ⟨s, H2⟩ }
⊢ p { toFun := fun j => if j = i then 0 else f j, support' := Trunc.mk ⟨s, H2⟩ }

Proof state:
case mk'.h.mk.empty
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
H : ∀ (i : ι), i ∈ 0 ∨ 0 i = 0
⊢ p { toFun := 0, support' := Trunc.mk ⟨0, H⟩ }

Tactic:
exact h0

Result:
no goals

Proof state:
case inl.inl.h
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f 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 { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
j : ι
H2 : j ∈ i ::ₘ s
H3 : j = i
⊢ (if j = i then 0 else f j) = 0

Tactic:
exact if_pos H3

Result:
no goals

Proof state:
case mk'.h.mk.empty
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
f : (i : ι) → β i
H : ∀ (i : ι), i ∈ 0 ∨ f i = 0
⊢ p { toFun := f, support' := Trunc.mk ⟨0, H⟩ }

Tactic:
have : f = 0 := funext fun i => (H i).resolve_left (Multiset.not_mem_zero _)

Result:
case mk'.h.mk.empty
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
f : (i : ι) → β i
H : ∀ (i : ι), i ∈ 0 ∨ f i = 0
this : f = 0
⊢ p { toFun := f, support' := Trunc.mk ⟨0, H⟩ }

Proof state:
case mk'.h.mk.cons.inl
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f 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 { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
H3 :
  single i ({ toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } i) +
      erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ } =
    { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
h : f i = 0
⊢ p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })

Tactic:
exact H2

Result:
no goals