awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : ∀ (x : M) (hx : x ∈ S), r • x ∈ A
⊢ r • i ∈ A
have refine₁ : HSMul.hSMul (β := M) r 0 ∈ A
Tactic: refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
-- 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
refine : ∀ (x : M) (hx : x ∈ S), r • x ∈ A
refine₁ : HSMul.hSMul (β := M) r 0 ∈ A
⊢ r • i ∈ A
have refine₂ : ∀ (x y : M),
  Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x →
    Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) y → ∀ (hx : r • x ∈ A) (hy : r • y ∈ A), r • (x + y) ∈ A
Tactic: refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
-- 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
refine : ∀ (x : M) (hx : x ∈ S), r • x ∈ A
refine₁ : HSMul.hSMul (β := M) r 0 ∈ A
refine₂ :
  ∀ (x y : M),
    Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x →
      Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) y →
        ∀ (hx : r • x ∈ A) (hy : r • y ∈ A), r • (x + y) ∈ A
⊢ r • i ∈ A
have refine₃ : ∀ (x : M), Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x → ∀ (hx : r • x ∈ A), r • -x ∈ A
Tactic: refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
-- 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
⊢ HSMul.hSMul (β := M) r 0 ∈ A
have simp_rw : 0 ∈ A
Tactic: simp_rw [smul_zero]
-- 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
x y : M
h : Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x
h_1 : Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) y
hx : r • x ∈ A
hy : r • y ∈ A
⊢ r • (x + y) ∈ A
have simp_rw : r • x + r • y ∈ A
Tactic: simp_rw [smul_add]
-- 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
x : M
h : Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x
hx : r • x ∈ A
⊢ r • -x ∈ A
have simp_rw : -(r • x) ∈ A
Tactic: simp_rw [smul_neg]
-- 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
x : M
h : Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x
hx : r • x ∈ A
⊢ r • -x ∈ A
have case : -(r • x) ∈ A
Tactic: case neg => simp_rw [smul_neg]; exact neg_mem hx
-- 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
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure 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 hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
Tactic: have hRA : ∀ r : R, ∀ i ∈ A, r • i ∈ A := fun r i hi ↦ by
    refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
    case base => exact AddSubgroup.subset_closure <| hRS <| Set.smul_mem_smul trivial hx
    case zero => simp_rw [smul_zero]; exact zero_mem _
    case add => simp_rw [smul_add]; exact add_mem hx hy
    case neg => simp_rw [smul_neg]; exact neg_mem hx
-- 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
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
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
-- 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
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
refine : ∀ (x : M) (hx : x ∈ S), r' • x ∈ A
⊢ r' • i ∈ A
have refine₁ : HSMul.hSMul (β := M) r' 0 ∈ A
Tactic: refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
-- 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
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
refine : ∀ (x : M) (hx : x ∈ S), r' • x ∈ A
refine₁ : HSMul.hSMul (β := M) r' 0 ∈ A
⊢ r' • i ∈ A
have refine₂ : ∀ (x y : M),
  Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x →
    Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) y →
      ∀ (hx : r' • x ∈ A) (hy : r' • y ∈ A), r' • (x + y) ∈ A
Tactic: refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
-- 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
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
refine : ∀ (x : M) (hx : x ∈ S), r' • x ∈ A
refine₁ : HSMul.hSMul (β := M) r' 0 ∈ A
refine₂ :
  ∀ (x y : M),
    Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x →
      Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) y →
        ∀ (hx : r' • x ∈ A) (hy : r' • y ∈ A), r' • (x + y) ∈ A
⊢ r' • i ∈ A
have refine₃ : ∀ (x : M), Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x → ∀ (hx : r' • x ∈ A), r' • -x ∈ A
Tactic: refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
-- 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
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
⊢ HSMul.hSMul (β := M) r' 0 ∈ A
have simp_rw : 0 ∈ A
Tactic: simp_rw [smul_zero]
-- 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
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
x y : M
h : Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x
h_1 : Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) y
hx : r' • x ∈ A
hy : r' • y ∈ A
⊢ r' • (x + y) ∈ A
have simp_rw : r' • x + r' • y ∈ A
Tactic: simp_rw [smul_add]
-- 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
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
x : M
h : Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x
hx : r' • x ∈ A
⊢ r' • -x ∈ A
have simp_rw : -(r' • x) ∈ A
Tactic: simp_rw [smul_neg]
-- 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
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
r' : R'
i : M
hi : i ∈ A
x : M
h : Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x
hx : r' • x ∈ A
⊢ r' • -x ∈ A
have case : -(r' • x) ∈ A
Tactic: case neg => simp_rw [smul_neg]; exact neg_mem hx
-- 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
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
⊢ ∃ (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'A : ∀ (r' : R'), ∀ i ∈ A, r' • i ∈ A
Tactic: have hR'A : ∀ r' : R', ∀ i ∈ A, r' • i ∈ A := fun r' i hi ↦ by
    refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
    case base => exact AddSubgroup.subset_closure <| hR'S <| Set.smul_mem_smul trivial hx
    case zero => simp_rw [smul_zero]; exact zero_mem _
    case add => simp_rw [smul_add]; exact add_mem hx hy
    case neg => simp_rw [smul_neg]; exact neg_mem hx
-- 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
hR'S : uR' • S ⊆ S
A : AddSubgroup M := AddSubgroup.closure S
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
hR'A : ∀ (r' : R'), ∀ i ∈ A, r' • i ∈ A
⊢ ∃ (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 A_sub_I : (↑A : Set M) ⊆ (↑I : Set M)
Tactic: have A_sub_I : (A : Set M) ⊆ I := I.toAddSubgroup.closure_le.mpr S_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
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
hRA : ∀ (r : R), ∀ i ∈ A, r • i ∈ A
hR'A : ∀ (r' : R'), ∀ i ∈ A, r' • i ∈ A
A_sub_I : (↑A : 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 J_sub_A : (↑J : Set M) ⊆ (↑A : Set M)
Tactic: have J_sub_A : (J : Set M) ⊆ A := subset_trans subset_union_left AddSubgroup.subset_closure
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (goal)
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
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : Tendsto m f (𝓝 0)
⊢ Tendsto (a • m) f (𝓝 0)
have rw : ∀ (ha : ∀ (i : Submodule R M), Membership.mem (γ := Filter M) (𝓝 0) (↑i : Set M) → ∀ᶠ (x : ι) in f, m x ∈ (↑i : Set M))
  (i : Submodule R M), Membership.mem (γ := Filter M) (𝓝 0) (↑i : Set M) → ∀ᶠ (x : ι) in f, (a • m) x ∈ (↑i : Set M)
Tactic: rw [hasBasis_submodule R |>.tendsto_right_iff] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (goal)
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
ι : Type u_4
f : Filter ι
a : ι → R
m : ι → M
ha : ∀ (i : Submodule R M), Membership.mem (γ := Filter M) (𝓝 0) (↑i : Set M) → ∀ᶠ (x : ι) in f, m x ∈ (↑i : Set M)
I : Submodule R M
hI : Membership.mem (γ := Filter M) (𝓝 0) (↑I : Set M)
⊢ ∀ᶠ (x : ι) in f, (a • m) x ∈ (↑I : Set M)
have h : ∀ (i : ι) (ai_mem : m i ∈ (↑I : Set M)), (a • m) i ∈ (↑I : Set M)
Tactic: filter_upwards [ha I hI] with i ai_mem