awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
refine₃ : ∀ (x : M), Membership.mem (γ := AddSubgroup M) (AddSubgroup.closure S) x → ∀ (hx : r' • x ∈ A), r' • -x ∈ A
⊢ r' • i ∈ A

Tactic:
refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) 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)
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
hx : x ∈ S
⊢ r' • x ∈ A

Tactic:
AddSubgroup.subset_closure <| hR'S <| Set.smul_mem_smul trivial hx

Premises used: trivial, Set.Mem, Set.smul_mem_smul, AddSubgroup.subset_closure
-- 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)
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
hx : x ∈ S
⊢ r' • x ∈ A

Tactic:
exact AddSubgroup.subset_closure <| hR'S <| Set.smul_mem_smul trivial hx

Premises used: AddSubgroup.subset_closure
-- 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)
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
hx : x ∈ S
⊢ r' • x ∈ A

Tactic:
case base => exact AddSubgroup.subset_closure <| hR'S <| Set.smul_mem_smul trivial hx

Premises used: AddSubgroup.subset_closure
-- 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)
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
simp_rw : 0 ∈ A
⊢ HSMul.hSMul (β := M) r' 0 ∈ A

Tactic:
simp_rw [smul_zero]

Premises used: smul_zero
-- 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)
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
⊢ 0 ∈ A

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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)
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
⊢ 0 ∈ A

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- 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)
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

Tactic:
case zero => simp_rw [smul_zero]; exact zero_mem _

Premises used: smul_zero, ZeroMemClass.zero_mem
-- 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)
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
simp_rw : r' • x + r' • y ∈ A
⊢ r' • (x + y) ∈ A

Tactic:
simp_rw [smul_add]

Premises used: smul_add
-- 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)
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 + r' • y ∈ A

Tactic:
add_mem hx hy

Premises used: AddMemClass.add_mem
-- 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)
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 + r' • y ∈ A

Tactic:
exact add_mem hx hy

Premises used: AddMemClass.add_mem
-- 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)
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

Tactic:
case add => simp_rw [smul_add]; exact add_mem hx hy

Premises used: AddMemClass.add_mem, smul_add
-- 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)
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
simp_rw : -(r' • x) ∈ A
⊢ r' • -x ∈ A

Tactic:
simp_rw [smul_neg]

Premises used: smul_neg
-- 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)
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

Tactic:
neg_mem hx

Premises used: NegMemClass.neg_mem
-- 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)
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

Tactic:
exact neg_mem hx

Premises used: NegMemClass.neg_mem
-- 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)
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
case case₁ : -(r' • x) ∈ A
⊢ r' • -x ∈ A

Tactic:
case neg => simp_rw [smul_neg]; exact neg_mem hx

Premises used: smul_neg, NegMemClass.neg_mem
-- 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)
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 ∈ 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
-- 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)
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 : Set M) ⊆ (↑I : Set M)

Tactic:
have A_sub_I : (A : Set M) ⊆ I := I.toAddSubgroup.closure_le.mpr S_sub_I
-- 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)
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)
⊢ (↑J : Set M) ⊆ (↑A : Set M)

Tactic:
have J_sub_A : (J : Set M) ⊆ A := subset_trans subset_union_left AddSubgroup.subset_closure
-- 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)
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)
J_sub_A : (↑J : Set M) ⊆ (↑A : 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:
⟨A, ⟨mem_of_superset hJ J_sub_A, hRA, hR'A⟩, A_sub_I⟩

Premises used: And.intro, Exists.intro, Filter.mem_of_superset
-- 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)
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)
J_sub_A : (↑J : Set M) ⊆ (↑A : 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:
exact ⟨A, ⟨mem_of_superset hJ J_sub_A, hRA, hR'A⟩, A_sub_I⟩
-- 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 : ContinuousAdd M
inst_8 : IsLinearTopology R M
inst_9 : IsLinearTopology R' M
⊢ HasBasis (α := M) (𝓝 0)
    (fun (I : AddSubgroup M) ↦
      IsOpen[inst_6] (↑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:
hasBasis_subbimodule R R' |>.congr
    (fun N ↦ and_congr_left' ⟨N.isOpen_of_mem_nhds, fun hN ↦ hN.mem_nhds (zero_mem N)⟩)
    (fun _ _ ↦ rfl)

Premises used: AddSubgroup.isOpen_of_mem_nhds, IsOpen.mem_nhds, and_congr_left', Iff.intro, ZeroMemClass.zero_mem, IsLinearTopology.hasBasis_subbimodule, Filter.HasBasis.congr, rfl