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
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
η : Type u_5
s : η → Set E
hs : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ (i : η), Orthonormal 𝕜 (E := E) fun (x : (↑(s i) : Type u_2)) ↦ (↑x : E)
rw rw₁ rw₂ :
  ∀ (v : E),
    Membership.mem (γ := Set E) (⋃ (i : η), s i) v →
      ∀ (w : E), Membership.mem (γ := Set E) (⋃ (i : η), s i) w → ⟪v, w⟫ = if v = w then 1 else 0
rw₃ :
  ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
    (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y), ⟪x, y⟫ = if x = y then 1 else 0
rw₄ :
  ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
    (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y) (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k),
    ⟪x, y⟫ = if x = y then 1 else 0
rw₅ :
  ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
    (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y) (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k)
    (h_orth : Orthonormal 𝕜 (E := E) fun (x : (↑(s k) : Type u_2)) ↦ (↑x : E)), ⟪x, y⟫ = if x = y then 1 else 0
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : η), s i) : Type u_2)) ↦ (↑x : E)
have rw₆ : ∀ (x : E) (i : η) (hxi : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) i) x) (y : E) (j : η)
  (hyj : Membership.mem (γ := Set E) ((fun (i : η) ↦ s i) j) y) (k : η) (hik : s i ⊆ s k) (hjk : s j ⊆ s k)
  (h_orth : ∀ v ∈ s k, ∀ w ∈ s k, ⟪v, w⟫ = if v = w then 1 else 0), ⟪x, y⟫ = if x = y then 1 else 0
Tactic: classical
  rw [orthonormal_subtype_iff_ite]
  rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩
  obtain ⟨k, hik, hjk⟩ := hs i j
  have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
  rw [orthonormal_subtype_iff_ite] at h_orth
  exact h_orth x (hik hxi) y (hjk hyj)
-- 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
s : Set (Set E)
hs : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, Orthonormal 𝕜 (E := E) fun (x : (↑a : Type u_2)) ↦ (↑x : E)
⊢ Orthonormal 𝕜 (E := E) fun (x : (↑(⋃₀ s) : Type u_2)) ↦ (↑x : E)
have rw : Orthonormal 𝕜 (E := E) fun (x : (↑(⋃ (i : (↑s : Type u_2)), (↑i : Set E)) : Type u_2)) ↦ (↑x : E)
Tactic: rw [Set.sUnion_eq_iUnion]
-- 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
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))
⊢ ∃ w ⊇ s,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
      ∀ u ⊇ w,
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
          u = w
have refine_2 : ∀
  (this :
    ∃ (m : Set E),
      s ⊆ m ∧
        Maximal
          (fun (x : Set E) ↦
            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))}
              x)
          m),
  ∃ w ⊇ s,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
      ∀ u ⊇ w,
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
          u = w
Tactic: have := zorn_subset_nonempty { b | Orthonormal 𝕜 (Subtype.val : b → E) } ?_ _ hs
-- 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
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))
refine_2 :
  ∀
    (this :
      ∃ (m : Set E),
        s ⊆ m ∧
          Maximal
            (fun (x : Set E) ↦
              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))}
                x)
            m),
    ∃ w ⊇ s,
      Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
        ∀ u ⊇ w,
          Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
            u = w
⊢ ∃ w ⊇ s,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
      ∀ u ⊇ w,
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
          u = w
have refine_1 : ∀
  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))},
  IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c →
    c.Nonempty →
      ∃ (ub : Set E),
        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))}
            ub ∧
          ∀ s ∈ c, s ⊆ ub
Tactic: have := zorn_subset_nonempty { b | Orthonormal 𝕜 (Subtype.val : b → E) } ?_ _ hs
-- 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
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))
this :
  ∃ (m : Set E),
    s ⊆ m ∧
      Maximal
        (fun (x : Set E) ↦
          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))}
            x)
        m
⊢ ∃ w ⊇ s,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
      ∀ u ⊇ w,
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
          u = w
have refine_2 : ∀ (b : Set E)
  (hb :
    s ⊆ b ∧
      Maximal
        (fun (x : Set E) ↦
          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))}
            x)
        b),
  ∃ w ⊇ s,
    Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w)) ∧
      ∀ u ⊇ w,
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) →
          u = w
Tactic: obtain ⟨b, hb⟩ := this
Cleared hypotheses: this
-- 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
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 ⊆
      {b : Set E |
        Orthonormal.{u_1, u_2, u_2} 𝕜 (E := E) (ι := { x : E // x ∈ b }) (Subtype.val (p := fun (x : E) ↦ x ∈ b))},
    IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set E),
          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))}
              ub ∧
            ∀ s ∈ c, s ⊆ ub
have refine_1 : ∀ (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: refine fun c hc cc _c0 => ⟨⋃₀ c, ?_, ?_⟩
-- 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
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))
refine_1 :
  ∀ (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)
⊢ ∀
    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))},
    IsChain (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c →
      c.Nonempty →
        ∃ (ub : Set E),
          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))}
              ub ∧
            ∀ s ∈ c, s ⊆ ub
have refine_1₁ : ∀ (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: refine fun c hc cc _c0 => ⟨⋃₀ c, ?_, ?_⟩
-- 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
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ v i ≠ 0
have refine : ‖v i‖ ≠ Norm.norm.{u_2} (E := E) 0
Tactic: refine ne_of_apply_ne norm ?_
-- 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
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ ‖v i‖ ≠ Norm.norm.{u_2} (E := E) 0
have rw : Ne (α := ℝ) 1 0
Tactic: rw [hv.1 i, norm_zero]
-- 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
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
v : ι → E
f : E →ₗᵢ[𝕜] E'
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') ((⇑f : (a : E) → E') ∘ v) ↔ Orthonormal 𝕜 v
have 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
Tactic: simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]
-- 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
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
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') ((⇑f : (a : E) → E') ∘ v) ↔ Orthonormal 𝕜 v
have 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
Tactic: simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]
-- 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
E' : Type u_7
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
v : ι → E
f : E →ₗᵢ[𝕜] E'
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') ((⇑f : (a : E) → E') ∘ v) ↔ Orthonormal 𝕜 v
have 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
Tactic: classical simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]
-- 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
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
⊢ Orthonormal.{u_1, u_7, u_4} 𝕜 (E := E') ((⇑f : (a : E) → E') ∘ v) ↔ Orthonormal 𝕜 v
have 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
Tactic: classical simp_rw [orthonormal_iff_ite, Function.comp_apply, LinearIsometry.inner_map_map]
-- 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 : 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,
      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
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,
      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
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')
    ((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: 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 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,
      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
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,
      Finsupp.apply_linearCombination, Finsupp.apply_linearCombination,
      hv.inner_finsupp_eq_sum_left, hf.inner_finsupp_eq_sum_left]