awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : StrongRankCondition R
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
hc : c = (e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
x : M
this :
  ∀ (x : M), x = HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R) ((e : (a : R) → M) 1 : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R)
      ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((e.symm : (a : M) → R) x : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((e.symm : (a : M) → R) ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M) : R) ((e : (a : R) → M) 1 : M))
have h : HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R)
    ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((e.symm : (a : M) → R) x : R)
    ((u : (a : M) → M) ((e : (a : R) → M) 1 : M) : M)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R_1 : Type u
S : Type u_1
M_1 M₁ : Type v
M' : Type v'
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : Free R_1 M_1
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M'
inst_6 : Free R_1 M'
inst_7 : AddCommMonoid M₁
inst_8 : Module R_1 M₁
inst_9 : Free R_1 M₁
inst_10 : StrongRankCondition R_1
R : Type u_2
inst_11 : CommSemiring R
inst_12 : StrongRankCondition R
M : Type u_3
inst_13 : AddCommMonoid M
inst_14 : Module R M
inst_15 : Free R M
d1 : finrank R M = 1
c d : R
⊢ HSMul.hSMul (β := M →ₗ[R] M) (c + d) LinearMap.id =
    HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id + HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id
have h : ∀ (x : M),
  Eq (α := M) ((HSMul.hSMul (β := M →ₗ[R] M) (c + d) LinearMap.id : (a : M) → M) x : M)
    ((HSMul.hSMul (β := M →ₗ[R] M) c LinearMap.id + HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id : (a : M) → M) x : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Free (goal)
Goal:
R_1 : Type u
S : Type u_1
M_1 M₁ : Type v
M' : Type v'
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : Free R_1 M_1
inst_4 : AddCommMonoid M'
inst_5 : Module R_1 M'
inst_6 : Free R_1 M'
inst_7 : AddCommMonoid M₁
inst_8 : Module R_1 M₁
inst_9 : Free R_1 M₁
inst_10 : StrongRankCondition R_1
R : Type u_2
inst_11 : CommSemiring R
inst_12 : StrongRankCondition R
M : Type u_3
inst_13 : AddCommMonoid M
inst_14 : Module R M
inst_15 : Free R M
d1 : finrank R M = 1
c d : R
⊢ HSMul.hSMul (β := M →ₗ[R] M) (c • d) LinearMap.id =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id)
have h : ∀ (x : M),
  Eq (α := M) ((HSMul.hSMul (β := M →ₗ[R] M) (c • d) LinearMap.id : (a : M) → M) x : M)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (HSMul.hSMul (β := M →ₗ[R] M) d LinearMap.id) :
          (a : M) → M)
        x :
      M)
Tactic: ext
-- 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 : IsEmpty ι
hV : Module.rank K V = 0
⊢ Subsingleton V
have obtain : ∀ (fst : Type v) (b : Basis fst K V), Subsingleton V
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
ι : Type u_1
inst_5 : IsEmpty ι
hV : Module.rank K V = 0
fst : Type v
b : Basis fst K V
⊢ Subsingleton V
have this : IsEmpty fst
Tactic: haveI := mk_eq_zero_iff.1 (hV ▸ 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
c : Cardinal.{v}
⊢ c ≤ Module.rank K V ↔ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
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
inst_4 : Free K V
c : Cardinal.{v}
this : Nontrivial K
⊢ c ≤ Module.rank K V ↔ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
have mp : c ≤ Module.rank K V → ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
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
c : Cardinal.{v}
this : Nontrivial K
mp : c ≤ Module.rank K V → ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
⊢ c ≤ Module.rank K V ↔ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
have mpr : (∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s) → c ≤ Module.rank 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
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
⊢ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
have mp : ∀ (κ : Type v) (t' : Basis κ K V), ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
Tactic: obtain ⟨κ, t'⟩ := 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
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range (ι := κ) (⇑t' : (a : κ) → V)) : Type v) K V := t'.reindexRange
⊢ LinearIndepOn.{v, u, v} (ι := V) K id (range (ι := κ) (⇑t' : (a : κ) → V))
have h₁ : Eq.{v + 1} (α := Set V) (range (ι := κ) (⇑t' : (a : κ) → V))
  (range (ι := (↑(range (ι := κ) (⇑t' : (a : κ) → V)) : Type v))
    (⇑t : (a : (↑(range (⇑t' : (a : κ) → V)) : Type v)) → V))
Tactic: convert! t.linearIndependent.linearIndepOn_id
-- 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
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range (ι := κ) (⇑t' : (a : κ) → V)) : Type v) K V := t'.reindexRange
⊢ Eq.{v + 1} (α := Set V) (range (ι := κ) (⇑t' : (a : κ) → V))
    (range (ι := (↑(range (ι := κ) (⇑t' : (a : κ) → V)) : Type v))
      (⇑t : (a : (↑(range (⇑t' : (a : κ) → V)) : Type v)) → V))
have h₁ : ∀ (x : V),
  Membership.mem (γ := Set V) (range (ι := κ) (⇑t' : (a : κ) → V)) x ↔
    Membership.mem (γ := Set V)
      (range (ι := (↑(range (ι := κ) (⇑t' : (a : κ) → V)) : Type v))
        (⇑t : (a : (↑(range (⇑t' : (a : κ) → V)) : Type v)) → V))
      x
Tactic: ext
-- 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
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range (ι := κ) (⇑t' : (a : κ) → V)) : Type v) K V := t'.reindexRange
⊢ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
have this₁ : LinearIndepOn.{v, u, v} (ι := V) K id (range (ι := κ) (⇑t' : (a : κ) → V))
Tactic: have : LinearIndepOn K id (Set.range t') := by
      convert! t.linearIndependent.linearIndepOn_id
      ext
      simp [t]
-- 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
c : Cardinal.{v}
this_1 : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range (ι := κ) (⇑t' : (a : κ) → V)) : Type v) K V := t'.reindexRange
this : LinearIndepOn.{v, u, v} (ι := V) K id (range (ι := κ) (⇑t' : (a : κ) → V))
⊢ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
have h₁ : ∃ p ⊆ range (ι := κ) (⇑t' : (a : κ) → V), #(↑p : Type v) = c
Tactic: rw [← t.mk_eq_rank'', le_mk_iff_exists_subset] at h
Cleared hypotheses: h, t, 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
c : Cardinal.{v}
this_1 : Nontrivial K
κ : Type v
t' : Basis κ K V
h : ∃ p ⊆ range (ι := κ) (⇑t' : (a : κ) → V), #(↑p : Type v) = c
t : Basis (↑(range (ι := κ) (⇑t' : (a : κ) → V)) : Type v) K V := t'.reindexRange
this : LinearIndepOn.{v, u, v} (ι := V) K id (range (ι := κ) (⇑t' : (a : κ) → V))
⊢ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
have mp : ∀ (s : Set V) (hst : s ⊆ range (ι := κ) (⇑t' : (a : κ) → V)) (hsc : #(↑s : Type v) = c),
  ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
Tactic: rcases h with ⟨s, hst, hsc⟩
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
n : ℕ
⊢ (↑n : Cardinal.{v}) ≤ Module.rank K V ↔
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K
          (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))
have simp : (∃ (s : Set V), (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn K id s) ↔
  ∃ (s : Finset V),
    s.card = n ∧
      LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K
        (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))
Tactic: simp only [le_rank_iff_exists_linearIndependent, mk_set_eq_nat_iff_finset]
-- 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
n : ℕ
⊢ (∃ (s : Set V), (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn K id s) ↔
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K
          (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))
have mp : (∃ (s : Set V), (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn K id s) →
  ∃ (s : Finset V),
    s.card = n ∧
      LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K
        (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set 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
n : ℕ
mp :
  (∃ (s : Set V), (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn K id s) →
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K
          (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))
⊢ (∃ (s : Set V), (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn K id s) ↔
    ∃ (s : Finset V),
      s.card = n ∧
        LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K
          (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))
have mpr : (∃ (s : Finset V),
    s.card = n ∧
      LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K
        (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))) →
  ∃ (s : Set V), (∃ (t : Finset V), (↑t : Set V) = s ∧ t.card = n) ∧ LinearIndepOn K id s
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
⊢ Module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
have obtain : ∀ (κ : Type v) (b : Basis κ K V), Module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
Tactic: obtain ⟨κ, b⟩ := 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
κ : Type v
b : Basis κ K V
⊢ Module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
have mp : Module.rank K V ≤ 1 → ∃ (v₀ : V), ∀ (v : V), ∃ (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
inst_4 : Free K V
κ : Type v
b : Basis κ K V
mp : Module.rank K V ≤ 1 → ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
⊢ Module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
have mpr : (∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v) → Module.rank K V ≤ 1
Tactic: constructor
-- 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
κ : Type v
b : Basis κ K V
hd : Module.rank K V ≤ 1
⊢ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
have hd₁ : Subsingleton κ
Tactic: rw [← b.mk_eq_rank'', le_one_iff_subsingleton] at hd
Cleared hypotheses: hd
-- 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 v
b : Basis κ K V
hd : Subsingleton κ
⊢ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
have mp : ∀ (hb : IsEmpty κ), ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
Tactic: rcases isEmpty_or_nonempty κ with hb | ⟨⟨i⟩⟩
-- 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 v
b : Basis κ K V
hd : Subsingleton κ
mp : ∀ (hb : IsEmpty κ), ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
⊢ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
have mp₁ : ∀ (i : κ), ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
Tactic: rcases isEmpty_or_nonempty κ with hb | ⟨⟨i⟩⟩
-- 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 v
b : Basis κ K V
hd : Subsingleton κ
hb : IsEmpty κ
⊢ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
have h : ∀ (v : V), ∃ (r : K), HSMul.hSMul (β := V) r 0 = v
Tactic: use 0
-- 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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
hb : IsEmpty κ
⊢ ∀ (v : V), ∃ (r : K), HSMul.hSMul (β := V) r 0 = v
have h' : ∀ (v : V), v = 0
Tactic: have h' : ∀ v : V, v = 0 := by
        simpa [range_eq_empty, Submodule.eq_bot_iff] using b.span_eq.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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
i : κ
⊢ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
have h : ∀ (v : V), ∃ (r : K), HSMul.hSMul (β := V) r ((b : (a : κ) → V) i : V) = v
Tactic: use b i
-- 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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
i : κ
⊢ ∀ (v : V), ∃ (r : K), HSMul.hSMul (β := V) r ((b : (a : κ) → V) i : V) = v
have h' : Eq (α := Submodule K V) (span K (singleton (α := V) ((b : (a : κ) → V) i : V))) ⊤
Tactic: have h' : K ∙ b i = ⊤ :=
        (subsingleton_range b).eq_singleton_of_mem (mem_range_self i) ▸ b.span_eq
-- 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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
i : κ
h' : Eq (α := Submodule K V) (span K (singleton (α := V) ((b : (a : κ) → V) i : V))) ⊤
v : V
⊢ ∃ (r : K), HSMul.hSMul (β := V) r ((b : (a : κ) → V) i : V) = v
have hv : Membership.mem (γ := Submodule K V) ⊤ v
Tactic: have hv : v ∈ (⊤ : Submodule K V) := mem_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 v
b : Basis κ K V
hd : Subsingleton κ
i : κ
h' : Eq (α := Submodule K V) (span K (singleton (α := V) ((b : (a : κ) → V) i : V))) ⊤
v : V
hv : Membership.mem (γ := Submodule K V) ⊤ v
⊢ ∃ (r : K), HSMul.hSMul (β := V) r ((b : (a : κ) → V) i : V) = v
have h : ∀ (hv : Membership.mem (γ := Submodule K V) (span K (singleton (α := V) ((b : (a : κ) → V) i : V))) v),
  ∃ (r : K), HSMul.hSMul (β := V) r ((b : (a : κ) → V) i : V) = v
Tactic: rwa [← h', mem_span_singleton] at hv
Cleared hypotheses: 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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
i : κ
h' : Eq (α := Submodule K V) (span K (singleton (α := V) ((b : (a : κ) → V) i : V))) ⊤
v : V
hv : Membership.mem (γ := Submodule K V) ⊤ v
h :
  ∀ (hv : Membership.mem (γ := Submodule K V) (span K (singleton (α := V) ((b : (a : κ) → V) i : V))) v),
    ∃ (r : K), HSMul.hSMul (β := V) r ((b : (a : κ) → V) i : V) = v
⊢ ∃ (r : K), HSMul.hSMul (β := V) r ((b : (a : κ) → V) i : V) = v
have h₁ : ∀ (hv : ∃ (a : K), HSMul.hSMul (β := V) a ((b : (a : κ) → V) i : V) = v),
  ∃ (r : K), HSMul.hSMul (β := V) r ((b : (a : κ) → V) i : V) = v
Tactic: rwa [← h', mem_span_singleton] at hv
Cleared hypotheses: 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
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ (r : K), r • v₀ = v
⊢ Eq (α := Submodule K V) (K ∙ v₀) ⊤
have h : ∀ (x : V), Membership.mem (γ := Submodule K V) (K ∙ v₀) x ↔ Membership.mem (γ := Submodule K V) ⊤ x
Tactic: ext
-- 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
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ (r : K), r • v₀ = v
⊢ Module.rank K V ≤ 1
have h : Eq (α := Submodule K V) (K ∙ v₀) ⊤
Tactic: have h : K ∙ v₀ = ⊤ := by
      ext
      simp [mem_span_singleton, 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
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ (r : K), r • v₀ = v
h : Eq (α := Submodule K V) (K ∙ v₀) ⊤
⊢ Module.rank K V ≤ 1
have mpr : Module.rank K ↥(K ∙ v₀) ≤ 1
Tactic: rw [← rank_top, ← 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
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ (r : K), r • v₀ = v
h : Eq (α := Submodule K V) (K ∙ v₀) ⊤
⊢ Module.rank K ↥(K ∙ v₀) ≤ 1
have mpr : #(↑{v₀} : Type v) = 1
Tactic: refine (rank_span_le _).trans_eq ?_
-- 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 ↔ ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = 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
inst_4 : Free K V
this : Nontrivial K
⊢ Module.rank K V = 1 ↔ ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
have refine_1 : ∀ (h : Module.rank K V = 1), ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
Tactic: refine ⟨fun h ↦ ?_, fun ⟨v₀, h, hv⟩ ↦ (rank_le_one_iff.2 ⟨v₀, hv⟩).antisymm ?_⟩
-- 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
refine_1 : ∀ (h : Module.rank K V = 1), ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
⊢ Module.rank K V = 1 ↔ ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
have refine_2 : (∃ (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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨v₀, h, hv⟩ ↦ (rank_le_one_iff.2 ⟨v₀, hv⟩).antisymm ?_⟩
-- 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 : Module.rank K V = 1
⊢ ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
have refine_1 : ∀ (v₀ : V) (hv : ∀ (v : V), ∃ (r : K), r • v₀ = v), ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
Tactic: obtain ⟨v₀, hv⟩ := rank_le_one_iff.1 h.le
-- 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 : Module.rank K V = 1
v₀ : V
hv : ∀ (v : V), ∃ (r : K), r • v₀ = v
⊢ ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
have refine_1 : ∀ (hzero : v₀ = 0), False
Tactic: refine ⟨v₀, fun hzero ↦ ?_, hv⟩
-- 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
hv : ∀ (v : V), ∃ (r : K), r • v₀ = v
hzero : v₀ = 0
⊢ False
have hv₁ : ∀ (v : V), 0 = v
Tactic: simp_rw [hzero, smul_zero, exists_const] at hv
Cleared hypotheses: hv