-- Mathlib/Analysis/InnerProductSpace/Completion.lean
theorem continuous_inner :
    Continuous (uncurry inner : Completion E × Completion E → 𝕜)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ Continuous (uncurry inner)

Tactic:
let inner' : E →+ E →+ 𝕜 :=
  { toFun := fun x => (innerₛₗ 𝕜 x).toAddMonoidHom
    map_zero' := by ext x; exact inner_zero_left _
    map_add' := fun x y => by ext z; exact inner_add_left _ _ _ }

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
⊢ Continuous (uncurry inner)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
this : Continuous fun p => (inner' p.1) p.2
⊢ Continuous (⋯.extend fun p => (inner' p.1) p.2)

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

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ ({ toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯ }.toFun (x + y)) z =
    ({ toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯ }.toFun x +
        { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯ }.toFun y)
      z

Tactic:
exact inner_add_left _ _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
this : Continuous fun p => (inner' p.1) p.2
⊢ Continuous (uncurry inner)

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

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
this : Continuous fun p => (inner' p.1) p.2
⊢ Continuous (⋯.extend (uncurry inner))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
⊢ Continuous (uncurry inner)

Tactic:
have : Continuous fun p : E × E => inner' p.1 p.2 := continuous_inner

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
this : Continuous fun p => (inner' p.1) p.2
⊢ Continuous (uncurry inner)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
this : Continuous fun p => (inner' p.1) p.2
⊢ Continuous (⋯.extend (uncurry inner))

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

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
inner' : E →+ E →+ 𝕜 := { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
this : Continuous fun p => (inner' p.1) p.2
⊢ Continuous (⋯.extend fun p => (inner' p.1) p.2)

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ((fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom) 0) x = 0 x

Tactic:
exact inner_zero_left _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯ }.toFun (x + y) =
    { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯ }.toFun x +
      { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯ }.toFun y

Tactic:
ext z

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ ({ toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯ }.toFun (x + y)) z =
    ({ toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯ }.toFun x +
        { toFun := fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom, map_zero' := ⋯ }.toFun y)
      z

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ (fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom) 0 = 0

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ((fun x => ((innerₛₗ 𝕜) x).toAddMonoidHom) 0) x = 0 x