case ofRepr
ι : Type u_1
ι' : Type ?u.731886
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.731915
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.731933
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.731953
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
g : OrthonormalBasis ι 𝕜 E
repr✝ : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g
ι : Type u_1
ι' : Type ?u.731886
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.731915
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.731933
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.731953
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
f g : OrthonormalBasis ι 𝕜 E
h : f.repr = g.repr
⊢ f = g
cases f
case ofRepr.ofRepr
ι : Type u_1
ι' : Type ?u.731886
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.731915
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.731933
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.731953
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
repr✝¹ repr✝ : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }
case ofRepr
ι : Type u_1
ι' : Type ?u.731886
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.731915
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.731933
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.731953
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
g : OrthonormalBasis ι 𝕜 E
repr✝ : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr✝ }.repr = g.repr
⊢ { repr := repr✝ } = g
cases g
no goals
case ofRepr.ofRepr
ι : Type u_1
ι' : Type ?u.731886
𝕜 : Type u_2
inst✝⁹ : IsROrC 𝕜
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.731915
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type ?u.731933
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type ?u.731953
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
repr✝¹ repr✝ : E ≃ₗᵢ[𝕜] EuclideanSpace 𝕜 ι
h : { repr := repr✝¹ }.repr = { repr := repr✝ }.repr
⊢ { repr := repr✝¹ } = { repr := repr✝ }
congr