awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
c : Set (Set E)
hc :
  c ⊆
    {b : Set E |
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
cc : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ Membership.mem (γ := Set (Set E))
    {b : Set E |
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
    (⋃₀ c)

Tactic:
exact orthonormal_sUnion_of_directed cc.directedOn fun x xc => hc xc

Premises used: IsChain.directedOn, orthonormal_sUnion_of_directed
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
c : Set (Set E)
hc :
  c ⊆
    {b : Set E |
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
cc : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c

Tactic:
fun _ => Set.subset_sUnion_of_mem

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
c : Set (Set E)
hc :
  c ⊆
    {b : Set E |
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))}
cc : IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c
_c0 : c.Nonempty
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c

Tactic:
exact fun _ => Set.subset_sUnion_of_mem

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Nonempty ι
v : ι → E
hv : Orthonormal 𝕜 v
card_eq : Fintype.card ι = finrank 𝕜 E
⊢ (⇑(basisOfOrthonormalOfCardEqFinrank hv card_eq) : (a : ι) → E) = v

Tactic:
coe_basisOfLinearIndependentOfCardEqFinrank _ _

Premises used: coe_basisOfLinearIndependentOfCardEqFinrank
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ v i ≠ 0

Tactic:
ne_of_apply_ne norm ?_

Premises used: Norm.norm, ne_of_apply_ne
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
refine : ‖v i‖ ≠ Norm.norm.{u_2} (E := E) 0
⊢ v i ≠ 0

Tactic:
refine ne_of_apply_ne norm ?_

Premises used: Norm.norm, ne_of_apply_ne
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
rw : Ne (α := ℝ) 1 0
⊢ ‖v i‖ ≠ Norm.norm.{u_2} (E := E) 0

Tactic:
rw [hv.1 i, norm_zero]

Premises used: norm_zero, And.left
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ Ne (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
v : ι → E
f : E →ₗᵢ[𝕜] E'
simp_rw :
  (∀ (i j : ι),
      inner.{u_1, u_7} 𝕜 (E := E') (((⇑f : (a : E) → E') ∘ v) i) (((⇑f : (a : E) → E') ∘ v) j) =
        if i = j then 1 else 0) ↔
    ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
simp_rw₁ :
  (∀ (i j : ι),
      inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') (v i) : E') ((f : (a : E) → E') (v j) : E') =
        if i = j then 1 else 0) ↔
    ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') ((⇑f : (a : E) → E') ∘ v) ↔ Orthonormal 𝕜 v

Tactic:
simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]

Premises used: LinearIsometry.inner_map_map, Function.comp_apply, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
v : ι → E
f : E →ₗᵢ[𝕜] E'
classical :
  (∀ (i j : ι),
      inner.{u_1, u_7} 𝕜 (E := E') (((⇑f : (a : E) → E') ∘ v) i) (((⇑f : (a : E) → E') ∘ v) j) =
        if i = j then 1 else 0) ↔
    ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
classical₁ :
  (∀ (i j : ι),
      inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') (v i) : E') ((f : (a : E) → E') (v j) : E') =
        if i = j then 1 else 0) ↔
    ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') ((⇑f : (a : E) → E') ∘ v) ↔ Orthonormal 𝕜 v

Tactic:
classical simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]

Premises used: LinearIsometry.inner_map_map, Function.comp_apply, orthonormal_iff_ite
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
v : ι → E
hv : Orthonormal 𝕜 v
f : E →ₗᵢ[𝕜] E'
rwa rwa₁ rwa₂ rwa₃ : Orthonormal 𝕜 v
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') ((⇑f : (a : E) → E') ∘ v)

Tactic:
rwa [f.orthonormal_comp_iff]

Premises used: LinearIsometry.orthonormal_comp_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
v : ι → E
hv : Orthonormal 𝕜 v
f : E ≃ₗᵢ[𝕜] E'
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') ((⇑f : (a : E) → E') ∘ v)

Tactic:
hv.comp_linearIsometry f.toLinearIsometry

Premises used: LinearIsometryEquiv.toLinearIsometry, Orthonormal.comp_linearIsometry
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
f : E ≃ₗᵢ[𝕜] E'
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι) (⇑(v.map f.toLinearEquiv) : (a : ι) → E')

Tactic:
hv.comp_linearIsometryEquiv f

Premises used: Orthonormal.comp_linearIsometryEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →ₗ[𝕜] E'
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
hf :
  Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑f : (a : E) → E') (⇑v : (a : ι) → E))
⊢ Eq (α := (a : E) → E') (⇑(f.isometryOfOrthonormal hv hf) : (a : E) → E') (⇑f : (a : E) → E')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →ₗ[𝕜] E'
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
hf :
  Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑f : (a : E) → E') (⇑v : (a : ι) → E))
⊢ (f.isometryOfOrthonormal hv hf).toLinearMap = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_5 : SeminormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_7 : SeminormedAddCommGroup E''
inst_8 : InnerProductSpace 𝕜 E''
f : E ≃ₗ[𝕜] E'
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
hf :
  Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑f : (a : E) → E') (⇑v : (a : ι) → E))
x y : E
rw :
  ∀
    (hf :
      Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
        (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(↑f : E →ₗ[𝕜] E') : (a : E) → E') (⇑v : (a : ι) → E)))
    (x y : E), inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
⊢ inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫

Tactic:
rw [← LinearEquiv.coe_coe] at hf

Premises used: LinearEquiv.coe_coe
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E ≃ₗ[𝕜] E'
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
hf :
  Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑f : (a : E) → E') (⇑v : (a : ι) → E))
⊢ Eq (α := (a : E) → E') (⇑(f.isometryOfOrthonormal hv hf) : (a : E) → E') (⇑f : (a : E) → E')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E ≃ₗ[𝕜] E'
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
hf :
  Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑f : (a : E) → E') (⇑v : (a : ι) → E))
⊢ (f.isometryOfOrthonormal hv hf).toLinearEquiv = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_5 : SeminormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_7 : SeminormedAddCommGroup E''
inst_8 : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
h :
  ∀ (i : ι),
    Eq.{u_7 + 1} (α := E')
      (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(v.equiv v' e) : (a : E) → E') (⇑v : (a : ι) → E) i)
      (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι') i)
⊢ Eq (α := ι → E')
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(v.equiv v' e) : (a : E) → E') (⇑v : (a : ι) → E))
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι'))

Tactic:
ext i
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_5 : SeminormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_7 : SeminormedAddCommGroup E''
inst_8 : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
i : ι
⊢ Eq.{u_7 + 1} (α := E')
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(v.equiv v' e) : (a : E) → E') (⇑v : (a : ι) → E) i)
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι') i)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_5 : SeminormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_7 : SeminormedAddCommGroup E''
inst_8 : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
⊢ Eq (α := ι → E')
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(v.equiv v' e) : (a : E) → E') (⇑v : (a : ι) → E))
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι'))

Tactic:
have h : v.equiv v' e ∘ v = v' ∘ e := by
        ext i
        simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_5 : SeminormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_7 : SeminormedAddCommGroup E''
inst_8 : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
h :
  Eq (α := ι → E')
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(v.equiv v' e) : (a : E) → E') (⇑v : (a : ι) → E))
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι'))
rw :
  Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι'))
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(v.equiv v' e) : (a : E) → E') (⇑v : (a : ι) → E))

Tactic:
rw [h]
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_5 : SeminormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_7 : SeminormedAddCommGroup E''
inst_8 : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
h :
  Eq (α := ι → E')
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(v.equiv v' e) : (a : E) → E') (⇑v : (a : ι) → E))
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι'))
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι'))

Tactic:
hv'.comp _ e.injective

Premises used: Orthonormal.comp, Equiv.injective
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_5 : SeminormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_7 : SeminormedAddCommGroup E''
inst_8 : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
h :
  Eq (α := ι → E')
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(v.equiv v' e) : (a : E) → E') (⇑v : (a : ι) → E))
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι'))
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι'))

Tactic:
exact hv'.comp _ e.injective

Premises used: Orthonormal.comp, Equiv.injective
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_5 : SeminormedAddCommGroup E'
inst_6 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_7 : SeminormedAddCommGroup E''
inst_8 : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
h :
  Eq (α := ι → E')
    (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑(v.equiv v' e) : (a : E) → E') (⇑v : (a : ι) → E))
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι'))
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') (ι := ι)
    (Function.comp.{u_4 + 1, u_5 + 1, u_7 + 1} (β := ι') (⇑v' : (a : ι') → E') (⇑e : (a : ι) → ι'))

Tactic:
classical exact hv'.comp _ e.injective

Premises used: Orthonormal.comp, Equiv.injective
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
⊢ (hv.equiv hv' e).toLinearEquiv = v.equiv v' e

Tactic:
rfl

Premises used: Module.Basis.equiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
ι' : Type u_9
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_9} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
i : ι
⊢ Eq.{u_7 + 1} (α := E') ((hv.equiv hv' e : (a : E) → E') ((v : (a : ι) → E) i : E) : E')
    ((v' : (a : ι') → E') ((e : (a : ι) → ι') i : ι') : E')

Tactic:
Basis.equiv_apply _ _ _ _

Premises used: Module.Basis.equiv_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst_5 : SeminormedAddCommGroup E''
inst_6 : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
v'' : Basis ι'' 𝕜 E''
hv'' : Orthonormal.{u_1, u_8, u_6} 𝕜 (E := E'') (ι := ι'') (⇑v'' : (a : ι'') → E'')
e' : ι' ≃ ι''
i : ι
⊢ Eq.{u_8 + 1} (α := E'') (((hv.equiv hv' e).trans (hv'.equiv hv'' e') : (a : E) → E'') ((v : (a : ι) → E) i : E) : E'')
    ((hv.equiv hv'' (e.trans e') : (a : E) → E'') ((v : (a : ι) → E) i : E) : E'')

Tactic:
simp only [LinearIsometryEquiv.trans_apply, Orthonormal.equiv_apply, e.coe_trans,
      Function.comp_apply]

Premises used: LinearIsometryEquiv.trans_apply, Function.comp_apply, Equiv.coe_trans, Orthonormal.equiv_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_7, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
⊢ v.map (hv.equiv hv' e).toLinearEquiv = v'.reindex e.symm

Tactic:
v.map_equiv _ _

Premises used: Module.Basis.map_equiv, Module.Basis.equiv, LinearEquiv.trans
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
i : ι
⊢ Eq (α := E) ((hv.equiv hv (Equiv.refl ι) : (a : E) → E) ((v : (a : ι) → E) i : E) : E)
    ((LinearIsometryEquiv.refl 𝕜 E : (a : E) → E) ((v : (a : ι) → E) i : E) : E)

Tactic:
simp only [Orthonormal.equiv_apply, Equiv.coe_refl, id, LinearIsometryEquiv.coe_refl]

Premises used: id, Equiv.coe_refl, LinearIsometryEquiv.coe_refl, Orthonormal.equiv_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
E' : Type u_6
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
v : Basis ι 𝕜 E
hv : Orthonormal.{u_1, u_2, u_4} 𝕜 (E := E) (ι := ι) (⇑v : (a : ι) → E)
v' : Basis ι' 𝕜 E'
hv' : Orthonormal.{u_1, u_6, u_5} 𝕜 (E := E') (ι := ι') (⇑v' : (a : ι') → E')
e : ι ≃ ι'
i : ι'
⊢ Eq.{u_6 + 1} (α := E')
    ((hv.equiv hv' e : (a : E) → E') (((hv.equiv hv' e).symm : (a : E') → E) ((v' : (a : ι') → E') i : E') : E) : E')
    ((hv.equiv hv' e : (a : E) → E') ((hv'.equiv hv e.symm : (a : E') → E) ((v' : (a : ι') → E') i : E') : E) : E')

Tactic:
simp only [LinearIsometryEquiv.apply_symm_apply, Orthonormal.equiv_apply, e.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, LinearIsometryEquiv.apply_symm_apply, Orthonormal.equiv_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫) (∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫)

Tactic:
hv.inner_left_right_finset

Premises used: Orthonormal.inner_left_right_finset
-- Module: Mathlib.Analysis.InnerProductSpace.Orthonormal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
x : E
v : ι → E
s : Finset ι
hv : Orthonormal 𝕜 v
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫) (∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫)

Tactic:
exact hv.inner_left_right_finset

Premises used: Orthonormal.inner_left_right_finset