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
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, smul_comm]

Premises used: Set.smul_union, SMulCommClass.smul_comm
-- 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
⊢ uR' • (↑J : Set M) ∪ uR • uR' • (↑J : Set M) ⊆ (↑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)
hRS : uR • S ⊆ 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
-- 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
r : R
i : M
hi : i ∈ A
⊢ r • i ∈ A

Tactic:
AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi

Premises used: AddSubgroup.closure_induction
-- 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
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
r : R
i : M
hi : i ∈ A
x : M
hx : x ∈ S
⊢ r • x ∈ A

Tactic:
AddSubgroup.subset_closure <| hRS <| 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
r : R
i : M
hi : i ∈ A
x : M
hx : x ∈ S
⊢ r • x ∈ A

Tactic:
exact AddSubgroup.subset_closure <| hRS <| 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
r : R
i : M
hi : i ∈ A
x : M
hx : x ∈ S
⊢ r • x ∈ A

Tactic:
case base => exact AddSubgroup.subset_closure <| hRS <| 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
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
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
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
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
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
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
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
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
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
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
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
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
⊢ ∀ (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
-- 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
⊢ r' • i ∈ A

Tactic:
AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi

Premises used: AddSubgroup.closure_induction