K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
⊢ 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
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
⊢ S = ⊥
nontriviality E
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
⊢ 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
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
⊢ S = ⊥
obtain ⟨m, _, he⟩ := Cardinal.exists_nat_eq_of_le_nat (h.trans_eq Nat.cast_one.symm)
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this : FiniteDimensional F { x // x ∈ S }
⊢ S = ⊥
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
⊢ S = ⊥
haveI : FiniteDimensional F S := finiteDimensional_of_rank_eq_nat he
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this : FiniteDimensional F { x // x ∈ S }
⊢ ¬↑toSubmodule ⊥ < ↑toSubmodule S
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this : FiniteDimensional F { x // x ∈ S }
⊢ S = ⊥
rw [← not_bot_lt_iff, ← Subalgebra.toSubmodule.lt_iff_lt]
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this✝ : FiniteDimensional F { x // x ∈ S }
this : FiniteDimensional F { x // x ∈ ↑toSubmodule S }
⊢ ¬↑toSubmodule ⊥ < ↑toSubmodule S
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this : FiniteDimensional F { x // x ∈ S }
⊢ ¬↑toSubmodule ⊥ < ↑toSubmodule S
haveI : FiniteDimensional F (Subalgebra.toSubmodule S) :=
  S.toSubmoduleEquiv.symm.finiteDimensional
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this✝ : FiniteDimensional F { x // x ∈ S }
this : FiniteDimensional F { x // x ∈ ↑toSubmodule S }
hl : ↑toSubmodule ⊥ < ↑toSubmodule S
⊢ ↑(finrank F { x // x ∈ ↑toSubmodule S }) ≤ ↑(finrank F { x // x ∈ ↑toSubmodule ⊥ })
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this✝ : FiniteDimensional F { x // x ∈ S }
this : FiniteDimensional F { x // x ∈ ↑toSubmodule S }
⊢ ¬↑toSubmodule ⊥ < ↑toSubmodule S
refine fun hl => (Submodule.finrank_lt_finrank_of_lt hl).not_le (natCast_le.1 ?_)
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this✝ : FiniteDimensional F { x // x ∈ S }
this : FiniteDimensional F { x // x ∈ ↑toSubmodule S }
hl : ↑toSubmodule ⊥ < ↑toSubmodule S
⊢ Module.rank F { x // x ∈ S } ≤ Module.rank F { x // x ∈ ⊥ }
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this✝ : FiniteDimensional F { x // x ∈ S }
this : FiniteDimensional F { x // x ∈ ↑toSubmodule S }
hl : ↑toSubmodule ⊥ < ↑toSubmodule S
⊢ ↑(finrank F { x // x ∈ ↑toSubmodule S }) ≤ ↑(finrank F { x // x ∈ ↑toSubmodule ⊥ })
iterate 2 rw [Subalgebra.finrank_toSubmodule, finrank_eq_rank]
no goals
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this✝ : FiniteDimensional F { x // x ∈ S }
this : FiniteDimensional F { x // x ∈ ↑toSubmodule S }
hl : ↑toSubmodule ⊥ < ↑toSubmodule S
⊢ Module.rank F { x // x ∈ S } ≤ Module.rank F { x // x ∈ ⊥ }
exact h.trans_eq Subalgebra.rank_bot.symm
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this✝ : FiniteDimensional F { x // x ∈ S }
this : FiniteDimensional F { x // x ∈ ↑toSubmodule S }
hl : ↑toSubmodule ⊥ < ↑toSubmodule S
⊢ Module.rank F { x // x ∈ S } ≤ Module.rank F { x // x ∈ ⊥ }
case intro.intro
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
S : Subalgebra F E
h : Module.rank F { x // x ∈ S } ≤ 1
✝ : Nontrivial E
m : ℕ
left✝ : m ≤ 1
he : Module.rank F { x // x ∈ S } = ↑m
this✝ : FiniteDimensional F { x // x ∈ S }
this : FiniteDimensional F { x // x ∈ ↑toSubmodule S }
hl : ↑toSubmodule ⊥ < ↑toSubmodule S
⊢ Module.rank F { x // x ∈ S } ≤ ↑(finrank F { x // x ∈ ↑toSubmodule ⊥ })
rw [Subalgebra.finrank_toSubmodule, finrank_eq_rank]