ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ (↑b = fun x => 1) ∨ ↑b = fun x => -1
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
⊢ (↑b = fun x => 1) ∨ ↑b = fun x => -1
have : Unique ι := b.toBasis.unique
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ↑b default = 1 ∨ ↑b default = -1
⊢ (↑b = fun x => 1) ∨ ↑b = fun x => -1
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ (↑b = fun x => 1) ∨ ↑b = fun x => -1
have : b default = 1 ∨ b default = -1 := by
  have : ‖b default‖ = 1 := b.orthonormal.1 _
  rwa [Real.norm_eq_abs, abs_eq (zero_le_one' ℝ)] at this
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ↑b default = 1 ∨ ↑b default = -1
⊢ (const ι (↑b default) = fun x => 1) ∨ const ι (↑b default) = fun x => -1
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ↑b default = 1 ∨ ↑b default = -1
⊢ (↑b = fun x => 1) ∨ ↑b = fun x => -1
rw [eq_const_of_unique b]
no goals
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ↑b default = 1 ∨ ↑b default = -1
⊢ (const ι (↑b default) = fun x => 1) ∨ const ι (↑b default) = fun x => -1
refine' this.imp _ _ <;> (intro; ext; simp [*])
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ‖↑b default‖ = 1
⊢ ↑b default = 1 ∨ ↑b default = -1
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ ↑b default = 1 ∨ ↑b default = -1
have : ‖b default‖ = 1 := b.orthonormal.1 _
no goals
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ‖↑b default‖ = 1
⊢ ↑b default = 1 ∨ ↑b default = -1
rwa [Real.norm_eq_abs, abs_eq (zero_le_one' ℝ)] at this
case refine'_2
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ↑b default = 1 ∨ ↑b default = -1
a✝ : ↑b default = -1
⊢ const ι (↑b default) = fun x => -1
case refine'_2
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ↑b default = 1 ∨ ↑b default = -1
⊢ ↑b default = -1 → const ι (↑b default) = fun x => -1
intro
case refine'_2.h
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ↑b default = 1 ∨ ↑b default = -1
a✝ : ↑b default = -1
x✝ : ι
⊢ const ι (↑b default) x✝ = -1
case refine'_2
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ↑b default = 1 ∨ ↑b default = -1
a✝ : ↑b default = -1
⊢ const ι (↑b default) = fun x => -1
ext
no goals
case refine'_2.h
ι : Type u_1
ι' : Type ?u.1652996
𝕜 : Type ?u.1652999
inst✝¹⁰ : IsROrC 𝕜
E : Type ?u.1653005
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : InnerProductSpace 𝕜 E
E' : Type ?u.1653025
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : InnerProductSpace 𝕜 E'
F : Type ?u.1653043
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type ?u.1653063
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ↑b default = 1 ∨ ↑b default = -1
a✝ : ↑b default = -1
x✝ : ι
⊢ const ι (↑b default) x✝ = -1
simp [*]