awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
⊢ False
have this₁ : Subsingleton V
Tactic: haveI : Subsingleton V := .intro fun _ _ ↦ by simp_rw [← hv]
-- 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
this : Nontrivial K
h_1 : ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ (r : K), r • v₀ = v
⊢ 1 ≤ Module.rank K V
have refine_2 : ∀ (H : ¬1 ≤ Module.rank K V), False
Tactic: by_contra H
-- 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
this : Nontrivial K
h_1 : ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ (r : K), r • v₀ = v
H : ¬1 ≤ Module.rank K V
⊢ False
have H₁ : Module.rank K V = 0
Tactic: rw [not_le, Cardinal.lt_one_iff] at H
Cleared hypotheses: H
-- 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
this : Nontrivial K
h_1 : ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ (r : K), r • v₀ = v
H : Module.rank K V = 0
⊢ False
have refine_2 : ∀ (κ : Type v) (b : Basis κ K V), False
Tactic: obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := 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
this : Nontrivial K
h_1 : ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ (r : K), r • v₀ = v
H : Module.rank K V = 0
κ : Type v
b : Basis κ K V
⊢ False
have this₁ : IsEmpty κ
Tactic: haveI := mk_eq_zero_iff.1 (H ▸ b.mk_eq_rank'')
-- 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
this_1 : Nontrivial K
h_1 : ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
v₀ : V
h : v₀ ≠ 0
hv : ∀ (v : V), ∃ (r : K), r • v₀ = v
H : Module.rank K V = 0
κ : Type v
b : Basis κ K V
this : IsEmpty κ
⊢ False
have this₁ : Subsingleton V
Tactic: haveI := b.repr.toEquiv.subsingleton
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀
have simp_rw : (∃ (v₀ : ↥s), ∀ (v : ↥s), ∃ (r : K), r • v₀ = v) ↔ ∃ v₀ ∈ s, ∀ v ∈ s, ∃ (r : K), r • v₀ = v
Tactic: simp_rw [rank_le_one_iff, le_span_singleton_iff]
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
⊢ Module.rank K ↥s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀
have simp_rw : (∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ (r : K), r • v₀ = v
Tactic: simp_rw [rank_eq_one_iff, le_span_singleton_iff]
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
h_1 : ∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ ≠ 0
h : ∀ (v : ↥s), ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = v
h' : v₀ = 0
⊢ False
have H₁ : ¬Subtype.mk (p := fun (x : V) ↦ x ∈ s) 0 sorry = 0
Tactic: simp only [h', ne_eq] at H
Cleared hypotheses: H
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
h_1 : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ (r : K), r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ (r : K), r • v₀ = v
h' : Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = 0
⊢ v₀ = 0
have rwa : ∀ (h' : v₀ = 0), v₀ = 0
Tactic: rwa [AddSubmonoid.mk_eq_zero] at h'
Cleared hypotheses: h'
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
⊢ (∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ (r : K), r • v₀ = v
have refine_1 : (∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v) →
  ∀ (v₀ : V) (hv₀ : v₀ ∈ s) (H : Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ ≠ 0)
    (h : ∀ (v : ↥s), ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = v) (v : V) (hv : v ∈ s),
    ∃ (r : K), r • v₀ = v
Tactic: refine ⟨fun ⟨⟨v₀, hv₀⟩, H, h⟩ ↦ ⟨v₀, hv₀, fun h' ↦ by
    simp only [h', ne_eq] at H; exact H rfl, fun v hv ↦ ?_⟩,
    fun ⟨v₀, hv₀, H, h⟩ ↦ ⟨⟨v₀, hv₀⟩,
      fun h' ↦ H (by rwa [AddSubmonoid.mk_eq_zero] at h'), fun ⟨v, hv⟩ ↦ ?_⟩⟩
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
refine_1 :
  (∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v) →
    ∀ (v₀ : V) (hv₀ : v₀ ∈ s) (H : Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ ≠ 0)
      (h : ∀ (v : ↥s), ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = v) (v : V) (hv : v ∈ s),
      ∃ (r : K), r • v₀ = v
⊢ (∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ (r : K), r • v₀ = v
have refine_2 : (∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ (r : K), r • v₀ = v) →
  ∀ (v₀ : V) (hv₀ : v₀ ∈ s) (H : v₀ ≠ 0) (h : ∀ v ∈ s, ∃ (r : K), r • v₀ = v) (x : ↥s) (v : V) (hv : v ∈ s),
    ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv
Tactic: refine ⟨fun ⟨⟨v₀, hv₀⟩, H, h⟩ ↦ ⟨v₀, hv₀, fun h' ↦ by
    simp only [h', ne_eq] at H; exact H rfl, fun v hv ↦ ?_⟩,
    fun ⟨v₀, hv₀, H, h⟩ ↦ ⟨⟨v₀, hv₀⟩,
      fun h' ↦ H (by rwa [AddSubmonoid.mk_eq_zero] at h'), fun ⟨v, hv⟩ ↦ ?_⟩⟩
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
h_1 : ∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ ≠ 0
h : ∀ (v : ↥s), ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = v
v : V
hv : v ∈ s
⊢ ∃ (r : K), r • v₀ = v
have refine_1 : ∀ (r : K) (hr : r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv),
  ∃ (r : K), r • v₀ = v
Tactic: obtain ⟨r, hr⟩ := h ⟨v, hv⟩
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
h_1 : ∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ ≠ 0
h : ∀ (v : ↥s), ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = v
v : V
hv : v ∈ s
r : K
hr : r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv
⊢ r • v₀ = v
have rwa : ∀
  (hr :
    (↑(r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀) : V) = (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv) : V)),
  r • v₀ = v
Tactic: rwa [Subtype.ext_iff, coe_smul] at hr
Cleared hypotheses: hr
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
h_1 : ∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ ≠ 0
h : ∀ (v : ↥s), ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = v
v : V
hv : v ∈ s
r : K
hr : r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv
rwa :
  ∀
    (hr :
      (↑(r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀) : V) = (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv) : V)),
    r • v₀ = v
⊢ r • v₀ = v
have rwa₁ : ∀
  (hr :
    r • (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀) : V) = (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv) : V)),
  r • v₀ = v
Tactic: rwa [Subtype.ext_iff, coe_smul] at hr
Cleared hypotheses: hr
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
h_1 : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ (r : K), r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ (r : K), r • v₀ = v
x : ↥s
v : V
hv : v ∈ s
⊢ ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv
have refine_2 : ∀ (r : K) (hr : r • v₀ = v),
  ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv
Tactic: obtain ⟨r, hr⟩ := h v hv
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
h_1 : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ (r : K), r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ (r : K), r • v₀ = v
x : ↥s
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
⊢ r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv
have rwa : (↑(r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀) : V) = (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv) : V)
Tactic: rwa [Subtype.ext_iff, coe_smul]
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
h_1 : ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ (r : K), r • v₀ = v
v₀ : V
hv₀ : v₀ ∈ s
H : v₀ ≠ 0
h : ∀ v ∈ s, ∃ (r : K), r • v₀ = v
x : ↥s
v : V
hv : v ∈ s
r : K
hr : r • v₀ = v
rwa : (↑(r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀) : V) = (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv) : V)
⊢ r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv
have rwa₁ : r • (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀) : V) = (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv) : V)
Tactic: rwa [Subtype.ext_iff, coe_smul]
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ (v₀ : V), s ≤ K ∙ v₀
have this : Nontrivial K
Tactic: haveI := nontrivial_of_invariantBasisNumber K
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
this : Nontrivial K
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ (v₀ : V), s ≤ K ∙ v₀
have mp : Module.rank K ↥s ≤ 1 → ∃ (v₀ : V), s ≤ K ∙ v₀
Tactic: constructor
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
this : Nontrivial K
mp : Module.rank K ↥s ≤ 1 → ∃ (v₀ : V), s ≤ K ∙ v₀
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ (v₀ : V), s ≤ K ∙ v₀
have mpr : (∃ (v₀ : V), s ≤ K ∙ v₀) → Module.rank K ↥s ≤ 1
Tactic: constructor
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
this : Nontrivial K
⊢ Module.rank K ↥s ≤ 1 → ∃ (v₀ : V), s ≤ K ∙ v₀
have mp : (∃ v₀ ∈ s, s ≤ K ∙ v₀) → ∃ (v₀ : V), s ≤ K ∙ v₀
Tactic: rw [rank_submodule_le_one_iff]
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
this : Nontrivial K
v₀ : V
h : s ≤ K ∙ v₀
⊢ Module.rank K ↥s ≤ 1
have mpr : ∀ (κ : Type v) (b : Basis κ K ↥s), Module.rank K ↥s ≤ 1
Tactic: obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := K) (M := s)
-- 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
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
⊢ Module.rank K ↥W ≤ 1 ↔ W.IsPrincipal
have simp : (∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v) ↔ ∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W
Tactic: simp only [rank_le_one_iff, Submodule.isPrincipal_iff, le_antisymm_iff, le_span_singleton_iff,
    span_singleton_le_iff_mem]
-- 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
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
⊢ (∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v) ↔ ∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W
have mp : (∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v) → ∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W
Tactic: constructor
-- 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
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
mp : (∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v) → ∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W
⊢ (∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v) ↔ ∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W
have mpr : (∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W) → ∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v
Tactic: constructor
-- 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
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
m : V
hm : m ∈ W
hm' : ∀ (v : ↥W), ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ W) m hm = v
⊢ ∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W
have mp : ∀ (f : (v : ↥W) → K) (hf : ∀ (v : ↥W), f v • Subtype.mk (p := fun (x : V) ↦ x ∈ W) m hm = v),
  ∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W
Tactic: choose f hf using hm'
Cleared hypotheses: hm'
-- 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
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
a : V
h : ∀ v ∈ W, ∃ (r : K), r • a = v
ha : a ∈ W
⊢ ∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v
have mpr : ∀ (f : (v : V) → v ∈ W → K) (hf : ∀ (v : V) (a_1 : v ∈ W), f v a_1 • a = v),
  ∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v
Tactic: choose f hf using h
Cleared hypotheses: h
-- 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
⊢ Module.rank K V ≤ 1 ↔ Submodule.IsPrincipal.{u, v} (R := K) (M := V) ⊤
have this : Free.{u, v} K ↥⊤
Tactic: haveI := Module.Free.of_equiv (topEquiv (R := K) (M := V)).symm
-- 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
this : Free.{u, v} K ↥⊤
⊢ Module.rank K V ≤ 1 ↔ Submodule.IsPrincipal.{u, v} (R := K) (M := V) ⊤
have rw : Module.rank K V ≤ 1 ↔ Module.rank K ↥⊤ ≤ 1
Tactic: rw [← Submodule.rank_le_one_iff_isPrincipal, rank_top]
-- 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
this : Free.{u, v} K ↥⊤
rw : Module.rank K V ≤ 1 ↔ Module.rank K ↥⊤ ≤ 1
⊢ Module.rank K V ≤ 1 ↔ Submodule.IsPrincipal.{u, v} (R := K) (M := V) ⊤
have rw₁ : Module.rank K V ≤ 1 ↔ Module.rank K V ≤ 1
Tactic: rw [← Submodule.rank_le_one_iff_isPrincipal, rank_top]
-- 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
ι : Type u_1
inst_5 : Unique ι
⊢ finrank K V = 1 ↔ Nonempty (Basis ι K V)
have mp : finrank K V = 1 → Nonempty (Basis ι K V)
Tactic: constructor
-- 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
ι : Type u_1
inst_5 : Unique ι
mp : finrank K V = 1 → Nonempty (Basis ι K V)
⊢ finrank K V = 1 ↔ Nonempty (Basis ι K V)
have mpr : Nonempty (Basis ι K V) → finrank K V = 1
Tactic: constructor
-- 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
⊢ finrank K V = 1 ↔ ∃ (v : V), v ≠ 0 ∧ ∀ (w : V), ∃ (c : K), c • v = w
have rw : finrank K V = 1 ↔ Module.rank K V = 1
Tactic: rw [← rank_eq_one_iff]
-- 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
⊢ finrank K V ≤ 1 ↔ ∃ (v : V), ∀ (w : V), ∃ (c : K), c • v = w
have rw : finrank K V ≤ 1 ↔ Module.rank K V ≤ 1
Tactic: rw [← rank_le_one_iff, ← finrank_eq_rank, Nat.cast_le_one]
-- 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
rw : finrank K V ≤ 1 ↔ Module.rank K V ≤ 1
⊢ finrank K V ≤ 1 ↔ ∃ (v : V), ∀ (w : V), ∃ (c : K), c • v = w
have rw₁ : finrank K V ≤ 1 ↔ LE.le.{v + 1} (α := Cardinal.{v}) (↑(finrank K V) : Cardinal.{v}) 1
Tactic: rw [← rank_le_one_iff, ← finrank_eq_rank, Nat.cast_le_one]
-- 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
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
⊢ finrank K V ≤ 1 ↔ ∃ (v : V), ∀ (w : V), ∃ (c : K), c • v = w
have rw₂ : finrank K V ≤ 1 ↔ finrank K V ≤ 1
Tactic: rw [← rank_le_one_iff, ← finrank_eq_rank, Nat.cast_le_one]
-- 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
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
inst_5 : Module.Finite.{u, v} K ↥W
⊢ finrank.{u, v} K ↥W ≤ 1 ↔ W.IsPrincipal
have rw : finrank.{u, v} K ↥W ≤ 1 ↔ Module.rank K ↥W ≤ 1
Tactic: rw [← W.rank_le_one_iff_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]
-- 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
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
⊢ finrank.{u, v} K ↥W ≤ 1 ↔ W.IsPrincipal
have rw₁ : finrank.{u, v} K ↥W ≤ 1 ↔ LE.le.{v + 1} (α := Cardinal.{v}) (↑(finrank.{u, v} K ↥W) : Cardinal.{v}) 1
Tactic: rw [← W.rank_le_one_iff_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]
-- 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
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
⊢ finrank.{u, v} K ↥W ≤ 1 ↔ W.IsPrincipal
have rw₂ : finrank.{u, v} K ↥W ≤ 1 ↔ finrank.{u, v} K ↥W ≤ 1
Tactic: rw [← W.rank_le_one_iff_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]
-- 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
⊢ finrank K V ≤ 1 ↔ Submodule.IsPrincipal.{u, v} (R := K) (M := V) ⊤
have rw : finrank K V ≤ 1 ↔ Module.rank K V ≤ 1
Tactic: rw [← Module.rank_le_one_iff_top_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]
-- 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
rw : finrank K V ≤ 1 ↔ Module.rank K V ≤ 1
⊢ finrank K V ≤ 1 ↔ Submodule.IsPrincipal.{u, v} (R := K) (M := V) ⊤
have rw₁ : finrank K V ≤ 1 ↔ LE.le.{v + 1} (α := Cardinal.{v}) (↑(finrank K V) : Cardinal.{v}) 1
Tactic: rw [← Module.rank_le_one_iff_top_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]
-- 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
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
⊢ finrank K V ≤ 1 ↔ Submodule.IsPrincipal.{u, v} (R := K) (M := V) ⊤
have rw₂ : finrank K V ≤ 1 ↔ finrank K V ≤ 1
Tactic: rw [← Module.rank_le_one_iff_top_isPrincipal, ← finrank_eq_rank, Nat.cast_le_one]
-- 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
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)
have this : Nontrivial K
Tactic: haveI := nontrivial_of_invariantBasisNumber K