mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
b : R
y : M₁
⊢ f (b • y) • x = (RingHom.id R) b • f y • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
⊢ f.smulRight 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : M
⊢ smulRight 0 x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
S : Type u_3
M : Type u_4
M₁ : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R M
inst✝⁶ : Module R M₁
inst✝⁵ : Semiring S
inst✝⁴ : Module R S
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : IsDomain S
f : M₁ →ₗ[R] S
x : M
inst✝ : Module.IsTorsionFree S M
⊢ f.smulRight x = 0 ↔ f = 0 ∨ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
m m' : M
⊢ f.smulRight (m + m') = f.smulRight m + f.smulRight m'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
f : M₂ →ₗ[R] R
c : R
m : M
⊢ f.smulRight (c • m) = (RingHom.id R) c • f.smulRight m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
f f' : M₂ →ₗ[R] R
⊢ { toFun := (f + f').smulRight, map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ } + { toFun := f'.smulRight, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f✝ : M →ₗ[R] M₂
c : R
f : M₂ →ₗ[R] R
⊢ { toFun := (c • f).smulRight, map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) c • { toFun := f.smulRight, map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ Commute LinearMap.id f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ Commute f LinearMap.id

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Basic

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝ : Module.IsTorsionFree R M
⊢ ∀ (r : R) (m : ↥p), ↑(r • m) = r • ↑m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
N : Submodule R M
ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ x ∉ N

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a : PUnit), 0 * a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a : PUnit), a * 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a b c : PUnit), a * (b + c) = a * b + a * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ (a b c : PUnit), (a + b) * c = a * c + b * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ {a : PUnit}, a ≠ 0 → IsLeftRegular a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.PUnit

Goal state before:
pp: ⊢ ∀ {a : PUnit}, a ≠ 0 → IsRightRegular a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
x y : M
hx : x ∈ C
hy : y ∈ C
⊢ x + y ∈ C

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
⊢ 0 ∈ C

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
c : R
x : M
hx : x ∈ C
⊢ c • x ∈ C

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p✝ q p : Submodule R M
s : Set M
hs : s = ↑p
⊢ 0 ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p✝ q p : Submodule R M
s : Set M
hs : s = ↑p
⊢ ∀ (c : R) {x : M}, x ∈ s → c • x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Zero R
⊢ ∀ (a : R), a • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Zero R
⊢ ∀ (m : PUnit), 0 • m = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (x y : R) (b : PUnit), (x * y) • b = x • y • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (b : PUnit), 1 • b = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (a : R), a • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst✝ : Invertible r
⊢ r • x ∈ p ↔ x ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (a : R) (x y : PUnit), a • (x + y) = a • x + a • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (r : R), r • 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Monoid R
⊢ ∀ (r : R) (x y : PUnit), r • (x * y) = r • x * r • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Semiring R
⊢ ∀ (r s : R) (x : PUnit), (r + s) • x = r • x + s • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a : S
⊢ a • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : Semiring R
⊢ ∀ (x : PUnit), 0 • x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : SMul R S
⊢ ∀ (m : PUnit) (n : R) (a : S), m • n • a = n • m • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.PUnit

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : SMul R S
⊢ ∀ (x : PUnit) (y : R) (z : S), (x • y) • z = x • y • z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x✝ y✝ : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a : S
x y : ↥p
⊢ a • (x + y) = a • x + a • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x✝ y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a b : S
x : ↥p
⊢ (a + b) • x = a • x + b • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst✝³ : Semiring S
inst✝² : SMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a : ↥p
⊢ 0 • a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hy : y ∈ p
⊢ x - y ∈ p ↔ x ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
⊢ x - y ∈ p ↔ y ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝² x✝¹ : S
x✝ : ↥t
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : ↥t
⊢ 1 • x✝ = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : S
⊢ x✝ • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝² : S
x✝¹ x✝ : ↥t
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝² x✝¹ : S
x✝ : ↥t
⊢ (x✝² + x✝¹) • x✝ = x✝² • x✝ + x✝¹ • x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
T : Type u_1
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Semiring S
inst✝⁶ : Module R M
inst✝⁵ : SMul S R
inst✝⁴ : Module S M
inst✝³ : IsScalarTower S R M
inst✝² : SetLike T M
inst✝¹ : AddSubmonoidClass T M
inst✝ : SMulMemClass T R M
t : T
x✝ : ↥t
⊢ 0 • x✝ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p q : Submodule R M
⊢ ∀ (c : R) {x : M}, x ∈ {0} → c • x ∈ {0}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
carrier : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier.carrier → c • x ∈ carrier.carrier
⊢ { toAddSubmonoid := carrier, smul_mem' := smul_mem' } = ⊥ ↔ carrier = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q p : Submodule R M
x : M
⊢ x ∈ ⊥ → x ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : ↥⊥
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u_1
M : Type u_2
S : Type u_3
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : SetLike S M
inst✝ : SMulMemClass S R M
N : S
x : M
h : ∀ (a : R), a • x ∈ N
⊢ x ∈ N

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝² : SetLike S M
inst✝¹ : SMul R M
inst✝ : SMulMemClass S R M
r : R
s : S
⊢ r • ↑s ⊆ ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ∀ (x y : ↥p), x = y
x : M
hx : x ∈ p
⊢ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ∀ x ∈ p, x = 0
x✝¹ x✝ : ↥p
x : M
hx : x ∈ p
y : M
hy : y ∈ p
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : SetLike S M
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : SMulMemClass S R M
s : S
r : Rˣ
x : M
hx : x ∈ ↑s
⊢ (fun x ↦ ↑r • x) (r⁻¹ • x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ Subsingleton ↥p ↔ p = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : SetLike S M
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : SMulMemClass S R M
s : S
r : Rˣ
⊢ r • ↑s = ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ Nontrivial ↥p ↔ p ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ ↑p = Set.univ ↔ p = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ p.toAddSubgroup = ⊤ ↔ p = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
carrier : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ carrier.carrier → c • x ∈ carrier.carrier
⊢ { toAddSubmonoid := carrier, smul_mem' := smul_mem' } = ⊤ ↔ carrier = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p q : SubMulAction R M
h : p.carrier = q.carrier
⊢ p = q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ ∀ {a b : M}, a ∈ ⋂ s ∈ S, ↑s → b ∈ ⋂ s ∈ S, ↑s → a + b ∈ ⋂ s ∈ S, ↑s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
⊢ ∀ (c : R) {x : M}, x ∈ ∅ → c • x ∈ ∅

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
⊢ ∀ (c : R) {x : M}, x ∈ Set.univ → c • x ∈ Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ 0 ∈ ⋂ s ∈ S, ↑s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
s t : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ ↑s ∪ ↑t → c • x ∈ ↑s ∪ ↑t

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
s t : SubMulAction R M
⊢ ∀ (c : R) {x : M}, x ∈ ↑s ∩ ↑t → c • x ∈ ↑s ∩ ↑t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S✝ M
inst✝¹ : SMul S✝ R
inst✝ : IsScalarTower S✝ R M
p q : Submodule R M
S : Set (Submodule R M)
⊢ ∀ (c : R) {x : M}, x ∈ ⋂ s ∈ S, ↑s → c • x ∈ ⋂ s ∈ S, ↑s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S✝ : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
S : Set (SubMulAction R M)
⊢ ∀ (c : R) {x : M}, x ∈ ⋃ s ∈ S, ↑s → c • x ∈ ⋃ s ∈ S, ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q✝ p q : Submodule R M
⊢ ∀ {a b : M}, a ∈ ↑p ∩ ↑q → b ∈ ↑p ∩ ↑q → a + b ∈ ↑p ∩ ↑q

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q✝ p q : Submodule R M
⊢ 0 ∈ ↑p ∩ ↑q

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S✝ : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
S : Set (SubMulAction R M)
⊢ ∀ (c : R) {x : M}, x ∈ ⋂ s ∈ S, ↑s → c • x ∈ ⋂ s ∈ S, ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q✝ p q : Submodule R M
⊢ ∀ (c : R) {x : M}, x ∈ ↑p ∩ ↑q → c • x ∈ ↑p ∩ ↑q

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝ : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ x ∈ ⨆ i, p i ↔ ∃ i, x ∈ p i

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝ : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
T : Type u''
R : Type u
M : Type v
inst✝ : SMul R M
p : SubMulAction R M
r : R
x : M
⊢ ∀ (m : R) (x : ↥p), ↑(m • x) = id m • ↑x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u'
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
p : SubMulAction R M
s : S
x : M
h : x ∈ p
⊢ s • x ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
⊢ ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)

Tactic:
by

Goal state after: