-- 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
φ : 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 ⇑φ ⇑φ = ⇑φ ∘ 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✝ : A × A
⊢ ((fun p => p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ) 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
τ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✝⁴

Tactic:
rw [continuous_iff_coinduced_le] at 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:
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:
rw [eq_moduleTopology 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
this : TopologicalSpace.coinduced (⇑φ) inst✝⁴ ≤ τB
⊢ moduleTopology R B ≤ TopologicalSpace.coinduced (⇑φ) inst✝⁴

Proof state:
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✝ : A × A
⊢ ((fun p => p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ) x✝ = (⇑φ ∘ fun p => p.1 + p.2) x✝

Tactic:
simp

Result:
no goals

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

Tactic:
letI : TopologicalSpace B := .coinduced φ inferInstance

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
⊢ 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:
exact Continuous.comp hφo.continuous hA

Result:
no goals

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:
exact Continuous.comp hφo.continuous hA

Result:
no goals

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

Tactic:
simp

Result:
no goals