awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
rw :
  Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℝ)
⊢ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℝ)

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
rw rw₁ :
  Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
⊢ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℝ)

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
iterate iterate₁ iterate₂ iterate₃ :
  Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℝ)
⊢ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℝ)

Tactic:
iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x : E
rw :
  Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
    ((Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) ((f : (a : E) → ℂ) x : ℂ) : ℂ)
rw₁ :
  Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
    ((rightAngleRotation
            (((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
                (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
              o) :
          (a : ℂ) → ℂ)
        ((f : (a : E) → ℂ) x : ℂ) :
      ℂ)
rw₂ :
  Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
    ((f : (a : E) → ℂ)
        ((o.rightAngleRotation : (a : E) → E) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E) :
      ℂ)
rw₃ rw₄ :
  Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
    ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
⊢ (f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) = HMul.hMul (β := ℂ) I ((f : (a : E) → ℂ) x : ℂ)

Tactic:
rw [← Complex.rightAngleRotation, ← hf, rightAngleRotation_map,
    LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply, Orientation.rightAngleRotation_map, Complex.rightAngleRotation
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
rw :
  Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℂ) :
          (a : E) → ℂ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℂ)
⊢ (((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y =
    HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : E) → ℂ) y : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : E) → ℂ) x : ℂ) : ℂ)

Tactic:
rw [← Complex.kahler, ← hf, kahler_map]

Premises used: Complex.kahler, Orientation.kahler_map
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
rw :
  Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℂ)
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℂ) :
          (a : E) → ℂ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℂ)

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
rw rw₁ :
  Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℂ)

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
iterate iterate₁ iterate₂ iterate₃ :
  Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℂ)
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℂ) :
          (a : E) → ℂ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℂ)

Tactic:
iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
A B : E →WOT[𝕜] F
h : ∀ (x : E) (y : F), ⟪y, (A : (a : E) → F) x⟫_𝕜 = ⟪y, (B : (a : E) → F) x⟫_𝕜
rw : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) x : F) ((B : (a : E) → F) x : F)
⊢ A = B

Tactic:
rw [ContinuousLinearMapWOT.ext_iff]

Premises used: ContinuousLinearMapWOT.ext_iff
-- Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
A B : E →WOT[𝕜] F
h : ∀ (x : E) (y : F), ⟪y, (A : (a : E) → F) x⟫_𝕜 = ⟪y, (B : (a : E) → F) x⟫_𝕜
⊢ ∀ (x : E), Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) x : F) ((B : (a : E) → F) x : F)

Tactic:
fun x => ext_inner_left 𝕜 fun y => h x y

Premises used: ext_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
A B : E →WOT[𝕜] F
h : ∀ (x : E) (y : F), ⟪y, (A : (a : E) → F) x⟫_𝕜 = ⟪y, (B : (a : E) → F) x⟫_𝕜
⊢ ∀ (x : E), Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) x : F) ((B : (a : E) → F) x : F)

Tactic:
exact fun x => ext_inner_left 𝕜 fun y => h x y

Premises used: ext_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : CompleteSpace F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
simp_rw :
  (∀ (x : E) (y : StrongDual 𝕜 F),
      Tendsto.{u_4, u_1} (β := 𝕜) (fun (a : α) ↦ ((y : (a : F) → 𝕜) ((f a : (a : E) → F) x : F) : 𝕜)) l
        (𝓝 ((y : (a : F) → 𝕜) ((A : (a : E) → F) x : F)) : Filter 𝕜)) ↔
    ∀ (x : E) (y : F), Tendsto (fun (a : α) ↦ ⟪y, (f a : (a : E) → F) x⟫_𝕜) l (𝓝 ⟪y, (A : (a : E) → F) x⟫_𝕜)
⊢ Tendsto f l (𝓝 A) ↔
    ∀ (x : E) (y : F), Tendsto (fun (a : α) ↦ ⟪y, (f a : (a : E) → F) x⟫_𝕜) l (𝓝 ⟪y, (A : (a : E) → F) x⟫_𝕜)

Tactic:
simp_rw [tendsto_iff_forall_dual_apply_tendsto]

Premises used: ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto
-- Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : CompleteSpace F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
⊢ (∀ (x : E) (y : StrongDual 𝕜 F),
      Tendsto.{u_4, u_1} (β := 𝕜) (fun (a : α) ↦ ((y : (a : F) → 𝕜) ((f a : (a : E) → F) x : F) : 𝕜)) l
        (𝓝 ((y : (a : F) → 𝕜) ((A : (a : E) → F) x : F)) : Filter 𝕜)) ↔
    ∀ (x : E) (y : F), Tendsto (fun (a : α) ↦ ⟪y, (f a : (a : E) → F) x⟫_𝕜) l (𝓝 ⟪y, (A : (a : E) → F) x⟫_𝕜)

Tactic:
.symm <| forall_congr' fun _ ↦
    Equiv.forall_congr (InnerProductSpace.toDual 𝕜 F) fun _ ↦ Iff.rfl

Premises used: InnerProductSpace.toDual, Iff.rfl, forall_congr', Equiv.forall_congr, EquivLike.toEquiv, Iff.symm
-- Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : CompleteSpace F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
⊢ (∀ (x : E) (y : StrongDual 𝕜 F),
      Tendsto.{u_4, u_1} (β := 𝕜) (fun (a : α) ↦ ((y : (a : F) → 𝕜) ((f a : (a : E) → F) x : F) : 𝕜)) l
        (𝓝 ((y : (a : F) → 𝕜) ((A : (a : E) → F) x : F)) : Filter 𝕜)) ↔
    ∀ (x : E) (y : F), Tendsto (fun (a : α) ↦ ⟪y, (f a : (a : E) → F) x⟫_𝕜) l (𝓝 ⟪y, (A : (a : E) → F) x⟫_𝕜)

Tactic:
exact .symm <| forall_congr' fun _ ↦
    Equiv.forall_congr (InnerProductSpace.toDual 𝕜 F) fun _ ↦ Iff.rfl

Premises used: forall_congr', Equiv.forall_congr
-- Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : CompleteSpace F
l : Filter (E →WOT[𝕜] F)
A : E →WOT[𝕜] F
⊢ l ≤ 𝓝 A ↔
    ∀ (x : E) (y : F), Filter.map (fun (T : E →WOT[𝕜] F) ↦ ⟪y, (T : (a : E) → F) x⟫_𝕜) l ≤ 𝓝 ⟪y, (A : (a : E) → F) x⟫_𝕜

Tactic:
tendsto_iff_forall_inner_apply_tendsto (f := id)

Premises used: ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto, Set.Mem, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫

Tactic:
.of_norm_bounded (lp.summable_mul ?_ f g) ?_

Premises used: lp.summable_mul, Summable.of_norm_bounded
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
refine_1 : (ENNReal.toReal 2).HolderConjugate (ENNReal.toReal 2)
refine_2 :
  ∀ (i : ι), ‖⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫‖ ≤ ‖(↑f : (i : ι) → G i) i‖ * ‖(↑g : (i : ι) → G i) i‖
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫

Tactic:
refine .of_norm_bounded (lp.summable_mul ?_ f g) ?_
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
refine_1 : 1 < ENNReal.toReal 2 ∧ (ENNReal.toReal 2)⁻¹ + (ENNReal.toReal 2)⁻¹ = 1
⊢ (ENNReal.toReal 2).HolderConjugate (ENNReal.toReal 2)

Tactic:
rw [Real.holderConjugate_iff]

Premises used: Real.holderConjugate_iff
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
⊢ 1 < ENNReal.toReal 2 ∧ (ENNReal.toReal 2)⁻¹ + (ENNReal.toReal 2)⁻¹ = 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
i : ι
⊢ ‖⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫‖ ≤ ‖(↑f : (i : ι) → G i) i‖ * ‖(↑g : (i : ι) → G i) i‖

Tactic:
norm_inner_le_norm (𝕜 := 𝕜) _ _

Premises used: norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.l2Space
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
i : ι
⊢ ‖⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫‖ ≤ ‖(↑f : (i : ι) → G i) i‖ * ‖(↑g : (i : ι) → G i) i‖

Tactic:
exact norm_inner_le_norm (𝕜 := 𝕜) _ _

Premises used: norm_inner_le_norm
-- 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)
f : ↥(lp G 2)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : HPow.hPow (β := ℕ) ‖f‖ 2 = HPow.hPow (β := ℕ) ‖f‖ 2
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 = ‖f‖ ^ ENNReal.toReal 2

Tactic:
norm_cast
-- 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)
f : ↥(lp G 2)
⊢ ‖f‖ ^ ENNReal.toReal 2 = ∑' (i : ι), ‖(↑f : (i : ι) → G i) i‖ ^ ENNReal.toReal 2

Tactic:
lp.norm_rpow_eq_tsum ?_ f

Premises used: lp.norm_rpow_eq_tsum
-- 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)
f : ↥(lp G 2)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := ℝ) (∑' (i : ι), HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2)
    (∑' (i : ι), HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2)
⊢ Eq (α := ℝ) (∑' (i : ι), ‖(↑f : (i : ι) → G i) i‖ ^ ENNReal.toReal 2)
    (∑' (i : ι), HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2)

Tactic:
norm_cast
-- 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)
f : ↥(lp G 2)
⊢ Eq (α := ℝ) (∑' (i : ι), HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2)
    (∑' (i : ι), (re : (a : 𝕜) → ℝ) ⟪(↑f : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫)

Tactic:
simp
-- 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)
f : ↥(lp G 2)
⊢ Eq (α := ℝ) (∑' (i : ι), (re : (a : 𝕜) → ℝ) ⟪(↑f : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫ : ℝ)
    ((re : (a : 𝕜) → ℝ) (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : ℝ)

Tactic:
(RCLike.reCLM.map_tsum ?_).symm

Premises used: RCLike.reCLM, ContinuousLinearMap.map_tsum, 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)
f : ↥(lp G 2)
calc_1 : 0 < ENNReal.toReal 2
calc_2 : Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 = (re : (a : 𝕜) → ℝ) (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫)

Tactic:
calc
        ‖f‖ ^ 2 = ‖f‖ ^ (2 : ℝ≥0∞).toReal := by norm_cast
        _ = ∑' i, ‖f i‖ ^ (2 : ℝ≥0∞).toReal := lp.norm_rpow_eq_tsum ?_ f
        _ = ∑' i, ‖f i‖ ^ (2 : ℕ) := by norm_cast
        _ = ∑' i, re ⟪f i, f i⟫ := by simp
        _ = re (∑' i, ⟪f i, f i⟫) := (RCLike.reCLM.map_tsum ?_).symm

Premises used: lp.norm_rpow_eq_tsum, RCLike.reCLM, ContinuousLinearMap.map_tsum, ENNReal.toReal, OfNat.ofNat, 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)
f : ↥(lp G 2)
⊢ 0 < ENNReal.toReal 2

Tactic:
norm_num
-- 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)
f : ↥(lp G 2)
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫

Tactic:
summable_inner f f

Premises used: lp.summable_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)
f : ↥(lp G 2)
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫

Tactic:
exact summable_inner f f

Premises used: lp.summable_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)
f g : ↥(lp G 2)
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)

Tactic:
congr
-- 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)
f g : ↥(lp G 2)
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∑' (i : ι), ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫) : 𝕜)
    (∑' (i : ι), (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫ : 𝕜)

Tactic:
RCLike.conjCLE.map_tsum

Premises used: ContinuousLinearEquiv.map_tsum, RCLike.conjCLE
-- 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)
f g : ↥(lp G 2)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑g : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫)
    (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)

Tactic:
simp only [inner_conj_symm]

Premises used: inner_conj_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)
f g : ↥(lp G 2)
⊢ Eq.{u_2 + 1} (α := 𝕜) (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)
    (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫)

Tactic:
congr