α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => p.fst * p.snd
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
⊢ Continuous fun p => p.fst * p.snd
let m := (AddMonoidHom.mul : α →+ α →+ α).compr₂ toCompl
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
this : Continuous fun p => ↑(↑m p.fst) p.snd
⊢ Continuous fun p => p.fst * p.snd
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => p.fst * p.snd
have : Continuous fun p : α × α => m p.1 p.2 := by
  apply (continuous_coe α).comp _
  simp only [AddMonoidHom.coe_mul, AddMonoidHom.coe_mulLeft]
  exact _root_.continuous_mul
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
this : Continuous fun p => ↑(↑m p.fst) p.snd
di : DenseInducing ↑toCompl
⊢ Continuous fun p => p.fst * p.snd
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
this : Continuous fun p => ↑(↑m p.fst) p.snd
⊢ Continuous fun p => p.fst * p.snd
have di : DenseInducing (toCompl : α → Completion α) := denseInducing_coe
no goals
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
this : Continuous fun p => ↑(↑m p.fst) p.snd
di : DenseInducing ↑toCompl
⊢ Continuous fun p => p.fst * p.snd
convert di.extend_Z_bilin di this
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => ↑(↑AddMonoidHom.mul p.fst) p.snd
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => ↑(↑m p.fst) p.snd
apply (continuous_coe α).comp _
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => p.fst * p.snd
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => ↑(↑AddMonoidHom.mul p.fst) p.snd
simp only [AddMonoidHom.coe_mul, AddMonoidHom.coe_mulLeft]
no goals
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => p.fst * p.snd
exact _root_.continuous_mul