no goals
K : Type u
V : Type v
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
cases hr.symm.trans (Subalgebra.bot_eq_top_iff_finrank_eq_one.1 h)
K : Type u
V : Type v
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 = ⊤
K : Type u
V : Type v
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 = ⊤
intro S
K : Type u
V : Type v
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 = ⊤
K : Type u
V : Type v
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 = ⊤
haveI : FiniteDimensional F E := finiteDimensional_of_finrank_eq_succ hr
K : Type u
V : Type v
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 { x // x ∈ S }
⊢ S = ⊥ ∨ S = ⊤
K : Type u
V : Type v
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 = ⊤
haveI : FiniteDimensional F S :=
  FiniteDimensional.finiteDimensional_submodule (Subalgebra.toSubmodule S)
K : Type u
V : Type v
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 { x // x ∈ S }
this : finrank F { x // x ∈ S } ≤ 2
⊢ S = ⊥ ∨ S = ⊤
K : Type u
V : Type v
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 { x // x ∈ S }
⊢ S = ⊥ ∨ S = ⊤
have : finrank F S ≤ 2 := hr ▸ S.toSubmodule.finrank_le
K : Type u
V : Type v
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 { x // x ∈ S }
this✝ : finrank F { x // x ∈ S } ≤ 2
this : 0 < finrank F { x // x ∈ S }
⊢ S = ⊥ ∨ S = ⊤
K : Type u
V : Type v
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 { x // x ∈ S }
this : finrank F { x // x ∈ S } ≤ 2
⊢ S = ⊥ ∨ S = ⊤
have : 0 < finrank F S := finrank_pos_iff.mpr inferInstance
case «1»
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = 1
this✝ : 1 ≤ 2
this : 0 < 1
⊢ S = ⊥ ∨ S = ⊤

case «2»
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = 2
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊥ ∨ S = ⊤
K : Type u
V : Type v
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 { x // x ∈ S }
this✝ : finrank F { x // x ∈ S } ≤ 2
this : 0 < finrank F { x // x ∈ S }
⊢ S = ⊥ ∨ S = ⊤
interval_cases h : finrank F { x // x ∈ S }
case «1».h
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = 1
this✝ : 1 ≤ 2
this : 0 < 1
⊢ S = ⊥
case «1»
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = 1
this✝ : 1 ≤ 2
this : 0 < 1
⊢ S = ⊥ ∨ S = ⊤
left
no goals
case «1».h
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = 1
this✝ : 1 ≤ 2
this : 0 < 1
⊢ S = ⊥
exact Subalgebra.eq_bot_of_finrank_one h
case «2».h
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = 2
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊤
case «2»
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = 2
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊥ ∨ S = ⊤
right
case «2».h
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = finrank F E
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊤
case «2».h
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = 2
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊤
rw [← hr] at h
case «2».h
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = finrank F E
this✝ : 2 ≤ 2
this : 0 < 2
⊢ ↑toSubmodule S = ⊤
case «2».h
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = finrank F E
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊤
rw [← Algebra.toSubmodule_eq_top]
no goals
case «2».h
K : Type u
V : Type v
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 { x // x ∈ S }
h : finrank F { x // x ∈ S } = finrank F E
this✝ : 2 ≤ 2
this : 0 < 2
⊢ ↑toSubmodule S = ⊤
exact Submodule.eq_top_of_finrank_eq h