-- 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:
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
τB : TopologicalSpace B
inst✝ : IsModuleTopology R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this : IsTopologicalAddGroup A
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴

Tactic:
haveI := topologicalAddGroup R B

Result:
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
τB : TopologicalSpace B
inst✝ : IsModuleTopology R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : IsTopologicalAddGroup A
this : IsTopologicalAddGroup B
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴

Proof state:
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 ⇑φ
⊢ moduleTopology R B ≤ TopologicalSpace.coinduced (⇑φ) inst✝³

Tactic:
refine sInf_le ⟨?_, ?_⟩

Result:
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

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

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
⊢ Continuous fun p => p.1 • p.2

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

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
⊢ 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
hφ2 : (fun p => p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ = ⇑φ ∘ fun p => p.1 + p.2
⊢ Continuous fun p => p.1 + p.2

Tactic:
rw [← (IsOpenQuotientMap.prodMap hφo hφo).continuous_comp_iff, hφ2]

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)

Proof state:
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

Tactic:
obtain ⟨hA⟩ : ContinuousSMul R A := inferInstance

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
⊢ Continuous fun p => p.1 • p.2

Proof state:
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

Tactic:
obtain ⟨hA⟩ := IsModuleTopology.toContinuousAdd R A

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
⊢ Continuous fun p => p.1 + p.2

Proof state:
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
τB : TopologicalSpace B
inst✝ : IsModuleTopology R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴

Tactic:
haveI := topologicalAddGroup R A

Result:
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
τB : TopologicalSpace B
inst✝ : IsModuleTopology R B
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this : IsTopologicalAddGroup A
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴