[GOAL]
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
src✝ : AddSubmonoid M := ⊥
⊢ ∀ (c : R) {x : M},
    x ∈
        {
              toAddSubsemigroup :=
                { carrier := {0},
                  add_mem' := (_ : ∀ {a b : M}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier) },
              zero_mem' := (_ : 0 ∈ src✝.carrier) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := {0},
                  add_mem' := (_ : ∀ {a b : M}, a ∈ src✝.carrier → b ∈ src✝.carrier → a + b ∈ src✝.carrier) },
              zero_mem' := (_ : 0 ∈ src✝.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simp
[GOAL]
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
⊢ restrictScalars S p = ⊥ ↔ p = ⊥
[PROOFSTEP]
simp [SetLike.ext_iff]
[GOAL]
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
[PROOFSTEP]
simp (config := { contextual := true }) [zero_mem]
[GOAL]
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
x y : { x // x ∈ ⊥ }
⊢ x = y
[PROOFSTEP]
rcases x with ⟨x, xm⟩
[GOAL]
case mk
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
y : { x // x ∈ ⊥ }
x : M
xm : x ∈ ⊥
⊢ { val := x, property := xm } = y
[PROOFSTEP]
rcases y with ⟨y, ym⟩
[GOAL]
case mk.mk
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
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ { val := x, property := xm } = { val := y, property := ym }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_val
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
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ x = y
[PROOFSTEP]
rw [(Submodule.eq_bot_iff _).mp rfl x xm]
[GOAL]
case mk.mk.e_val
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
x : M
xm : x ∈ ⊥
y : M
ym : y ∈ ⊥
⊢ 0 = y
[PROOFSTEP]
rw [(Submodule.eq_bot_iff _).mp rfl y ym]
[GOAL]
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
⊢ p ≠ ⊥ ↔ ∃ x, x ∈ p ∧ x ≠ 0
[PROOFSTEP]
simp only [ne_eq, p.eq_bot_iff, not_forall, exists_prop]
[GOAL]
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
inst✝ : Subsingleton { x // x ∈ p }
⊢ p = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
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
inst✝ : Subsingleton { x // x ∈ p }
⊢ p ≤ ⊥
[PROOFSTEP]
intro v hv
[GOAL]
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
inst✝ : Subsingleton { x // x ∈ p }
v : M
hv : v ∈ p
⊢ v ∈ ⊥
[PROOFSTEP]
exact congr_arg Subtype.val (Subsingleton.elim (⟨v, hv⟩ : p) 0)
[GOAL]
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
⊢ restrictScalars S p = ⊤ ↔ p = ⊤
[PROOFSTEP]
simp [SetLike.ext_iff]
[GOAL]
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 : Submodule R M) (_ : s ∈ S), ↑s →
      b ∈ ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s → a + b ∈ ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s
[PROOFSTEP]
simp (config := { contextual := true }) [add_mem]
[GOAL]
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 ∈
    { carrier := ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s,
        add_mem' :=
          (_ :
            ∀ (a a_1 : M),
              a ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i →
                a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i → a + a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i) }.carrier
[PROOFSTEP]
simp [zero_mem]
[GOAL]
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 ∈
        {
              toAddSubsemigroup :=
                { carrier := ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s,
                  add_mem' :=
                    (_ :
                      ∀ (a a_1 : M),
                        a ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i →
                          a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i →
                            a + a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i) },
              zero_mem' := (_ : 0 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := ⋂ (s : Submodule R M) (_ : s ∈ S), ↑s,
                  add_mem' :=
                    (_ :
                      ∀ (a a_1 : M),
                        a ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i →
                          a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i →
                            a + a_1 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i) },
              zero_mem' := (_ : 0 ∈ ⋂ (i : Submodule R M) (_ : i ∈ S), ↑i) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simp (config := { contextual := true }) [smul_mem]
[GOAL]
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
[PROOFSTEP]
simp (config := { contextual := true }) [add_mem]
[GOAL]
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 ∈ { carrier := ↑p ∩ ↑q, add_mem' := (_ : ∀ (a a_1 : M), a ∈ ↑p ∩ ↑q → a_1 ∈ ↑p ∩ ↑q → a + a_1 ∈ ↑p ∩ ↑q) }.carrier
[PROOFSTEP]
simp [zero_mem]
[GOAL]
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 ∈
        {
              toAddSubsemigroup :=
                { carrier := ↑p ∩ ↑q,
                  add_mem' := (_ : ∀ (a a_1 : M), a ∈ ↑p ∩ ↑q → a_1 ∈ ↑p ∩ ↑q → a + a_1 ∈ ↑p ∩ ↑q) },
              zero_mem' := (_ : 0 ∈ ↑p ∩ ↑q) }.toAddSubsemigroup.carrier →
      c • x ∈
        {
              toAddSubsemigroup :=
                { carrier := ↑p ∩ ↑q,
                  add_mem' := (_ : ∀ (a a_1 : M), a ∈ ↑p ∩ ↑q → a_1 ∈ ↑p ∩ ↑q → a + a_1 ∈ ↑p ∩ ↑q) },
              zero_mem' := (_ : 0 ∈ ↑p ∩ ↑q) }.toAddSubsemigroup.carrier
[PROOFSTEP]
simp (config := { contextual := true }) [smul_mem]
[GOAL]
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
src✝¹ : OrderTop (Submodule R M) := inferInstance
src✝ : OrderBot (Submodule R M) := inferInstance
x✝² : Set (Submodule R M)
x✝¹ : Submodule R M
hs : x✝¹ ∈ x✝²
x✝ : Submodule R M
hq : x✝ ∈ fun x => ∀ (b : Submodule R M), b ∈ x✝² → b ≤ x
⊢ x✝¹ ≤ x✝
[PROOFSTEP]
exact hq _ hs
[GOAL]
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
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
⊢ ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
[PROOFSTEP]
letI := Classical.decEq ι
[GOAL]
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
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
[PROOFSTEP]
refine' s.induction_on _ fun i s _ ih ↦ _
[GOAL]
case refine'_1
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
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
⊢ ↑(Finset.inf ∅ p) = ⋂ (i : ι) (_ : i ∈ ∅), ↑(p i)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
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
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
ih : ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
⊢ ↑(Finset.inf (insert i s) p) = ⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), ↑(p i_1)
[PROOFSTEP]
rw [Finset.inf_insert, inf_coe, ih]
[GOAL]
case refine'_2
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
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
ih : ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
⊢ ↑(p i) ∩ ⋂ (i : ι) (_ : i ∈ s), ↑(p i) = ⋂ (i_1 : ι) (_ : i_1 ∈ insert i s), ↑(p i_1)
[PROOFSTEP]
simp
[GOAL]
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
ι : Sort u_4
p : ι → Submodule R M
⊢ ↑(⨅ (i : ι), p i) = ⋂ (i : ι), ↑(p i)
[PROOFSTEP]
rw [iInf, sInf_coe]
[GOAL]
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
ι : Sort u_4
p : ι → Submodule R M
⊢ ⋂ (p_1 : Submodule R M) (_ : p_1 ∈ Set.range fun i => p i), ↑p_1 = ⋂ (i : ι), ↑(p i)
[PROOFSTEP]
simp only [Set.mem_range, Set.iInter_exists, Set.iInter_iInter_eq']
[GOAL]
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
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ x ∈ ⨅ (i : ι), p i ↔ ∀ (i : ι), x ∈ p i
[PROOFSTEP]
rw [← SetLike.mem_coe, iInf_coe, Set.mem_iInter]
[GOAL]
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
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ (∀ (i : ι), x ∈ ↑(p i)) ↔ ∀ (i : ι), x ∈ p i
[PROOFSTEP]
rfl
[GOAL]
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
ι : Type u_4
s : Finset ι
p : ι → Submodule R M
x : M
⊢ x ∈ Finset.inf s p ↔ ∀ (i : ι), i ∈ s → x ∈ p i
[PROOFSTEP]
simp only [← SetLike.mem_coe, finset_inf_coe, Set.mem_iInter]
[GOAL]
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 S T : Submodule R M
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
have : S ≤ S ⊔ T := le_sup_left
[GOAL]
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 S T : Submodule R M
this : S ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
rw [LE.le] at this 
[GOAL]
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 S T : Submodule R M
this : Preorder.toLE.1 S (S ⊔ T)
⊢ ∀ {x : M}, x ∈ S → x ∈ S ⊔ T
[PROOFSTEP]
exact this
[GOAL]
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 S T : Submodule R M
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
have : T ≤ S ⊔ T := le_sup_right
[GOAL]
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 S T : Submodule R M
this : T ≤ S ⊔ T
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
rw [LE.le] at this 
[GOAL]
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 S T : Submodule R M
this : Preorder.toLE.1 T (S ⊔ T)
⊢ ∀ {x : M}, x ∈ T → x ∈ S ⊔ T
[PROOFSTEP]
exact this
[GOAL]
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
R' : Type u_4
M' : Type u_5
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s - t ∈ S ⊔ T
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
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
R' : Type u_4
M' : Type u_5
inst✝² : Ring R'
inst✝¹ : AddCommGroup M'
inst✝ : Module R' M'
S T : Submodule R' M'
s t : M'
hs : s ∈ S
ht : t ∈ T
⊢ s + -t ∈ S ⊔ T
[PROOFSTEP]
exact add_mem_sup hs (neg_mem ht)
[GOAL]
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)
s : Submodule R M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
have := le_sSup hs
[GOAL]
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)
s : Submodule R M
hs : s ∈ S
this : s ≤ sSup S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
rw [LE.le] at this 
[GOAL]
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)
s : Submodule R M
hs : s ∈ S
this : Preorder.toLE.1 s (sSup S)
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S
[PROOFSTEP]
exact this
[GOAL]
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 p' : Submodule R M
⊢ (∀ (x : M), x ∈ p ∧ x ∈ p' → x ∈ {0}) ↔ ∀ (x : M), x ∈ p → x ∈ p' → x = 0
[PROOFSTEP]
simp
[GOAL]
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
hpq : Disjoint p q
a : { x // x ∈ p }
ha : ↑a ∈ q
⊢ a = 0
[PROOFSTEP]
exact_mod_cast disjoint_def.mp hpq a (coe_mem a) ha
