-- Mathlib/Data/Finsupp/Single.lean
theorem induction₂ {p : (α →₀ M) → Prop} (f : α →₀ M) (h0 : p 0)
    (ha : ∀ (a b) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)) : p f :=
  suffices ∀ (s) (f : α →₀ M), f.support = s → p f from this _ _ rfl
  fun s =>
  Finset.cons_induction_on s (fun f hf => by rwa [support_eq_empty.1 hf]) fun a s has ih f hf => by
    suffices p (f.erase a + single a (f a)) by rwa [erase_add_single] at this
    classical
      apply ha
      · rw [support_erase, mem_erase]
        exact fun H => H.1 rfl
      · rw [← mem_support_iff, hf]
        exact mem_cons_self _ _
      · apply ih _ _
        rw [support_erase, hf, Finset.erase_cons]

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f + single a (f a))

Tactic:
apply ha

Result:
case a
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ a ∉ (erase a f).support

case a
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ f a ≠ 0

case a
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s : Finset α
f : α →₀ M
hf : f.support = ∅
⊢ p f

Tactic:
rwa [support_eq_empty.1 hf]

Result:
no goals

Proof state:
case a
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f)

Tactic:
apply ih _ _

Result:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ (erase a f).support = s

Proof state:
case a
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ f a ≠ 0

Tactic:
rw [← mem_support_iff, hf]

Result:
case a
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ a ∈ cons a s has

Proof state:
case a
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ a ∈ cons a s has

Tactic:
exact mem_cons_self _ _

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ (erase a f).support = s

Tactic:
rw [support_erase, hf, Finset.erase_cons]

Result:
no goals

Proof state:
case a
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)

Tactic:
exact fun H => H.1 rfl

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
this : p (erase a f + single a (f a))
⊢ p f

Tactic:
rwa [erase_add_single] at this

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p f

Tactic:
suffices p (f.erase a + single a (f a)) by rwa [erase_add_single] at this

Result:
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f + single a (f a))

Proof state:
case a
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ a ∉ (erase a f).support

Tactic:
rw [support_erase, mem_erase]

Result:
case a
α : Type u_1
M : Type u_5
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)