-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem rank_eq_one_iff [Nontrivial E] [Module.Free F S] : Module.rank F S = 1 ↔ S = ⊥

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
⊢ Module.rank F ↥⊥ = 1

Tactic:
obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := (⊥ : Subalgebra F E))

Result:
case intro.mk
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ Module.rank F ↥⊥ = 1

Proof state:
case intro.mk.refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
this : IsEmpty κ
⊢ False

Tactic:
haveI := b.repr.toEquiv.subsingleton

Result:
case intro.mk.refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
this✝ : IsEmpty κ
this : Subsingleton ↥⊥
⊢ False

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ Module.rank F ↥S = 1 ↔ S = ⊥

Tactic:
refine ⟨fun h ↦ Subalgebra.eq_bot_of_rank_le_one h.le, ?_⟩

Result:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ S = ⊥ → Module.rank F ↥S = 1

Proof state:
case intro.mk.refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ 1 ≤ Module.rank F ↥⊥

Tactic:
by_contra H

Result:
case intro.mk.refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : ¬1 ≤ Module.rank F ↥⊥
⊢ False

Proof state:
case intro.mk.refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
⊢ False

Tactic:
haveI := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')

Result:
case intro.mk.refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
this : IsEmpty κ
⊢ False

Proof state:
case intro.mk.refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ Module.rank F ↥⊥ ≤ 1

Tactic:
have := lift_rank_range_le (Algebra.linearMap F E)

Result:
case intro.mk.refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
this : lift.{u_1, u_2} (Module.rank F ↥(LinearMap.range (Algebra.linearMap F E))) ≤ lift.{u_2, u_1} (Module.rank F F)
⊢ Module.rank F ↥⊥ ≤ 1

Proof state:
case intro.mk.refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : ¬1 ≤ Module.rank F ↥⊥
⊢ False

Tactic:
rw [not_le, lt_one_iff_zero] at H

Result:
case intro.mk.refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
⊢ False

Proof state:
case intro.mk.refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : Module.rank F ↥⊥ = 0
this✝ : IsEmpty κ
this : Subsingleton ↥⊥
⊢ False

Tactic:
exact one_ne_zero congr((⊥ : Subalgebra F E).val $(Subsingleton.elim 1 0))

Result:
no goals

Proof state:
case intro.mk.refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
this : lift.{u_1, u_2} (Module.rank F ↥(LinearMap.range (Algebra.linearMap F E))) ≤ lift.{u_2, u_1} (Module.rank F F)
⊢ Module.rank F ↥⊥ ≤ 1

Tactic:
rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff,
  ← Algebra.toSubmodule_bot, rank_toSubmodule] at this

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
S : Subalgebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥S
⊢ S = ⊥ → Module.rank F ↥S = 1

Tactic:
rintro rfl

Result:
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
⊢ Module.rank F ↥⊥ = 1

Proof state:
case intro.mk
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ Module.rank F ↥⊥ = 1

Tactic:
refine le_antisymm ?_ ?_

Result:
case intro.mk.refine_1
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ Module.rank F ↥⊥ ≤ 1

case intro.mk.refine_2
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : StrongRankCondition F
inst✝³ : Ring E
inst✝² : Algebra F E
inst✝¹ : Nontrivial E
inst✝ : Free F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ 1 ≤ Module.rank F ↥⊥