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 : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := (↑(↑e : A ≃ₛₗ[σ] B') : A →ₛₗ[σ] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
h₁ :
  ∀ (τ : TopologicalSpace B'),
    Membership.mem (γ := Set (TopologicalSpace B'))
        (Set.image.{u_3, u_5} (α := TopologicalSpace A) (TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A))
          {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A})
        τ ↔
      Membership.mem (γ := Set (TopologicalSpace B')) {t : TopologicalSpace B' | ContinuousSMul S B' ∧ ContinuousAdd B'}
        τ
⊢ Eq.{u_5 + 1} (α := Set (TopologicalSpace B'))
    (Set.image.{u_3, u_5} (α := TopologicalSpace A) (TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A))
      {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A})
    {t : TopologicalSpace B' | ContinuousSMul S B' ∧ ContinuousAdd B'}

Tactic:
ext τ
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := (↑(↑e : A ≃ₛₗ[σ] B') : A →ₛₗ[σ] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
τ : TopologicalSpace B'
h₁ :
  (∃ (x : TopologicalSpace A),
      Membership.mem (γ := Set (TopologicalSpace A)) {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A} x ∧
        TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A) x = τ) →
    Membership.mem (γ := Set (TopologicalSpace B')) {t : TopologicalSpace B' | ContinuousSMul S B' ∧ ContinuousAdd B'} τ
h₂ :
  Membership.mem (γ := Set (TopologicalSpace B')) {t : TopologicalSpace B' | ContinuousSMul S B' ∧ ContinuousAdd B'} τ →
    ∃ (x : TopologicalSpace A),
      Membership.mem (γ := Set (TopologicalSpace A)) {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A} x ∧
        TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A) x = τ
⊢ (∃ (x : TopologicalSpace A),
      Membership.mem (γ := Set (TopologicalSpace A)) {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A} x ∧
        TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A) x = τ) ↔
    Membership.mem (γ := Set (TopologicalSpace B')) {t : TopologicalSpace B' | ContinuousSMul S B' ∧ ContinuousAdd B'} τ

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
σ_1 : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ_1 σ'
inst_3 : RingHomInvPair σ' σ_1
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ_1 : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ_1] B'
g : A →ₛₗ[σ_1] B' := (↑(↑e : A ≃ₛₗ[σ_1] B') : A →ₛₗ[σ_1] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
σ : TopologicalSpace A
hσ1 : ContinuousSMul R A
hσ2 : ContinuousAdd A
⊢ Membership.mem (γ := Set (TopologicalSpace B')) {t : TopologicalSpace B' | ContinuousSMul S B' ∧ ContinuousAdd B'}
    (TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A) σ)

Tactic:
⟨continuousSMul_inducedₛₗ g' hσ', continuousAdd_induced h'⟩

Premises used: Set.Mem, setOf, continuousAdd_induced, And.intro, continuousSMul_inducedₛₗ
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
σ_1 : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ_1 σ'
inst_3 : RingHomInvPair σ' σ_1
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ_1 : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ_1] B'
g : A →ₛₗ[σ_1] B' := (↑(↑e : A ≃ₛₗ[σ_1] B') : A →ₛₗ[σ_1] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
σ : TopologicalSpace A
hσ1 : ContinuousSMul R A
hσ2 : ContinuousAdd A
⊢ Membership.mem (γ := Set (TopologicalSpace B')) {t : TopologicalSpace B' | ContinuousSMul S B' ∧ ContinuousAdd B'}
    (TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A) σ)

Tactic:
exact ⟨continuousSMul_inducedₛₗ g' hσ', continuousAdd_induced h'⟩
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := (↑(↑e : A ≃ₛₗ[σ] B') : A →ₛₗ[σ] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
h₁ :
  Membership.mem (γ := Set (TopologicalSpace A)) {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A}
      (TopologicalSpace.induced (⇑e : (a : A) → B') τ) ∧
    TopologicalSpace.induced.{u_5, u_3} (Y := A) (⇑e.toHomeomorph.symm : (a : B') → A)
        (TopologicalSpace.induced (⇑e : (a : A) → B') τ) =
      τ
⊢ ∃ (x : TopologicalSpace A),
    Membership.mem (γ := Set (TopologicalSpace A)) {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A} x ∧
      TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A) x = τ

Tactic:
use τ.induced e

Premises used: TopologicalSpace.induced, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := (↑(↑e : A ≃ₛₗ[σ] B') : A →ₛₗ[σ] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
h₁ :
  Membership.mem (γ := Set (TopologicalSpace A)) {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A}
      (TopologicalSpace.induced (⇑e : (a : A) → B') τ) ∧
    TopologicalSpace.induced
        (Function.comp.{u_5 + 1, u_3 + 1, u_5 + 1} (β := A) (⇑e : (a : A) → B') (⇑e.toHomeomorph.symm : (a : B') → A))
        τ =
      τ
⊢ Membership.mem (γ := Set (TopologicalSpace A)) {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A}
      (TopologicalSpace.induced (⇑e : (a : A) → B') τ) ∧
    TopologicalSpace.induced.{u_5, u_3} (Y := A) (⇑e.toHomeomorph.symm : (a : B') → A)
        (TopologicalSpace.induced (⇑e : (a : A) → B') τ) =
      τ

Tactic:
rw [induced_compose]

Premises used: induced_compose
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := (↑(↑e : A ≃ₛₗ[σ] B') : A →ₛₗ[σ] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ Membership.mem (γ := Set (TopologicalSpace A)) {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A}
      (TopologicalSpace.induced (⇑e : (a : A) → B') τ) ∧
    TopologicalSpace.induced
        (Function.comp.{u_5 + 1, u_3 + 1, u_5 + 1} (β := A) (⇑e : (a : A) → B') (⇑e.toHomeomorph.symm : (a : B') → A))
        τ =
      τ

Tactic:
⟨⟨continuousSMul_inducedₛₗ g hσ, continuousAdd_induced h⟩, ?_⟩

Premises used: continuousAdd_induced, And.intro, continuousSMul_inducedₛₗ
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := (↑(↑e : A ≃ₛₗ[σ] B') : A →ₛₗ[σ] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
h₁ :
  TopologicalSpace.induced
      (Function.comp.{u_5 + 1, u_3 + 1, u_5 + 1} (β := A) (⇑e : (a : A) → B') (⇑e.toHomeomorph.symm : (a : B') → A)) τ =
    τ
⊢ Membership.mem (γ := Set (TopologicalSpace A)) {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A}
      (TopologicalSpace.induced (⇑e : (a : A) → B') τ) ∧
    TopologicalSpace.induced
        (Function.comp.{u_5 + 1, u_3 + 1, u_5 + 1} (β := A) (⇑e : (a : A) → B') (⇑e.toHomeomorph.symm : (a : B') → A))
        τ =
      τ

Tactic:
refine ⟨⟨continuousSMul_inducedₛₗ g hσ, continuousAdd_induced h⟩, ?_⟩
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := (↑(↑e : A ≃ₛₗ[σ] B') : A →ₛₗ[σ] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
h₁ :
  TopologicalSpace.induced
      (Function.comp.{u_5 + 1, u_3 + 1, u_5 + 1} (β := A) (⇑e : (a : A) → B') (⇑e.toHomeomorph.symm : (a : B') → A)) τ =
    TopologicalSpace.induced id τ
⊢ TopologicalSpace.induced
      (Function.comp.{u_5 + 1, u_3 + 1, u_5 + 1} (β := A) (⇑e : (a : A) → B') (⇑e.toHomeomorph.symm : (a : B') → A)) τ =
    τ

Tactic:
nth_rw 2 [← induced_id (t := τ)]

Premises used: induced_id
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
A : Type u_3
inst_4 : AddCommMonoid A
inst_5 : Module R A
τA : TopologicalSpace A
inst_6 : IsModuleTopology R A
B' : Type u_5
inst_7 : AddCommMonoid B'
inst_8 : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
hσ' : Continuous.{u_2, u_1} (X := S) (Y := R) (⇑σ' : (a : S) → R)
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := (↑(↑e : A ≃ₛₗ[σ] B') : A →ₛₗ[σ] B')
g' : B' →ₛₗ[σ'] A := (↑(↑e.symm : B' ≃ₛₗ[σ'] A) : B' →ₛₗ[σ'] A)
h : A →+ B' := (↑e : A →+ B')
h' : B' →+ A := (↑e.symm : B' →+ A)
τ : TopologicalSpace B'
h1 : ContinuousSMul S B'
h2 : ContinuousAdd B'
⊢ TopologicalSpace.induced
      (Function.comp.{u_5 + 1, u_3 + 1, u_5 + 1} (β := A) (⇑e : (a : A) → B') (⇑e.toHomeomorph.symm : (a : B') → A)) τ =
    TopologicalSpace.induced id τ

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
τR : TopologicalSpace R
inst : Semiring R
A : Type u_3
inst_1 : AddCommMonoid A
inst_2 : Module R A
τA : TopologicalSpace A
inst_3 : IsModuleTopology R A
B : Type u_4
inst_4 : AddCommMonoid B
inst_5 : Module R B
τB : TopologicalSpace B
e : A ≃L[R] B
⊢ IsModuleTopology R B

Tactic:
IsModuleTopology.isoₛₗ continuous_id continuous_id e

Premises used: IsModuleTopology.isoₛₗ
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
h : Continuous.{u_1, u_1} (X := R) id
⊢ IsModuleTopology R R

Tactic:
apply of_continuous_id

Premises used: IsModuleTopology.of_continuous_id
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
h : ∀ (x : R), id x = ((fun (rs : R × R) ↦ rs.1 • rs.2) ∘ fun (r : R) ↦ (r, 1)) x
⊢ Eq.{u_1 + 1} (α := (a : R) → R) id ((fun (rs : R × R) ↦ rs.1 • rs.2) ∘ fun (r : R) ↦ (r, 1))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
x : R
⊢ id x = ((fun (rs : R × R) ↦ rs.1 • rs.2) ∘ fun (r : R) ↦ (r, 1)) x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
h : Continuous.{u_1, u_1} (X := R) (Y := R) ((fun (rs : R × R) ↦ rs.1 • rs.2) ∘ fun (r : R) ↦ (r, 1))
⊢ Continuous.{u_1, u_1} (X := R) id

Tactic:
rw [show (id : R → R) = (fun rs ↦ rs.1 • rs.2) ∘ (fun r ↦ (r, 1)) by ext; simp]
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
h : Continuous (Y := R) fun (rs : R × R) ↦ rs.1 • rs.2
h₁ : Continuous (Y := R × R) fun (r : R) ↦ (r, 1)
⊢ Continuous.{u_1, u_1} (X := R) (Y := R) ((fun (rs : R × R) ↦ rs.1 • rs.2) ∘ fun (r : R) ↦ (r, 1))

Tactic:
apply @Continuous.comp R (R × R) R τR (@instTopologicalSpaceProd R R τR (moduleTopology R R))
      (moduleTopology R R)

Premises used: Continuous.comp
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
⊢ Continuous (Y := R) fun (rs : R × R) ↦ rs.1 • rs.2

Tactic:
@continuous_smul _ _ _ _ (moduleTopology R R) <| ModuleTopology.continuousSMul ..

Premises used: ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
⊢ Continuous (Y := R) fun (rs : R × R) ↦ rs.1 • rs.2

Tactic:
exact @continuous_smul _ _ _ _ (moduleTopology R R) <| ModuleTopology.continuousSMul ..

Premises used: ModuleTopology.continuousSMul, ContinuousSMul.continuous_smul
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
⊢ Continuous (Y := R × R) fun (r : R) ↦ (r, 1)

Tactic:
@Continuous.prodMk _ _ _ _ (moduleTopology R R) _ _ _ continuous_id <|
      @continuous_const _ _ _ (moduleTopology R R) _

Premises used: continuous_const, continuous_id, Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
⊢ Continuous (Y := R × R) fun (r : R) ↦ (r, 1)

Tactic:
exact @Continuous.prodMk _ _ _ _ (moduleTopology R R) _ _ _ continuous_id <|
      @continuous_const _ _ _ (moduleTopology R R) _

Premises used: continuous_const, continuous_id, Continuous.prodMk
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
⊢ IsModuleTopology Rᵐᵒᵖ R

Tactic:
.iso (MulOpposite.opContinuousLinearEquiv Rᵐᵒᵖ).symm

Premises used: ContinuousLinearEquiv.symm, MulOpposite, MulOpposite.opContinuousLinearEquiv, IsModuleTopology.iso
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
A : Type u_3
inst_2 : AddCommMonoid A
inst_3 : Module R A
aA : TopologicalSpace A
inst_4 : IsModuleTopology R A
B' : Type u_5
inst_5 : AddCommMonoid B'
inst_6 : Module S B'
aB' : TopologicalSpace B'
inst_7 : ContinuousAdd B'
inst_8 : ContinuousSMul S B'
σ : R →* S
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₑ+[σ] B'
rw : moduleTopology R A ≤ TopologicalSpace.induced (⇑φ : (a : A) → B') aB'
⊢ Continuous.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')

Tactic:
rw [eq_moduleTopology R A, continuous_iff_le_induced]

Premises used: continuous_iff_le_induced, eq_moduleTopology
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
A : Type u_3
inst_2 : AddCommMonoid A
inst_3 : Module R A
aA : TopologicalSpace A
inst_4 : IsModuleTopology R A
B' : Type u_5
inst_5 : AddCommMonoid B'
inst_6 : Module S B'
aB' : TopologicalSpace B'
inst_7 : ContinuousAdd B'
inst_8 : ContinuousSMul S B'
σ : R →* S
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₑ+[σ] B'
⊢ moduleTopology R A ≤ TopologicalSpace.induced (⇑φ : (a : A) → B') aB'

Tactic:
sInf_le <| ⟨continuousSMul_inducedₛₗ φ hσ, continuousAdd_induced φ⟩

Premises used: continuousAdd_induced, sInf_le, And.intro, continuousSMul_inducedₛₗ
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
A : Type u_3
inst_2 : AddCommMonoid A
inst_3 : Module R A
aA : TopologicalSpace A
inst_4 : IsModuleTopology R A
B' : Type u_5
inst_5 : AddCommMonoid B'
inst_6 : Module S B'
aB' : TopologicalSpace B'
inst_7 : ContinuousAdd B'
inst_8 : ContinuousSMul S B'
σ : R →* S
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₑ+[σ] B'
⊢ moduleTopology R A ≤ TopologicalSpace.induced (⇑φ : (a : A) → B') aB'

Tactic:
exact sInf_le <| ⟨continuousSMul_inducedₛₗ φ hσ, continuousAdd_induced φ⟩

Premises used: sInf_le
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
τR : TopologicalSpace R
inst : Semiring R
A : Type u_3
inst_1 : AddCommMonoid A
inst_2 : Module R A
aA : TopologicalSpace A
inst_3 : IsModuleTopology R A
B : Type u_4
inst_4 : AddCommMonoid B
inst_5 : Module R B
aB : TopologicalSpace B
inst_6 : ContinuousAdd B
inst_7 : ContinuousSMul R B
φ : A →+[R] B
⊢ Continuous.{u_3, u_4} (X := A) (Y := B) (⇑φ : (a : A) → B)

Tactic:
continuous_of_distribMulActionHomₑ continuous_id φ

Premises used: IsModuleTopology.continuous_of_distribMulActionHomₑ
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst : Semiring R
inst_1 : Semiring S
A : Type u_3
inst_2 : AddCommMonoid A
inst_3 : Module R A
aA : TopologicalSpace A
inst_4 : IsModuleTopology R A
B' : Type u_5
inst_5 : AddCommMonoid B'
inst_6 : Module S B'
aB' : TopologicalSpace B'
inst_7 : ContinuousAdd B'
inst_8 : ContinuousSMul S B'
σ : R →+* S
hσ : Continuous.{u_1, u_2} (X := R) (Y := S) (⇑σ : (a : R) → S)
φ : A →ₛₗ[σ] B'
⊢ Continuous.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')

Tactic:
continuous_of_distribMulActionHomₑ hσ φ.toDistribMulActionHom

Premises used: LinearMap.toDistribMulActionHom, IsModuleTopology.continuous_of_distribMulActionHomₑ
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
τR : TopologicalSpace R
inst : Semiring R
A : Type u_3
inst_1 : AddCommMonoid A
inst_2 : Module R A
aA : TopologicalSpace A
inst_3 : IsModuleTopology R A
B : Type u_4
inst_4 : AddCommMonoid B
inst_5 : Module R B
aB : TopologicalSpace B
inst_6 : ContinuousAdd B
inst_7 : ContinuousSMul R B
φ : A →ₗ[R] B
⊢ Continuous.{u_3, u_4} (X := A) (Y := B) (⇑φ : (a : A) → B)

Tactic:
continuous_of_distribMulActionHom φ.toDistribMulActionHom

Premises used: LinearMap.toDistribMulActionHom, IsModuleTopology.continuous_of_distribMulActionHom
-- Module: Mathlib.Topology.Algebra.Module.ModuleTopology
Goal:
R : Type u_1
τR : TopologicalSpace R
inst : Semiring R
C : Type u_6
inst_1 : AddCommGroup C
inst_2 : Module R C
inst_3 : TopologicalSpace C
inst_4 : IsModuleTopology R C
⊢ Continuous (Y := C) fun (a : C) ↦ -a

Tactic:
haveI : ContinuousAdd C := IsModuleTopology.toContinuousAdd R C
  continuous_of_linearMap (LinearEquiv.neg R).toLinearMap

Premises used: IsModuleTopology.continuous_of_linearMap, LinearEquiv.toLinearMap, LinearEquiv.neg
-- 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))
r : R
m : A
simp :
  HMul.hMul (α := B) (β := B) ((φ : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B) ((φ : (a : A) → B) m : B) =
    HSMul.hSMul (β := B) r ((φ : (a : A) → B) m : B)
⊢ AddHom.toFun (↑φ : A →ₙ+ B) (r • m) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (AddHom.toFun (↑φ : A →ₙ+ B) m)

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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))
r : R
m : A
⊢ HMul.hMul (α := B) (β := B) ((φ : (a : A) → B) ((algebraMap R A : (a : R) → A) r : A) : B) ((φ : (a : A) → B) m : B) =
    HSMul.hSMul (β := B) r ((φ : (a : A) → B) m : B)

Tactic:
rfl