-- Mathlib/Algebra/Order/Antidiag/Pi.lean
@[simp] lemma mem_piAntidiag : f ∈ piAntidiag s n ↔ s.sum f = n ∧ ∀ i, f i ≠ 0 → i ∈ s

Proof state:
case a.mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
⊢ (∃ a, ∑ i : Fin #s, a i = n ∧ (fun i => if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f) →
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
rintro ⟨f, ⟨hf, rfl⟩, rfl⟩

Result:
case a.mp.intro.intro.refl
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : { x // x ∈ s } ≃ Fin #s
f : Fin #s → μ
⊢ (∑ i ∈ s, if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) = ∑ i : Fin #s, f i ∧
    ∀ (i : ι), (fun i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) i ≠ 0 → i ∈ s

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : { x // x ∈ s } ≃ Fin #s
f : Fin #s → μ
⊢ ∀ (x : { x // x ∈ s }), f (e ⟨↑x, ⋯⟩) = f (e x)

Tactic:
simp

Result:
no goals

Proof state:
case a.mp.intro.intro.refl
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : { x // x ∈ s } ≃ Fin #s
f : Fin #s → μ
⊢ ∑ i : { x // x ∈ s }, f (e ⟨↑i, ⋯⟩) = ∑ i : Fin #s, f i ∧
    ∀ (i : ι), (fun i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) i ≠ 0 → i ∈ s

Tactic:
exact ⟨Fintype.sum_equiv e _ _ (by simp), by simp +contextual⟩

Result:
no goals

Proof state:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
i : ι
⊢ (if hi : i ∈ s then (f ∘ Subtype.val ∘ ⇑e.symm) (e ⟨i, hi⟩) else 0) = f i

Tactic:
have := not_imp_comm.1 (hf i)

Result:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
i : ι
this : i ∉ s → f i = 0
⊢ (if hi : i ∈ s then (f ∘ Subtype.val ∘ ⇑e.symm) (e ⟨i, hi⟩) else 0) = f i

Proof state:
case a
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
⊢ f ∈
      Trunc.lift
        (fun e =>
          map { toFun := fun f i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n))
        ⋯ (Trunc.mk e) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
simp only [Trunc.lift_mk, mem_map, mem_finAntidiagonal, Embedding.coeFn_mk]

Result:
case a
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
⊢ (∃ a, ∑ i : Fin #s, a i = n ∧ (fun i => if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : { x // x ∈ s } ≃ Fin #s
f : Fin #s → μ
⊢ ∀ (i : ι), (fun i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) i ≠ 0 → i ∈ s

Tactic:
simp +contextual

Result:
no goals

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ f ∈ s.piAntidiag n ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
rw [piAntidiag]

Result:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ f ∈
      Trunc.lift
        (fun e =>
          map { toFun := fun f i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n))
        ⋯ (Fintype.truncEquivFinOfCardEq ⋯) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Proof state:
case a.mpr.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∑ i : Fin #s, (f ∘ Subtype.val ∘ ⇑e.symm) i = s.sum f

Tactic:
rw [← sum_attach s]

Result:
case a.mpr.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∑ i : Fin #s, (f ∘ Subtype.val ∘ ⇑e.symm) i = ∑ x ∈ s.attach, f ↑x

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∀ (x : Fin #s), (f ∘ Subtype.val ∘ ⇑e.symm) x = f ↑(e.symm x)

Tactic:
simp

Result:
no goals

Proof state:
case a.mp.intro.intro.refl
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : { x // x ∈ s } ≃ Fin #s
f : Fin #s → μ
⊢ (∑ i ∈ s, if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) = ∑ i : Fin #s, f i ∧
    ∀ (i : ι), (fun i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) i ≠ 0 → i ∈ s

Tactic:
rw [sum_dite_of_true fun _ ↦ id]

Result:
case a.mp.intro.intro.refl
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
e : { x // x ∈ s } ≃ Fin #s
f : Fin #s → μ
⊢ ∑ i : { x // x ∈ s }, f (e ⟨↑i, ⋯⟩) = ∑ i : Fin #s, f i ∧
    ∀ (i : ι), (fun i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0) i ≠ 0 → i ∈ s

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ (fun i => if hi : i ∈ s then (f ∘ Subtype.val ∘ ⇑e.symm) (e ⟨i, hi⟩) else 0) = f

Tactic:
ext i

Result:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
i : ι
⊢ (if hi : i ∈ s then (f ∘ Subtype.val ∘ ⇑e.symm) (e ⟨i, hi⟩) else 0) = f i

Proof state:
case a.mpr.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∃ a, ∑ i : Fin #s, a i = s.sum f ∧ (fun i => if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f

Tactic:
refine ⟨f ∘ (↑) ∘ e.symm, ?_, by ext i; have := not_imp_comm.1 (hf i); aesop⟩

Result:
case a.mpr.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∑ i : Fin #s, (f ∘ Subtype.val ∘ ⇑e.symm) i = s.sum f

Proof state:
case h
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
i : ι
this : i ∉ s → f i = 0
⊢ (if hi : i ∈ s then (f ∘ Subtype.val ∘ ⇑e.symm) (e ⟨i, hi⟩) else 0) = f i

Tactic:
aesop

Result:
no goals