𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inner' : E →+ E →+ 𝕜 :=
  {
    toZeroHom :=
      { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
        map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x y : E),
          ZeroHom.toFun
              { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
              (x + y) =
            ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                x +
              ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                y) }
⊢ Continuous (uncurry inner)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
⊢ Continuous (uncurry inner)
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 _ _ _ }
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inner' : E →+ E →+ 𝕜 :=
  {
    toZeroHom :=
      { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
        map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x y : E),
          ZeroHom.toFun
              { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
              (x + y) =
            ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                x +
              ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                y) }
this : Continuous fun p => ↑(↑inner' p.fst) p.snd
⊢ Continuous (uncurry inner)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inner' : E →+ E →+ 𝕜 :=
  {
    toZeroHom :=
      { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
        map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x y : E),
          ZeroHom.toFun
              { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
              (x + y) =
            ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                x +
              ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                y) }
⊢ Continuous (uncurry inner)
have : Continuous fun p : E × E => inner' p.1 p.2 := continuous_inner
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inner' : E →+ E →+ 𝕜 :=
  {
    toZeroHom :=
      { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
        map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x y : E),
          ZeroHom.toFun
              { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
              (x + y) =
            ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                x +
              ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                y) }
this : Continuous fun p => ↑(↑inner' p.fst) p.snd
⊢ Continuous (DenseInducing.extend (_ : DenseInducing fun p => (↑E p.fst, ↑E p.snd)) (uncurry inner))
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inner' : E →+ E →+ 𝕜 :=
  {
    toZeroHom :=
      { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
        map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x y : E),
          ZeroHom.toFun
              { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
              (x + y) =
            ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                x +
              ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                y) }
this : Continuous fun p => ↑(↑inner' p.fst) p.snd
⊢ Continuous (uncurry inner)
rw [Completion.toInner, inner, uncurry_curry _]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inner' : E →+ E →+ 𝕜 :=
  {
    toZeroHom :=
      { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
        map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x y : E),
          ZeroHom.toFun
              { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
              (x + y) =
            ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                x +
              ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                y) }
this : Continuous fun p => ↑(↑inner' p.fst) p.snd
⊢ Continuous
    (DenseInducing.extend (_ : DenseInducing fun p => (↑toCompl p.fst, ↑toCompl p.snd)) fun p => ↑(↑inner' p.fst) p.snd)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inner' : E →+ E →+ 𝕜 :=
  {
    toZeroHom :=
      { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
        map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x y : E),
          ZeroHom.toFun
              { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
              (x + y) =
            ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                x +
              ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                y) }
this : Continuous fun p => ↑(↑inner' p.fst) p.snd
⊢ Continuous (DenseInducing.extend (_ : DenseInducing fun p => (↑E p.fst, ↑E p.snd)) (uncurry inner))
change
  Continuous
    (((denseInducing_toCompl E).prod (denseInducing_toCompl E)).extend fun p : E × E =>
      inner' p.1 p.2)
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
inner' : E →+ E →+ 𝕜 :=
  {
    toZeroHom :=
      { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
        map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) },
    map_add' :=
      (_ :
        ∀ (x y : E),
          ZeroHom.toFun
              { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
              (x + y) =
            ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                x +
              ZeroHom.toFun
                { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
                  map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
                y) }
this : Continuous fun p => ↑(↑inner' p.fst) p.snd
⊢ Continuous
    (DenseInducing.extend (_ : DenseInducing fun p => (↑toCompl p.fst, ↑toCompl p.snd)) fun p => ↑(↑inner' p.fst) p.snd)
exact (denseInducing_toCompl E).extend_Z_bilin (denseInducing_toCompl E) this
case h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ↑((fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0) x = ↑0 x
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
⊢ (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0
ext x
no goals
case h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x : E
⊢ ↑((fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0) x = ↑0 x
exact inner_zero_left _
case h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y z : E
⊢ ↑(ZeroHom.toFun
          { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
            map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
          (x + y))
      z =
    ↑(ZeroHom.toFun
            { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
              map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
            x +
          ZeroHom.toFun
            { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
              map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
            y)
      z
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ZeroHom.toFun
      { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
        map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
      (x + y) =
    ZeroHom.toFun
        { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
          map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
        x +
      ZeroHom.toFun
        { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
          map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
        y
ext z
no goals
case h
𝕜 : Type u_2
E : Type u_1
F : Type ?u.4201279
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y z : E
⊢ ↑(ZeroHom.toFun
          { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
            map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
          (x + y))
      z =
    ↑(ZeroHom.toFun
            { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
              map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
            x +
          ZeroHom.toFun
            { toFun := fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x),
              map_zero' := (_ : (fun x => LinearMap.toAddMonoidHom (↑(innerₛₗ 𝕜) x)) 0 = 0) }
            y)
      z
exact inner_add_left _ _ _