awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 : 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:
exact subset_span ⟨i, rfl⟩
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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))
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)
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E) (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → 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⟩

Premises used: eq_top_iff, SetLike.mem_coe, sum_mem, Submodule.smul_mem
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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.{u_2, u_1} (α := 𝕜)
    (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)) :
        𝕜))
    ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) : (a : E) → 𝕜) y : 𝕜)

Tactic:
(b.hasSum_repr y).mapL (innerSL 𝕜 x)

Premises used: innerSL, HilbertBasis.hasSum_repr, HasSum.mapL, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
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))
⊢ HasSum (fun (i : ι) ↦ ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫) ⟪x, y⟫

Tactic:
convert! (b.hasSum_repr y).mapL (innerSL 𝕜 x) using 1

Premises used: innerSL, HilbertBasis.hasSum_repr, HasSum.mapL, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
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))
⊢ 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:
ext i
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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⟫
h₃ h₄ : ⟪(b : (a : ι) → E) i, y⟫ * ⟪x, (b : (a : ι) → E) i⟫ = ⟪(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))

Tactic:
rw [innerSL_apply_apply, b.repr_apply_apply, inner_smul_right, mul_comm]

Premises used: innerSL_apply_apply, HilbertBasis.repr_apply_apply, inner_smul_right, mul_comm
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪x, (b : (a : ι) → E) i⟫ * ⟪(b : (a : ι) → E) i, y⟫

Tactic:
(b.hasSum_inner_mul_inner x y).summable

Premises used: HasSum.summable, HilbertBasis.hasSum_inner_mul_inner
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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⟫ = ⟪x, y⟫

Tactic:
(b.hasSum_inner_mul_inner x y).tsum_eq

Premises used: HasSum.tsum_eq, HilbertBasis.hasSum_inner_mul_inner
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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)))

Tactic:
Eq.ge ?_

Premises used: Eq.ge
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
refine : Eq.{u_3 + 1} (α := Submodule 𝕜 E) (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))) ⊤
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) ⊤ (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E)))

Tactic:
refine Eq.ge ?_

Premises used: Eq.ge
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
⊢ 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
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
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:
simpa only [Finset.coe_image, Finset.coe_univ, Set.image_univ, HilbertBasis.dense_span] using
        this.submodule_topologicalClosure_eq.symm

Premises used: Set.image_univ, Finset.coe_univ, IsClosed.submodule_topologicalClosure_eq, Finset.coe_image, HilbertBasis.dense_span, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
have 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))) ⊤
⊢ 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

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_image, HilbertBasis.dense_span
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
b : HilbertBasis ι 𝕜 E
⊢ Eq (α := (a : ι) → E) (⇑b.toOrthonormalBasis : (a : ι) → E) (⇑b : (a : ι) → E)

Tactic:
OrthonormalBasis.coe_mk _ _

Premises used: OrthonormalBasis.coe_mk
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : CompleteSpace.{u_3} ↥U
b : HilbertBasis.{u_1, u_2, u_3} ι 𝕜 ↥U
x : E
⊢ HasSum (α := ↥U) (fun (i : ι) ↦ HSMul.hSMul (β := ↥U) ⟪(↑((b : (a : ι) → ↥U) i) : E), x⟫ ((b : (a : ι) → ↥U) i : ↥U))
    ((U.orthogonalProjection : (a : E) → ↥U) x : ↥U)

Tactic:
simpa only [b.repr_apply_apply, inner_orthogonalProjection_eq_of_mem_left] using
    b.hasSum_repr (U.orthogonalProjection x)

Premises used: HilbertBasis.hasSum_repr, Submodule.orthogonalProjection, Submodule.inner_orthogonalProjection_eq_of_mem_left, HilbertBasis.repr_apply_apply, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
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))))
⊢ 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)))

Tactic:
simp_rw [← Submodule.span_iUnion]

Premises used: Submodule.span_iUnion
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 (span 𝕜 (⋃ (i : Finset ι), (↑(Finset.image (⇑b : (a : ι) → E) i) : Set E))))

Tactic:
topologicalClosure_mono (span_mono <| Set.range_subset_iff.mpr fun i =>
      Set.mem_iUnion_of_mem {i} <| Finset.mem_coe.mpr <| Finset.mem_image_of_mem _ <|
      Finset.mem_singleton_self i)

Premises used: Iff.mpr, Finset.mem_singleton_self, Submodule.topologicalClosure_mono, Submodule.span_mono, Set.mem_iUnion_of_mem, Finset.mem_image_of_mem, Set.range_subset_iff, Singleton.singleton, DFunLike.coe, Finset.mem_coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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 (span 𝕜 (⋃ (i : Finset ι), (↑(Finset.image (⇑b : (a : ι) → E) i) : Set E))))

Tactic:
exact topologicalClosure_mono (span_mono <| Set.range_subset_iff.mpr fun i =>
      Set.mem_iUnion_of_mem {i} <| Finset.mem_coe.mpr <| Finset.mem_image_of_mem _ <|
      Finset.mem_singleton_self i)

Premises used: Iff.mpr, Submodule.topologicalClosure_mono, Submodule.span_mono, Set.mem_iUnion_of_mem, Set.range_subset_iff, Finset.mem_coe
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
rw₂ rw₃ : 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

Tactic:
rw [IsHilbertSum.linearIsometryEquiv_symm_apply_single, LinearIsometry.toSpanSingleton_apply,
    one_smul]

Premises used: LinearIsometry.toSpanSingleton_apply, one_smul, IsHilbertSum.linearIsometryEquiv_symm_apply_single
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))
⊢ (⇑(HilbertBasis.mk hv hsp) : (a : ι) → E) = v

Tactic:
apply funext <| Orthonormal.linearIsometryEquiv_symm_apply_single_one hv hsp

Premises used: Orthonormal.linearIsometryEquiv_symm_apply_single_one, funext
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))
⊢ (⇑(HilbertBasis.mk hv hsp) : (a : ι) → E) = v

Tactic:
classical
  apply funext <| Orthonormal.linearIsometryEquiv_symm_apply_single_one hv hsp

Premises used: funext
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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))ᗮ ⊥
rw₃ rw₄ : Eq.{u_3 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
⊢ LE.le (α := Submodule 𝕜 E) ⊤ (topologicalClosure (span 𝕜 (Set.range v)))

Tactic:
rw [← orthogonal_orthogonal_eq_closure, ← eq_top_iff, orthogonal_eq_top_iff, hsp]

Premises used: eq_top_iff, Submodule.orthogonal_orthogonal_eq_closure, Submodule.orthogonal_eq_top_iff
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (Set.range v))ᗮ ⊥
⊢ (⇑(HilbertBasis.mkOfOrthogonalEqBot hv hsp) : (a : ι) → E) = v

Tactic:
HilbertBasis.coe_mk hv _

Premises used: HilbertBasis.coe_mk
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
inst_6 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ LE.le.{u_3} (α := Submodule 𝕜 E) ⊤
    (topologicalClosure (span 𝕜 (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → E))))

Tactic:
simpa only [← OrthonormalBasis.coe_toBasis, b.toBasis.span_eq, eq_top_iff] using
      @subset_closure E _ _

Premises used: eq_top_iff, subset_closure, OrthonormalBasis.coe_toBasis, Module.Basis.span_eq, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
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
inst_4 : Fintype ι
b : OrthonormalBasis ι 𝕜 E
⊢ Eq (α := (a : ι) → E) (⇑b.toHilbertBasis : (a : ι) → E) (⇑b : (a : ι) → E)

Tactic:
HilbertBasis.coe_mk _ _

Premises used: HilbertBasis.coe_mk
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
s : Set E
hs : Orthonormal.{u_2, u_3, u_3} 𝕜 (E := E) (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))
w : Set E
hws : w ⊇ s
hw_ortho : Orthonormal.{u_2, u_3, u_3} 𝕜 (E := E) (ι := { x : E // x ∈ w }) (Subtype.val (p := fun (x : E) ↦ x ∈ w))
hw_max :
  ∀ u ⊇ w,
    Orthonormal.{u_2, u_3, u_3} 𝕜 (E := E) (ι := { x : E // x ∈ u }) (Subtype.val (p := fun (x : E) ↦ x ∈ u)) → u = w
⊢ Eq.{u_3 + 1} (α := Submodule 𝕜 E)
    (span 𝕜 (Set.range (ι := (↑w : Type u_3)) (Subtype.val (p := fun (x : E) ↦ x ∈ w))))ᗮ ⊥

Tactic:
simpa only [Subtype.range_coe_subtype, Set.setOf_mem_eq,
      maximal_orthonormal_iff_orthogonalComplement_eq_bot hw_ortho] using hw_max

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq, maximal_orthonormal_iff_orthogonalComplement_eq_bot
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
⊢ ∃ (w : Set E) (b : HilbertBasis (↑w : Type u_3) 𝕜 E),
    Eq.{u_3 + 1} (α := (a : (↑w : Type u_3)) → E) (⇑b : (a : (↑w : Type u_3)) → E)
      (Subtype.val (p := fun (x : E) ↦ x ∈ w))

Tactic:
let ⟨w, hw, _, hw''⟩ := (orthonormal_empty 𝕜 E).exists_hilbertBasis_extension
  ⟨w, hw, hw''⟩

Premises used: orthonormal_empty, Orthonormal.exists_hilbertBasis_extension, _private.0.exists_hilbertBasis.match_1, Exists, Exists.intro, Subtype.val, Eq, DFunLike.coe
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Mul G
inst_1 : Inv G
f g : G → ℝ≥0∞
μ : Measure G
x : G
⊢ (f ⋆ₘₗ[μ] g) x = ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ

Tactic:
rfl

Premises used: MeasureTheory.mlconvolution, rfl
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Mul G
inst_1 : Inv G
f : G → ℝ≥0∞
μ : Measure G
h : ∀ (x : G), (0 ⋆ₘₗ[μ] f) x = 0 x
⊢ 0 ⋆ₘₗ[μ] f = 0

Tactic:
ext
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Mul G
inst_1 : Inv G
f : G → ℝ≥0∞
μ : Measure G
x : G
⊢ (0 ⋆ₘₗ[μ] f) x = 0 x

Tactic:
simp [mlconvolution]

Premises used: MeasureTheory.mlconvolution
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Mul G
inst_1 : Inv G
f : G → ℝ≥0∞
μ : Measure G
h : ∀ (x : G), (f ⋆ₘₗ[μ] 0) x = 0 x
⊢ f ⋆ₘₗ[μ] 0 = 0

Tactic:
ext
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Mul G
inst_1 : Inv G
f : G → ℝ≥0∞
μ : Measure G
x : G
⊢ (f ⋆ₘₗ[μ] 0) x = 0 x

Tactic:
simp [mlconvolution]

Premises used: MeasureTheory.mlconvolution
-- Module: Mathlib.Analysis.LConvolution
Goal:
G : Type u_1
mG : MeasurableSpace G
inst : Mul G
inst_1 : Inv G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
f g : G → ℝ≥0∞
μ : Measure G
inst_4 : SFinite μ
hf : Measurable f
hg : Measurable g
⊢ Measurable (β := ℝ≥0∞) fun (x : G) ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.LConvolution
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
funProp₂ : map (fun (a : G × G) ↦ a.1) (μ.prod μ) ≪ μ
funProp₃ : mG ≤ mG
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ g a0
funProp₅ : map (fun (a : G × G) ↦ a.1⁻¹ * a.2) (μ.prod μ) ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : G) ↦ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ) μ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.LConvolution
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 k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
h : ∀ (x : G), (f ⋆ₘₗ[μ] g ⋆ₘₗ[μ] k) x = ((f ⋆ₘₗ[μ] g) ⋆ₘₗ[μ] k) x
⊢ f ⋆ₘₗ[μ] g ⋆ₘₗ[μ] k = (f ⋆ₘₗ[μ] g) ⋆ₘₗ[μ] k

Tactic:
ext x
-- Module: Mathlib.Analysis.LConvolution
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 k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x y : G
funProp : mG ≤ mG
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : G) ↦ k a0
funProp₂ : map (fun (a : G) ↦ a⁻¹ * (y⁻¹ * x)) μ ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y_1 : G) ↦ g y_1 * k (y_1⁻¹ * (y⁻¹ * x))) μ

Tactic:
fun_prop