-- Mathlib/Topology/Algebra/Module/ModuleTopology.lean
theorem isQuotientMap_of_surjective [τB : TopologicalSpace B] [IsModuleTopology R B]
    {φ : A →ₗ[R] B} (hφ : Function.Surjective φ) :
    IsQuotientMap φ where
  surjective := hφ
  eq_coinduced

Proof state:
case refine_1.continuous_smul.mk
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : IsTopologicalAddGroup A
this : TopologicalSpace B := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
hA : Continuous fun p => p.1 • p.2
hφ2 : (fun p => p.1 • p.2) ∘ Prod.map id ⇑φ = ⇑φ ∘ fun p => p.1 • p.2
⊢ Continuous fun p => p.1 • p.2

Tactic:
have hoq : IsOpenQuotientMap (_ : R × A → R × B) := IsOpenQuotientMap.prodMap .id hφo

Result:
case refine_1.continuous_smul.mk
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : IsTopologicalAddGroup A
this : TopologicalSpace B := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
hA : Continuous fun p => p.1 • p.2
hφ2 : (fun p => p.1 • p.2) ∘ Prod.map id ⇑φ = ⇑φ ∘ fun p => p.1 • p.2
hoq : IsOpenQuotientMap (Prod.map id ⇑φ)
⊢ Continuous fun p => p.1 • p.2

Proof state:
case refine_2
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : IsTopologicalAddGroup A
this : TopologicalSpace B := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousAdd B

Tactic:
apply ContinuousAdd.mk

Result:
case refine_2.continuous_add
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : IsTopologicalAddGroup A
this : TopologicalSpace B := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ Continuous fun p => p.1 + p.2

Proof state:
case refine_1
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : IsTopologicalAddGroup A
this : TopologicalSpace B := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousSMul R B

Tactic:
apply ContinuousSMul.mk

Result:
case refine_1.continuous_smul
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : IsTopologicalAddGroup A
this : TopologicalSpace B := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ Continuous fun p => p.1 • p.2

Proof state:
case refine_2.continuous_add.mk
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : IsTopologicalAddGroup A
this : TopologicalSpace B := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
hA : Continuous fun p => p.1 + p.2
⊢ Continuous fun p => p.1 + p.2

Tactic:
have hφ2 : (fun p ↦ p.1 + p.2 : B × B → B) ∘ (Prod.map φ φ) =
  φ ∘ (fun p ↦ p.1 + p.2 : A × A → A) := by ext; simp

Result:
case refine_2.continuous_add.mk
R : Type u_1
τR : TopologicalSpace R
inst✝⁶ : Ring R
A : Type u_2
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B : Type u_3
inst✝¹ : AddCommGroup B
inst✝ : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : IsTopologicalAddGroup A
this : TopologicalSpace B := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
hA : Continuous fun p => p.1 + p.2
hφ2 : (fun p => p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ = ⇑φ ∘ fun p => p.1 + p.2
⊢ Continuous fun p => p.1 + p.2