R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ⊥ ≠ ⊤
⊢ ∃ y, 0 ≠ y
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
⊢ ∃ y, 0 ≠ y
have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ¬∃ y, 0 ≠ y
⊢ ⊥ = ⊤
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ⊥ ≠ ⊤
⊢ ∃ y, 0 ≠ y
contrapose! h
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h✝ : ¬∃ y, 0 ≠ y
h : ∀ (y : M), 0 = y
⊢ ⊥ = ⊤
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ¬∃ y, 0 ≠ y
⊢ ⊥ = ⊤
have h : ∀ (y : M), 0 = y := by
  intro y
  have em := Classical.em (0 = y)
  match em with
  | .inl h' => exact h'
  | .inr h' => apply False.elim <| h ⟨y,h'⟩
case h
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h✝ : ¬∃ y, 0 ≠ y
h : ∀ (y : M), 0 = y
x : M
⊢ x ∈ ⊥ ↔ x ∈ ⊤
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h✝ : ¬∃ y, 0 ≠ y
h : ∀ (y : M), 0 = y
⊢ ⊥ = ⊤
ext x
no goals
case h
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h✝ : ¬∃ y, 0 ≠ y
h : ∀ (y : M), 0 = y
x : M
⊢ x ∈ ⊥ ↔ x ∈ ⊤
simp [Submodule.mem_bot, Submodule.mem_top, h x]
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ¬∃ y, 0 ≠ y
y : M
⊢ 0 = y
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ¬∃ y, 0 ≠ y
⊢ ∀ (y : M), 0 = y
intro y
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ¬∃ y, 0 ≠ y
y : M
em : 0 = y ∨ ¬0 = y
⊢ 0 = y
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ¬∃ y, 0 ≠ y
y : M
⊢ 0 = y
have em := Classical.em (0 = y)
no goals
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ¬∃ y, 0 ≠ y
y : M
em : 0 = y ∨ ¬0 = y
⊢ 0 = y
match em with
| .inl h' => exact h'
| .inr h' => apply False.elim <| h ⟨y,h'⟩
no goals
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ¬∃ y, 0 ≠ y
y : M
em : 0 = y ∨ ¬0 = y
h' : 0 = y
⊢ 0 = y
exact h'
no goals
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ¬∃ y, 0 ≠ y
y : M
em : 0 = y ∨ ¬0 = y
h' : ¬0 = y
⊢ 0 = y
apply False.elim <| h ⟨y,h'⟩