[GOAL]
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
[PROOFSTEP]
cases p
[GOAL]
case mk
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
q : Submodule R M
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h : (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ } = (fun s => s.carrier) q
⊢ { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ } = q
[PROOFSTEP]
cases q
[GOAL]
case mk.mk
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
toAddSubmonoid✝¹ : AddSubmonoid M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
⊢ { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toAddSubmonoid
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
toAddSubmonoid✝¹ : AddSubmonoid M
smul_mem'✝¹ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝¹.carrier → c • x ∈ toAddSubmonoid✝¹.carrier
toAddSubmonoid✝ : AddSubmonoid M
smul_mem'✝ : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid✝.carrier → c • x ∈ toAddSubmonoid✝.carrier
h :
  (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝¹, smul_mem' := smul_mem'✝¹ } =
    (fun s => s.carrier) { toAddSubmonoid := toAddSubmonoid✝, smul_mem' := smul_mem'✝ }
⊢ toAddSubmonoid✝¹ = toAddSubmonoid✝
[PROOFSTEP]
exact SetLike.coe_injective' h
[GOAL]
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 ∈ { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier
[PROOFSTEP]
simpa [hs] using p.zero_mem'
[GOAL]
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 ∈
        { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := s,
                        add_mem' :=
                          (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier →
      c • x ∈
        { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) },
              zero_mem' :=
                (_ :
                  0 ∈
                    { carrier := s,
                        add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simpa [hs] using p.smul_mem'
[GOAL]
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
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : S
⊢ a • 0 = 0
[PROOFSTEP]
ext
[GOAL]
case a
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
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : S
⊢ ↑(a • 0) = ↑0
[PROOFSTEP]
simp
[GOAL]
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
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : S
x y : { x // x ∈ p }
⊢ a • (x + y) = a • x + a • y
[PROOFSTEP]
ext
[GOAL]
case a
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
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : S
x y : { x // x ∈ p }
⊢ ↑(a • (x + y)) = ↑(a • x + a • y)
[PROOFSTEP]
simp [smul_add]
[GOAL]
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
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a b : S
x : { x // x ∈ p }
⊢ (a + b) • x = a • x + b • x
[PROOFSTEP]
ext
[GOAL]
case a
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
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a b : S
x : { x // x ∈ p }
⊢ ↑((a + b) • x) = ↑(a • x + b • x)
[PROOFSTEP]
simp [add_smul]
[GOAL]
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
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : { x // x ∈ p }
⊢ 0 • a = 0
[PROOFSTEP]
ext
[GOAL]
case a
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
src✝ : MulAction S { x // x ∈ p } :=
  let_fun this := SubMulAction.mulAction' (toSubMulAction p);
  this
a : { x // x ∈ p }
⊢ ↑(0 • a) = ↑0
[PROOFSTEP]
simp
[GOAL]
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
⊢ { x // x ∈ p } →ₗ[R] M
[PROOFSTEP]
refine' { toFun := Subtype.val .. }
[GOAL]
case refine'_1
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
⊢ ∀ (x y : { x // x ∈ p }), ↑(x + y) = ↑x + ↑y
[PROOFSTEP]
simp [coe_smul]
[GOAL]
case refine'_2
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
⊢ ∀ (r : R) (x : { x // x ∈ p }),
    AddHom.toFun { toFun := Subtype.val, map_add' := (_ : ∀ (a a_1 : { x // x ∈ p }), ↑a + ↑a_1 = ↑a + ↑a_1) } (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun { toFun := Subtype.val, map_add' := (_ : ∀ (a a_1 : { x // x ∈ p }), ↑a + ↑a_1 = ↑a + ↑a_1) } x
[PROOFSTEP]
simp [coe_smul]
[GOAL]
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✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p : Submodule R M
⊢ Module R { x // x ∈ p }
[PROOFSTEP]
infer_instance
[GOAL]
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✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
⊢ ∀ {a b : Submodule R M},
    ↑{ toFun := restrictScalars S, inj' := (_ : Injective (restrictScalars S)) } a ≤
        ↑{ toFun := restrictScalars S, inj' := (_ : Injective (restrictScalars S)) } b ↔
      a ≤ b
[PROOFSTEP]
simp [SetLike.le_def]
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p p' : Submodule R M
r : R
x y : M
hy : y ∈ p
⊢ x - y ∈ p ↔ x ∈ p
[PROOFSTEP]
rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p p' : Submodule R M
r : R
x y : M
hx : x ∈ p
⊢ x - y ∈ p ↔ y ∈ p
[PROOFSTEP]
rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : ι → M
x : M
N : Submodule R M
ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0
⊢ ¬x ∈ N
[PROOFSTEP]
intro hx
[GOAL]
G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b : ι → M
x : M
N : Submodule R M
ortho : ∀ (c : R) (y : M), y ∈ N → c • x + y = 0 → c = 0
hx : x ∈ N
⊢ False
[PROOFSTEP]
simpa using ortho (-1) x hx
