case mk
R : Type u_2
S : Type ?u.34876
M : Type u_1
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
R : Type u_2
S : Type ?u.34876
M : Type u_1
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
rcases x with ⟨x, xm⟩
case mk.mk
R : Type u_2
S : Type ?u.34876
M : Type u_1
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 }
case mk
R : Type u_2
S : Type ?u.34876
M : Type u_1
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
rcases y with ⟨y, ym⟩
case mk.mk.e_val
R : Type u_2
S : Type ?u.34876
M : Type u_1
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
case mk.mk
R : Type u_2
S : Type ?u.34876
M : Type u_1
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 }
congr
case mk.mk.e_val
R : Type u_2
S : Type ?u.34876
M : Type u_1
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
case mk.mk.e_val
R : Type u_2
S : Type ?u.34876
M : Type u_1
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
rw [(Submodule.eq_bot_iff _).mp rfl x xm]
no goals
case mk.mk.e_val
R : Type u_2
S : Type ?u.34876
M : Type u_1
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
rw [(Submodule.eq_bot_iff _).mp rfl y ym]