-- Mathlib/Algebra/Order/Antidiag/Finsupp.lean
theorem mem_finsuppAntidiag_insert {a : ι} {s : Finset ι}
    (h : a ∉ s) (n : μ) {f : ι →₀ μ} :
    f ∈ finsuppAntidiag (insert a s) n ↔
      ∃ m ∈ antidiagonal n, ∃ (g : ι →₀ μ),
        f = Finsupp.update g a m.1 ∧ g ∈ finsuppAntidiag s m.2

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ ∀ x ∈ s, Function.update (⇑g) a n1 x = g x

Tactic:
intro x hx

Result:
case mpr.intro.intro.intro.intro.intro.intro.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
x : ι
hx : x ∈ s
⊢ Function.update (⇑g) a n1 x = g x

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ f ∈ (insert a s).finsuppAntidiag n ↔ ∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2

Tactic:
simp only [mem_finsuppAntidiag, mem_antidiagonal, Prod.exists, sum_insert h]

Result:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ f a + ∑ x ∈ s, f x = n ∧ f.support ⊆ insert a s ↔
    ∃ a_1 b, a_1 + b = n ∧ ∃ g, f = g.update a a_1 ∧ s.sum ⇑g = b ∧ g.support ⊆ s

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ f a + ∑ x ∈ s, f x = n ∧ f.support ⊆ insert a s ↔
    ∃ a_1 b, a_1 + b = n ∧ ∃ g, f = g.update a a_1 ∧ s.sum ⇑g = b ∧ g.support ⊆ s

Tactic:
constructor

Result:
case mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ f a + ∑ x ∈ s, f x = n ∧ f.support ⊆ insert a s →
    ∃ a_2 b, a_2 + b = n ∧ ∃ g, f = g.update a a_2 ∧ s.sum ⇑g = b ∧ g.support ⊆ s

case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ a_1 b, a_1 + b = n ∧ ∃ g, f = g.update a a_1 ∧ s.sum ⇑g = b ∧ g.support ⊆ s) →
    f a + ∑ x ∈ s, f x = n ∧ f.support ⊆ insert a s

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ ∑ x ∈ s, Function.update (⇑g) a n1 x = s.sum ⇑g

Tactic:
apply sum_congr rfl

Result:
case mpr.intro.intro.intro.intro.intro.intro.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ ∀ x ∈ s, Function.update (⇑g) a n1 x = g x

Proof state:
case mpr.intro.intro.intro.intro.intro.intro.hy
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
x : ι
hx : x ∈ s
⊢ Function.update (⇑g) a n1 x = g x

Tactic:
rw [update_of_ne (ne_of_mem_of_not_mem hx h) n1 ⇑g]

Result:
no goals