awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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'
⊢ moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
have refine_2 : ContinuousAdd B'
Tactic: refine sInf_le ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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 S B'
have refine_1 : Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : S × B') ↦ p.1 • p.2
Tactic: apply ContinuousSMul.mk
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : S × B') ↦
    p.1 • p.2
have hA : Continuous[instTopologicalSpaceProd, inst_4] fun (p : R × A) ↦ p.1 • p.2
Tactic: obtain ⟨hA⟩ : ContinuousSMul R A := inferInstance
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : S × B') ↦
    p.1 • p.2
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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)
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : S × B') ↦
    p.1 • p.2
have hoq : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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] fun (p : S × B') ↦
    p.1 • p.2
have 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'))
Tactic: rw [← hoq.continuous_comp_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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]
    ((fun (p : S × B') ↦ p.1 • p.2) ∘ Prod.map (⇑σ : (a : R) → S) (⇑φ : (a : A) → B'))
have 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)
Tactic: rw [hφ2]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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')
⊢ ContinuousAdd B'
have refine_2 : Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : B' × B') ↦
  p.1 + p.2
Tactic: apply ContinuousAdd.mk
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : B' × B') ↦
    p.1 + p.2
have hA : Continuous[instTopologicalSpaceProd, inst_4] fun (p : A × A) ↦ p.1 + p.2
Tactic: obtain ⟨hA⟩ := IsModuleTopology.toContinuousAdd R A
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4] fun (p : B' × B') ↦
    p.1 + p.2
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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] fun (p : B' × B') ↦
    p.1 + p.2
have 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)
Tactic: rw [← (IsOpenQuotientMap.prodMap hφo hφo).continuous_comp_iff, hφ2]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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')
have hOpenMap : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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'
⊢ moduleTopology S B' = TopologicalSpace.coinduced.{u_3, u_5} (X := A) (⇑φ : (a : A) → B') inferInstance
have this₁ : IsModuleTopology S B'
Tactic: haveI : IsModuleTopology S B' := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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
⊢ IsModuleTopology.{u_1, u_3} R (A ⧸ S)
have eq_moduleTopology' : QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)
have this : ContinuousAdd A
Tactic: have := toContinuousAdd R A
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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 = moduleTopology R (A ⧸ S)
have quot : QuotientModule.Quotient.topologicalSpace S = TopologicalSpace.coinduced (⇑S.mkQ : (a : A) → A ⧸ S) inst_4
Tactic: have quot := (Submodule.isOpenQuotientMap_mkQ S).isQuotientMap.eq_coinduced
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)
have module : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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)
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)
have eq_moduleTopology' : Eq (α := TopologicalSpace (A ⧸ S)) (TopologicalSpace.coinduced (⇑S.mkQ : (a : A) → A ⧸ S) inst_4)
  (moduleTopology R (A ⧸ S))
Tactic: rw [quot, module]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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))
⊢ QuotientModule.Quotient.topologicalSpace S = moduleTopology R (A ⧸ S)
have 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)
Tactic: rw [quot, module]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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
⊢ IsModuleTopology R (M × N)
have eq_moduleTopology' : Eq (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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 (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))
have this : ContinuousAdd M
Tactic: have : ContinuousAdd M := toContinuousAdd R M
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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
⊢ Eq (α := TopologicalSpace (M × N)) instTopologicalSpaceProd (moduleTopology R (M × N))
have this₁ : ContinuousAdd N
Tactic: have : ContinuousAdd N := toContinuousAdd R N