[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
let m := (AddMonoidHom.mul : α →+ α →+ α).compr₂ toCompl
[GOAL]
α : 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
[PROOFSTEP]
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
[GOAL]
α : 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
[PROOFSTEP]
apply (continuous_coe α).comp _
[GOAL]
α : 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
[PROOFSTEP]
simp only [AddMonoidHom.coe_mul, AddMonoidHom.coe_mulLeft]
[GOAL]
α : 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
[PROOFSTEP]
exact _root_.continuous_mul
[GOAL]
α : 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
[PROOFSTEP]
have di : DenseInducing (toCompl : α → Completion α) := denseInducing_coe
[GOAL]
α : 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
[PROOFSTEP]
convert di.extend_Z_bilin di this
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑α a * (↑α b + ↑α c) = ↑α a * ↑α b + ↑α a * ↑α c
[PROOFSTEP]
rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ b✝ c✝ : Completion α
a b c : α
⊢ (↑α a + ↑α b) * ↑α c = ↑α a * ↑α c + ↑α b * ↑α c
[PROOFSTEP]
rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_mul]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ : Completion α
a : α
⊢ 0 * ↑α a = 0
[PROOFSTEP]
rw [← coe_zero, ← coe_mul, zero_mul]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ : Completion α
a : α
⊢ ↑α a * 0 = 0
[PROOFSTEP]
rw [← coe_zero, ← coe_mul, mul_zero]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑α a * ↑α b * ↑α c = ↑α a * (↑α b * ↑α c)
[PROOFSTEP]
rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ : Completion α
a : α
⊢ 1 * ↑α a = ↑α a
[PROOFSTEP]
rw [← coe_one, ← coe_mul, one_mul]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ : Completion α
a : α
⊢ ↑α a * 1 = ↑α a
[PROOFSTEP]
rw [← coe_one, ← coe_mul, mul_one]
[GOAL]
α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : TopologicalRing α
inst✝⁶ : UniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : UniformAddGroup β
inst✝² : TopologicalRing β
f : α →+* β
hf✝ : Continuous ↑f
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf' : Continuous ↑↑f
hf : UniformContinuous ↑f
⊢ Completion.extension (↑f) 1 = 1
[PROOFSTEP]
rw [← coe_one, extension_coe hf, f.map_one]
[GOAL]
α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : TopologicalRing α
inst✝⁶ : UniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : UniformAddGroup β
inst✝² : TopologicalRing β
f : α →+* β
hf✝ : Continuous ↑f
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf' : Continuous ↑↑f
hf : UniformContinuous ↑f
a✝ b✝ : Completion α
a b : α
⊢ OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) } (↑α a * ↑α b) =
    OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) } (↑α a) *
      OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) } (↑α b)
[PROOFSTEP]
simp_rw [← coe_mul, extension_coe hf, f.map_mul]
[GOAL]
α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : TopologicalRing α
inst✝⁶ : UniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : UniformAddGroup β
inst✝² : TopologicalRing β
f : α →+* β
hf✝ : Continuous ↑f
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf' : Continuous ↑↑f
hf : UniformContinuous ↑f
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : Completion α),
                OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                    (a * b) =
                  OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      a *
                    OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      b) })
      0 =
    0
[PROOFSTEP]
simp_rw [← coe_zero, extension_coe hf, f.map_zero]
[GOAL]
α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : TopologicalRing α
inst✝⁶ : UniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : UniformAddGroup β
inst✝² : TopologicalRing β
f : α →+* β
hf✝ : Continuous ↑f
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf' : Continuous ↑↑f
hf : UniformContinuous ↑f
a✝ b✝ : Completion α
a b : α
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : Completion α),
                OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                    (a * b) =
                  OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      a *
                    OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      b) })
      (↑α a + ↑α b) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : Completion α),
                  OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      (a * b) =
                    OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                        a *
                      OneHom.toFun
                        { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) } b) })
        (↑α a) +
      OneHom.toFun
        (↑{ toOneHom := { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : Completion α),
                  OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      (a * b) =
                    OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                        a *
                      OneHom.toFun
                        { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) } b) })
        (↑α b)
[PROOFSTEP]
simp_rw [← coe_add, extension_coe hf, f.map_add]
[GOAL]
α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
⊢ Completion.map ((fun x x_1 => x • x_1) r) = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r))
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
⊢ Completion.map ((fun x x_1 => x • x_1) r) x = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) x
[PROOFSTEP]
refine' Completion.induction_on x _ fun a => _
[GOAL]
case h.refine'_1
α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
⊢ IsClosed
    {a |
      Completion.map ((fun x x_1 => x • x_1) r) a = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) a}
[PROOFSTEP]
exact isClosed_eq Completion.continuous_map (continuous_mul_left _)
[GOAL]
case h.refine'_2
α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
a : (fun x => A) r
⊢ Completion.map ((fun x x_1 => x • x_1) r) (↑((fun x => A) r) a) =
    (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) (↑((fun x => A) r) a)
[PROOFSTEP]
simp_rw [map_coe (uniformContinuous_const_smul r) a, Algebra.smul_def, coe_mul]
[GOAL]
α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
src✝ : R →+* Completion A := RingHom.comp coeRingHom (algebraMap R A)
r : R
x : (fun x => Completion A) r
a : A
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r *
      ↑A a =
    ↑A a *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r
[PROOFSTEP]
simpa only [coe_mul] using congr_arg ((↑) : A → Completion A) (Algebra.commutes r a)
[GOAL]
α : Type u_1
inst✝¹¹ : Ring α
inst✝¹⁰ : UniformSpace α
inst✝⁹ : TopologicalRing α
inst✝⁸ : UniformAddGroup α
β : Type u
inst✝⁷ : UniformSpace β
inst✝⁶ : Ring β
inst✝⁵ : UniformAddGroup β
inst✝⁴ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
inst✝¹ : UniformAddGroup R
inst✝ : TopologicalRing R
src✝ : Ring (Completion R) := ring
a✝ b✝ : Completion R
a b : R
⊢ ↑R a * ↑R b = ↑R b * ↑R a
[PROOFSTEP]
rw [← coe_mul, ← coe_mul, mul_comm]
[GOAL]
α : Type u_1
inst✝¹¹ : Ring α
inst✝¹⁰ : UniformSpace α
inst✝⁹ : TopologicalRing α
inst✝⁸ : UniformAddGroup α
β : Type u
inst✝⁷ : UniformSpace β
inst✝⁶ : Ring β
inst✝⁵ : UniformAddGroup β
inst✝⁴ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
inst✝¹ : UniformAddGroup R
inst✝ : TopologicalRing R
⊢ Algebra R (Completion R)
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
x y : α
⊢ x - y ∈ closure {0} ↔ x - y ∈ Ideal.closure ⊥
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
α : Type u
r : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
[PROOFSTEP]
rw [@ring_sep_rel α r]
[GOAL]
α✝ : Type u_1
α : Type u
r : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (Submodule.quotientRel (Ideal.closure ⊥)) = (α ⧸ Ideal.closure ⊥)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
α : Type ?u.345143
r : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
x y : α
⊢ x - y ∈ closure {0} ↔ x - y ∈ Ideal.closure ⊥
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ CommRing (Quotient (separationSetoid α))
[PROOFSTEP]
rw [ring_sep_quot α]
[GOAL]
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ CommRing (α ⧸ Ideal.closure ⊥)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ TopologicalRing (Quotient (separationSetoid α))
[PROOFSTEP]
convert topologicalRing_quotient (⊥ : Ideal α).closure
[GOAL]
case h.e'_1
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
[PROOFSTEP]
try congr; apply ring_sep_rel
[GOAL]
case h.e'_1
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
[PROOFSTEP]
congr
[GOAL]
case h.e'_1.e_s
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ separationSetoid α = Submodule.quotientRel (Ideal.closure ⊥)
[PROOFSTEP]
apply ring_sep_rel
[GOAL]
case h.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq instTopologicalSpaceQuotient (topologicalRingQuotientTopology (Ideal.closure ⊥))
[PROOFSTEP]
try congr; apply ring_sep_rel
[GOAL]
case h.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq instTopologicalSpaceQuotient (topologicalRingQuotientTopology (Ideal.closure ⊥))
[PROOFSTEP]
congr
[GOAL]
case h.e'_2.e_2.h
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ separationSetoid α = Submodule.quotientRel (Ideal.closure ⊥)
[PROOFSTEP]
apply ring_sep_rel
[GOAL]
case h.e'_3.e'_2.e'_2.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq commRing (Ideal.Quotient.commRing (Ideal.closure ⊥))
[PROOFSTEP]
try congr; apply ring_sep_rel
[GOAL]
case h.e'_3.e'_2.e'_2.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq commRing (Ideal.Quotient.commRing (Ideal.closure ⊥))
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.e'_2.e'_2.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq commRing (Ideal.Quotient.commRing (Ideal.closure ⊥))
[PROOFSTEP]
apply ring_sep_rel
[GOAL]
case h.e'_3.e'_2.e'_2.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq commRing (Ideal.Quotient.commRing (Ideal.closure ⊥))
[PROOFSTEP]
simp [commRing]
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ extend (_ : DenseInducing ↑i) (↑f) 1 = 1
[PROOFSTEP]
convert DenseInducing.extend_eq (ue.denseInducing dr) hf.continuous 1
[GOAL]
case h.e'_2.h.e'_10
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ 1 = ↑i 1
case h.e'_3
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ 1 = ↑f 1
[PROOFSTEP]
exacts [i.map_one.symm, f.map_one.symm]
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ ∀ (x y : β),
    OneHom.toFun
        { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
        (x * y) =
      OneHom.toFun
          { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) } x *
        OneHom.toFun
          { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) } y
[PROOFSTEP]
have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
⊢ ∀ (x y : β),
    OneHom.toFun
        { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
        (x * y) =
      OneHom.toFun
          { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) } x *
        OneHom.toFun
          { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) } y
[PROOFSTEP]
refine' fun x y => DenseRange.induction_on₂ dr _ (fun a b => _) x y
[GOAL]
case refine'_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
x y : β
⊢ IsClosed
    {q |
      OneHom.toFun
          { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
          (q.fst * q.snd) =
        OneHom.toFun
            { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
            q.fst *
          OneHom.toFun
            { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
            q.snd}
[PROOFSTEP]
exact isClosed_eq (Continuous.comp h continuous_mul) ((h.comp continuous_fst).mul (h.comp continuous_snd))
[GOAL]
case refine'_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
x y : β
a b : α
⊢ OneHom.toFun { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
      (↑i a * ↑i b) =
    OneHom.toFun
        { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
        (↑i a) *
      OneHom.toFun
        { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) } (↑i b)
[PROOFSTEP]
simp_rw [← i.map_mul, DenseInducing.extend_eq (ue.denseInducing dr) hf.continuous _, ← f.map_mul]
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : β),
                OneHom.toFun
                    { toFun := extend (_ : DenseInducing ↑i) ↑f,
                      map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
convert DenseInducing.extend_eq (ue.denseInducing dr) hf.continuous 0
[GOAL]
case h.e'_2.h.e'_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ 0 = ↑i 0
[PROOFSTEP]
simp only [map_zero]
[GOAL]
case h.e'_3
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ 0 = ↑f 0
[PROOFSTEP]
simp only [map_zero]
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ ∀ (x y : β),
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : β),
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := extend (_ : DenseInducing ↑i) ↑f,
                  map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := extend (_ : DenseInducing ↑i) ↑f,
                  map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          y) })
          y
[PROOFSTEP]
have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
⊢ ∀ (x y : β),
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : β),
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := extend (_ : DenseInducing ↑i) ↑f,
                  map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := extend (_ : DenseInducing ↑i) ↑f,
                  map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          y) })
          y
[PROOFSTEP]
refine' fun x y => DenseRange.induction_on₂ dr _ (fun a b => _) x y
[GOAL]
case refine'_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
x y : β
⊢ IsClosed
    {q |
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := extend (_ : DenseInducing ↑i) ↑f,
                  map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          y) })
          (q.fst + q.snd) =
        OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := extend (_ : DenseInducing ↑i) ↑f,
                    map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : β),
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := extend (_ : DenseInducing ↑i) ↑f,
                              map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := extend (_ : DenseInducing ↑i) ↑f,
                              map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                            y) })
            q.fst +
          OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := extend (_ : DenseInducing ↑i) ↑f,
                    map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : β),
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := extend (_ : DenseInducing ↑i) ↑f,
                              map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := extend (_ : DenseInducing ↑i) ↑f,
                              map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                            y) })
            q.snd}
[PROOFSTEP]
exact isClosed_eq (Continuous.comp h continuous_add) ((h.comp continuous_fst).add (h.comp continuous_snd))
[GOAL]
case refine'_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
x y : β
a b : α
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : β),
                OneHom.toFun
                    { toFun := extend (_ : DenseInducing ↑i) ↑f,
                      map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      y) })
      (↑i a + ↑i b) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : β),
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        y) })
        (↑i a) +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : β),
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        y) })
        (↑i b)
[PROOFSTEP]
simp_rw [← i.map_add, DenseInducing.extend_eq (ue.denseInducing dr) hf.continuous _, ← f.map_add]
