-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma piAntidiag_cons (hi : i ∉ s) (n : μ) :
    piAntidiag (cons i s hi) n = (antidiagonal n).disjiUnion (fun p : μ × μ ↦
      (piAntidiag s p.snd).map (addRightEmbedding fun t ↦ if t = i then p.fst else 0))
        (pairwiseDisjoint_piAntidiag_map_addRightEmbedding hi _)

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
⊢ (cons i s hi).piAntidiag n =
    (antidiagonal n).disjiUnion (fun p => map (addRightEmbedding fun t => if t = i then p.1 else 0) (s.piAntidiag p.2))
      ⋯

Tactic:
ext f

Result:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ f ∈ (cons i s hi).piAntidiag n ↔
    f ∈
      (antidiagonal n).disjiUnion
        (fun p => map (addRightEmbedding fun t => if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
⊢ (addRightEmbedding fun t => if t = i then f i else 0) (update f i 0) = f

Tactic:
aesop

Result:
no goals

Proof state:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ f ∈ (cons i s hi).piAntidiag n ↔
    f ∈
      (antidiagonal n).disjiUnion
        (fun p => map (addRightEmbedding fun t => if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯

Tactic:
simp only [mem_piAntidiag, sum_cons, ne_eq, mem_cons, mem_disjiUnion, mem_antidiagonal, mem_map,
  addLeftEmbedding_apply, Prod.exists]

Result:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) ↔
    ∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧ (addRightEmbedding fun t => if t = i then a else 0) a_1 = f

Proof state:
case h.mpr.intro.intro.intro.intro.intro.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a : μ
g : ι → μ
hg : ∀ (i : ι), ¬g i = 0 → i ∈ s
hn : a + s.sum g = n
this : ¬g i = 0 → i ∈ s
⊢ (addRightEmbedding fun t => if t = i then a else 0) g i +
        ∑ x ∈ s, (addRightEmbedding fun t => if t = i then a else 0) g x =
      n ∧
    ∀ (i_1 : ι), ¬(addRightEmbedding fun t => if t = i then a else 0) g i_1 = 0 → i_1 = i ∨ i_1 ∈ s

Tactic:
aesop (add simp [sum_add_distrib])

Result:
no goals

Proof state:
case h.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun t => if t = i then a else 0) a_1 = f) →
    f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s

Tactic:
rintro ⟨a, _, hn, g, ⟨rfl, hg⟩, rfl⟩

Result:
case h.mpr.intro.intro.intro.intro.intro.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a : μ
g : ι → μ
hg : ∀ (i : ι), ¬g i = 0 → i ∈ s
hn : a + s.sum g = n
⊢ (addRightEmbedding fun t => if t = i then a else 0) g i +
        ∑ x ∈ s, (addRightEmbedding fun t => if t = i then a else 0) g x =
      n ∧
    ∀ (i_1 : ι), ¬(addRightEmbedding fun t => if t = i then a else 0) g i_1 = 0 → i_1 = i ∨ i_1 ∈ s

Proof state:
case h.mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s) →
    ∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧ (addRightEmbedding fun t => if t = i then a else 0) a_1 = f

Tactic:
rintro ⟨hn, hf⟩

Result:
case h.mp.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
⊢ ∃ a b,
    a + b = n ∧
      ∃ a_1,
        (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧ (addRightEmbedding fun t => if t = i then a else 0) a_1 = f

Proof state:
case h.mp.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
j : ι
this : ¬f j = 0 → ¬j = i → j ∈ s
⊢ ¬update f i 0 j = 0 → j ∈ s

Tactic:
aesop (add simp [update])

Result:
no goals

Proof state:
case h.mp.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
j : ι
⊢ ¬update f i 0 j = 0 → j ∈ s

Tactic:
have := fun h₁ h₂ ↦ (hf j h₁).resolve_left h₂

Result:
case h.mp.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
j : ι
this : ¬f j = 0 → ¬j = i → j ∈ s
⊢ ¬update f i 0 j = 0 → j ∈ s

Proof state:
case h.mp.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
⊢ ∃ a b,
    a + b = n ∧
      ∃ a_1,
        (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧ (addRightEmbedding fun t => if t = i then a else 0) a_1 = f

Tactic:
refine ⟨_, _, hn, update f i 0, ⟨sum_update_of_not_mem hi _ _, fun j ↦ ?_⟩, by aesop⟩

Result:
case h.mp.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
hn : f i + ∑ x ∈ s, f x = n
hf : ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s
j : ι
⊢ ¬update f i 0 j = 0 → j ∈ s