awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Order (hypothesis)
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 : ι) in p, ∀ x ∈ K, f i x < v
have hf₁ : ∀ ⦃p_1 : β × β → Prop⦄,
  (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
Tactic: simp only [tendstoUniformlyOn_iff_tendsto, uniformity_eq_comap_neg_add_nhds_zero,
    tendsto_iff_eventually, eventually_comap, Prod.forall] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Order (goal)
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 :
  ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
| ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
have enter : ∀ (p_1 : β × β → Prop),
  (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
Tactic: enter [2]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Order (goal)
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 :
  ∀ ⦃p_2 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_2 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_2 (g x.2, f x.1 x.2)
p_1 : β × β → Prop
| (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
have rw : (∃ (v : Set β), Membership.mem (γ := Filter β) (𝓝 0) v ∧ ∀ y ∈ v, ∀ (a b : β), -a + b = y → p_1 (a, b)) →
  ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
Tactic: rw [eventually_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Order (goal)
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 :
  ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
| ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
have enter : ∀ (p_1 : β × β → Prop),
  (∃ (v : Set β), Membership.mem (γ := Filter β) (𝓝 0) v ∧ ∀ y ∈ v, ∀ (a b : β), -a + b = y → p_1 (a, b)) →
    ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
Tactic: enter [2]; rw [eventually_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Order (hypothesis)
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 :
  ∀ ⦃p_1 : β × β → Prop⦄,
    (∀ᶠ (b : β) in 𝓝 0, ∀ (a b_1 : β), -a + b_1 = b → p_1 (a, b_1)) → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, p_1 (g x.2, f x.1 x.2)
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x < v
have 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)
Tactic: conv at hf => enter [2]; rw [eventually_iff_exists_mem]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Order (hypothesis)
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)
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x < v
have hf2 : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 K, (fun (x : β × β) ↦ -x.1 + x.2 < -u + v) (g x.2, f x.1 x.2)
Tactic: have hf2 := hf (fun x ↦ -x.1 + x.2 < -u + v) ⟨_, (isOpen_gt' (-u + v)).mem_nhds (by simp [huv]),
    fun y hy a b hab ↦ (hab.symm ▸ hy :)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Order (goal)
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 : ι) in p, ∀ x ∈ K, f i x < v
have h : ∀ (i : ι) (hi : ∀ y ∈ K, -g y + f i y < -u + v) (x : α) (hx : x ∈ K), f i x < v
Tactic: filter_upwards [eventually_prod_principal_iff.mp hf2] with i hi x hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Order (goal)
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 : ι) in p, ∀ x ∈ K, f i x ≤ v
have 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
Tactic: filter_upwards [hf.eventually_forall_lt huv hg] with i hi x hx using (hi x hx).le
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsUniformGroup.Order (goal)
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
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x ≤ v
have h₁ : ∀ (a : ι), (∀ x ∈ K, f a x < v) → ∀ x ∈ K, f a x ≤ v
Tactic: filter_upwards [hf.eventually_forall_lt huv hg] with i hi x hx using (hi x hx).le
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearMapCompletion (goal)
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 α
⊢ 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)
have hp : IsClosed.{u_1} (X := Completion α)
  {a : Completion α |
    ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion sorry) : ZeroHom (Completion α) (Completion β)) (r • a) =
      HSMul.hSMul.{u_4, u_2, u_2} (α := R₂) ((σ : (a : R₁) → R₂) r : R₂)
        (ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion sorry) : ZeroHom (Completion α) (Completion β)) a)}
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearMapCompletion (goal)
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)}
⊢ 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)
have ih : ∀ (x : α),
  ZeroHom.toFun (↑((↑f : α →ₛₗ[σ] β).toAddMonoidHom.completion sorry) : 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 sorry) : ZeroHom (Completion α) (Completion β))
        (↑x : Completion α))
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (goal)
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) (𝓝 0) (fun (x : Unit) ↦ True) fun (x : Unit) ↦ (↑⊥ : Set M)
have rw : HasBasis.{u_3, 1} (α := M) (pure 0) (fun (x : Unit) ↦ True) fun (x : Unit) ↦ (↑⊥ : Set M)
Tactic: rw [nhds_discrete]
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (goal)
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)
have 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)
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⟩)
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases (hasBasis_submodule R').mem_iff.mp hI with ⟨J, hJ, J_sub_I⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (hypothesis)
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
⊢ ∃ (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)
have hRR : uR * uR ⊆ uR
Tactic: have hRR : uR * uR ⊆ uR := subset_univ _
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (hypothesis)
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
⊢ ∃ (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)
have hRI : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (hypothesis)
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)
⊢ ∃ (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)
have hR'J : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (hypothesis)
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)
⊢ ∃ (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)
have hRJ : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (hypothesis)
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)
⊢ ∃ (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)
have S_sub_I : S ⊆ (↑I : Set M)
Tactic: have S_sub_I : S ⊆ I := union_subset J_sub_I hRJ
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (goal)
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)
⊢ uR • S = uR • (↑J : Set M) ∪ (uR * uR) • (↑J : Set M)
have simp_rw₁ : uR • (↑J : Set M) ∪ uR • uR • (↑J : Set M) = uR • (↑J : Set M) ∪ (uR * uR) • (↑J : Set M)
Tactic: simp_rw [S, smul_union, mul_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (hypothesis)
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)
⊢ ∃ (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)
have hRS : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (goal)
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)
hRS : uR • S ⊆ S
simp_rw : uR' • ((↑J : Set M) ∪ uR • (↑J : Set M)) = uR' • (↑J : Set M) ∪ uR • uR' • (↑J : Set M)
⊢ uR' • S = uR' • (↑J : Set M) ∪ uR • uR' • (↑J : Set M)
have simp_rw₁ : uR' • (↑J : Set M) ∪ uR' • uR • (↑J : Set M) = uR' • (↑J : Set M) ∪ uR • uR' • (↑J : Set M)
Tactic: simp_rw [S, smul_union, smul_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (hypothesis)
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)
hRS : uR • S ⊆ S
⊢ ∃ (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)
have hR'S : uR' • S ⊆ S
Tactic: have hR'S : uR' • S ⊆ S := calc
    uR' • S = uR' • (J : Set M) ∪ uR • uR' • (J : Set M) := by simp_rw [S, smul_union, smul_comm]
    _ ⊆ J ∪ uR • J := by gcongr
    _ = S := rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (goal)
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)
hRS : uR • S ⊆ S
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
r : R
i : M
hi : i ∈ A
⊢ r • i ∈ A
have refine : ∀ (x : M) (hx : x ∈ S), r • x ∈ A
Tactic: refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi