Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: case e'_2.e'_5
𝕜 : 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
inst✝ : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun i ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2
⊢ ∑ x ∈ s₁ \ s₂, (V x) (f x) = ∑ i ∈ s₁ \ s₂, (V i) (F i)

pp: case e'_2.e'_6
𝕜 : 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
inst✝ : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun i ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2
⊢ ∑ x ∈ s₂ \ s₁, -(V x) (f x) = ∑ i ∈ s₂ \ s₁, (V i) (F i)

pp: case e'_3.e'_5.a
𝕜 : 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
inst✝ : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun i ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2
x✝ : ι
a✝ : x✝ ∈ s₁ \ s₂
⊢ ‖f x✝‖ = ‖F x✝‖

pp: case e'_3.e'_6.a
𝕜 : 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
inst✝ : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun i ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2
x✝ : ι
a✝ : x✝ ∈ s₂ \ s₁
⊢ ‖f x✝‖ = ‖F x✝‖

Tactic:
· refine Finset.sum_congr rfl fun i hi => ?_
    simp only [hF₁ i hi]

Goal state after:
case e'_2.e'_6
𝕜 : 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
inst✝ : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun i ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2
⊢ ∑ x ∈ s₂ \ s₁, -(V x) (f x) = ∑ i ∈ s₂ \ s₁, (V i) (F i)

case e'_3.e'_5.a
𝕜 : 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
inst✝ : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun i ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2
x✝ : ι
a✝ : x✝ ∈ s₁ \ s₂
⊢ ‖f x✝‖ = ‖F x✝‖

case e'_3.e'_6.a
𝕜 : 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
inst✝ : DecidableEq ι
f : (i : ι) → G i
s₁ s₂ : Finset ι
F : (i : ι) → G i := fun i ↦ if i ∈ s₁ then f i else -f i
hF₁ : ∀ i ∈ s₁ \ s₂, F i = f i
hF₂ : ∀ i ∈ s₂ \ s₁, F i = -f i
hF : ∀ (i : ι), ‖F i‖ = ‖f i‖
this :
  ‖∑ i ∈ s₁ \ s₂, (V i) (F i) + ∑ i ∈ s₂ \ s₁, (V i) (F i)‖ ^ 2 = ∑ i ∈ s₁ \ s₂, ‖F i‖ ^ 2 + ∑ i ∈ s₂ \ s₁, ‖F i‖ ^ 2
x✝ : ι
a✝ : x✝ ∈ s₂ \ s₁
⊢ ‖f x✝‖ = ‖F x✝‖