-- 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
this✝ : IsTopologicalAddGroup B
this : TopologicalSpace.coinduced (⇑φ) inst✝⁴ ≤ τB
⊢ moduleTopology R B ≤ TopologicalSpace.coinduced (⇑φ) inst✝⁴

Tactic:
clear! τ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
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this : IsTopologicalAddGroup A
⊢ moduleTopology R B ≤ TopologicalSpace.coinduced (⇑φ) inst✝³

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
hoq : IsOpenQuotientMap (Prod.map id ⇑φ)
⊢ Continuous fun p => p.1 • p.2

Tactic:
rw [← hoq.continuous_comp_iff]

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) ∘ Prod.map id ⇑φ)

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
this✝ : IsTopologicalAddGroup B
this : TopologicalSpace.coinduced (⇑φ) inst✝⁴ ≤ τB
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴

Tactic:
refine le_antisymm ?_ this

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
this : TopologicalSpace.coinduced (⇑φ) inst✝⁴ ≤ τB
⊢ τB ≤ TopologicalSpace.coinduced (⇑φ) inst✝⁴

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

Tactic:
rw [hφ2]

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:
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✝⁴

Tactic:
have this : Continuous φ := continuous_of_linearMap φ

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
this : Continuous ⇑φ
⊢ τ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 ⇑φ
hA : Continuous fun p => p.1 • p.2
⊢ (fun p => p.1 • p.2) ∘ Prod.map id ⇑φ = ⇑φ ∘ fun p => p.1 • p.2

Tactic:
ext

Result:
case h
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
x✝ : R × A
⊢ ((fun p => p.1 • p.2) ∘ Prod.map id ⇑φ) x✝ = (⇑φ ∘ fun p => p.1 • p.2) x✝

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

Tactic:
have hφo : IsOpenQuotientMap φ := AddMonoidHom.isOpenQuotientMap_of_isQuotientMap ⟨hφ, rfl⟩

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
φ : A →ₗ[R] B
hφ : Function.Surjective ⇑φ
this✝ : IsTopologicalAddGroup A
this : TopologicalSpace B := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ moduleTopology R B ≤ TopologicalSpace.coinduced (⇑φ) inst✝³