awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hg : ∀ x ∈ K, g x ≤ u
hf :
  ∀ (a : β × β → Prop),
    (∃ (v : Set β), Membership.mem (γ := Filter β) (𝓝 0) v ∧ ∀ y ∈ v, ∀ (a_2 b : β), -a_2 + b = y → a (a_2, b)) →
      ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, a (g x.2, f x.1 x.2)
hf2 : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, (fun (x : β × β) ↦ -x.1 + x.2 < -u + v) (g x.2, f x.1 x.2)
i : ι
hi : ∀ y ∈ K, -g y + f i y < -u + v
x : α
hx : x ∈ K
⊢ f i x < v

Tactic:
simpa using add_lt_add_of_le_of_lt (hg x hx) (hi x hx)

Premises used: add_lt_add_of_le_of_lt
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hf : TendstoUniformlyOn f g p K
hg : ∀ x ∈ K, g x ≤ u
i : ι
hi : ∀ x ∈ K, f i x < v
x : α
hx : x ∈ K
⊢ f i x ≤ v

Tactic:
(hi x hx).le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Order
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : UniformSpace β
inst_1 : AddGroup β
inst_2 : IsUniformAddGroup β
inst_3 : PartialOrder β
inst_4 : OrderTopology β
inst_5 : AddLeftMono β
inst_6 : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hf : TendstoUniformlyOn f g p K
hg : ∀ x ∈ K, g x ≤ u
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ ∀ x ∈ K, f i x < v) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ ∀ x ∈ K, f i x ≤ v) x} x}
      a
h₁ h₂ : ∀ (i : ι) (hi : ∀ x ∈ K, f i x < v) (x : α) (hx : x ∈ K), f i x ≤ v
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x ≤ v

Tactic:
filter_upwards [hf.eventually_forall_lt huv hg] with i hi x hx using (hi x hx).le

Premises used: TendstoUniformlyOn.eventually_forall_lt
-- Module: Mathlib.Topology.Algebra.LinearMapCompletion
Goal:
α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R₁
inst_4 : Module R₁ α
inst_5 : UniformContinuousConstSMul R₁ α
inst_6 : Semiring R₂
inst_7 : UniformSpace β
inst_8 : AddCommGroup β
inst_9 : IsUniformAddGroup β
inst_10 : Module R₂ β
inst_11 : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
f : α →SL[σ] β
r : R₁
⊢ IsClosed.{u_1} (X := Completion α)
    {a : Completion α |
      ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β)) (r • a) =
        HSMul.hSMul.{u_4, u_2, u_2} (α := R₂) ((σ : (a : R₁) → R₂) r : R₂)
          (ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β)) a)}

Tactic:
isClosed_eq (continuous_map.comp <| continuous_const_smul r)
        (continuous_map.const_smul _)

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp, isClosed_eq, UniformSpace.Completion.continuous_map, Continuous.const_smul
-- Module: Mathlib.Topology.Algebra.LinearMapCompletion
Goal:
α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R₁
inst_4 : Module R₁ α
inst_5 : UniformContinuousConstSMul R₁ α
inst_6 : Semiring R₂
inst_7 : UniformSpace β
inst_8 : AddCommGroup β
inst_9 : IsUniformAddGroup β
inst_10 : Module R₂ β
inst_11 : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
f : α →SL[σ] β
r : R₁
⊢ IsClosed.{u_1} (X := Completion α)
    {a : Completion α |
      ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β)) (r • a) =
        HSMul.hSMul.{u_4, u_2, u_2} (α := R₂) ((σ : (a : R₁) → R₂) r : R₂)
          (ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β)) a)}

Tactic:
exact isClosed_eq (continuous_map.comp <| continuous_const_smul r)
        (continuous_map.const_smul _)

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp, isClosed_eq, UniformSpace.Completion.continuous_map, Continuous.const_smul
-- Module: Mathlib.Topology.Algebra.LinearMapCompletion
Goal:
α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R₁
inst_4 : Module R₁ α
inst_5 : UniformContinuousConstSMul R₁ α
inst_6 : Semiring R₂
inst_7 : UniformSpace β
inst_8 : AddCommGroup β
inst_9 : IsUniformAddGroup β
inst_10 : Module R₂ β
inst_11 : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
f : α →SL[σ] β
r : R₁
x : α
⊢ ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β))
      (HSMul.hSMul (β := Completion α) r (↑x : Completion α)) =
    HSMul.hSMul.{u_4, u_2, u_2} (α := R₂) ((σ : (a : R₁) → R₂) r : R₂)
      (ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β))
        (↑x : Completion α))

Tactic:
simp [← Completion.coe_smul]

Premises used: UniformSpace.Completion.coe_smul
-- Module: Mathlib.Topology.Algebra.LinearMapCompletion
Goal:
α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R₁
inst_4 : Module R₁ α
inst_5 : UniformContinuousConstSMul R₁ α
inst_6 : Semiring R₂
inst_7 : UniformSpace β
inst_8 : AddCommGroup β
inst_9 : IsUniformAddGroup β
inst_10 : Module R₂ β
inst_11 : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
f : α →SL[σ] β
r : R₁
x : Completion α
hp :
  IsClosed.{u_1} (X := Completion α)
    {a : Completion α |
      ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β)) (r • a) =
        HSMul.hSMul.{u_4, u_2, u_2} (α := R₂) ((σ : (a : R₁) → R₂) r : R₂)
          (ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β)) a)}
ih :
  ∀ (x : α),
    ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β))
        (HSMul.hSMul (β := Completion α) r (↑x : Completion α)) =
      HSMul.hSMul.{u_4, u_2, u_2} (α := R₂) ((σ : (a : R₁) → R₂) r : R₂)
        (ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β))
          (↑x : Completion α))
⊢ ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β)) (r • x) =
    HSMul.hSMul.{u_4, u_2, u_2} (α := R₂) ((σ : (a : R₁) → R₂) r : R₂)
      (ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯) : ZeroHom (Completion α) (Completion β)) x)

Tactic:
induction x using induction_on with
    | hp =>
      exact isClosed_eq (continuous_map.comp <| continuous_const_smul r)
        (continuous_map.const_smul _)
    | ih x => simp [← Completion.coe_smul]

Premises used: ContinuousConstSMul.continuous_const_smul, Continuous.comp, UniformSpace.Completion.coe_smul, isClosed_eq, UniformSpace.Completion.continuous_map, Continuous.const_smul
-- Module: Mathlib.Topology.Algebra.LinearMapCompletion
Goal:
α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R₁
inst_4 : Module R₁ α
inst_5 : UniformContinuousConstSMul R₁ α
inst_6 : Semiring R₂
inst_7 : UniformSpace β
inst_8 : AddCommGroup β
inst_9 : IsUniformAddGroup β
inst_10 : Module R₂ β
inst_11 : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
f : α →SL[σ] β
⊢ Eq (α := AddMonoidHom.{u_1, u_2} (Completion α) (Completion β))
    (LinearMap.toAddMonoidHom (modM₁ := instModule) (modM₂ := instModule)
      (↑f.completion : Completion α →ₛₗ[σ] Completion β))
    ((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion ⋯)

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, AddMonoidHom.extension, UniformSpace.Completion.extension, AbstractCompletion.extend, rfl, AddMonoidHom.completion, ite
-- Module: Mathlib.Topology.Algebra.LinearMapCompletion
Goal:
α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R₁
inst_4 : Module R₁ α
inst_5 : UniformContinuousConstSMul R₁ α
inst_6 : Semiring R₂
inst_7 : UniformSpace β
inst_8 : AddCommGroup β
inst_9 : IsUniformAddGroup β
inst_10 : Module R₂ β
inst_11 : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
f : α →SL[σ] β
⊢ Eq (α := (a : Completion α) → Completion β) (⇑f.completion : (a : Completion α) → Completion β)
    (Completion.map (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: UniformSpace.Completion.map, UniformSpace.Completion.coe', Quotient, SeparationQuotient, SeparationQuotient.mk, UniformSpace.Completion.extension, AbstractCompletion.map, AbstractCompletion.extend, UniformSpace.Completion, rfl, ite
-- Module: Mathlib.Topology.Algebra.LinearMapCompletion
Goal:
α : Type u_1
β : Type u_2
R₁ : Type u_3
R₂ : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R₁
inst_4 : Module R₁ α
inst_5 : UniformContinuousConstSMul R₁ α
inst_6 : Semiring R₂
inst_7 : UniformSpace β
inst_8 : AddCommGroup β
inst_9 : IsUniformAddGroup β
inst_10 : Module R₂ β
inst_11 : UniformContinuousConstSMul R₂ β
σ : R₁ →+* R₂
f : α →SL[σ] β
a : α
⊢ Eq.{u_2 + 1} (α := Completion β)
    (((f.completion : ContinuousLinearMap.{u_3, u_4, u_1, u_2} σ (Completion α) (Completion β)) :
          (a : Completion α) → Completion β)
        (↑a : Completion α) :
      Completion β)
    ((↑((f : (a : α) → β) a) : Completion β) : Completion β)

Tactic:
simp [coe_completion, map_coe]

Premises used: UniformSpace.Completion.map_coe, ContinuousLinearMap.coe_completion
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : IsLinearTopology R M
⊢ HasBasis (α := M) (𝓝 0) (fun (N : Submodule R M) ↦ Membership.mem (γ := Filter M) (𝓝 0) (↑N : Set M))
    fun (N : Submodule R M) ↦ (↑N : Set M)

Tactic:
IsLinearTopology.hasBasis_submodule'

Premises used: IsLinearTopology.hasBasis_submodule'
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : ContinuousAdd M
inst_5 : IsLinearTopology R M
⊢ HasBasis (α := M) (𝓝 0) (fun (N : Submodule R M) ↦ IsOpen[inst_3] (↑N : Set M)) fun (N : Submodule R M) ↦ (↑N : Set M)

Tactic:
hasBasis_submodule R |>.congr
    (fun N ↦ ⟨N.toAddSubgroup.isOpen_of_mem_nhds, fun hN ↦ hN.mem_nhds (zero_mem N)⟩)
    (fun _ _ ↦ rfl)

Premises used: IsLinearTopology.hasBasis_submodule, AddSubgroup.isOpen_of_mem_nhds, Submodule.toAddSubgroup, IsOpen.mem_nhds, Iff.intro, ZeroMemClass.zero_mem, Filter.HasBasis.congr, rfl
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
ι : Sort u_4
S : Type u_5
inst_4 : SetLike S M
inst_5 : SMulMemClass S R M
inst_6 : AddSubmonoidClass S M
p : ι → Prop
s : ι → S
h : HasBasis.{u_3, u_4} (α := M) (𝓝 0) p fun (i : ι) ↦ (↑(s i) : Set M)
⊢ IsLinearTopology R M

Tactic:
mk_of_hasBasis' R h fun _ ↦ SMulMemClass.smul_mem

Premises used: SMulMemClass.smul_mem, IsLinearTopology.mk_of_hasBasis'
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
⊢ IsLinearTopology R M ↔
    HasBasis (α := M) (𝓝 0) (fun (N : Submodule R M) ↦ Membership.mem (γ := Filter M) (𝓝 0) (↑N : Set M))
      fun (N : Submodule R M) ↦ (↑N : Set M)

Tactic:
⟨fun _ ↦ hasBasis_submodule R, fun h ↦ .mk_of_hasBasis R h⟩

Premises used: IsLinearTopology.hasBasis_submodule, IsLinearTopology.mk_of_hasBasis, Iff.intro
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : ContinuousAdd M
⊢ IsLinearTopology R M ↔
    HasBasis (α := M) (𝓝 0) (fun (N : Submodule R M) ↦ IsOpen[inst_3] (↑N : Set M)) fun (N : Submodule R M) ↦
      (↑N : Set M)

Tactic:
⟨fun _ ↦ hasBasis_open_submodule R, fun h ↦ .mk_of_hasBasis R h⟩

Premises used: IsLinearTopology.hasBasis_open_submodule, IsLinearTopology.mk_of_hasBasis, Iff.intro
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : DiscreteTopology M
rw : HasBasis.{u_3, 1} (α := M) (pure 0) (fun (x : Unit) ↦ True) fun (x : Unit) ↦ (↑⊥ : Set M)
⊢ HasBasis.{u_3, 1} (α := M) (𝓝 0) (fun (x : Unit) ↦ True) fun (x : Unit) ↦ (↑⊥ : Set M)

Tactic:
rw [nhds_discrete]

Premises used: nhds_discrete
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : DiscreteTopology M
⊢ HasBasis.{u_3, 1} (α := M) (pure 0) (fun (x : Unit) ↦ True) fun (x : Unit) ↦ (↑⊥ : Set M)

Tactic:
hasBasis_pure _

Premises used: Filter.hasBasis_pure, setOf, Set.singleton
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : DiscreteTopology M
⊢ HasBasis.{u_3, 1} (α := M) (pure 0) (fun (x : Unit) ↦ True) fun (x : Unit) ↦ (↑⊥ : Set M)

Tactic:
exact hasBasis_pure _

Premises used: Filter.hasBasis_pure
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
⊢ HasBasis (α := M) (𝓝 0)
    (fun (I : AddSubgroup M) ↦
      Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M) ∧
        (∀ (r : R), ∀ x ∈ I, r • x ∈ I) ∧ ∀ (r' : R'), ∀ x ∈ I, r' • x ∈ I)
    fun (I : AddSubgroup M) ↦ (↑I : Set M)

Tactic:
IsLinearTopology.hasBasis_submodule R |>.to_hasBasis (fun I hI ↦ ?_)
    (fun I hI ↦ ⟨{I with smul_mem' := fun r x hx ↦ hI.2.1 r x hx}, hI.1, subset_rfl⟩)

Premises used: IsLinearTopology.hasBasis_submodule, And.right, And.left, And.intro, Exists.intro, Submodule.mk, Filter.HasBasis.to_hasBasis, AddSubgroup.toAddSubmonoid, subset_rfl
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
refine :
  ∀ (I : Submodule R M) (hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)),
    ∃ (i' : AddSubgroup M),
      (Membership.mem (γ := Filter M) (𝓝 0) (↑i' : Set M) ∧
          (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧
        (↑i' : Set M) ⊆ (↑I : Set M)
⊢ HasBasis (α := M) (𝓝 0)
    (fun (I : AddSubgroup M) ↦
      Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M) ∧
        (∀ (r : R), ∀ x ∈ I, r • x ∈ I) ∧ ∀ (r' : R'), ∀ x ∈ I, r' • x ∈ I)
    fun (I : AddSubgroup M) ↦ (↑I : Set M)

Tactic:
refine IsLinearTopology.hasBasis_submodule R |>.to_hasBasis (fun I hI ↦ ?_)
    (fun I hI ↦ ⟨{I with smul_mem' := fun r x hx ↦ hI.2.1 r x hx}, hI.1, subset_rfl⟩)

Premises used: IsLinearTopology.hasBasis_submodule, And.intro, Exists.intro, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
rcases :
  ∀ (J : Submodule R' M) (hJ : Membership.mem (γ := Filter M) (𝓝 0) (↑J : Set M))
    (J_sub_I : (↑J : Set M) ⊆ (↑I : Set M)),
    ∃ (i' : AddSubgroup M),
      (Membership.mem (γ := Filter M) (𝓝 0) (↑i' : Set M) ∧
          (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧
        (↑i' : Set M) ⊆ (↑I : Set M)
⊢ ∃ (i' : AddSubgroup M),
    (Membership.mem (γ := Filter M) (𝓝 0) (↑i' : Set M) ∧
        (∀ (r : R), ∀ x ∈ i', r • x ∈ i') ∧ ∀ (r' : R'), ∀ x ∈ i', r' • x ∈ i') ∧
      (↑i' : Set M) ⊆ (↑I : Set M)

Tactic:
rcases (hasBasis_submodule R').mem_iff.mp hI with ⟨J, hJ, J_sub_I⟩

Premises used: Filter.HasBasis.mem_iff, IsLinearTopology.hasBasis_submodule, Iff.mp
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
J : Submodule R' M
hJ : Membership.mem (γ := Filter M) (𝓝 0) (↑J : Set M)
J_sub_I : (↑J : Set M) ⊆ (↑I : Set M)
uR : Set R := univ
uR' : Set R' := univ
⊢ uR * uR ⊆ uR

Tactic:
have hRR : uR * uR ⊆ uR := subset_univ _
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
J : Submodule R' M
hJ : Membership.mem (γ := Filter M) (𝓝 0) (↑J : Set M)
J_sub_I : (↑J : Set M) ⊆ (↑I : Set M)
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
⊢ uR • (↑I : Set M) ⊆ (↑I : Set M)

Tactic:
have hRI : uR • (I : Set M) ⊆ I := smul_subset_iff.mpr fun x _ i hi ↦ I.smul_mem x hi
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
J : Submodule R' M
hJ : Membership.mem (γ := Filter M) (𝓝 0) (↑J : Set M)
J_sub_I : (↑J : Set M) ⊆ (↑I : Set M)
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • (↑I : Set M) ⊆ (↑I : Set M)
⊢ uR' • (↑J : Set M) ⊆ (↑J : Set M)

Tactic:
have hR'J : uR' • (J : Set M) ⊆ J := smul_subset_iff.mpr fun x _ j hj ↦ J.smul_mem x hj
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
J : Submodule R' M
hJ : Membership.mem (γ := Filter M) (𝓝 0) (↑J : Set M)
J_sub_I : (↑J : Set M) ⊆ (↑I : Set M)
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • (↑I : Set M) ⊆ (↑I : Set M)
hR'J : uR' • (↑J : Set M) ⊆ (↑J : Set M)
⊢ uR • (↑J : Set M) ⊆ (↑I : Set M)

Tactic:
have hRJ : uR • (J : Set M) ⊆ I := subset_trans (smul_subset_smul_left J_sub_I) hRI
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
J : Submodule R' M
hJ : Membership.mem (γ := Filter M) (𝓝 0) (↑J : Set M)
J_sub_I : (↑J : Set M) ⊆ (↑I : Set M)
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • (↑I : Set M) ⊆ (↑I : Set M)
hR'J : uR' • (↑J : Set M) ⊆ (↑J : Set M)
hRJ : uR • (↑J : Set M) ⊆ (↑I : Set M)
S : Set M := (↑J : Set M) ∪ uR • (↑J : Set M)
⊢ S ⊆ (↑I : Set M)

Tactic:
have S_sub_I : S ⊆ I := union_subset J_sub_I hRJ
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
J : Submodule R' M
hJ : Membership.mem (γ := Filter M) (𝓝 0) (↑J : Set M)
J_sub_I : (↑J : Set M) ⊆ (↑I : Set M)
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • (↑I : Set M) ⊆ (↑I : Set M)
hR'J : uR' • (↑J : Set M) ⊆ (↑J : Set M)
hRJ : uR • (↑J : Set M) ⊆ (↑I : Set M)
S : Set M := (↑J : Set M) ∪ uR • (↑J : Set M)
S_sub_I : S ⊆ (↑I : Set M)
simp_rw : uR • ((↑J : Set M) ∪ uR • (↑J : Set M)) = uR • (↑J : Set M) ∪ (uR * uR) • (↑J : Set M)
simp_rw₁ : uR • (↑J : Set M) ∪ uR • uR • (↑J : Set M) = uR • (↑J : Set M) ∪ (uR * uR) • (↑J : Set M)
⊢ uR • S = uR • (↑J : Set M) ∪ (uR * uR) • (↑J : Set M)

Tactic:
simp_rw [S, smul_union, mul_smul]

Premises used: Set.smul_union, SemigroupAction.mul_smul
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
J : Submodule R' M
hJ : Membership.mem (γ := Filter M) (𝓝 0) (↑J : Set M)
J_sub_I : (↑J : Set M) ⊆ (↑I : Set M)
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • (↑I : Set M) ⊆ (↑I : Set M)
hR'J : uR' • (↑J : Set M) ⊆ (↑J : Set M)
hRJ : uR • (↑J : Set M) ⊆ (↑I : Set M)
S : Set M := (↑J : Set M) ∪ uR • (↑J : Set M)
S_sub_I : S ⊆ (↑I : Set M)
⊢ uR • (↑J : Set M) ∪ (uR * uR) • (↑J : Set M) ⊆ uR • (↑J : Set M) ∪ uR • (↑J : Set M)

Tactic:
gcongr
-- Module: Mathlib.Topology.Algebra.LinearTopology
Goal:
R : Type u_1
R' : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Ring R'
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module R' M
inst_5 : SMulCommClass R R' M
inst_6 : TopologicalSpace M
inst_7 : IsLinearTopology R M
inst_8 : IsLinearTopology R' M
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
J : Submodule R' M
hJ : Membership.mem (γ := Filter M) (𝓝 0) (↑J : Set M)
J_sub_I : (↑J : Set M) ⊆ (↑I : Set M)
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • (↑I : Set M) ⊆ (↑I : Set M)
hR'J : uR' • (↑J : Set M) ⊆ (↑J : Set M)
hRJ : uR • (↑J : Set M) ⊆ (↑I : Set M)
S : Set M := (↑J : Set M) ∪ uR • (↑J : Set M)
S_sub_I : S ⊆ (↑I : Set M)
⊢ uR • S ⊆ S

Tactic:
have hRS : uR • S ⊆ S := calc
    uR • S = uR • (J : Set M) ∪ (uR * uR) • (J : Set M) := by simp_rw [S, smul_union, mul_smul]
    _ ⊆ uR • (J : Set M) ∪ uR • (J : Set M) := by gcongr
    _ = uR • (J : Set M) := union_self _
    _ ⊆ S := subset_union_right