-- Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean
theorem Subalgebra.isSimpleOrder_of_finrank_prime (F A) [Field F] [Ring A] [IsDomain A]
    [Algebra F A] (hp : (finrank F A).Prime) : IsSimpleOrder (Subalgebra F A) :=
  { toNontrivial :=
      ⟨⟨⊥, ⊤, fun he =>
          Nat.not_prime_one ((Subalgebra.bot_eq_top_iff_finrank_eq_one.1 he).subst hp)⟩⟩
    eq_bot_or_eq_top := fun K => by
      haveI : FiniteDimensional _ _ := .of_finrank_pos hp.pos
      letI := divisionRingOfFiniteDimensional F K
      refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp ?_ fun h => ?_
      · exact fun h' => Subalgebra.eq_bot_of_finrank_one h'
      · exact
          Algebra.toSubmodule_eq_top.1 (eq_top_of_finrank_eq <| K.finrank_toSubmodule.trans h) }

Proof state:
case refine_2
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
h : finrank F ↥K = finrank F A
⊢ K = ⊤

Tactic:
exact
  Algebra.toSubmodule_eq_top.1 (eq_top_of_finrank_eq <| K.finrank_toSubmodule.trans h)

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this : FiniteDimensional F A
⊢ K = ⊥ ∨ K = ⊤

Tactic:
letI := divisionRingOfFiniteDimensional F K

Result:
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
⊢ K = ⊥ ∨ K = ⊤

Proof state:
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
⊢ K = ⊥ ∨ K = ⊤

Tactic:
haveI : FiniteDimensional _ _ := .of_finrank_pos hp.pos

Result:
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this : FiniteDimensional F A
⊢ K = ⊥ ∨ K = ⊤

Proof state:
case refine_1
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
⊢ finrank F ↥K = 1 → K = ⊥

Tactic:
exact fun h' => Subalgebra.eq_bot_of_finrank_one h'

Result:
no goals

Proof state:
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
⊢ K = ⊥ ∨ K = ⊤

Tactic:
refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp ?_ fun h => ?_

Result:
case refine_1
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
⊢ finrank F ↥K = 1 → K = ⊥

case refine_2
F : Type u_1
A : Type u_2
inst✝³ : Field F
inst✝² : Ring A
inst✝¹ : IsDomain A
inst✝ : Algebra F A
hp : Nat.Prime (finrank F A)
K : Subalgebra F A
this✝ : FiniteDimensional F A
this : DivisionRing ↥K := divisionRingOfFiniteDimensional F ↥K
h : finrank F ↥K = finrank F A
⊢ K = ⊤