case inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3605350
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
G : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
i j : ι
v : G i
w : G j
h : i = j
⊢ inner (↑(V i) v) (↑(V j) w) = inner (↑(V i) v) (↑(V j) w)

case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3605350
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
G : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
i j : ι
v : G i
w : G j
h : ¬i = j
⊢ inner (↑(V i) v) (↑(V j) w) = 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3605350
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
G : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
i j : ι
v : G i
w : G j
⊢ inner (↑(V i) v) (↑(V j) w) = if i = j then inner (↑(V i) v) (↑(V j) w) else 0
split_ifs with h
no goals
case inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3605350
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
G : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
i j : ι
v : G i
w : G j
h : i = j
⊢ inner (↑(V i) v) (↑(V j) w) = inner (↑(V i) v) (↑(V j) w)
rfl
no goals
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.3605350
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
G : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
V : (i : ι) → G i →ₗᵢ[𝕜] E
hV : OrthogonalFamily 𝕜 G V
dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)
i j : ι
v : G i
w : G j
h : ¬i = j
⊢ inner (↑(V i) v) (↑(V j) w) = 0
exact hV h v w