Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

Tactic:
<;>

Goal state after:
case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = v i
hj : w j = -v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0

case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : i = j
hv : ⟪v i, v j⟫ = 1
⊢ ⟪w i, w j⟫ = 1

case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
i j : ι
hi : w i = -v i
hj : w j = -v j
h : ¬i = j
hv : ⟪v i, v j⟫ = 0
⊢ ⟪w i, w j⟫ = 0