-- Mathlib/Analysis/InnerProductSpace/Subspace.lean
theorem OrthogonalFamily.inner_sum (l₁ l₂ : ∀ i, G i) (s : Finset ι) :
    ⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ inner (∑ i ∈ s, (V i) (l₁ i)) (∑ j ∈ s, (V j) (l₂ j)) = ∑ i ∈ s, inner (l₁ i) (l₂ i)

Tactic:
classical
calc
  ⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ j ∈ s, ∑ i ∈ s, ⟪V i (l₁ i), V j (l₂ j)⟫ := by
    simp only [sum_inner, inner_sum]
  _ = ∑ j ∈ s, ∑ i ∈ s, ite (i = j) ⟪V i (l₁ i), V j (l₂ j)⟫ 0 := by
    congr with i
    congr with j
    apply hV.eq_ite
  _ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
    simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
      imp_self, imp_true_iff]

Result:
no goals

Proof state:
case e_f.h
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
i : ι
⊢ ∑ i_1 ∈ s, inner ((V i_1) (l₁ i_1)) ((V i) (l₂ i)) =
    ∑ i_1 ∈ s, if i_1 = i then inner ((V i_1) (l₁ i_1)) ((V i) (l₂ i)) else 0

Tactic:
congr with j

Result:
case e_f.h.e_f.h
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
i j : ι
⊢ inner ((V j) (l₁ j)) ((V i) (l₂ i)) = if j = i then inner ((V j) (l₁ j)) ((V i) (l₂ i)) else 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ inner (∑ i ∈ s, (V i) (l₁ i)) (∑ j ∈ s, (V j) (l₂ j)) = ∑ j ∈ s, ∑ i ∈ s, inner ((V i) (l₁ i)) ((V j) (l₂ j))

Tactic:
simp only [sum_inner, inner_sum]

Result:
no goals

Proof state:
case e_f.h.e_f.h
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
i j : ι
⊢ inner ((V j) (l₁ j)) ((V i) (l₂ i)) = if j = i then inner ((V j) (l₁ j)) ((V i) (l₂ i)) else 0

Tactic:
apply hV.eq_ite

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ (∑ j ∈ s, ∑ i ∈ s, if i = j then inner ((V i) (l₁ i)) ((V j) (l₂ j)) else 0) = ∑ i ∈ s, inner (l₁ i) (l₂ i)

Tactic:
simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
  imp_self, imp_true_iff]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ inner (∑ i ∈ s, (V i) (l₁ i)) (∑ j ∈ s, (V j) (l₂ j)) = ∑ i ∈ s, inner (l₁ i) (l₂ i)

Tactic:
calc
  ⟪∑ i ∈ s, V i (l₁ i), ∑ j ∈ s, V j (l₂ j)⟫ = ∑ j ∈ s, ∑ i ∈ s, ⟪V i (l₁ i), V j (l₂ j)⟫ := by
    simp only [sum_inner, inner_sum]
  _ = ∑ j ∈ s, ∑ i ∈ s, ite (i = j) ⟪V i (l₁ i), V j (l₂ j)⟫ 0 := by
    congr with i
    congr with j
    apply hV.eq_ite
  _ = ∑ i ∈ s, ⟪l₁ i, l₂ i⟫ := by
    simp only [Finset.sum_ite_of_true, Finset.sum_ite_eq', LinearIsometry.inner_map_map,
      imp_self, imp_true_iff]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
⊢ ∑ j ∈ s, ∑ i ∈ s, inner ((V i) (l₁ i)) ((V j) (l₂ j)) =
    ∑ j ∈ s, ∑ i ∈ s, if i = j then inner ((V i) (l₁ i)) ((V j) (l₂ j)) else 0

Tactic:
congr with i

Result:
case e_f.h
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
G : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
l₁ l₂ : (i : ι) → G i
s : Finset ι
i : ι
⊢ ∑ i_1 ∈ s, inner ((V i_1) (l₁ i_1)) ((V i) (l₂ i)) =
    ∑ i_1 ∈ s, if i_1 = i then inner ((V i_1) (l₁ i_1)) ((V i) (l₂ i)) else 0