-- Mathlib/Data/Finsupp/Single.lean
theorem induction_on_max₂ (f : α →₀ M) (h0 : p 0)
    (ha : ∀ (a b) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)) :
    p f

Proof state:
case refine_2
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
⊢ p f

Tactic:
have hs' : (erase a f).support = s := by
  rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]

Result:
case refine_2
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ p f

Proof state:
case refine_2
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ p f

Tactic:
rw [← erase_add_single a f]

Result:
case refine_2
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ p (erase a f + single a (f a))

Proof state:
case refine_2
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ f a ≠ 0

Tactic:
rw [← mem_support_iff, hs]

Result:
case refine_2
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ a ∈ insert a s

Proof state:
case refine_1
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s : Finset α
f : α →₀ M
h : f.support = ∅
⊢ p f

Tactic:
rwa [support_eq_empty.1 h]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ a ∈ insert a s

Tactic:
exact mem_insert_self a s

Result:
no goals

Proof state:
case refine_2
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ p (erase a f + single a (f a))

Tactic:
refine ha _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')

Result:
case refine_2
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ f a ≠ 0

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
⊢ p f

Tactic:
suffices ∀ (s) (f : α →₀ M), f.support = s → p f from this _ _ rfl

Result:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
⊢ ∀ (s : Finset α) (f : α →₀ M), f.support = s → p f

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

Tactic:
refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)

Result:
case refine_1
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s : Finset α
f : α →₀ M
h : f.support = ∅
⊢ p f

case refine_2
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
⊢ p f

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder α
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
hm : ∀ x ∈ s, x < a
hf : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hs : f.support = insert a s
⊢ (erase a f).support = s

Tactic:
rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]

Result:
no goals