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 : 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)
⊢ Eq.{u_5 + 1} (α := TopologicalSpace B')
    (sInf
      (Set.image.{u_3, u_5} (α := TopologicalSpace A) (TopologicalSpace.induced (⇑e.toHomeomorph.symm : (a : B') → A))
        {t : TopologicalSpace A | ContinuousSMul R A ∧ ContinuousAdd A}))
    (sInf {t : TopologicalSpace B' | ContinuousSMul S B' ∧ ContinuousAdd B'})
have h₁ : 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: apply congr_arg
-- 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 : 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)
⊢ 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'}
have 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'} τ
Tactic: ext τ
-- 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 : 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'
⊢ (∃ (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'} τ
have 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'} τ
Tactic: constructor
-- 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 : 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'} τ
⊢ (∃ (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'} τ
have 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 = τ
Tactic: constructor
-- 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 : 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'
⊢ ∃ (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 = τ
have 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') τ) =
    τ
Tactic: use τ.induced e
-- 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 : 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.{u_5, u_3} (Y := A) (⇑e.toHomeomorph.symm : (a : B') → A)
        (TopologicalSpace.induced (⇑e : (a : A) → B') τ) =
      τ
have 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)) τ =
    τ
Tactic: rw [induced_compose]
-- 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 : 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))
        τ =
      τ
have 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)) τ =
  τ
Tactic: refine ⟨⟨continuousSMul_inducedₛₗ g hσ, continuousAdd_induced h⟩, ?_⟩
-- 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 : 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)) τ =
    τ
have 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 τ
Tactic: nth_rw 2 [← induced_id (t := τ)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
⊢ IsModuleTopology R R
have h : Continuous.{u_1, u_1} (X := R) id
Tactic: apply of_continuous_id
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
⊢ Eq.{u_1 + 1} (α := (a : R) → R) id ((fun (rs : R × R) ↦ rs.1 • rs.2) ∘ fun (r : R) ↦ (r, 1))
have h : ∀ (x : R), id x = ((fun (rs : R × R) ↦ rs.1 • rs.2) ∘ fun (r : R) ↦ (r, 1)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
⊢ Continuous.{u_1, u_1} (X := R) id
have h : Continuous.{u_1, u_1} (X := R) (Y := R) ((fun (rs : R × R) ↦ rs.1 • rs.2) ∘ fun (r : R) ↦ (r, 1))
Tactic: rw [show (id : R → R) = (fun rs ↦ rs.1 • rs.2) ∘ (fun r ↦ (r, 1)) by ext; simp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
Goal:
R : Type u_1
inst : Semiring R
τR : TopologicalSpace R
inst_1 : IsTopologicalSemiring R
⊢ Continuous.{u_1, u_1} (X := R) (Y := R) ((fun (rs : R × R) ↦ rs.1 • rs.2) ∘ fun (r : R) ↦ (r, 1))
have h : Continuous (Y := R) fun (rs : R × R) ↦ rs.1 • rs.2
Tactic: apply @Continuous.comp R (R × R) R τR (@instTopologicalSpaceProd R R τR (moduleTopology R R))
      (moduleTopology R R)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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
⊢ Continuous.{u_1, u_1} (X := R) (Y := R) ((fun (rs : R × R) ↦ rs.1 • rs.2) ∘ fun (r : R) ↦ (r, 1))
have h₁ : Continuous (Y := R × R) fun (r : R) ↦ (r, 1)
Tactic: apply @Continuous.comp R (R × R) R τR (@instTopologicalSpaceProd R R τR (moduleTopology R R))
      (moduleTopology R R)
-- 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 : 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')
have rw : moduleTopology R A ≤ TopologicalSpace.induced (⇑φ : (a : A) → B') aB'
Tactic: rw [eq_moduleTopology R A, continuous_iff_le_induced]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (goal)
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
⊢ AddHom.toFun (↑φ : A →ₙ+ B) (r • m) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (AddHom.toFun (↑φ : A →ₙ+ B) m)
have 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)
Tactic: simp [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ModuleTopology (hypothesis)
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' := ⋯ }
⊢ Continuous.{u_7, u_8} (X := A) (Y := B) (⇑φ : (a : A) → B)
have this : ContinuousSMul R B
Tactic: have : ContinuousSMul R B := ⟨(hφ.comp continuous_fst).mul continuous_snd⟩
-- 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'
τ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')
⊢ τB = TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
have this : ContinuousAdd A
Tactic: haveI := IsModuleTopology.toContinuousAdd R A
-- 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'
τ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
⊢ τB = TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
have this₁ : ContinuousAdd B'
Tactic: haveI := IsModuleTopology.toContinuousAdd S B'
-- 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'
τ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'
⊢ τB = TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
have this₁ : Continuous[inst_4, τB] (⇑φ : (a : A) → B')
Tactic: have this : Continuous φ := continuous_of_linearMapₛₗ hσ.continuous φ
-- 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'
τ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')
⊢ τB = TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
have this₁ : TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4 ≤ τB
Tactic: rw [continuous_iff_coinduced_le] at this
Cleared hypotheses: this
-- 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'
τ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
have refine : τB ≤ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
Tactic: refine le_antisymm ?_ this
-- 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'
τ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
have rw : moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
Tactic: rw [eq_moduleTopology S B']
-- 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
⊢ moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
have hφo : IsOpenQuotientMap.{u_3, u_5} (X := A) (Y := B') (⇑φ : (a : A) → B')
Tactic: have hφo : IsOpenQuotientMap φ := AddMonoidHom.isOpenQuotientMap_of_isQuotientMap ⟨⟨rfl⟩, hφ⟩
-- 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')
⊢ moduleTopology S B' ≤ TopologicalSpace.coinduced (⇑φ : (a : A) → B') inst_4
have refine_1 : ContinuousSMul S B'
Tactic: refine sInf_le ⟨?_, ?_⟩