case refine'_1
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous ↑(algebraMap R A)
⊢ Continuous fun p => p.fst • p.snd

case refine'_2
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous fun p => p.fst • p.snd
⊢ Continuous ↑(algebraMap R A)
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
⊢ Continuous ↑(algebraMap R A) ↔ Continuous fun p => p.fst • p.snd
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous ↑(algebraMap R A)
⊢ Continuous fun p => ↑(algebraMap R A) p.fst * p.snd
case refine'_1
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous ↑(algebraMap R A)
⊢ Continuous fun p => p.fst • p.snd
simp only [Algebra.smul_def]
no goals
case refine'_1
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous ↑(algebraMap R A)
⊢ Continuous fun p => ↑(algebraMap R A) p.fst * p.snd
exact (h.comp continuous_fst).mul continuous_snd
case refine'_2
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous fun p => p.fst • p.snd
⊢ Continuous fun r => r • 1
case refine'_2
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous fun p => p.fst • p.snd
⊢ Continuous ↑(algebraMap R A)
rw [algebraMap_eq_smul_one']
no goals
case refine'_2
R : Type u_1
A : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSemiring A
h : Continuous fun p => p.fst • p.snd
⊢ Continuous fun r => r • 1
exact h.comp (continuous_id.prod_mk continuous_const)