awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : A × A) ↦ p.1 + p.2

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

Premises used: IsModuleTopology.toContinuousAdd
-- 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 : A × A) ↦ p.1 + p.2
h :
  ∀ (x : A × A),
    Eq.{u_5 + 1} (α := B') (((fun (p : B' × B') ↦ p.1 + p.2) ∘ Prod.map (⇑φ : (a : A) → B') (⇑φ : (a : A) → B')) x)
      (Function.comp (β := A) (⇑φ : (a : A) → B') (fun (p : A × A) ↦ p.1 + p.2) x)
⊢ Eq (α := A × A → B') ((fun (p : B' × B') ↦ p.1 + p.2) ∘ Prod.map (⇑φ : (a : A) → B') (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : A × 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 : A × A) ↦ p.1 + p.2
x : A × A
⊢ Eq.{u_5 + 1} (α := B') (((fun (p : B' × B') ↦ p.1 + p.2) ∘ Prod.map (⇑φ : (a : A) → B') (⇑φ : (a : A) → B')) x)
    (Function.comp (β := A) (⇑φ : (a : A) → B') (fun (p : A × 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 : A × A) ↦ p.1 + p.2
⊢ Eq (α := A × A → B') ((fun (p : B' × B') ↦ p.1 + p.2) ∘ Prod.map (⇑φ : (a : A) → B') (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : A × A) ↦ 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
-- 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 : A × A) ↦ p.1 + p.2
hφ2 :
  Eq (α := A × A → B') ((fun (p : B' × B') ↦ p.1 + p.2) ∘ Prod.map (⇑φ : (a : A) → B') (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : A × A) ↦ p.1 + p.2)
refine_2 :
  Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4]
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : A × A) ↦ p.1 + p.2)
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : B' × B') ↦
    p.1 + p.2

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

Premises used: IsOpenQuotientMap.prodMap, 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 : A × A) ↦ p.1 + p.2
hφ2 :
  Eq (α := A × A → B') ((fun (p : B' × B') ↦ p.1 + p.2) ∘ Prod.map (⇑φ : (a : A) → B') (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : A × A) ↦ p.1 + p.2)
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4]
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : A × 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 : A × A) ↦ p.1 + p.2
hφ2 :
  Eq (α := A × A → B') ((fun (p : B' × B') ↦ p.1 + p.2) ∘ Prod.map (⇑φ : (a : A) → B') (⇑φ : (a : A) → B'))
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : A × A) ↦ p.1 + p.2)
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4]
    (Function.comp (β := A) (⇑φ : (a : A) → B') fun (p : A × 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
τR : TopologicalSpace R
inst : Ring R
A : Type u_3
inst_1 : AddCommGroup A
inst_2 : Module R A
inst_3 : TopologicalSpace A
inst_4 : IsModuleTopology R A
B : Type u_4
inst_5 : AddCommGroup B
inst_6 : Module R B
τB : TopologicalSpace B
inst_7 : IsModuleTopology R B
φ : A →ₗ[R] B
hφ : Function.Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
⊢ IsQuotientMap.{u_3, u_4} (X := A) (Y := B) (⇑φ : (a : A) → B)

Tactic:
isQuotientMap_of_surjectiveₛₗ .id φ hφ

Premises used: IsModuleTopology.isQuotientMap_of_surjectiveₛₗ
-- 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'
inst_8 : TopologicalSpace B'
inst_9 : 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')
⊢ IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')

Tactic:
have := toContinuousAdd R A
  AddMonoidHom.isOpenQuotientMap_of_isQuotientMap <| isQuotientMap_of_surjectiveₛₗ hσ φ hφ

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

Tactic:
isOpenQuotientMap_of_surjectiveₛₗ .id φ hφ

Premises used: IsModuleTopology.isOpenQuotientMap_of_surjectiveₛₗ
-- 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
B' : Type u_5
inst_5 : AddCommGroup B'
inst_6 : Module S B'
inst_7 : TopologicalSpace B'
inst_8 : IsModuleTopology S B'
inst_9 : ContinuousAdd A
inst_10 : ContinuousSMul R A
σ : 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')
⊢ IsOpenMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')

Tactic:
have hOpenMap :=
    letI : TopologicalSpace A := moduleTopology R A
    have : IsModuleTopology R A := ⟨rfl⟩
    isOpenQuotientMap_of_surjectiveₛₗ hσ φ hφ |>.isOpenMap
-- 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
B' : Type u_5
inst_5 : AddCommGroup B'
inst_6 : Module S B'
inst_7 : TopologicalSpace B'
inst_8 : IsModuleTopology S B'
inst_9 : ContinuousAdd A
inst_10 : ContinuousSMul R A
σ : 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')
hOpenMap : IsOpenMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
U : Set A
hU : IsOpen U
⊢ IsOpen.{u_5} (X := B') ((⇑φ : (a : A) → B') '' U)

Tactic:
hOpenMap U <| moduleTopology_le R A U hU

Premises used: moduleTopology_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
B' : Type u_5
inst_5 : AddCommGroup B'
inst_6 : Module S B'
inst_7 : TopologicalSpace B'
inst_8 : IsModuleTopology S B'
inst_9 : ContinuousAdd A
inst_10 : ContinuousSMul R A
σ : 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')
hOpenMap : IsOpenMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
U : Set A
hU : IsOpen U
⊢ IsOpen.{u_5} (X := B') ((⇑φ : (a : A) → B') '' U)

Tactic:
exact hOpenMap U <| moduleTopology_le R A U hU

Premises used: moduleTopology_le
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
τR : TopologicalSpace R
inst : Ring R
A : Type u_3
inst_1 : AddCommGroup A
inst_2 : Module R A
inst_3 : TopologicalSpace A
B : Type u_4
inst_4 : AddCommGroup B
inst_5 : Module R B
inst_6 : TopologicalSpace B
inst_7 : IsModuleTopology R B
inst_8 : ContinuousAdd A
inst_9 : ContinuousSMul R A
φ : A →ₗ[R] B
hφ : Function.Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
⊢ IsOpenMap.{u_3, u_4} (X := A) (Y := B) (⇑φ : (a : A) → B)

Tactic:
isOpenMap_of_surjectiveₛₗ .id φ hφ

Premises used: IsModuleTopology.isOpenMap_of_surjectiveₛₗ
-- 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 : TopologicalSpace B' := moduleTopology S B'
⊢ IsModuleTopology S B'

Tactic:
haveI : IsModuleTopology S B' := ⟨rfl⟩
-- 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 : TopologicalSpace B' := moduleTopology S B'
this : IsModuleTopology S B'
⊢ moduleTopology S B' = TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance

Tactic:
(isQuotientMap_of_surjectiveₛₗ hσ φ hφ).eq_coinduced

Premises used: Topology.IsCoinducing.eq_coinduced, Topology.IsQuotientMap.isCoinducing, IsModuleTopology.isQuotientMap_of_surjectiveₛₗ
-- 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 : TopologicalSpace B' := moduleTopology S B'
this : IsModuleTopology S B'
⊢ moduleTopology S B' = TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance

Tactic:
exact (isQuotientMap_of_surjectiveₛₗ hσ φ hφ).eq_coinduced

Premises used: Topology.IsCoinducing.eq_coinduced, Topology.IsQuotientMap.isCoinducing, IsModuleTopology.isQuotientMap_of_surjectiveₛₗ
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
τR : TopologicalSpace R
inst : Ring R
A : Type u_3
inst_1 : AddCommGroup A
inst_2 : Module R A
inst_3 : TopologicalSpace A
inst_4 : IsModuleTopology R A
B : Type u_4
inst_5 : AddCommGroup B
inst_6 : Module R B
φ : A →ₗ[R] B
hφ : Function.Surjective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑φ : (a : A) → B)
⊢ moduleTopology R B = TopologicalSpace.coinduced.{u_3, u_4} (X := A) (⇑φ : (a : A) → B) inferInstance

Tactic:
ModuleTopology.eq_coinduced_of_surjectiveₛₗ .id φ hφ

Premises used: ModuleTopology.eq_coinduced_of_surjectiveₛₗ
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S_1 : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S_1
inst : Ring R
inst_1 : Ring S_1
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_4
inst_6 : AddCommGroup B
inst_7 : Module R B
B' : Type u_5
inst_8 : AddCommGroup B'
inst_9 : Module S_1 B'
S : Submodule R A
eq_moduleTopology' : QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)
⊢ IsModuleTopology.{u_1, u_3} R (A ⧸ S)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S_1 : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S_1
inst : Ring R
inst_1 : Ring S_1
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_4
inst_6 : AddCommGroup B
inst_7 : Module R B
B' : Type u_5
inst_8 : AddCommGroup B'
inst_9 : Module S_1 B'
S : Submodule R A
⊢ ContinuousAdd A

Tactic:
have := toContinuousAdd R A
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S_1 : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S_1
inst : Ring R
inst_1 : Ring S_1
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_4
inst_6 : AddCommGroup B
inst_7 : Module R B
B' : Type u_5
inst_8 : AddCommGroup B'
inst_9 : Module S_1 B'
S : Submodule R A
this : ContinuousAdd A
⊢ QuotientModule.Quotient.topologicalSpace S = TopologicalSpace.coinduced (⇑S.mkQ : (a : A) → A ⧸ S) inst_4

Tactic:
have quot := (Submodule.isOpenQuotientMap_mkQ S).isQuotientMap.eq_coinduced
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S_1 : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S_1
inst : Ring R
inst_1 : Ring S_1
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_4
inst_6 : AddCommGroup B
inst_7 : Module R B
B' : Type u_5
inst_8 : AddCommGroup B'
inst_9 : Module S_1 B'
S : Submodule R A
this : ContinuousAdd A
quot : QuotientModule.Quotient.topologicalSpace S = TopologicalSpace.coinduced (⇑S.mkQ : (a : A) → A ⧸ S) inst_4
⊢ Eq (α := TopologicalSpace (A ⧸ S)) (moduleTopology R (A ⧸ S))
    (TopologicalSpace.coinduced (X := A) (⇑S.mkQ : (a : A) → A ⧸ S) inferInstance)

Tactic:
have module := ModuleTopology.eq_coinduced_of_surjective <| Submodule.mkQ_surjective S
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S_1 : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S_1
inst : Ring R
inst_1 : Ring S_1
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_4
inst_6 : AddCommGroup B
inst_7 : Module R B
B' : Type u_5
inst_8 : AddCommGroup B'
inst_9 : Module S_1 B'
S : Submodule R A
this : ContinuousAdd A
quot : QuotientModule.Quotient.topologicalSpace S = TopologicalSpace.coinduced (⇑S.mkQ : (a : A) → A ⧸ S) inst_4
module :
  Eq (α := TopologicalSpace (A ⧸ S)) (moduleTopology R (A ⧸ S))
    (TopologicalSpace.coinduced (X := A) (⇑S.mkQ : (a : A) → A ⧸ S) inferInstance)
eq_moduleTopology' :
  Eq (α := TopologicalSpace (A ⧸ S)) (TopologicalSpace.coinduced (⇑S.mkQ : (a : A) → A ⧸ S) inst_4)
    (moduleTopology R (A ⧸ S))
eq_moduleTopology'₁ eq_moduleTopology'₂ :
  Eq (α := TopologicalSpace (A ⧸ S)) (TopologicalSpace.coinduced (⇑S.mkQ : (a : A) → A ⧸ S) inst_4)
    (TopologicalSpace.coinduced (X := A) (⇑S.mkQ : (a : A) → A ⧸ S) inferInstance)
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)

Tactic:
rw [quot, module]
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
eq_moduleTopology' : Eq (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))
⊢ IsModuleTopology R (M × N)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
⊢ ContinuousAdd M

Tactic:
have : ContinuousAdd M := toContinuousAdd R M
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this : ContinuousAdd M
⊢ ContinuousAdd N

Tactic:
have : ContinuousAdd N := toContinuousAdd R N
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this : ContinuousAdd N
⊢ Eq (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))

Tactic:
le_antisymm ?_ <| sInf_le ⟨Prod.continuousSMul, Prod.continuousAdd⟩

Premises used: Prod.continuousAdd, le_antisymm, Prod.continuousSMul, sInf_le, And.intro
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this : ContinuousAdd N
eq_moduleTopology' : LE.le (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))
⊢ Eq (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))

Tactic:
refine le_antisymm ?_ <| sInf_le ⟨Prod.continuousSMul, Prod.continuousAdd⟩

Premises used: le_antisymm
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
⊢ IsModuleTopology R P

Tactic:
have : IsModuleTopology R P := ⟨rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : IsModuleTopology R M
N : Type u_3
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : TopologicalSpace N
inst_9 : IsModuleTopology R N
this_1 : ContinuousAdd M
this_2 : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this : IsModuleTopology R P
⊢ ContinuousAdd P

Tactic:
have : ContinuousAdd P := ModuleTopology.continuousAdd R P