awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
M₂ : Type u_5
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
f : M₂ →ₗ[R] N →ₗ[R] P
g : M →ₗ[R] M₂
p : Submodule R M
q : Submodule R N
rw : map₂ (f.flip.compl₂ g).flip p q = map₂ (f ∘ₗ g) p q
⊢ map₂ f (map g p) q = map₂ (f ∘ₗ g) p q

Tactic:
rw [← map₂_flip, map₂_map_right, ← map₂_flip]

Premises used: Submodule.map₂_map_right, Submodule.map₂_flip
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
M₂ : Type u_5
inst_7 : AddCommMonoid M₂
inst_8 : Module R M₂
f : M₂ →ₗ[R] N →ₗ[R] P
g : M →ₗ[R] M₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.flip.compl₂ g).flip p q = map₂ (f ∘ₗ g) p q

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
M₂ : Type u_5
N₂ : Type u_6
inst_7 : AddCommMonoid M₂
inst_8 : AddCommMonoid N₂
inst_9 : Module R M₂
inst_10 : Module R N₂
f : M₂ →ₗ[R] N₂ →ₗ[R] P
g : M →ₗ[R] M₂
h : N →ₗ[R] N₂
p : Submodule R M
q : Submodule R N
rw : map₂ (f.compl₂ h ∘ₗ g) p q = map₂ (f.compl₁₂ g h) p q
⊢ map₂ f (map g p) (map h q) = map₂ (f.compl₁₂ g h) p q

Tactic:
rw [map₂_map_right, map₂_map_left]

Premises used: Submodule.map₂_map_left, Submodule.map₂_map_right
-- Module: Mathlib.Algebra.Module.Submodule.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
M₂ : Type u_5
N₂ : Type u_6
inst_7 : AddCommMonoid M₂
inst_8 : AddCommMonoid N₂
inst_9 : Module R M₂
inst_10 : Module R N₂
f : M₂ →ₗ[R] N₂ →ₗ[R] P
g : M →ₗ[R] M₂
h : N →ₗ[R] N₂
p : Submodule R M
q : Submodule R N
⊢ map₂ (f.compl₂ h ∘ₗ g) p q = map₂ (f.compl₁₂ g h) p q

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
h : Eq.{v + 1} (α := Set M) ((fun (s : Submodule R M) ↦ s.carrier) p) ((fun (s : Submodule R M) ↦ s.carrier) q)
mk :
  ∀ (toAddSubmonoid : AddSubmonoid M)
    (smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier)
    (h :
      Eq.{v + 1} (α := Set M)
        ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' })
        ((fun (s : Submodule R M) ↦ s.carrier) q)),
    { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M } = q
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
q : Submodule R M
toAddSubmonoid : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
h :
  Eq.{v + 1} (α := Set M)
    ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' })
    ((fun (s : Submodule R M) ↦ s.carrier) q)
mk :
  ∀ (toAddSubmonoid_1 : AddSubmonoid M)
    (smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier)
    (h :
      Eq.{v + 1} (α := Set M)
        ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' })
        ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 })),
    { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M } =
      { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 }
⊢ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M } = q

Tactic:
cases q
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
toAddSubmonoid : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
toAddSubmonoid_1 : AddSubmonoid M
smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier
h :
  Eq.{v + 1} (α := Set M)
    ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' })
    ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 })
mk : toAddSubmonoid = toAddSubmonoid_1
⊢ { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' : Submodule R M } =
    { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
toAddSubmonoid : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
toAddSubmonoid_1 : AddSubmonoid M
smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier
h :
  Eq.{v + 1} (α := Set M)
    ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' })
    ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 })
⊢ toAddSubmonoid = toAddSubmonoid_1

Tactic:
SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
toAddSubmonoid : AddSubmonoid M
smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier
toAddSubmonoid_1 : AddSubmonoid M
smul_mem'_1 : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid_1.carrier → c • x ∈ toAddSubmonoid_1.carrier
h :
  Eq.{v + 1} (α := Set M)
    ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' })
    ((fun (s : Submodule R M) ↦ s.carrier) { toAddSubmonoid := toAddSubmonoid_1, smul_mem' := smul_mem'_1 })
⊢ toAddSubmonoid = toAddSubmonoid_1

Tactic:
exact SetLike.coe_injective' h

Premises used: SetLike.coe_injective'
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Submodule R M
⊢ s.carrier = (↑s : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : 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:
simpa [one_smul] using linearComb x hx y hy 1 1

Premises used: one_smul, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
obtain : ∀ (x : M) (hx : x ∈ C), 0 ∈ C
⊢ 0 ∈ C

Tactic:
obtain ⟨x, hx⟩ := nonempty
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
C : Set M
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
x : M
hx : x ∈ C
⊢ 0 ∈ C

Tactic:
simpa [zero_smul, add_zero] using linearComb x hx x hx 0 0

Premises used: zero_smul, add_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : 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:
simpa using linearComb x hx x hx c 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
x : M
⊢ x ∈ p.toAddSubmonoid ↔ x ∈ p

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : AddSubmonoid M
x : M
h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier
⊢ x ∈ { toAddSubmonoid := S, smul_mem' := h : Submodule R M } ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : AddSubmonoid M
h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier
⊢ (↑{ toAddSubmonoid := S, smul_mem' := h : Submodule R M } : Set M) = (↑S : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : ∀ (c : R) {x : M}, x ∈ p.carrier → c • x ∈ p.carrier
⊢ { toAddSubmonoid := p.toAddSubmonoid, smul_mem' := h : Submodule R M } = p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S S' : AddSubmonoid M
h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier
h' : ∀ (c : R) {x : M}, x ∈ S'.carrier → c • x ∈ S'.carrier
⊢ { toAddSubmonoid := S, smul_mem' := h : Submodule R M } ≤ { toAddSubmonoid := S', smul_mem' := h' } ↔ S ≤ S'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
h : ∀ (x : M), x ∈ p ↔ x ∈ q
⊢ p = q

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p_1 q p : Submodule R M
s : Set M
hs : s = (↑p : Set M)
⊢ 0 ∈ s

Tactic:
simp [hs]
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p_1 q p : Submodule R M
s : Set M
hs : s = (↑p : Set M)
⊢ ∀ (c : R) {x : M}, x ∈ s → c • x ∈ s

Tactic:
simpa [hs] using p.smul_mem'

Premises used: Submodule.smul_mem'
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Submodule R M
s : Set M
hs : s = (↑S : Set M)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Injective.{v + 1, v + 1} (α := Submodule R M) toAddSubmonoid

Tactic:
fun p q h => SetLike.ext'_iff.2 (show (p.toAddSubmonoid : Set M) = q from SetLike.ext'_iff.1 h)

Premises used: Iff.mpr, Iff.mp, SetLike.ext'_iff, Function.Injective
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
⊢ p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q

Tactic:
toAddSubmonoid_injective.eq_iff

Premises used: Submodule.toAddSubmonoid_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ (↑p.toAddSubmonoid : Set M) = (↑p : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Injective.{v + 1, v + 1} (α := Submodule R M) toSubMulAction

Tactic:
fun p q h => SetLike.ext'_iff.2 (show (p.toSubMulAction : Set M) = q from SetLike.ext'_iff.1 h)

Premises used: Iff.mpr, Iff.mp, SetLike.ext'_iff, Function.Injective
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
⊢ p.toSubMulAction = q.toSubMulAction ↔ p = q

Tactic:
toSubMulAction_injective.eq_iff

Premises used: Function.Injective.eq_iff, Submodule.toSubMulAction_injective
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ (↑p.toSubMulAction : Set M) = (↑p : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : M
⊢ x ∈ p.carrier ↔ x ∈ (↑p : Set M)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
⊢ 0 ∈ p

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x y : M
h₁ : x ∈ p
h₂ : y ∈ p
⊢ x + y ∈ p

Tactic:
add_mem h₁ h₂

Premises used: AddMemClass.add_mem
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : M
r : R
h : x ∈ p
⊢ r • x ∈ p

Tactic:
p.smul_mem' r h

Premises used: Submodule.smul_mem', Set.Mem
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
S : Type u'
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : M
inst_2 : SMul S R
inst_3 : SMul S M
inst_4 : IsScalarTower S R M
r : S
h : x ∈ p
⊢ r • x ∈ p

Tactic:
p.toSubMulAction.smul_of_tower_mem r h

Premises used: Set.Mem, SubMulAction.smul_of_tower_mem, Submodule.toSubMulAction
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : M
inst_2 : Group G
inst_3 : MulAction G M
inst_4 : SMul G R
inst_5 : IsScalarTower G R M
g : G
⊢ g • x ∈ p ↔ x ∈ p

Tactic:
p.toSubMulAction.smul_mem_iff' g

Premises used: Set.Mem, Submodule.toSubMulAction, SubMulAction.smul_mem_iff'
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst_2 : Invertible r
⊢ r • x ∈ p ↔ x ∈ p

Tactic:
⟨fun h ↦ ?_, p.smul_mem r⟩

Premises used: Iff.intro, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst_2 : Invertible r
refine : ∀ (h : r • x ∈ p), x ∈ p
⊢ r • x ∈ p ↔ x ∈ p

Tactic:
refine ⟨fun h ↦ ?_, p.smul_mem r⟩
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst_2 : Invertible r
h : r • x ∈ p
rw : @Invertible.invOf _ MulOne.toMul MulOne.toOne r _ • r • x ∈ p
⊢ x ∈ p

Tactic:
rw [← invOf_smul_smul r x]

Premises used: invOf_smul_smul
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst_2 : Invertible r
h : r • x ∈ p
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne r _ • r • x ∈ p

Tactic:
p.smul_mem _ h

Premises used: Set.Mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst_2 : Invertible r
h : r • x ∈ p
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne r _ • r • x ∈ p

Tactic:
exact p.smul_mem _ h

Premises used: Submodule.smul_mem
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
hr : IsUnit r
⊢ r • x ∈ p ↔ x ∈ p

Tactic:
let _ : Invertible r := hr.invertible
  smul_mem_iff'' p

Premises used: IsUnit.invertible, Submodule.smul_mem_iff''
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst_2 : SMul S R
inst_3 : SMul S M
inst_4 : IsScalarTower S R M
⊢ IsScalarTower.{u', u, v} S R ↥p

Tactic:
p.toSubMulAction.isScalarTower

Premises used: Set.Mem, Submodule.toSubMulAction, SubMulAction.isScalarTower
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
S' : Type u_1
inst_2 : SMul S R
inst_3 : SMul S M
inst_4 : SMul S' R
inst_5 : SMul S' M
inst_6 : SMul S S'
inst_7 : IsScalarTower S' R M
inst_8 : IsScalarTower S S' M
inst_9 : IsScalarTower S R M
⊢ IsScalarTower.{u', u_1, v} S S' ↥p

Tactic:
p.toSubMulAction.isScalarTower'

Premises used: Set.Mem, Submodule.toSubMulAction, SubMulAction.isScalarTower'
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
⊢ (↑p : Set M).Nonempty

Tactic:
⟨0, p.zero_mem⟩

Premises used: Set.Nonempty, Submodule.zero_mem, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : M
h : x ∈ p
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ p) x h = 0 ↔ x = 0

Tactic:
Subtype.ext_iff

Premises used: Subtype.ext_iff
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : ↥p
⊢ (↑x : M) = 0 ↔ x = 0

Tactic:
(SetLike.coe_eq_coe : (x : M) = (0 : p) ↔ x = 0)

Premises used: SetLike.coe_eq_coe
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x y : ↥p
⊢ (↑(x + y) : M) = (↑x : M) + (↑y : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
⊢ Eq.{v + 1} (α := M) (↑0 : M) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : ↥p
⊢ (↑(r • x) : M) = r • (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
S : Type u'
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
inst_2 : SMul S R
inst_3 : SMul S M
inst_4 : IsScalarTower S R M
r : S
x : ↥p
⊢ (↑(r • x) : M) = r • (↑x : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : M
hx : x ∈ p
⊢ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p : Submodule R M
x : ↥p
⊢ (↑x : M) ∈ p

Tactic:
x.2

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a : S
a₁ : (↑(HSMul.hSMul (β := ↥p) a 0) : M) = (↑0 : M)
⊢ HSMul.hSMul (β := ↥p) a 0 = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a : S
⊢ (↑(HSMul.hSMul (β := ↥p) a 0) : M) = (↑0 : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x_1 y_1 : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a : S
x y : ↥p
a₁ : (↑(a • (x + y)) : M) = (↑(a • x + a • y) : M)
⊢ a • (x + y) = a • x + a • y

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x_1 y_1 : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a : S
x y : ↥p
⊢ (↑(a • (x + y)) : M) = (↑(a • x + a • y) : M)

Tactic:
simp [smul_add]

Premises used: smul_add
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x_1 y : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a b : S
x : ↥p
a₁ : (↑((a + b) • x) : M) = (↑(a • x + b • x) : M)
⊢ (a + b) • x = a • x + b • x

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x_1 y : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a b : S
x : ↥p
⊢ (↑((a + b) • x) : M) = (↑(a • x + b • x) : M)

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a : ↥p
a₁ : (↑(HSMul.hSMul.{u', v, v} (α := S) 0 a) : M) = (↑0 : M)
⊢ HSMul.hSMul.{u', v, v} (α := S) 0 a = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
module_M : Module R M
p q : Submodule R M
r : R
x y : M
inst_2 : Semiring S
inst_3 : SMul S R
inst_4 : Module S M
inst_5 : IsScalarTower S R M
a : ↥p
⊢ (↑(HSMul.hSMul.{u', v, v} (α := S) 0 a) : M) = (↑0 : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p p' : Submodule R M
r : R
x y : M
inst_2 : Module R M
⊢ AddSubgroupClass (Submodule R M) M

Tactic:
{ Submodule.addSubmonoidClass with neg_mem := fun p {_} => p.toSubMulAction.neg_mem }

Premises used: Submodule.addSubmonoidClass, AddSubgroupClass.mk
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
x : M
hx : x ∈ p
⊢ -x ∈ p

Tactic:
neg_mem hx

Premises used: NegMemClass.neg_mem
-- Module: Mathlib.Algebra.Module.Submodule.Defs
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
module_M : Module R M
p : Submodule R M
⊢ (↑p.toAddSubgroup : Set M) = (↑p : Set M)

Tactic:
rfl

Premises used: rfl