awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
⊢ finrank K V = 1 ↔ Module.rank K V = 1

Tactic:
toNat_eq_iff one_ne_zero

Premises used: Cardinal.toNat_eq_iff, one_ne_zero, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
⊢ finrank K V = 1 ↔ Module.rank K V = 1

Tactic:
exact toNat_eq_iff one_ne_zero

Premises used: Cardinal.toNat_eq_iff, one_ne_zero
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
rw : finrank K V ≤ 1 ↔ Module.rank K V ≤ 1
rw₁ : finrank K V ≤ 1 ↔ LE.le.{v + 1} (α := Cardinal.{v}) (↑(finrank K V) : Cardinal.{v}) 1
rw₂ rw₃ : finrank K V ≤ 1 ↔ finrank K V ≤ 1
⊢ finrank K V ≤ 1 ↔ ∃ (v : V), ∀ (w : V), ∃ (c : K), c • v = w

Tactic:
rw [← rank_le_one_iff, ← finrank_eq_rank, Nat.cast_le_one]

Premises used: Module.finrank_eq_rank, rank_le_one_iff, Nat.cast_le_one
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
inst_5 : Module.Finite.{u, v} K ↥W
rw : finrank.{u, v} K ↥W ≤ 1 ↔ Module.rank K ↥W ≤ 1
rw₁ : finrank.{u, v} K ↥W ≤ 1 ↔ LE.le.{v + 1} (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥W) : Cardinal.{v}) 1
rw₂ rw₃ : finrank.{u, v} K ↥W ≤ 1 ↔ finrank.{u, v} K ↥W ≤ 1
⊢ finrank.{u, v} K ↥W ≤ 1 ↔ W.IsPrincipal

Tactic:
rw [← W.rank_le_one_iff_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]

Premises used: Module.finrank_eq_rank, Submodule.rank_le_one_iff_isPrincipal, Nat.cast_le_one
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
rw : finrank K V ≤ 1 ↔ Module.rank K V ≤ 1
rw₁ : finrank K V ≤ 1 ↔ LE.le.{v + 1} (α := Cardinal.{v}) (↑(finrank K V) : Cardinal.{v}) 1
rw₂ rw₃ : finrank K V ≤ 1 ↔ finrank K V ≤ 1
⊢ finrank K V ≤ 1 ↔ Submodule.IsPrincipal.{u, v} (R := K) (M := V) ⊤

Tactic:
rw [← Module.rank_le_one_iff_top_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]

Premises used: Module.finrank_eq_rank, Module.rank_le_one_iff_top_isPrincipal, Nat.cast_le_one
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
⊢ Nontrivial K

Tactic:
haveI := nontrivial_of_invariantBasisNumber K
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
this : Nontrivial K
obtain : ∀ (s : Type v) (hs : Basis s K V), lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Tactic:
obtain ⟨s, hs⟩ := Module.Free.exists_basis (R := K) (M := V)

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
this : Nontrivial K
s : Type v
hs : Basis s K V
obtain : ∀ (t : Finset V) (ht : Eq (α := Submodule K V) (span K (↑t : Set V)) ⊤), Finite s
⊢ Finite s

Tactic:
obtain ⟨t, ht⟩ := ‹Module.Finite K V›

Premises used: Module.Finite
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
this : Nontrivial K
s : Type v
hs : Basis s K V
t : Finset V
ht : Eq (α := Submodule K V) (span K (↑t : Set V)) ⊤
⊢ Finite s

Tactic:
basis_finite_of_finite_spans t.finite_toSet ht hs

Premises used: basis_finite_of_finite_spans, Finset.finite_toSet
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
this : Nontrivial K
s : Type v
hs : Basis s K V
t : Finset V
ht : Eq (α := Submodule K V) (span K (↑t : Set V)) ⊤
⊢ Finite s

Tactic:
exact basis_finite_of_finite_spans t.finite_toSet ht hs

Premises used: basis_finite_of_finite_spans, Finset.finite_toSet
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
this : Nontrivial K
s : Type v
hs : Basis s K V
⊢ Finite s

Tactic:
haveI : Finite s := by
    obtain ⟨t, ht⟩ := ‹Module.Finite K V›
    exact basis_finite_of_finite_spans t.finite_toSet ht hs
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
this_1 : Nontrivial K
s : Type v
hs : Basis s K V
this : Finite s
⊢ lift.{max u v, v} #V = lift.{v, max u v} #(s →₀ K)

Tactic:
have := lift_mk_eq'.2 ⟨hs.repr.toEquiv⟩
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
this_1 : Nontrivial K
s : Type v
hs : Basis s K V
this_2 : Finite s
this : lift.{max u v, v} #V = lift.{v, max u v} #(s →₀ K)
rwa :
  ∀ (this : lift.{max u v, v} #V = lift.{v, max u v} #(s → K)),
    lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
rwa₁ :
  ∀ (this : lift.{max u v, v} #V = lift.{v, max u v} (lift.{v, u} #K ^ lift.{u, v} #s)),
    lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
rwa₂ :
  ∀ (this : lift.{max u v, v} #V = lift.{v, max u v} (lift.{v, u} #K ^ lift.{u, v} (Module.rank K V))),
    lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
rwa₃ :
  ∀
    (this :
      lift.{max u v, v} #V = lift.{v, max u v} (lift.{v, u} #K) ^ lift.{v, max u v} (lift.{u, v} (Module.rank K V))),
    lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
rwa₄ :
  ∀ (this : lift.{max u v, v} #V = lift.{v, u} #K ^ lift.{v, max u v} (lift.{u, v} (Module.rank K V))),
    lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
rwa₅ :
  ∀ (this : lift.{max u v, v} #V = lift.{v, u} #K ^ lift.{max u v, v} (Module.rank K V)),
    lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
rwa₆ rwa₇ rwa₈ rwa₉ :
  ∀ (this : lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)),
    lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Tactic:
rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
    lift_lift, lift_umax] at this

Premises used: Cardinal.lift_lift, Finsupp.equivFunOnFinite, Cardinal.mk_arrow, Cardinal.lift_umax, Cardinal.lift_power, Module.Basis.mk_eq_rank'', Equiv.cardinal_eq
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K V : Type u
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
inst_5 : Module.Finite K V
⊢ #V = #K ^ Module.rank K V

Tactic:
simpa using lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V

Premises used: lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Finite K
inst_5 : Free K V
inst_6 : Module.Finite K V
rw : lift.{v, u} #K ^ lift.{u, v} (Module.rank K V) < ℵ₀
⊢ #V < ℵ₀

Tactic:
rw [← lift_lt_aleph0.{v, u}, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V]

Premises used: lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Finite K
inst_5 : Free K V
inst_6 : Module.Finite K V
⊢ lift.{v, u} #K ^ lift.{u, v} (Module.rank K V) < ℵ₀

Tactic:
power_lt_aleph0 (lift_lt_aleph0.2 (lt_aleph0_of_finite K))
    (lift_lt_aleph0.2 (rank_lt_aleph0 K V))

Premises used: Iff.mpr, Cardinal.lift_lt_aleph0, Cardinal.lt_aleph0_of_finite, Cardinal.power_lt_aleph0, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Finite K
inst_5 : Free K V
inst_6 : Module.Finite K V
⊢ lift.{v, u} #K ^ lift.{u, v} (Module.rank K V) < ℵ₀

Tactic:
exact power_lt_aleph0 (lift_lt_aleph0.2 (lt_aleph0_of_finite K))
    (lift_lt_aleph0.2 (rank_lt_aleph0 K V))

Premises used: Iff.mpr, Cardinal.lift_lt_aleph0, Cardinal.lt_aleph0_of_finite, Cardinal.power_lt_aleph0, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
⊢ Nontrivial E

Tactic:
nontriviality E
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
obtain : ∀ (κ : Type u_2) (b : Basis κ F ↥S), S = ⊥
⊢ S = ⊥

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

Premises used: Membership.mem, Subtype, Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
pos : ∀ (h1 : Module.rank F ↥S = 1), S = ⊥
neg : ∀ (h1 : ¬Module.rank F ↥S = 1), S = ⊥
⊢ S = ⊥

Tactic:
by_cases h1 : Module.rank F S = 1

Premises used: Membership.mem, Subtype, Module.rank
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : Module.rank F ↥S = 1
⊢ S = ⊥

Tactic:
bot_unique fun x hx ↦ Algebra.mem_bot.2 ?_

Premises used: Iff.mpr, Algebra.mem_bot, bot_unique
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : Module.rank F ↥S = 1
pos :
  ∀ (x : E) (hx : x ∈ S),
    Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
⊢ S = ⊥

Tactic:
refine bot_unique fun x hx ↦ Algebra.mem_bot.2 ?_

Premises used: bot_unique
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : Module.rank F ↥S = 1
x : E
hx : x ∈ S
pos :
  ∀ (h1 : Nonempty.{max 1 (u_2 + 1)} (Unique κ)) (x : E) (hx : x ∈ S),
    Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
⊢ Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x

Tactic:
rw [← b.mk_eq_rank'', eq_one_iff_unique, ← unique_iff_subsingleton_and_nonempty] at h1

Premises used: Cardinal.eq_one_iff_unique, unique_iff_subsingleton_and_nonempty, Module.Basis.mk_eq_rank''
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : Nonempty.{max 1 (u_2 + 1)} (Unique κ)
x : E
hx : x ∈ S
pos : ∀ (h1 : Unique κ), Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
⊢ Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x

Tactic:
obtain ⟨h1⟩ := h1
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
x : E
hx : x ∈ S
h1 : Unique κ
pos :
  ∀ (y : F) (hy : (algebraMap F ↥S : (a : F) → ↥S) y = Subtype.mk (p := fun (x : E) ↦ x ∈ S) x hx),
    Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
⊢ Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x

Tactic:
obtain ⟨y, hy⟩ := (bijective_algebraMap_of_linearEquiv (b.repr ≪≫ₗ
      Finsupp.uniqueLinearEquiv _ _ default).symm).surjective ⟨x, hx⟩

Premises used: Inhabited.default, LinearEquiv.symm, Finsupp.uniqueLinearEquiv, bijective_algebraMap_of_linearEquiv, Module.Basis.repr, Subtype.mk, Function.Bijective.surjective, LinearEquiv.trans
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
x : E
hx : x ∈ S
h1 : Unique κ
y : F
hy : (algebraMap F ↥S : (a : F) → ↥S) y = Subtype.mk (p := fun (x : E) ↦ x ∈ S) x hx
⊢ Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x

Tactic:
⟨y, congr(Subtype.val $(hy))⟩

Premises used: congrArg, Set.Mem, setOf, id, Exists.intro, Set.range, Subtype.val
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
x : E
hx : x ∈ S
h1 : Unique κ
y : F
hy : (algebraMap F ↥S : (a : F) → ↥S) y = Subtype.mk (p := fun (x : E) ↦ x ∈ S) x hx
⊢ Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x

Tactic:
exact ⟨y, congr(Subtype.val $(hy))⟩
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : ¬Module.rank F ↥S = 1
⊢ IsEmpty κ

Tactic:
haveI := mk_eq_zero_iff.1 (b.mk_eq_rank''.symm ▸ Cardinal.lt_one_iff.1 (h.lt_of_ne h1))
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : ¬Module.rank F ↥S = 1
this : IsEmpty κ
⊢ Subsingleton.{u_2 + 1} ↥S

Tactic:
haveI := b.repr.toEquiv.subsingleton
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : ¬Module.rank F ↥S = 1
this_1 : IsEmpty κ
this : Subsingleton.{u_2 + 1} ↥S
⊢ S = ⊥

Tactic:
False.elim <| one_ne_zero congr(S.val $(Subsingleton.elim 1 0))

Premises used: congrArg, False.elim, Subalgebra.val, id, Subsingleton.elim, one_ne_zero, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S ≤ 1
inst_4 : Free.{u_1, u_2} F ↥S
h_1 : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
h1 : ¬Module.rank F ↥S = 1
this_1 : IsEmpty κ
this : Subsingleton.{u_2 + 1} ↥S
⊢ S = ⊥

Tactic:
exact False.elim <| one_ne_zero congr(S.val $(Subsingleton.elim 1 0))

Premises used: congrArg, False.elim, Subalgebra.val, id, Subsingleton.elim, one_ne_zero, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : finrank.{u_1, u_2} F ↥S = 1
inst_4 : Free.{u_1, u_2} F ↥S
⊢ S = ⊥

Tactic:
Subalgebra.eq_bot_of_rank_le_one ?_

Premises used: Subalgebra.eq_bot_of_rank_le_one
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : finrank.{u_1, u_2} F ↥S = 1
inst_4 : Free.{u_1, u_2} F ↥S
refine : Module.rank F ↥S ≤ 1
⊢ S = ⊥

Tactic:
refine Subalgebra.eq_bot_of_rank_le_one ?_

Premises used: Subalgebra.eq_bot_of_rank_le_one
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : finrank.{u_1, u_2} F ↥S = 1
inst_4 : Free.{u_1, u_2} F ↥S
⊢ Module.rank F ↥S = 1

Tactic:
rw [finrank, toNat_eq_one] at h

Premises used: Cardinal.toNat_eq_one, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : finrank.{u_1, u_2} F ↥S = 1
inst_4 : Free.{u_1, u_2} F ↥S
h₁ : Module.rank F ↥S = 1
⊢ Free.{u_1, u_2} F ↥S

Tactic:
rw [finrank, toNat_eq_one] at h

Premises used: Cardinal.toNat_eq_one, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
h : Module.rank F ↥S = 1
inst_4 : Free.{u_1, u_2} F ↥S
rw rw₁ : LE.le.{u_2 + 1} (α := Cardinal.{u_2}) 1 1
⊢ Module.rank F ↥S ≤ 1

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥S
⊢ Module.rank F ↥S = 1 ↔ S = ⊥

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

Premises used: Eq.le, Iff.intro, Subalgebra.eq_bot_of_rank_le_one
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
S : Subalgebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥S
refine : S = ⊥ → Module.rank F ↥S = 1
⊢ Module.rank F ↥S = 1 ↔ S = ⊥

Tactic:
refine ⟨fun h ↦ Subalgebra.eq_bot_of_rank_le_one h.le, ?_⟩
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
obtain : ∀ (κ : Type u_2) (b : Basis κ F ↥⊥), Module.rank F ↥⊥ = 1
⊢ Module.rank F ↥⊥ = 1

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

Premises used: Membership.mem, Subtype, Bot.bot, Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ Module.rank F ↥⊥ = 1

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
refine_1 : Module.rank F ↥⊥ ≤ 1
refine_2 : 1 ≤ Module.rank F ↥⊥
⊢ Module.rank F ↥⊥ = 1

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
⊢ lift.{u_1, u_2} (Module.rank F ↥(LinearMap.range (Algebra.linearMap F E))) ≤ lift.{u_2, u_1} (Module.rank F F)

Tactic:
have := lift_rank_range_le (Algebra.linearMap F E)
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} 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)
refine_1 : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ lift.{u_2, u_1} (Module.rank F F)), Module.rank F ↥⊥ ≤ 1
refine_1₁ : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ lift.{u_2, u_1} 1), Module.rank F ↥⊥ ≤ 1
refine_1₂ : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ 1), Module.rank F ↥⊥ ≤ 1
refine_1₃ : ∀ (this : Module.rank F ↥1 ≤ 1), Module.rank F ↥⊥ ≤ 1
refine_1₄ :
  ∀ (this : Module.rank F ↥((toSubmodule : (a : Subalgebra F E) → Submodule F E) ⊥ : Submodule F E) ≤ 1),
    Module.rank F ↥⊥ ≤ 1
refine_1₅ refine_1₆ refine_1₇ refine_1₈ : ∀ (this : Module.rank F ↥⊥ ≤ 1), Module.rank F ↥⊥ ≤ 1
⊢ Module.rank F ↥⊥ ≤ 1

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

Premises used: Algebra.toSubmodule_bot, Cardinal.lift_le_one_iff, Module.rank_self, Cardinal.lift_one, Submodule.one_eq_range, Subalgebra.rank_toSubmodule
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
refine_2 : ∀ (H : ¬1 ≤ Module.rank F ↥⊥), False
⊢ 1 ≤ Module.rank F ↥⊥

Tactic:
by_contra H
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
F : Type u_1
E : Type u_2
inst : CommRing F
inst_1 : StrongRankCondition F
inst_2 : Ring E
inst_3 : Algebra F E
inst_4 : Nontrivial E
inst_5 : Free.{u_1, u_2} F ↥⊥
κ : Type u_2
b : Basis κ F ↥⊥
H : ¬1 ≤ Module.rank F ↥⊥
⊢ Module.rank F ↥⊥ = 0

Tactic:
rw [not_le, Cardinal.lt_one_iff] at H

Premises used: not_le, Cardinal.lt_one_iff