awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst_1 : CommSemiring R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace A
inst_7 : IsModuleTopology R A
inst_8 : TopologicalSpace B
inst_9 : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous.{u_6, u_8} (X := R) (Y := B) (⇑(φ.comp (algebraMap R A)) : (a : R) → B)
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
φ' : A →ₗ[R] B := { toAddHom := (↑φ : A →ₙ+ B), map_smul' := ⋯ }
⊢ ContinuousSMul R B

Tactic:
have : ContinuousSMul R B := ⟨(hφ.comp continuous_fst).mul continuous_snd⟩
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst_1 : CommSemiring R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace A
inst_7 : IsModuleTopology R A
inst_8 : TopologicalSpace B
inst_9 : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous.{u_6, u_8} (X := R) (Y := B) (⇑(φ.comp (algebraMap R A)) : (a : R) → B)
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
φ' : A →ₗ[R] B := { toAddHom := (↑φ : A →ₙ+ B), map_smul' := ⋯ }
this : ContinuousSMul R B
⊢ Continuous.{u_7, u_8} (X := A) (Y := B) (⇑φ : (a : A) → B)

Tactic:
continuous_of_linearMap φ'

Premises used: IsModuleTopology.continuous_of_linearMap
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst_1 : CommSemiring R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Semiring B
inst_5 : TopologicalSpace R
inst_6 : TopologicalSpace A
inst_7 : IsModuleTopology R A
inst_8 : TopologicalSpace B
inst_9 : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous.{u_6, u_8} (X := R) (Y := B) (⇑(φ.comp (algebraMap R A)) : (a : R) → B)
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
φ' : A →ₗ[R] B := { toAddHom := (↑φ : A →ₙ+ B), map_smul' := ⋯ }
this : ContinuousSMul R B
⊢ Continuous.{u_7, u_8} (X := A) (Y := B) (⇑φ : (a : A) → B)

Tactic:
exact continuous_of_linearMap φ'

Premises used: IsModuleTopology.continuous_of_linearMap
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
τB : TopologicalSpace B'
inst_8 : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
⊢ ContinuousAdd A

Tactic:
haveI := IsModuleTopology.toContinuousAdd R A
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
τB : TopologicalSpace B'
inst_8 : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this : ContinuousAdd A
⊢ ContinuousAdd B'

Tactic:
haveI := IsModuleTopology.toContinuousAdd S B'
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
τB : TopologicalSpace B'
inst_8 : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : ContinuousAdd B'
⊢ Continuous[inst_4, τB] (⇑φ : (a : A) → B')

Tactic:
have this : Continuous φ := continuous_of_linearMapₛₗ hσ.continuous φ
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
τB : TopologicalSpace B'
inst_8 : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this_2 : ContinuousAdd B'
this : Continuous[inst_4, τB] (⇑φ : (a : A) → B')
⊢ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4 ≤ τB

Tactic:
rw [continuous_iff_coinduced_le] at this

Premises used: continuous_iff_coinduced_le
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
τB : TopologicalSpace B'
inst_8 : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this_2 : ContinuousAdd B'
this : TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4 ≤ τB
⊢ τB = TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4

Tactic:
le_antisymm ?_ this

Premises used: le_antisymm
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
τB : TopologicalSpace B'
inst_8 : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this_2 : ContinuousAdd B'
this : TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4 ≤ τB
refine : τB ≤ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
⊢ τB = TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4

Tactic:
refine le_antisymm ?_ this

Premises used: le_antisymm
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
τB : TopologicalSpace B'
inst_8 : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this_2 : ContinuousAdd B'
this : TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4 ≤ τB
rw : moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
⊢ τB ≤ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4

Tactic:
rw [eq_moduleTopology S B']

Premises used: eq_moduleTopology
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
⊢ IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')

Tactic:
have hφo : IsOpenQuotientMap φ := AddMonoidHom.isOpenQuotientMap_of_isQuotientMap ⟨⟨rfl⟩, hφ⟩
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
⊢ moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4

Tactic:
sInf_le ⟨?_, ?_⟩

Premises used: sInf_le, And.intro
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
refine_1 : ContinuousSMul S B'
refine_2 : ContinuousAdd B'
⊢ moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4

Tactic:
refine sInf_le ⟨?_, ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
refine_1 :
  Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : S × B') ↦
    p.1 • p.2
⊢ ContinuousSMul S B'

Tactic:
apply ContinuousSMul.mk

Premises used: ContinuousSMul.mk
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
⊢ ContinuousSMul R A

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
⊢ Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2

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

Premises used: ContinuousSMul
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
hA : Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
h :
  ∀ (x : R × A),
    Eq.{u_5 + 1} (α := B') (((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B')) x)
      (Function.comp (β := A) (⇑φ : (a : A) → B') (fun (p : R × A) ↦ p.1 • p.2) x)
⊢ Eq (α := R × A → B') ((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : R × A) ↦ p.1 • p.2)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
hA : Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
x : R × A
⊢ Eq.{u_5 + 1} (α := B') (((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B')) x)
    (Function.comp (β := A) (⇑φ : (a : A) → B') (fun (p : R × A) ↦ p.1 • p.2) x)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
hA : Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
⊢ Eq (α := R × A → B') ((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : R × A) ↦ p.1 • p.2)

Tactic:
have hφ2 : (fun p ↦ p.1 • p.2 : S × B' → B') ∘ (Prod.map σ φ) =
        φ ∘ (fun p ↦ p.1 • p.2 : R × A → A) := by ext; simp
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
hA : Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
hφ2 :
  Eq (α := R × A → B') ((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : R × A) ↦ p.1 • p.2)
⊢ IsOpenQuotientMap (X := R × A) (Y := S × B') (Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))

Tactic:
have hoq : IsOpenQuotientMap (_ : R × A → S × B') := IsOpenQuotientMap.prodMap hσ hφo
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
hA : Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
hφ2 :
  Eq (α := R × A → B') ((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : R × A) ↦ p.1 • p.2)
hoq : IsOpenQuotientMap (X := R × A) (Y := S × B') (Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
refine_1 :
  Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4]
    ((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : S × B') ↦
    p.1 • p.2

Tactic:
rw [← hoq.continuous_comp_iff]

Premises used: IsOpenQuotientMap.continuous_comp_iff
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
hA : Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
hφ2 :
  Eq (α := R × A → B') ((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : R × A) ↦ p.1 • p.2)
hoq : IsOpenQuotientMap (X := R × A) (Y := S × B') (Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
refine_1 :
  Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4]
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : R × A) ↦ p.1 • p.2)
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4]
    ((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))

Tactic:
rw [hφ2]
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
hA : Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
hφ2 :
  Eq (α := R × A → B') ((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : R × A) ↦ p.1 • p.2)
hoq : IsOpenQuotientMap (X := R × A) (Y := S × B') (Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4]
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : R × A) ↦ p.1 • p.2)

Tactic:
Continuous.comp hφo.continuous hA

Premises used: IsOpenQuotientMap.continuous, Continuous.comp
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
hA : Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
hφ2 :
  Eq (α := R × A → B') ((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : R × A) ↦ p.1 • p.2)
hoq : IsOpenQuotientMap (X := R × A) (Y := S × B') (Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4]
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : R × A) ↦ p.1 • p.2)

Tactic:
exact Continuous.comp hφo.continuous hA

Premises used: IsOpenQuotientMap.continuous, Continuous.comp
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Ring R
inst_1 : Ring S
A : Type u_3
inst_2 : AddCommGroup A
inst_3 : Module R A
inst_4 : TopologicalSpace A
inst_5 : IsModuleTopology R A
B' : Type u_5
inst_6 : AddCommGroup B'
inst_7 : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := A) (β := B') (⇑φ : (a : A) → B')
this_1 : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
refine_2 :
  Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : B' × B') ↦
    p.1 + p.2
⊢ ContinuousAdd B'

Tactic:
apply ContinuousAdd.mk

Premises used: ContinuousAdd.mk