awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have obtain : ∀ (s : Type v) (hs : Basis s 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
have obtain : ∀ (t : Finset V) (ht : Eq (α := Submodule K V) (span K (↑t : Set V)) ⊤), Finite s
Tactic: obtain ⟨t, ht⟩ := ‹Module.Finite K V›
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
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
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have this₁ : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
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.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have this₁ : lift.{max u v, v} #V = lift.{v, max u v} #(s →₀ K)
Tactic: have := lift_mk_eq'.2 ⟨hs.repr.toEquiv⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have 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)
Tactic: rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
    lift_lift, lift_umax] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have 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)
Tactic: rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
    lift_lift, lift_umax] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have 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)
Tactic: rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
    lift_lift, lift_umax] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have 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)
Tactic: rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
    lift_lift, lift_umax] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have 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)
Tactic: rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
    lift_lift, lift_umax] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have 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)
Tactic: rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
    lift_lift, lift_umax] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have 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)
Tactic: rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
    lift_lift, lift_umax] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ #V < ℵ₀
have rw : lift.{v, u} #K ^ lift.{u, v} (Module.rank K V) < ℵ₀
Tactic: rw [← lift_lt_aleph0.{v, u}, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
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
⊢ S = ⊥
have a : Nontrivial E
Tactic: nontriviality E
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ S = ⊥
have obtain : ∀ (κ : Type u_2) (b : Basis κ F ↥S), S = ⊥
Tactic: obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := S)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ S = ⊥
have pos : ∀ (h1 : Module.rank F ↥S = 1), S = ⊥
Tactic: by_cases h1 : Module.rank F S = 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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 = ⊥
⊢ S = ⊥
have neg : ∀ (h1 : ¬Module.rank F ↥S = 1), S = ⊥
Tactic: by_cases h1 : Module.rank F S = 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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 = ⊥
have pos : ∀ (x : E) (hx : x ∈ S), Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
Tactic: refine bot_unique fun x hx ↦ Algebra.mem_bot.2 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
have 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
Tactic: rw [← b.mk_eq_rank'', eq_one_iff_unique, ← unique_iff_subsingleton_and_nonempty] at h1
Cleared hypotheses: h1, x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
have pos : ∀ (h1 : Unique κ), Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
Tactic: obtain ⟨h1⟩ := h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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 κ
⊢ Membership.mem (γ := Set E) (range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E)) x
have 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
Tactic: obtain ⟨y, hy⟩ := (bijective_algebraMap_of_linearEquiv (b.repr ≪≫ₗ
      Finsupp.uniqueLinearEquiv _ _ default).symm).surjective ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
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 = ⊥
have this : IsEmpty κ
Tactic: haveI := mk_eq_zero_iff.1 (b.mk_eq_rank''.symm ▸ Cardinal.lt_one_iff.1 (h.lt_of_ne h1))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
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 κ
⊢ S = ⊥
have this₁ : Subsingleton.{u_2 + 1} ↥S
Tactic: haveI := b.repr.toEquiv.subsingleton
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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 = ⊥
have refine : Module.rank F ↥S ≤ 1
Tactic: refine Subalgebra.eq_bot_of_rank_le_one ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
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
have h₁ : Module.rank F ↥S = 1
Tactic: rw [finrank, toNat_eq_one] at h
Cleared hypotheses: h, inst_4
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ Module.rank F ↥S ≤ 1
have rw : LE.le.{u_2 + 1} (α := Cardinal.{u_2}) 1 1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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 = ⊥
have refine : S = ⊥ → Module.rank F ↥S = 1
Tactic: refine ⟨fun h ↦ Subalgebra.eq_bot_of_rank_le_one h.le, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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 ↥⊥
⊢ Module.rank F ↥⊥ = 1
have obtain : ∀ (κ : Type u_2) (b : Basis κ F ↥⊥), Module.rank F ↥⊥ = 1
Tactic: obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := (⊥ : Subalgebra F E))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
have refine_1 : Module.rank F ↥⊥ ≤ 1
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ Module.rank F ↥⊥ = 1
have refine_2 : 1 ≤ Module.rank F ↥⊥
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (hypothesis)
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
have this : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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)
⊢ Module.rank F ↥⊥ ≤ 1
have 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
Tactic: rwa [← one_eq_range, rank_self, lift_one, lift_le_one_iff,
      ← Algebra.toSubmodule_bot, rank_toSubmodule] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ Module.rank F ↥⊥ ≤ 1
have refine_1₁ : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ lift.{u_2, u_1} 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ Module.rank F ↥⊥ ≤ 1
have refine_1₂ : ∀ (this : lift.{u_1, u_2} (Module.rank F ↥1) ≤ 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition (goal)
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
⊢ Module.rank F ↥⊥ ≤ 1
have refine_1₃ : ∀ (this : Module.rank F ↥1 ≤ 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
Cleared hypotheses: this