awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
x y : 𝕜
simp :
  (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x * y) =
    HSMul.hSMul (β := E) x ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) y : E)
⊢ Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x * y) : E)
    (((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) ∘ₗ
            (adjoint : (a : 𝕜 ⊗[𝕜] E →ₗ[𝕜] 𝕜 ⊗[𝕜] 𝕜) → 𝕜 ⊗[𝕜] 𝕜 →ₗ[𝕜] 𝕜 ⊗[𝕜] E) (LinearMap.lTensor 𝕜 counit) :
          (a : 𝕜 ⊗[𝕜] 𝕜) → E)
        (x ⊗ₜ[𝕜] y) :
      E)

Tactic:
simp only [LinearIsometryEquiv.symm_symm, toLinearEquiv_lidIsometry, adjoint_lTensor,
          coe_comp, LinearEquiv.coe_coe, Function.comp_apply, lTensor_tmul, lid_tmul]

Premises used: TensorProduct.toLinearEquiv_lidIsometry, TensorProduct.lid_tmul, LinearMap.adjoint_lTensor, LinearMap.coe_comp, Function.comp_apply, LinearIsometryEquiv.symm_symm, LinearEquiv.coe_coe, LinearMap.lTensor_tmul
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
x y : 𝕜
rw :
  (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x • y) =
    HSMul.hSMul (β := E) x ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) y : E)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x • y) : E)
    ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x • y) : E)
⊢ (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) (x * y) =
    HSMul.hSMul (β := E) x ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) y : E)

Tactic:
rw [← smul_eq_mul, ← _root_.map_smul]

Premises used: smul_eq_mul, map_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
r : 𝕜
x : E
dsimp :
  Eq (α := E)
    ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
        ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r ⊗ₜ[𝕜] x : E ⊗[𝕜] E) :
      E)
    ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
        (x ⊗ₜ[𝕜] (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r : E ⊗[𝕜] E) :
      E)
⊢ HMul.hMul (α := E)
      (({ toFun := (⇑((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E), map_one' := ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ : 𝕜 →+* E } :
            (a : 𝕜) → E)
          r :
        E)
      x =
    HMul.hMul (β := E) x
      (({ toFun := (⇑((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E), map_one' := ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : 𝕜) → E)
          r :
        E)

Tactic:
dsimp
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
r : 𝕜
x : E
simp_rw :
  Eq.{u_2 + 1} (α := E)
    (((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
          (a : 𝕜 ⊗[𝕜] E) → E)
        (r ⊗ₜ[𝕜] x) :
      E)
    (((↑(toLinearEquiv
                (LinearIsometryEquiv.symm
                  (LinearIsometryEquiv.symm (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))))) :
            E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) :
          (a : E ⊗[𝕜] 𝕜) → E)
        (x ⊗ₜ[𝕜] r) :
      E)
⊢ Eq (α := E)
    ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
        ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r ⊗ₜ[𝕜] x : E ⊗[𝕜] E) :
      E)
    ((((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
        (x ⊗ₜ[𝕜] (((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r : E ⊗[𝕜] E) :
      E)

Tactic:
simp_rw [← rTensor_tmul, ← lTensor_tmul, ← adjoint_lTensor, ← adjoint_rTensor,
      ← comp_apply, ← adjoint_comp, rTensor_counit_comp_comul, lTensor_counit_comp_comul,
      ← toLinearMap_symm_rid, ← toLinearMap_symm_lid, ← comm_trans_lid,
      ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans,
      ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm]

Premises used: TensorProduct.toLinearEquiv_lidIsometry, LinearMap.rTensor_tmul, LinearIsometryEquiv.toLinearEquiv_symm, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, TensorProduct.comm_trans_lid, LinearMap.adjoint_rTensor, LinearMap.comp_apply, TensorProduct.toLinearEquiv_commIsometry, Coalgebra.rTensor_counit_comp_comul, LinearMap.adjoint_lTensor, LinearMap.adjoint_comp, TensorProduct.toLinearMap_symm_lid, Coalgebra.lTensor_counit_comp_comul, TensorProduct.toLinearMap_symm_rid, LinearMap.lTensor_tmul, LinearIsometryEquiv.toLinearEquiv_trans
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ Eq.{u_2 + 1} (α := E)
    (((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
          (a : 𝕜 ⊗[𝕜] E) → E)
        (r ⊗ₜ[𝕜] x) :
      E)
    (((↑(toLinearEquiv
                (LinearIsometryEquiv.symm
                  (LinearIsometryEquiv.symm (LinearIsometryEquiv.trans (commIsometry 𝕜 E 𝕜) (lidIsometry 𝕜 E))))) :
            E ⊗[𝕜] 𝕜 →ₗ[𝕜] E) :
          (a : E ⊗[𝕜] 𝕜) → E)
        (x ⊗ₜ[𝕜] r) :
      E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
r : 𝕜
x : E
dsimp :
  r • x =
    (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
      ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r ⊗ₜ[𝕜] x : E ⊗[𝕜] E)
⊢ r • x =
    HMul.hMul (α := E)
      (({ toFun := (⇑((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E), map_one' := ⋯,
              map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : 𝕜) → E)
          r :
        E)
      x

Tactic:
dsimp
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
r : 𝕜
x : E
simp_rw :
  r • x =
    ((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
        (a : 𝕜 ⊗[𝕜] E) → E)
      (r ⊗ₜ[𝕜] x)
⊢ r • x =
    (((adjoint : (a : E →ₗ[𝕜] E ⊗[𝕜] E) → E ⊗[𝕜] E →ₗ[𝕜] E) comul : E ⊗[𝕜] E →ₗ[𝕜] E) : (a : E ⊗[𝕜] E) → E)
      ((((adjoint : (a : E →ₗ[𝕜] 𝕜) → 𝕜 →ₗ[𝕜] E) counit : 𝕜 →ₗ[𝕜] E) : (a : 𝕜) → E) r ⊗ₜ[𝕜] x : E ⊗[𝕜] E)

Tactic:
simp_rw [← rTensor_tmul, ← adjoint_rTensor, ← comp_apply, ← adjoint_comp,
      rTensor_counit_comp_comul, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry,
      ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm]

Premises used: TensorProduct.toLinearEquiv_lidIsometry, LinearMap.rTensor_tmul, LinearIsometryEquiv.toLinearEquiv_symm, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, LinearMap.adjoint_rTensor, LinearMap.comp_apply, Coalgebra.rTensor_counit_comp_comul, LinearMap.adjoint_comp, TensorProduct.toLinearMap_symm_lid
-- Module: Mathlib.Analysis.InnerProductSpace.Coalgebra
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
inst_4 : Coalgebra 𝕜 E
r : 𝕜
x : E
⊢ r • x =
    ((↑(toLinearEquiv (LinearIsometryEquiv.symm (LinearIsometryEquiv.symm (lidIsometry 𝕜 E)))) : 𝕜 ⊗[𝕜] E →ₗ[𝕜] E) :
        (a : 𝕜 ⊗[𝕜] E) → E)
      (r ⊗ₜ[𝕜] x)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x₁ x₂ y₁ y₂ : E
hx : Inseparable x₁ x₂
hy : Inseparable y₁ y₂
⊢ ⟪x₁, y₁⟫ = ⟪x₂, y₂⟫

Tactic:
((hx.prod hy).map continuous_inner).eq

Premises used: Inseparable.eq, continuous_inner, Inseparable.prod, Inseparable.map
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ inner 𝕜 (E := SeparationQuotient E) (mk x) (mk y) = ⟪x, y⟫

Tactic:
rfl

Premises used: SeparationQuotient.lift₂, rfl, Quotient.liftOn₂'
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
a b : E
⊢ inner 𝕜 (E := Completion E) (↑a : Completion E) (↑b : Completion E) = ⟪a, b⟫

Tactic:
(isDenseInducing_coe.prodMap isDenseInducing_coe).extend_eq
    (continuous_inner : Continuous (uncurry (inner 𝕜))) (a, b)

Premises used: Classical.epsilon, Set.Mem, Prod.mk, Prod.map, continuous_inner, Filter.lim, IsDenseInducing.prodMap, Filter.limUnder, IsDenseInducing.extend, UniformSpace.Completion.isDenseInducing_coe, IsDenseInducing.extend_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
h :
  ∀ (x : E),
    Eq.{u_1 + 1} (α := 𝕜)
      ((LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
              RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) 0) :
            (a : E) → 𝕜)
          x :
        𝕜)
      ((0 : (a : E) → 𝕜) x : 𝕜)
⊢ Eq (α := E →+ 𝕜)
    (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) 0) :
      E →+ 𝕜)
    0

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
            RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) 0) :
          (a : E) → 𝕜)
        x :
      𝕜)
    ((0 : (a : E) → 𝕜) x : 𝕜)

Tactic:
inner_zero_left _

Premises used: inner_zero_left
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
            RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) 0) :
          (a : E) → 𝕜)
        x :
      𝕜)
    ((0 : (a : E) → 𝕜) x : 𝕜)

Tactic:
exact inner_zero_left _

Premises used: inner_zero_left
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
h :
  ∀ (z : E),
    Eq.{u_1 + 1} (α := 𝕜)
      ((LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
              RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) (x + y)) :
            (a : E) → 𝕜)
          z :
        𝕜)
      ((HAdd.hAdd (α := E →+ 𝕜) (β := E →+ 𝕜)
              (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule)
                  (σ := RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) :
                E →+ 𝕜)
              (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule)
                (σ := RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) y)) :
            (a : E) → 𝕜)
          z :
        𝕜)
⊢ LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
      RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) (x + y)) =
    HAdd.hAdd (α := E →+ 𝕜) (β := E →+ 𝕜)
      (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
          RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) :
        E →+ 𝕜)
      (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) y))

Tactic:
ext z
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y z : E
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
            RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) (x + y)) :
          (a : E) → 𝕜)
        z :
      𝕜)
    ((HAdd.hAdd (α := E →+ 𝕜) (β := E →+ 𝕜)
            (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule)
                (σ := RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) :
              E →+ 𝕜)
            (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule)
              (σ := RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) y)) :
          (a : E) → 𝕜)
        z :
      𝕜)

Tactic:
inner_add_left _ _ _

Premises used: inner_add_left
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y z : E
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
            RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) (x + y)) :
          (a : E) → 𝕜)
        z :
      𝕜)
    ((HAdd.hAdd (α := E →+ 𝕜) (β := E →+ 𝕜)
            (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule)
                (σ := RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) :
              E →+ 𝕜)
            (LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule)
              (σ := RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) y)) :
          (a : E) → 𝕜)
        z :
      𝕜)

Tactic:
exact inner_add_left _ _ _

Premises used: inner_add_left
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 :=
  {
    toFun := fun (x : E) ↦
      LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x),
    map_zero' := ⋯, map_add' := ⋯ }
⊢ Continuous.{u_2, u_1} (Y := 𝕜) fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2

Tactic:
have : Continuous fun p : E × E => inner' p.1 p.2 := continuous_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 :=
  {
    toFun := fun (x : E) ↦
      LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x),
    map_zero' := ⋯, map_add' := ⋯ }
this : Continuous.{u_2, u_1} (Y := 𝕜) fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2
rw : Continuous.{u_2, u_1} (X := Completion E × Completion E) (IsDenseInducing.extend ⋯ (uncurry (inner 𝕜)))
⊢ Continuous.{u_2, u_1} (X := Completion E × Completion E) (uncurry (inner 𝕜))

Tactic:
rw [Completion.toInner, inner, uncurry_curry _]

Premises used: Function.uncurry_curry, Inner.inner, UniformSpace.Completion.toInner
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 :=
  {
    toFun := fun (x : E) ↦
      LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x),
    map_zero' := ⋯, map_add' := ⋯ }
this : Continuous.{u_2, u_1} (Y := 𝕜) fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2
fun :
  Continuous.{u_2, u_1} (X := Completion E × Completion E) (Y := 𝕜)
    (IsDenseInducing.extend (i := Prod.map (⇑toCompl : (a : E) → Completion E) (⇑toCompl : (a : E) → Completion E)) ⋯
      fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2)
⊢ Continuous.{u_2, u_1} (X := Completion E × Completion E) (IsDenseInducing.extend ⋯ (uncurry (inner 𝕜)))

Tactic:
change
    Continuous
      (((isDenseInducing_toCompl E).prodMap (isDenseInducing_toCompl E)).extend fun p : E × E =>
        inner' p.1 p.2)

Premises used: Continuous, Prod.fst, IsDenseInducing.prodMap, UniformSpace.Completion.isDenseInducing_toCompl, Prod.snd, DFunLike.coe, IsDenseInducing.extend
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 :=
  {
    toFun := fun (x : E) ↦
      LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x),
    map_zero' := ⋯, map_add' := ⋯ }
this : Continuous.{u_2, u_1} (Y := 𝕜) fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2
⊢ Continuous.{u_2, u_1} (X := Completion E × Completion E) (Y := 𝕜)
    (IsDenseInducing.extend (i := Prod.map (⇑toCompl : (a : E) → Completion E) (⇑toCompl : (a : E) → Completion E)) ⋯
      fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2)

Tactic:
(isDenseInducing_toCompl E).extend_Z_bilin (isDenseInducing_toCompl E) this

Premises used: IsDenseInducing.extend_Z_bilin, UniformSpace.Completion.isDenseInducing_toCompl
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 :=
  {
    toFun := fun (x : E) ↦
      LinearMap.toAddMonoidHom (R := 𝕜) (S := 𝕜) (modM₁ := NormedSpace.toModule) (modM₂ := Semiring.toModule) (σ :=
        RingHom.id 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x),
    map_zero' := ⋯, map_add' := ⋯ }
this : Continuous.{u_2, u_1} (Y := 𝕜) fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2
⊢ Continuous.{u_2, u_1} (X := Completion E × Completion E) (Y := 𝕜)
    (IsDenseInducing.extend (i := Prod.map (⇑toCompl : (a : E) → Completion E) (⇑toCompl : (a : E) → Completion E)) ⋯
      fun (p : E × E) ↦ (((inner' : (a : E) → E →+ 𝕜) p.1 : E →+ 𝕜) : (a : E) → 𝕜) p.2)

Tactic:
exact (isDenseInducing_toCompl E).extend_Z_bilin (isDenseInducing_toCompl E) this

Premises used: IsDenseInducing.extend_Z_bilin, UniformSpace.Completion.isDenseInducing_toCompl
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : Type u_4
inst_3 : TopologicalSpace α
f g : α → Completion E
hf : Continuous f
hg : Continuous g
⊢ Continuous.{u_4, u_1} (Y := 𝕜) fun (x : α) ↦ ⟪f x, g x⟫

Tactic:
UniformSpace.Completion.continuous_inner.comp (hf.prodMk hg :)

Premises used: Continuous.comp, UniformSpace.Completion.continuous_inner, Continuous.prodMk
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : Completion E
⊢ Continuous (Y := ℝ) fun (a : Completion E) ↦ HPow.hPow (β := ℕ) ‖a‖ 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : Completion E
⊢ Continuous (Y := ℝ) fun (a : Completion E) ↦ (re : (a : 𝕜) → ℝ) ⟪a, a⟫

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : Completion E
a : E
⊢ HPow.hPow (β := ℕ) (norm (E := Completion E) (↑a : Completion E)) 2 =
    (re : (a : 𝕜) → ℝ) (inner 𝕜 (E := Completion E) (↑a : Completion E) (↑a : Completion E))

Tactic:
simp only [norm_coe, inner_coe, inner_self_eq_norm_sq]

Premises used: UniformSpace.Completion.norm_coe, inner_self_eq_norm_sq, UniformSpace.Completion.inner_coe
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : Completion E
⊢ Continuous.{u_2, u_1} (Y := 𝕜) fun (x : Completion E × Completion E) ↦ ⟪x.2, x.1⟫

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : Completion E
⊢ Continuous.{u_2, u_1} (Y := 𝕜) fun (x : Completion E × Completion E) ↦ ⟪x.1, x.2⟫

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : Completion E
a b : E
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (inner 𝕜 (E := Completion E) (↑b : Completion E) (↑a : Completion E)) =
    inner 𝕜 (E := Completion E) (↑a : Completion E) (↑b : Completion E)

Tactic:
simp only [inner_coe, inner_conj_symm]

Premises used: UniformSpace.Completion.inner_coe, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y z : Completion E
⊢ Continuous.{u_2, u_1} (Y := 𝕜) fun (x : Completion E × Completion E × Completion E) ↦ ⟪x.1 + x.2.1, x.2.2⟫

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y z : Completion E
⊢ Continuous.{u_2, u_1} (Y := 𝕜) fun (x : Completion E × Completion E × Completion E) ↦ ⟪x.1, x.2.2⟫ + ⟪x.2.1, x.2.2⟫

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y z : Completion E
a b c : E
⊢ ⟪HAdd.hAdd (α := Completion E) (↑a : Completion E) (↑b : Completion E), (↑c : Completion E)⟫ =
    inner 𝕜 (E := Completion E) (↑a : Completion E) (↑c : Completion E) +
      inner 𝕜 (E := Completion E) (↑b : Completion E) (↑c : Completion E)

Tactic:
simp only [← coe_add, inner_coe, inner_add_left]

Premises used: inner_add_left, UniformSpace.Completion.inner_coe, UniformSpace.Completion.coe_add
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : Completion E
c : 𝕜
⊢ Continuous.{u_2, u_1} (Y := 𝕜) fun (x : Completion E × Completion E) ↦ ⟪x.1, x.2⟫

Tactic:
fun_prop