-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem Subalgebra.isSimpleOrder_of_finrank (hr : finrank F E = 2) :
    IsSimpleOrder (Subalgebra F E) :=
  let i := nontrivial_of_finrank_pos (zero_lt_two.trans_eq hr.symm)
  { toNontrivial :=
      ⟨⟨⊥, ⊤, fun h => by cases hr.symm.trans (Subalgebra.bot_eq_top_iff_finrank_eq_one.1 h)⟩⟩
    eq_bot_or_eq_top

Proof state:
case «2».h
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = finrank F E
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊤

Tactic:
rw [← Algebra.toSubmodule_eq_top]

Result:
case «2».h
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = finrank F E
this✝ : 2 ≤ 2
this : 0 < 2
⊢ toSubmodule S = ⊤

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
⊢ S = ⊥ ∨ S = ⊤

Tactic:
haveI : FiniteDimensional F E := .of_finrank_eq_succ hr

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this : FiniteDimensional F E
⊢ S = ⊥ ∨ S = ⊤

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝ : FiniteDimensional F E
this : FiniteDimensional F ↥S
⊢ S = ⊥ ∨ S = ⊤

Tactic:
have : finrank F S ≤ 2 := hr ▸ S.toSubmodule.finrank_le

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝¹ : FiniteDimensional F E
this✝ : FiniteDimensional F ↥S
this : finrank F ↥S ≤ 2
⊢ S = ⊥ ∨ S = ⊤

Proof state:
case «2».h
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = 2
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊤

Tactic:
rw [← hr] at h

Result:
case «2».h
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = finrank F E
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊤

Proof state:
case «2»
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = 2
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊥ ∨ S = ⊤

Tactic:
right

Result:
case «2».h
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = 2
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊤

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this : FiniteDimensional F E
⊢ S = ⊥ ∨ S = ⊤

Tactic:
haveI : FiniteDimensional F S :=
  FiniteDimensional.finiteDimensional_submodule (Subalgebra.toSubmodule S)

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝ : FiniteDimensional F E
this : FiniteDimensional F ↥S
⊢ S = ⊥ ∨ S = ⊤

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
h : ⊥ = ⊤
⊢ False

Tactic:
cases hr.symm.trans (Subalgebra.bot_eq_top_iff_finrank_eq_one.1 h)

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
this✝ : finrank F ↥S ≤ 2
this : 0 < finrank F ↥S
⊢ S = ⊥ ∨ S = ⊤

Tactic:
interval_cases h : finrank F { x // x ∈ S }

Result:
case «1»
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = 1
this✝ : 1 ≤ 2
this : 0 < 1
⊢ S = ⊥ ∨ S = ⊤

case «2»
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = 2
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊥ ∨ S = ⊤

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝¹ : FiniteDimensional F E
this✝ : FiniteDimensional F ↥S
this : finrank F ↥S ≤ 2
⊢ S = ⊥ ∨ S = ⊤

Tactic:
have : 0 < finrank F S := finrank_pos_iff.mpr inferInstance

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
this✝ : finrank F ↥S ≤ 2
this : 0 < finrank F ↥S
⊢ S = ⊥ ∨ S = ⊤

Proof state:
case «2».h
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = finrank F E
this✝ : 2 ≤ 2
this : 0 < 2
⊢ toSubmodule S = ⊤

Tactic:
exact eq_top_of_finrank_eq h

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
⊢ ∀ (a : Subalgebra F E), a = ⊥ ∨ a = ⊤

Tactic:
intro S

Result:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
⊢ S = ⊥ ∨ S = ⊤