𝕜 : Type u_2
E : Type u_3
F : Type ?u.2137301
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
ι' : Type u_1
v : ι → E
hv : Orthonormal 𝕜 v
f : ι' → ι
hf : Function.Injective f
em✝ : (a : Prop) → Decidable a
⊢ Orthonormal 𝕜 (v ∘ f)
𝕜 : Type u_2
E : Type u_3
F : Type ?u.2137301
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
ι' : Type u_1
v : ι → E
hv : Orthonormal 𝕜 v
f : ι' → ι
hf : Function.Injective f
⊢ Orthonormal 𝕜 (v ∘ f)
classical!
𝕜 : Type u_2
E : Type u_3
F : Type ?u.2137301
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
ι' : Type u_1
v : ι → E
f : ι' → ι
hf : Function.Injective f
em✝ : (a : Prop) → Decidable a
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ ∀ (i j : ι'), inner ((v ∘ f) i) ((v ∘ f) j) = if i = j then 1 else 0
𝕜 : Type u_2
E : Type u_3
F : Type ?u.2137301
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
ι' : Type u_1
v : ι → E
hv : Orthonormal 𝕜 v
f : ι' → ι
hf : Function.Injective f
em✝ : (a : Prop) → Decidable a
⊢ Orthonormal 𝕜 (v ∘ f)
rw [orthonormal_iff_ite] at hv ⊢
𝕜 : Type u_2
E : Type u_3
F : Type ?u.2137301
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
ι' : Type u_1
v : ι → E
f : ι' → ι
hf : Function.Injective f
em✝ : (a : Prop) → Decidable a
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i j : ι'
⊢ inner ((v ∘ f) i) ((v ∘ f) j) = if i = j then 1 else 0
𝕜 : Type u_2
E : Type u_3
F : Type ?u.2137301
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
ι' : Type u_1
v : ι → E
f : ι' → ι
hf : Function.Injective f
em✝ : (a : Prop) → Decidable a
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ ∀ (i j : ι'), inner ((v ∘ f) i) ((v ∘ f) j) = if i = j then 1 else 0
intro i j
case h.e'_3
𝕜 : Type u_2
E : Type u_3
F : Type ?u.2137301
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
ι' : Type u_1
v : ι → E
f : ι' → ι
hf : Function.Injective f
em✝ : (a : Prop) → Decidable a
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i j : ι'
⊢ (if i = j then 1 else 0) = if f i = f j then 1 else 0
𝕜 : Type u_2
E : Type u_3
F : Type ?u.2137301
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
ι' : Type u_1
v : ι → E
f : ι' → ι
hf : Function.Injective f
em✝ : (a : Prop) → Decidable a
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i j : ι'
⊢ inner ((v ∘ f) i) ((v ∘ f) j) = if i = j then 1 else 0
convert hv (f i) (f j) using 1
no goals
case h.e'_3
𝕜 : Type u_2
E : Type u_3
F : Type ?u.2137301
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_4
dec_ι : DecidableEq ι
ι' : Type u_1
v : ι → E
f : ι' → ι
hf : Function.Injective f
em✝ : (a : Prop) → Decidable a
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i j : ι'
⊢ (if i = j then 1 else 0) = if f i = f j then 1 else 0
simp [hf.eq_iff]