awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
classical :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      ((f : (a : E) → E') y : E') =
    ⟪(linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜), y⟫
classical₁ :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
        E') =
    inner.{u_1, u_2} 𝕜 (E := E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
⊢ inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
have classical₂ : inner.{u_1, u_7} 𝕜 (E := E')
    ((linearCombination 𝕜 (Function.comp.{u_4 + 1, u_2 + 1, u_7 + 1} (β := E) (⇑f : (a : E) → E') (⇑v : (a : ι) → E)) :
          (a : ι →₀ 𝕜) → E')
        ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) :
      E')
    ((f : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
      E') =
  inner.{u_1, u_2} 𝕜 (E := E)
    ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
    ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
Tactic: classical rw [← v.linearCombination_repr x, ← v.linearCombination_repr y,
      Finsupp.apply_linearCombination, Finsupp.apply_linearCombination,
      hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
⊢ inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
have 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⟫
Tactic: rw [← LinearEquiv.coe_coe] at hf
Cleared hypotheses: hf, x, y
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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 : 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⟫
have rw : inner.{u_1, u_7} 𝕜 (E := E')
    ((f : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
      E')
    ((f : (a : E) → E') y : E') =
  ⟪(linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜), y⟫
Tactic: rw [← v.linearCombination_repr x, ← v.linearCombination_repr y,
      ← LinearEquiv.coe_coe f, Finsupp.apply_linearCombination,
      Finsupp.apply_linearCombination, hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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 : E →ₗ[𝕜] E') : (a : E) → E') (⇑v : (a : ι) → E))
x y : E
rw :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      ((f : (a : E) → E') y : E') =
    ⟪(linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜), y⟫
⊢ inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
have rw₁ : inner.{u_1, u_7} 𝕜 (E := E')
    ((f : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
      E')
    ((f : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
      E') =
  inner.{u_1, u_2} 𝕜 (E := E)
    ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
    ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
Tactic: rw [← v.linearCombination_repr x, ← v.linearCombination_repr y,
      ← LinearEquiv.coe_coe f, Finsupp.apply_linearCombination,
      Finsupp.apply_linearCombination, hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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 : E →ₗ[𝕜] E') : (a : E) → E') (⇑v : (a : ι) → E))
x y : E
rw :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      ((f : (a : E) → E') y : E') =
    ⟪(linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜), y⟫
rw₁ :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
        E') =
    inner.{u_1, u_2} 𝕜 (E := E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
⊢ inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
have rw₂ : inner.{u_1, u_7} 𝕜 (E := E')
    (((↑f : E →ₗ[𝕜] E') : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
      E')
    (((↑f : E →ₗ[𝕜] E') : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
      E') =
  inner.{u_1, u_2} 𝕜 (E := E)
    ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
    ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
Tactic: rw [← v.linearCombination_repr x, ← v.linearCombination_repr y,
      ← LinearEquiv.coe_coe f, Finsupp.apply_linearCombination,
      Finsupp.apply_linearCombination, hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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 : 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⟫
have classical : inner.{u_1, u_7} 𝕜 (E := E')
    ((f : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
      E')
    ((f : (a : E) → E') y : E') =
  ⟪(linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜), y⟫
Tactic: classical rw [← v.linearCombination_repr x, ← v.linearCombination_repr y,
      ← LinearEquiv.coe_coe f, Finsupp.apply_linearCombination,
      Finsupp.apply_linearCombination, hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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 : E →ₗ[𝕜] E') : (a : E) → E') (⇑v : (a : ι) → E))
x y : E
classical :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      ((f : (a : E) → E') y : E') =
    ⟪(linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜), y⟫
⊢ inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
have classical₁ : inner.{u_1, u_7} 𝕜 (E := E')
    ((f : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
      E')
    ((f : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
      E') =
  inner.{u_1, u_2} 𝕜 (E := E)
    ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
    ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
Tactic: classical rw [← v.linearCombination_repr x, ← v.linearCombination_repr y,
      ← LinearEquiv.coe_coe f, Finsupp.apply_linearCombination,
      Finsupp.apply_linearCombination, hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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 : E →ₗ[𝕜] E') : (a : E) → E') (⇑v : (a : ι) → E))
x y : E
classical :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      ((f : (a : E) → E') y : E') =
    ⟪(linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜), y⟫
classical₁ :
  inner.{u_1, u_7} 𝕜 (E := E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
        E')
      ((f : (a : E) → E')
          ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
        E') =
    inner.{u_1, u_2} 𝕜 (E := E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
      ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
⊢ inner.{u_1, u_7} 𝕜 (E := E') ((f : (a : E) → E') x : E') ((f : (a : E) → E') y : E') = ⟪x, y⟫
have classical₂ : inner.{u_1, u_7} 𝕜 (E := E')
    (((↑f : E →ₗ[𝕜] E') : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E) :
      E')
    (((↑f : E →ₗ[𝕜] E') : (a : E) → E')
        ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E) :
      E') =
  inner.{u_1, u_2} 𝕜 (E := E)
    ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : E)
    ((linearCombination 𝕜 (⇑v : (a : ι) → E) : (a : ι →₀ 𝕜) → E) ((v.repr : (a : E) → ι →₀ 𝕜) y : ι →₀ 𝕜) : E)
Tactic: classical rw [← v.linearCombination_repr x, ← v.linearCombination_repr y,
      ← LinearEquiv.coe_coe f, Finsupp.apply_linearCombination,
      Finsupp.apply_linearCombination, hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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 : ι) → ι'))
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
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 : ι ≃ ι'
⊢ 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))
have 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 : ι) → ι'))
Tactic: have h : v.equiv v' e ∘ v = v' ∘ e := by
        ext i
        simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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_2 + 1, u_7 + 1} (β := E) (⇑(v.equiv v' e) : (a : E) → E') (⇑v : (a : ι) → E))
have 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 : ι) → ι'))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
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
⊢ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
have h₂ : 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: have h₂ :
    (∑ i ∈ s, ∑ j ∈ s, ⟪v i, x⟫ * ⟪x, v j⟫ * ⟪v j, v i⟫) = (∑ k ∈ s, ⟪v k, x⟫ * ⟪x, v k⟫ : 𝕜) := by
    classical exact hv.inner_left_right_finset
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
h₂ : 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⟫)
z : 𝕜
⊢ (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)) = HPow.hPow (β := ℕ) ‖z‖ 2
have simp : (re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖z‖ : 𝕜) 2) = HPow.hPow (β := ℕ) ‖z‖ 2
Tactic: simp only [mul_conj]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
h₂ : 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⟫)
z : 𝕜
⊢ (re : (a : 𝕜) → ℝ) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖z‖ : 𝕜) 2) = HPow.hPow (β := ℕ) ‖z‖ 2
have norm_cast : HPow.hPow (β := ℕ) ‖z‖ 2 = HPow.hPow (β := ℕ) ‖z‖ 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (hypothesis)
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
h₂ : 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⟫)
⊢ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
have h₃ : ∀ (z : 𝕜), (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)) = HPow.hPow (β := ℕ) ‖z‖ 2
Tactic: have h₃ : ∀ z : 𝕜, re (z * conj z) = ‖z‖ ^ 2 := by
    intro z
    simp only [mul_conj]
    norm_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
h₂ : 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⟫)
h₃ :
  ∀ (z : 𝕜), (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)) = HPow.hPow (β := ℕ) ‖z‖ 2
hbf :
  HPow.hPow (β := ℕ) ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ 2 =
    HPow.hPow (β := ℕ) ‖x‖ 2 - ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
⊢ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
have rw : 0 ≤ HPow.hPow (β := ℕ) ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ 2
Tactic: rw [← sub_nonneg, ← hbf]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orthonormal (goal)
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
h₂ : 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⟫)
h₃ :
  ∀ (z : 𝕜), (re : (a : 𝕜) → ℝ) (HMul.hMul (β := 𝕜) z ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) z : 𝕜)) = HPow.hPow (β := ℕ) ‖z‖ 2
⊢ ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
have suffices : HPow.hPow (β := ℕ) ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2 - ∑ i ∈ s, HPow.hPow (β := ℕ) ‖⟪v i, x⟫‖ 2
Tactic: suffices hbf : ‖x - ∑ i ∈ s, ⟪v i, x⟫ • v i‖ ^ 2 = ‖x‖ ^ 2 - ∑ i ∈ s, ‖⟪v i, x⟫‖ ^ 2 by
    rw [← sub_nonneg, ← hbf]
    simp only [norm_nonneg, pow_nonneg]