-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem is_simple_module_of_finrank_eq_one {A} [Semiring A] [Module A V] [SMul K A]
    [IsScalarTower K A V] (h : finrank K V = 1) : IsSimpleOrder (Submodule A V)

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
⊢ IsSimpleOrder (Submodule A V)

Tactic:
refine ⟨fun S => or_iff_not_imp_left.2 fun hn => ?_⟩

Result:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬S = ⊥
⊢ S = ⊤

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this✝ : Nontrivial V
S : Submodule A V
hn : ¬restrictScalars K S = restrictScalars K ⊥
this : FiniteDimensional K V
⊢ finrank K V ≤ finrank K ↥(restrictScalars K S)

Tactic:
simpa only [h, finrank_bot] using Submodule.finrank_strictMono (Ne.bot_lt hn)

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬restrictScalars K S = restrictScalars K ⊥
⊢ restrictScalars K S = restrictScalars K ⊤

Tactic:
haveI : FiniteDimensional _ _ := .of_finrank_eq_succ h

Result:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this✝ : Nontrivial V
S : Submodule A V
hn : ¬restrictScalars K S = restrictScalars K ⊥
this : FiniteDimensional K V
⊢ restrictScalars K S = restrictScalars K ⊤

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬S = ⊥
⊢ S = ⊤

Tactic:
rw [← restrictScalars_inj K] at hn ⊢

Result:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬restrictScalars K S = restrictScalars K ⊥
⊢ restrictScalars K S = restrictScalars K ⊤

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
⊢ IsSimpleOrder (Submodule A V)

Tactic:
haveI := nontrivial_of_finrank_eq_succ h

Result:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
⊢ IsSimpleOrder (Submodule A V)

Proof state:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this✝ : Nontrivial V
S : Submodule A V
hn : ¬restrictScalars K S = restrictScalars K ⊥
this : FiniteDimensional K V
⊢ restrictScalars K S = restrictScalars K ⊤

Tactic:
refine eq_top_of_finrank_eq ((Submodule.finrank_le _).antisymm ?_)

Result:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this✝ : Nontrivial V
S : Submodule A V
hn : ¬restrictScalars K S = restrictScalars K ⊥
this : FiniteDimensional K V
⊢ finrank K V ≤ finrank K ↥(restrictScalars K S)