awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
rw rw₁ rw₂ :
  LE.le.{u_3} (α := Submodule 𝕜 E) ⊤
    (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
rw₃ :
  ∀ ⦃x : E⦄,
    Membership.mem (γ := Submodule 𝕜 E)
      (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x
rw₄ rw₅ :
  ∀ ⦃x : E⦄ (s : Finset ι),
    ∑ b_1 ∈ s,
        (fun (i : ι) ↦
            HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
              ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
              ((b : (a : ι) → E) i : E))
          b_1 ∈
      (↑(toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) : Set E)
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⊤
have rw₆ : ∀ ⦃x : E⦄ (s : Finset ι),
  Membership.mem (γ := AddSubmonoid E) (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (∑ x_1 ∈ s,
      HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) x_1) ((b : (a : ι) → E) x_1 : E))
Tactic: classical
    rw [eq_top_iff]
    rintro x -
    refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)
    intro s
    simp only [SetLike.mem_coe]
    refine sum_mem ?_
    rintro i -
    refine smul_mem _ _ ?_
    exact subset_span ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
rw rw₁ rw₂ :
  LE.le.{u_3} (α := Submodule 𝕜 E) ⊤
    (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
rw₃ :
  ∀ ⦃x : E⦄,
    Membership.mem (γ := Submodule 𝕜 E)
      (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x
rw₄ rw₅ :
  ∀ ⦃x : E⦄ (s : Finset ι),
    ∑ b_1 ∈ s,
        (fun (i : ι) ↦
            HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
              ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
              ((b : (a : ι) → E) i : E))
          b_1 ∈
      (↑(toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) : Set E)
rw₆ :
  ∀ ⦃x : E⦄ (s : Finset ι),
    Membership.mem (γ := AddSubmonoid E)
      (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
      (∑ x_1 ∈ s,
        HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
          ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) x_1) ((b : (a : ι) → E) x_1 : E))
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⊤
have rw₇ : ∀ ⦃x : E⦄ (s : Finset ι),
  ∀ c ∈ s,
    Membership.mem (γ := AddSubmonoid E)
      (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
      (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) c) ((b : (a : ι) → E) c : E))
Tactic: classical
    rw [eq_top_iff]
    rintro x -
    refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)
    intro s
    simp only [SetLike.mem_coe]
    refine sum_mem ?_
    rintro i -
    refine smul_mem _ _ ?_
    exact subset_span ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
rw rw₁ rw₂ :
  LE.le.{u_3} (α := Submodule 𝕜 E) ⊤
    (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
rw₃ :
  ∀ ⦃x : E⦄,
    Membership.mem (γ := Submodule 𝕜 E)
      (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x
rw₄ rw₅ :
  ∀ ⦃x : E⦄ (s : Finset ι),
    ∑ b_1 ∈ s,
        (fun (i : ι) ↦
            HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
              ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
              ((b : (a : ι) → E) i : E))
          b_1 ∈
      (↑(toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) : Set E)
rw₆ :
  ∀ ⦃x : E⦄ (s : Finset ι),
    Membership.mem (γ := AddSubmonoid E)
      (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
      (∑ x_1 ∈ s,
        HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
          ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) x_1) ((b : (a : ι) → E) x_1 : E))
rw₇ :
  ∀ ⦃x : E⦄ (s : Finset ι),
    ∀ c ∈ s,
      Membership.mem (γ := AddSubmonoid E)
        (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
        (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
          ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) c) ((b : (a : ι) → E) c : E))
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⊤
have rw₈ : ∀ ⦃x : E⦄ (s : Finset ι) (i : ι),
  Membership.mem (γ := AddSubmonoid E) (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
      ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) i) ((b : (a : ι) → E) i : E))
Tactic: classical
    rw [eq_top_iff]
    rintro x -
    refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)
    intro s
    simp only [SetLike.mem_coe]
    refine sum_mem ?_
    rintro i -
    refine smul_mem _ _ ?_
    exact subset_span ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
rw rw₁ rw₂ :
  LE.le.{u_3} (α := Submodule 𝕜 E) ⊤
    (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
rw₃ :
  ∀ ⦃x : E⦄,
    Membership.mem (γ := Submodule 𝕜 E)
      (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) x
rw₄ rw₅ :
  ∀ ⦃x : E⦄ (s : Finset ι),
    ∑ b_1 ∈ s,
        (fun (i : ι) ↦
            HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
              ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
              ((b : (a : ι) → E) i : E))
          b_1 ∈
      (↑(toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))) : Set E)
rw₆ :
  ∀ ⦃x : E⦄ (s : Finset ι),
    Membership.mem (γ := AddSubmonoid E)
      (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
      (∑ x_1 ∈ s,
        HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
          ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) x_1) ((b : (a : ι) → E) x_1 : E))
rw₇ :
  ∀ ⦃x : E⦄ (s : Finset ι),
    ∀ c ∈ s,
      Membership.mem (γ := AddSubmonoid E)
        (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
        (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
          ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) c) ((b : (a : ι) → E) c : E))
rw₈ :
  ∀ ⦃x : E⦄ (s : Finset ι) (i : ι),
    Membership.mem (γ := AddSubmonoid E)
      (toAddSubmonoid (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
      (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) x) : (i : ι) → 𝕜) i) ((b : (a : ι) → E) i : E))
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⊤
have rw₉ : ∀ ⦃x : E⦄ (s : Finset ι) (i : ι),
  Membership.mem.{u_3, u_3} (α := E) (γ := Submodule 𝕜 E)
    (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))) ((b : (a : ι) → E) i : E)
Tactic: classical
    rw [eq_top_iff]
    rintro x -
    refine mem_closure_of_tendsto (b.hasSum_repr x) (Eventually.of_forall ?_)
    intro s
    simp only [SetLike.mem_coe]
    refine sum_mem ?_
    rintro i -
    refine smul_mem _ _ ?_
    exact subset_span ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
⊢ HasSum (fun (i : ι) ↦ ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫) ⟪x, y⟫
have h : Eq (α := ι → 𝕜) (fun (i : ι) ↦ ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫) fun (b_1 : ι) ↦
  (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) b_1) (β := E)
      ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) b_1)
      ((b : (a : ι) → E) b_1 : E))
Tactic: convert! (b.hasSum_repr y).mapL (innerSL 𝕜 x) using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
⊢ Eq (α := ι → 𝕜) (fun (i : ι) ↦ ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫) fun (b_1 : ι) ↦
    (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) b_1) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) b_1)
        ((b : (a : ι) → E) b_1 : E))
have h : ∀ (i : ι),
  ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
    (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
        ((b : (a : ι) → E) i : E))
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
⊢ ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
    (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
        ((b : (a : ι) → E) i : E))
have h : ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
  ⟪x,
    HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
      ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
      ((b : (a : ι) → E) i : E)⟫
Tactic: rw [innerSL_apply_apply, b.repr_apply_apply, inner_smul_right, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
h :
  ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
    ⟪x,
      HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
        ((b : (a : ι) → E) i : E)⟫
⊢ ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
    (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
        ((b : (a : ι) → E) i : E))
have h₁ : ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
  ⟪x, HSMul.hSMul (β := E) ⟪(b : (a : ι) → E) i, y⟫ ((b : (a : ι) → E) i : E)⟫
Tactic: rw [innerSL_apply_apply, b.repr_apply_apply, inner_smul_right, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
h :
  ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
    ⟪x,
      HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
        ((b : (a : ι) → E) i : E)⟫
h₁ :
  ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
    ⟪x, HSMul.hSMul (β := E) ⟪(b : (a : ι) → E) i, y⟫ ((b : (a : ι) → E) i : E)⟫
⊢ ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
    (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
        ((b : (a : ι) → E) i : E))
have h₂ : ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ = ⟪(b : (a : ι) → E) i, y⟫ * ⟪x, (b : (a : ι) → E) i⟫
Tactic: rw [innerSL_apply_apply, b.repr_apply_apply, inner_smul_right, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
h :
  ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
    ⟪x,
      HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
        ((b : (a : ι) → E) i : E)⟫
h₁ :
  ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
    ⟪x, HSMul.hSMul (β := E) ⟪(b : (a : ι) → E) i, y⟫ ((b : (a : ι) → E) i : E)⟫
h₂ : ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ = ⟪(b : (a : ι) → E) i, y⟫ * ⟪x, (b : (a : ι) → E) i⟫
⊢ ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫ =
    (((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := (fun (x : ι) ↦ 𝕜) i) (β := E)
        ((↑((b.repr : (a : E) → ↥(lp (fun (x : ι) ↦ 𝕜) 2)) y) : (i : ι) → (fun (x : ι) ↦ 𝕜) i) i)
        ((b : (a : ι) → E) i : E))
have h₃ : ⟪(b : (a : ι) → E) i, y⟫ * ⟪x, (b : (a : ι) → E) i⟫ = ⟪(b : (a : ι) → E) i, y⟫ * ⟪x, (b : (a : ι) → E) i⟫
Tactic: rw [innerSL_apply_apply, b.repr_apply_apply, inner_smul_right, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : Fintype ι
b : HilbertBasis ι 𝕜 E
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))
have refine : Eq.{u_3 + 1} (α := Submodule 𝕜 E) (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))) ⊤
Tactic: refine Eq.ge ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (hypothesis)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : Fintype ι
b : HilbertBasis ι 𝕜 E
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))) ⊤
have this : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
  (↑(span 𝕜 (↑(Finset.image.{u_1, u_3} (α := ι) (⇑b : (a : ι) → E) Finset.univ) : Set E)) : Set E)
Tactic: have := (span 𝕜 (Finset.univ.image b : Set E)).closed_of_finiteDimensional
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : Fintype ι
b : HilbertBasis ι 𝕜 E
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))) ⊤
have have : ∀
  (this :
    IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (↑(span 𝕜 (↑(Finset.image.{u_1, u_3} (α := ι) (⇑b : (a : ι) → E) Finset.univ) : Set E)) : Set E)),
  Eq.{u_3 + 1} (α := Submodule 𝕜 E) (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))) ⊤
Tactic: classical
      have := (span 𝕜 (Finset.univ.image b : Set E)).closed_of_finiteDimensional
      simpa only [Finset.coe_image, Finset.coe_univ, Set.image_univ, HilbertBasis.dense_span] using
        this.submodule_topologicalClosure_eq.symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq E
b : HilbertBasis ι 𝕜 E
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (topologicalClosure (⨆ (J : Finset ι), span 𝕜 (↑(Finset.image (⇑b : (a : ι) → E) J) : Set E)))
have simp_rw : LE.le.{u_3} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))
  (topologicalClosure (span 𝕜 (⋃ (i : Finset ι), (↑(Finset.image (⇑b : (a : ι) → E) i) : Set E))))
Tactic: simp_rw [← Submodule.span_iUnion]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
inst_4 : DecidableEq ι
h : LE.le (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))
i : ι
⊢ ((IsHilbertSum.linearIsometryEquiv (G := fun (x : ι) ↦ 𝕜) ⋯).symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
      (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) =
    v i
have rw : ((LinearIsometry.toSpanSingleton 𝕜 E sorry : 𝕜 →ₗᵢ[𝕜] E) : (a : 𝕜) → E) 1 = v i
Tactic: rw [IsHilbertSum.linearIsometryEquiv_symm_apply_single, LinearIsometry.toSpanSingleton_apply,
    one_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
inst_4 : DecidableEq ι
h : LE.le (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))
i : ι
rw : ((LinearIsometry.toSpanSingleton 𝕜 E ⋯ : 𝕜 →ₗᵢ[𝕜] E) : (a : 𝕜) → E) 1 = v i
⊢ ((IsHilbertSum.linearIsometryEquiv (G := fun (x : ι) ↦ 𝕜) ⋯).symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
      (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) =
    v i
have rw₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 1 (v i) = v i
Tactic: rw [IsHilbertSum.linearIsometryEquiv_symm_apply_single, LinearIsometry.toSpanSingleton_apply,
    one_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
inst_4 : DecidableEq ι
h : LE.le (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))
i : ι
rw : ((LinearIsometry.toSpanSingleton 𝕜 E ⋯ : 𝕜 →ₗᵢ[𝕜] E) : (a : 𝕜) → E) 1 = v i
rw₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕜) 1 (v i) = v i
⊢ ((IsHilbertSum.linearIsometryEquiv (G := fun (x : ι) ↦ 𝕜) ⋯).symm : (a : ↥(lp (fun (x : ι) ↦ 𝕜) 2)) → E)
      (lp.single (E := fun (x : ι) ↦ 𝕜) 2 i 1) =
    v i
have rw₂ : v i = v i
Tactic: rw [IsHilbertSum.linearIsometryEquiv_symm_apply_single, LinearIsometry.toSpanSingleton_apply,
    one_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (Set.range v))ᗮ ⊥
⊢ LE.le (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))
have rw : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (Set.range v))ᗮᗮ
Tactic: rw [← orthogonal_orthogonal_eq_closure, ← eq_top_iff, orthogonal_eq_top_iff, hsp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (Set.range v))ᗮ ⊥
rw : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (Set.range v))ᗮᗮ
⊢ LE.le (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))
have rw₁ : Eq (α := Submodule 𝕜 E) (span 𝕜 (Set.range v))ᗮᗮ ⊤
Tactic: rw [← orthogonal_orthogonal_eq_closure, ← eq_top_iff, orthogonal_eq_top_iff, hsp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
inst_5 : CompleteSpace E
v : ι → E
hv : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (Set.range v))ᗮ ⊥
rw : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (Set.range v))ᗮᗮ
rw₁ : Eq (α := Submodule 𝕜 E) (span 𝕜 (Set.range v))ᗮᗮ ⊤
rw₂ : Eq (α := Submodule 𝕜 E) (span 𝕜 (Set.range v))ᗮ ⊥
⊢ LE.le (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))
have rw₃ : Eq.{u_3 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
Tactic: rw [← orthogonal_orthogonal_eq_closure, ← eq_top_iff, orthogonal_eq_top_iff, hsp]
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Mul G
inst_1 : Inv G
f : G → ℝ≥0∞
μ : Measure G
⊢ 0 ⋆ₘₗ[μ] f = 0
have h : ∀ (x : G), (0 ⋆ₘₗ[μ] f) x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Mul G
inst_1 : Inv G
f : G → ℝ≥0∞
μ : Measure G
⊢ f ⋆ₘₗ[μ] 0 = 0
have h : ∀ (x : G), (f ⋆ₘₗ[μ] 0) x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : G) ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ) μ
have funProp : mG ≤ mG
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
funProp : mG ≤ mG
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : G) ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ) μ
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.LConvolution (goal)
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Group G
inst_1 : MeasurableMul₂ G
inst_2 : MeasurableInv G
μ : Measure G
inst_3 : μ.IsMulLeftInvariant
inst_4 : SFinite μ
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ f a0
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : G) ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ) μ
have funProp₂ : map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
Tactic: fun_prop