-- Mathlib/Algebra/BigOperators/Sym.lean
theorem Finset.sum_sym2_filter_not_isDiag {ι α} [LinearOrder ι] [AddCommMonoid α]
    (s : Finset ι) (p : Sym2 ι → α) :
    ∑ i ∈ s.sym2 with ¬ i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 < i.2, p s(i.1, i.2)

Proof state:
case refine_1.mk.mk
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
i₁ j₁ : ι
hij₁ : (i₁, j₁).1 ≤ (i₁, j₁).2
⊢ ⟨(i₁, j₁), hij₁⟩ ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag ↔
    Sym2.sortEquiv.symm ⟨(i₁, j₁), hij₁⟩ ∈ filter (fun i => ¬i.IsDiag) s.sym2

Tactic:
simp [and_assoc]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
⊢ ∑ i ∈ filter (fun i => ¬i.IsDiag) s.sym2, p i = ∑ i ∈ filter (fun i => i.1 ≤ i.2) s.offDiag, p s(i.1, i.2)

Tactic:
conv_rhs => rw [← Finset.sum_subtype_eq_sum_filter]

Result:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
⊢ ∑ i ∈ filter (fun i => ¬i.IsDiag) s.sym2, p i =
    ∑ x ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag, p s((↑x).1, (↑x).2)

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
⊢ ∑ i ∈ filter (fun i => ¬i.IsDiag) s.sym2, p i = ∑ i ∈ filter (fun i => i.1 < i.2) s.offDiag, p s(i.1, i.2)

Tactic:
rw [Finset.offDiag_filter_lt_eq_filter_le]

Result:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
⊢ ∑ i ∈ filter (fun i => ¬i.IsDiag) s.sym2, p i = ∑ i ∈ filter (fun i => i.1 ≤ i.2) s.offDiag, p s(i.1, i.2)

Proof state:
case refine_1
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
⊢ ∀ (i : { p // p.1 ≤ p.2 }),
    i ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag ↔ Sym2.sortEquiv.symm i ∈ filter (fun i => ¬i.IsDiag) s.sym2

Tactic:
rintro ⟨⟨i₁, j₁⟩, hij₁⟩

Result:
case refine_1.mk.mk
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
i₁ j₁ : ι
hij₁ : (i₁, j₁).1 ≤ (i₁, j₁).2
⊢ ⟨(i₁, j₁), hij₁⟩ ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag ↔
    Sym2.sortEquiv.symm ⟨(i₁, j₁), hij₁⟩ ∈ filter (fun i => ¬i.IsDiag) s.sym2

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
⊢ ∑ i ∈ filter (fun i => ¬i.IsDiag) s.sym2, p i =
    ∑ x ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag, p s((↑x).1, (↑x).2)

Tactic:
refine (Finset.sum_equiv Sym2.sortEquiv.symm ?_ ?_).symm

Result:
case refine_1
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
⊢ ∀ (i : { p // p.1 ≤ p.2 }),
    i ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag ↔ Sym2.sortEquiv.symm i ∈ filter (fun i => ¬i.IsDiag) s.sym2

case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
⊢ ∀ i ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag, p s((↑i).1, (↑i).2) = p (Sym2.sortEquiv.symm i)

Proof state:
case refine_2
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
⊢ ∀ i ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag, p s((↑i).1, (↑i).2) = p (Sym2.sortEquiv.symm i)

Tactic:
rintro ⟨⟨i₁, j₁⟩, hij₁⟩

Result:
case refine_2.mk.mk
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
i₁ j₁ : ι
hij₁ : (i₁, j₁).1 ≤ (i₁, j₁).2
⊢ ⟨(i₁, j₁), hij₁⟩ ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag →
    p s((↑⟨(i₁, j₁), hij₁⟩).1, (↑⟨(i₁, j₁), hij₁⟩).2) = p (Sym2.sortEquiv.symm ⟨(i₁, j₁), hij₁⟩)

Proof state:
case refine_2.mk.mk
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid α
s : Finset ι
p : Sym2 ι → α
i₁ j₁ : ι
hij₁ : (i₁, j₁).1 ≤ (i₁, j₁).2
⊢ ⟨(i₁, j₁), hij₁⟩ ∈ Finset.subtype (fun i => i.1 ≤ i.2) s.offDiag →
    p s((↑⟨(i₁, j₁), hij₁⟩).1, (↑⟨(i₁, j₁), hij₁⟩).2) = p (Sym2.sortEquiv.symm ⟨(i₁, j₁), hij₁⟩)

Tactic:
simp

Result:
no goals