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
c : Cardinal.{v}
this : Nontrivial K
mp : c ≤ Module.rank K V → ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
mpr : (∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s) → c ≤ Module.rank K V
⊢ c ≤ Module.rank K V ↔ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s

Tactic:
constructor
-- 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
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
mp : ∀ (κ : Type v) (t' : Basis κ K V), ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s
⊢ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s

Tactic:
obtain ⟨κ, t'⟩ := 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
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 (ι := (↑(range (ι := κ) (⇑t' : (a : κ) → V)) : Type v))
      (⇑t : (a : (↑(range (⇑t' : (a : κ) → V)) : Type v)) → V))

Tactic:
t.linearIndependent.linearIndepOn_id

Premises used: LinearIndependent.linearIndepOn_id, Module.Basis.linearIndependent
-- 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
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
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))
⊢ LinearIndepOn.{v, u, v} (ι := V) K id (range (ι := κ) (⇑t' : (a : κ) → V))

Tactic:
convert! t.linearIndependent.linearIndepOn_id

Premises used: LinearIndependent.linearIndepOn_id, Module.Basis.linearIndependent
-- 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
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
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
⊢ 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:
ext
-- 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
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
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:
simp [t]
-- 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
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))

Tactic:
have : LinearIndepOn K id (Set.range t') := by
      convert! t.linearIndependent.linearIndepOn_id
      ext
      simp [t]
-- 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
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))
⊢ ∃ p ⊆ range (ι := κ) (⇑t' : (a : κ) → V), #(↑p : Type v) = c

Tactic:
rw [← t.mk_eq_rank'', le_mk_iff_exists_subset] at h

Premises used: Cardinal.le_mk_iff_exists_subset, Module.Basis.mk_eq_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 : 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))
h₁ : ∃ p ⊆ range (ι := κ) (⇑t' : (a : κ) → V), #(↑p : Type v) = c
⊢ LinearIndepOn.{v, u, v} (ι := V) K id (range (ι := κ) (⇑t' : (a : κ) → V))

Tactic:
rw [← t.mk_eq_rank'', le_mk_iff_exists_subset] at h

Premises used: Cardinal.le_mk_iff_exists_subset, Module.Basis.mk_eq_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 : 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))
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
⊢ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s

Tactic:
rcases h with ⟨s, hst, hsc⟩
-- 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
c : Cardinal.{v}
this_1 : Nontrivial K
κ : 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
hst : s ⊆ range (ι := κ) (⇑t' : (a : κ) → V)
hsc : #(↑s : Type v) = c
⊢ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s

Tactic:
⟨s, hsc, this.mono hst⟩

Premises used: LinearIndepOn.mono, And.intro, Exists.intro
-- 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
c : Cardinal.{v}
this_1 : Nontrivial K
κ : 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
hst : s ⊆ range (ι := κ) (⇑t' : (a : κ) → V)
hsc : #(↑s : Type v) = c
⊢ ∃ (s : Set V), #(↑s : Type v) = c ∧ LinearIndepOn K id s

Tactic:
exact ⟨s, hsc, this.mono hst⟩
-- 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
this : Nontrivial K
s : Set V
si : LinearIndepOn K id s
⊢ #(↑s : Type v) ≤ Module.rank K V

Tactic:
si.cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_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 : Free K V
this : Nontrivial K
s : Set V
si : LinearIndepOn K id s
⊢ #(↑s : Type v) ≤ Module.rank K V

Tactic:
exact si.cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_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 : Free K V
n : ℕ
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)))
⊢ (↑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)))

Tactic:
simp only [le_rank_iff_exists_linearIndependent, mk_set_eq_nat_iff_finset]

Premises used: le_rank_iff_exists_linearIndependent, Cardinal.mk_set_eq_nat_iff_finset
-- 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
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)))
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
⊢ (∃ (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
-- 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
t : Finset V
si : LinearIndepOn K id (↑t : Set V)
⊢ ∃ (s : Finset V),
    s.card = t.card ∧
      LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K
        (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))

Tactic:
⟨t, rfl, si⟩

Premises used: And.intro, Exists.intro, rfl
-- 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
t : Finset V
si : LinearIndepOn K id (↑t : Set V)
⊢ ∃ (s : Finset V),
    s.card = t.card ∧
      LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K
        (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))

Tactic:
exact ⟨t, rfl, si⟩
-- 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
s : Finset V
si :
  LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))
⊢ ∃ (s_1 : Set V), (∃ (t : Finset V), (↑t : Set V) = s_1 ∧ t.card = s.card) ∧ LinearIndepOn K id s_1

Tactic:
⟨s, ⟨s, rfl, rfl⟩, si⟩

Premises used: SetLike.coe, And.intro, Exists.intro, rfl
-- 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
s : Finset V
si :
  LinearIndependent.{v, u, v} (ι := { x : V // x ∈ (↑s : Set V) }) K (Subtype.val (p := fun (x : V) ↦ x ∈ (↑s : Set V)))
⊢ ∃ (s_1 : Set V), (∃ (t : Finset V), (↑t : Set V) = s_1 ∧ t.card = s.card) ∧ LinearIndepOn K id s_1

Tactic:
exact ⟨s, ⟨s, rfl, rfl⟩, si⟩
-- 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
obtain : ∀ (κ : Type v) (b : Basis κ K V), 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

Tactic:
obtain ⟨κ, b⟩ := 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
κ : Type v
b : Basis κ K V
mp : Module.rank K V ≤ 1 → ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
mpr : (∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v) → Module.rank K V ≤ 1
⊢ Module.rank K V ≤ 1 ↔ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v

Tactic:
constructor
-- 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
κ : Type v
b : Basis κ K V
hd : Module.rank K V ≤ 1
⊢ Subsingleton κ

Tactic:
rw [← b.mk_eq_rank'', le_one_iff_subsingleton] at hd

Premises used: Cardinal.le_one_iff_subsingleton, Module.Basis.mk_eq_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 : Free K V
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
mp : ∀ (hb : IsEmpty κ), ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
mp₁ : ∀ (i : κ), ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v
⊢ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v

Tactic:
rcases isEmpty_or_nonempty κ with hb | ⟨⟨i⟩⟩

Premises used: isEmpty_or_nonempty
-- 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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
hb : IsEmpty κ
h : ∀ (v : V), ∃ (r : K), HSMul.hSMul (β := V) r 0 = v
⊢ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v

Tactic:
use 0
-- 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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
hb : IsEmpty κ
⊢ ∀ (v : V), v = 0

Tactic:
simpa [range_eq_empty, Submodule.eq_bot_iff] using b.span_eq.symm

Premises used: Submodule.eq_bot_iff, Set.range_eq_empty, Module.Basis.span_eq, Eq.symm
-- 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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
hb : IsEmpty κ
⊢ ∀ (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
-- 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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
hb : IsEmpty κ
h' : ∀ (v : V), v = 0
v : V
⊢ ∃ (r : K), HSMul.hSMul (β := V) r 0 = v

Tactic:
simp [h' v]
-- 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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
i : κ
h : ∀ (v : V), ∃ (r : K), HSMul.hSMul (β := V) r ((b : (a : κ) → V) i : V) = v
⊢ ∃ (v₀ : V), ∀ (v : V), ∃ (r : K), r • v₀ = v

Tactic:
use b i

Premises used: DFunLike.coe
-- 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
κ : Type v
b : Basis κ K V
hd : Subsingleton κ
i : κ
⊢ 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
-- 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
κ : 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
⊢ Membership.mem (γ := Submodule K V) ⊤ v

Tactic:
have hv : v ∈ (⊤ : Submodule K V) := mem_top
-- 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
κ : 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
h₁ h₂ h₃ 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
⊢ ∃ (r : K), HSMul.hSMul (β := V) r ((b : (a : κ) → V) i : V) = v

Tactic:
rwa [← h', mem_span_singleton] at hv

Premises used: Submodule.mem_span_singleton
-- 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
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ (r : K), r • v₀ = v
h : ∀ (x : V), Membership.mem (γ := Submodule K V) (K ∙ v₀) x ↔ Membership.mem (γ := Submodule K V) ⊤ x
⊢ Eq (α := Submodule K V) (K ∙ v₀) ⊤

Tactic:
ext
-- 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
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ (r : K), r • v₀ = v
x : V
⊢ Membership.mem (γ := Submodule K V) (K ∙ v₀) x ↔ Membership.mem (γ := Submodule K V) ⊤ x

Tactic:
simp [mem_span_singleton, hv₀]

Premises used: Submodule.mem_span_singleton
-- 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
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ (r : K), r • v₀ = v
⊢ Eq (α := Submodule K V) (K ∙ v₀) ⊤

Tactic:
have h : K ∙ v₀ = ⊤ := by
      ext
      simp [mem_span_singleton, hv₀]
-- 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
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ (r : K), r • v₀ = v
h : Eq (α := Submodule K V) (K ∙ v₀) ⊤
mpr : Module.rank K ↥(K ∙ v₀) ≤ 1
⊢ Module.rank K V ≤ 1

Tactic:
rw [← rank_top, ← h]

Premises used: rank_top
-- 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
κ : 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

Tactic:
(rank_span_le _).trans_eq ?_

Premises used: LE.le.trans_eq, rank_span_le
-- 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
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ (r : K), r • v₀ = v
h : Eq (α := Submodule K V) (K ∙ v₀) ⊤
mpr : #(↑{v₀} : Type v) = 1
⊢ Module.rank K ↥(K ∙ v₀) ≤ 1

Tactic:
refine (rank_span_le _).trans_eq ?_

Premises used: LE.le.trans_eq, rank_span_le
-- 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
κ : Type v
b : Basis κ K V
v₀ : V
hv₀ : ∀ (v : V), ∃ (r : K), r • v₀ = v
h : Eq (α := Submodule K V) (K ∙ v₀) ⊤
⊢ #(↑{v₀} : Type v) = 1

Tactic:
simp
-- 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
⊢ 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
this : Nontrivial K
⊢ Module.rank K V = 1 ↔ ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v

Tactic:
⟨fun h ↦ ?_, fun ⟨v₀, h, hv⟩ ↦ (rank_le_one_iff.2 ⟨v₀, hv⟩).antisymm ?_⟩

Premises used: Iff.mpr, LE.le.antisymm, Iff.intro, Exists.intro, _private.0.rank_eq_one_iff.match_1, Module.rank, OfNat.ofNat, rank_le_one_iff, Eq
-- 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
this : Nontrivial K
refine_1 : ∀ (h : Module.rank K V = 1), ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v
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
⊢ 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 ?_⟩
-- 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
this : Nontrivial K
h : Module.rank K V = 1
refine_1 : ∀ (v₀ : V) (hv : ∀ (v : V), ∃ (r : K), r • v₀ = v), ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (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

Premises used: Eq.le, Iff.mp, rank_le_one_iff
-- 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
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

Tactic:
⟨v₀, fun hzero ↦ ?_, hv⟩

Premises used: And.intro, Exists.intro
-- 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
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hv : ∀ (v : V), ∃ (r : K), r • v₀ = v
refine_1 : ∀ (hzero : v₀ = 0), False
⊢ ∃ (v₀ : V), v₀ ≠ 0 ∧ ∀ (v : V), ∃ (r : K), r • v₀ = v

Tactic:
refine ⟨v₀, fun hzero ↦ ?_, hv⟩