-- Mathlib/Topology/Algebra/Module/Simple.lean
theorem LinearMap.isClosed_or_dense_ker (l : M →ₗ[R] N) :
    IsClosed (LinearMap.ker l : Set M) ∨ Dense (LinearMap.ker l : Set M)

Proof state:
case inl
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
⊢ IsClosed ↑(ker l) ∨ Dense ↑(ker l)

Tactic:
exact l.ker.isClosed_or_dense_of_isCoatom (LinearMap.isCoatom_ker_of_surjective hl)

Result:
no goals

Proof state:
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
l : M →ₗ[R] N
⊢ IsClosed ↑(ker l) ∨ Dense ↑(ker l)

Tactic:
rcases l.surjective_or_eq_zero with (hl | rfl)

Result:
case inl
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
⊢ IsClosed ↑(ker l) ∨ Dense ↑(ker l)

case inr
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑(ker 0) ∨ Dense ↑(ker 0)

Proof state:
case inr.h
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑⊤

Tactic:
exact isClosed_univ

Result:
no goals

Proof state:
case inr
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑(ker 0) ∨ Dense ↑(ker 0)

Tactic:
rw [LinearMap.ker_zero]

Result:
case inr
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑⊤ ∨ Dense ↑⊤

Proof state:
case inr
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑⊤ ∨ Dense ↑⊤

Tactic:
left

Result:
case inr.h
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑⊤