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
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hv : ∀ (v : V), ∃ (r : K), r • v₀ = v
hzero : v₀ = 0
⊢ ∀ (v : V), 0 = v

Tactic:
simp_rw [hzero, smul_zero, exists_const] at hv

Premises used: smul_zero, exists_const
-- 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
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
x x_1 : V
⊢ x = x_1

Tactic:
simp_rw [← 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
this : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
⊢ Subsingleton V

Tactic:
haveI : Subsingleton V := .intro fun _ _ ↦ by simp_rw [← 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
this_1 : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
this : Subsingleton V
⊢ False

Tactic:
one_ne_zero (h ▸ rank_subsingleton' K V)

Premises used: one_ne_zero
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
this_1 : Nontrivial K
h : Module.rank K V = 1
v₀ : V
hzero : v₀ = 0
hv : ∀ (v : V), 0 = v
this : Subsingleton V
⊢ False

Tactic:
exact one_ne_zero (h ▸ rank_subsingleton' K V)

Premises used: one_ne_zero
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : Free K V
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
refine_2 : ∀ (H : ¬1 ≤ Module.rank K V), False
⊢ 1 ≤ Module.rank K V

Tactic:
by_contra H
-- 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_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
⊢ Module.rank K V = 0

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

Premises used: not_le, Cardinal.lt_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_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
refine_2 : ∀ (κ : Type v) (b : Basis κ K V), False
⊢ False

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
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
⊢ IsEmpty κ

Tactic:
haveI := mk_eq_zero_iff.1 (H ▸ b.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
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 κ
⊢ Subsingleton V

Tactic:
haveI := b.repr.toEquiv.subsingleton
-- 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_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_2 : IsEmpty κ
this : Subsingleton V
⊢ False

Tactic:
h (Subsingleton.elim _ _)

Premises used: Subsingleton.elim
-- 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_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_2 : IsEmpty κ
this : Subsingleton V
⊢ False

Tactic:
exact h (Subsingleton.elim _ _)

Premises used: Subsingleton.elim
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
simp_rw : (∃ (v₀ : ↥s), ∀ (v : ↥s), ∃ (r : K), r • v₀ = v) ↔ ∃ v₀ ∈ s, ∀ v ∈ s, ∃ (r : K), r • v₀ = v
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀

Tactic:
simp_rw [rank_le_one_iff, le_span_singleton_iff]

Premises used: Submodule.le_span_singleton_iff, 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
⊢ (∃ (v₀ : ↥s), ∀ (v : ↥s), ∃ (r : K), r • v₀ = v) ↔ ∃ v₀ ∈ s, ∀ v ∈ s, ∃ (r : K), r • v₀ = v

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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
simp_rw : (∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ v ∈ s, ∃ (r : K), r • v₀ = v
⊢ Module.rank K ↥s = 1 ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ s ≤ K ∙ v₀

Tactic:
simp_rw [rank_eq_one_iff, le_span_singleton_iff]

Premises used: rank_eq_one_iff, Submodule.le_span_singleton_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
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
⊢ ¬Subtype.mk (p := fun (x : V) ↦ x ∈ s) 0 ⋯ = 0

Tactic:
simp only [h', ne_eq] at H

Premises used: ne_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
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 : ↥s), ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = v
h' : v₀ = 0
H : ¬Subtype.mk (p := fun (x : V) ↦ x ∈ s) 0 ⋯ = 0
⊢ False

Tactic:
H rfl

Premises used: 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
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 : ↥s), ∃ (r : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = v
h' : v₀ = 0
H : ¬Subtype.mk (p := fun (x : V) ↦ x ∈ s) 0 ⋯ = 0
⊢ False

Tactic:
exact H rfl

Premises used: 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
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (h' : v₀ = 0), v₀ = 0
⊢ v₀ = 0

Tactic:
rwa [AddSubmonoid.mk_eq_zero] at h'

Premises used: AddSubmonoid.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
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
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
⊢ (∃ (v₀ : ↥s), v₀ ≠ 0 ∧ ∀ (v : ↥s), ∃ (r : K), r • v₀ = v) ↔ ∃ v₀ ∈ s, v₀ ≠ 0 ∧ ∀ 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⟩ ↦ ?_⟩⟩
-- 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
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
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
⊢ ∃ (r : K), r • v₀ = v

Tactic:
obtain ⟨r, hr⟩ := h ⟨v, hv⟩

Premises used: Subtype.mk
-- 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
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
rwa₁ rwa₂ rwa₃ 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

Tactic:
rwa [Subtype.ext_iff, coe_smul] at hr

Premises used: Subtype.ext_iff, Submodule.coe_smul
-- 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
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 : K), r • v₀ = v

Tactic:
exact ⟨r, by rwa [Subtype.ext_iff, coe_smul] at hr⟩
-- 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
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
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
⊢ ∃ (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
-- 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
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)
rwa₁ rwa₂ rwa₃ 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

Tactic:
rwa [Subtype.ext_iff, coe_smul]

Premises used: Subtype.ext_iff, Submodule.coe_smul
-- 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
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 : K), r • Subtype.mk (p := fun (x : V) ↦ x ∈ s) v₀ hv₀ = Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv

Tactic:
exact ⟨r, by rwa [Subtype.ext_iff, coe_smul]⟩
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
⊢ 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
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₀
mpr : (∃ (v₀ : V), s ≤ K ∙ v₀) → Module.rank K ↥s ≤ 1
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ (v₀ : V), s ≤ K ∙ 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
this : Nontrivial K
mp : (∃ v₀ ∈ s, s ≤ K ∙ v₀) → ∃ (v₀ : V), s ≤ K ∙ v₀
⊢ Module.rank K ↥s ≤ 1 → ∃ (v₀ : V), s ≤ K ∙ v₀

Tactic:
rw [rank_submodule_le_one_iff]

Premises used: rank_submodule_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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
this : Nontrivial K
v₀ : V
left : v₀ ∈ s
h : s ≤ K ∙ v₀
⊢ ∃ (v₀ : V), s ≤ K ∙ v₀

Tactic:
⟨v₀, h⟩

Premises used: 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
this : Nontrivial K
v₀ : V
left : v₀ ∈ s
h : s ≤ K ∙ v₀
⊢ ∃ (v₀ : V), s ≤ K ∙ v₀

Tactic:
exact ⟨v₀, h⟩
-- 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
this : Nontrivial K
v₀ : V
h : s ≤ K ∙ v₀
mpr : ∀ (κ : Type v) (b : Basis κ K ↥s), Module.rank K ↥s ≤ 1
⊢ Module.rank K ↥s ≤ 1

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

Premises used: Membership.mem, Subtype, 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
s : Submodule K V
inst_4 : Free.{u, v} K ↥s
this : Nontrivial K
v₀ : V
h : s ≤ K ∙ v₀
κ : Type v
b : Basis κ K ↥s
⊢ Module.rank K ↥s ≤ 1

Tactic:
simpa [b.mk_eq_rank''] using b.linearIndependent.map' _ (ker_inclusion _ _ h)
      |>.cardinal_le_rank.trans (rank_span_le {v₀})

Premises used: LinearIndependent.cardinal_le_rank, LinearIndependent.map', Submodule.ker_inclusion, rank_span_le, Module.Basis.linearIndependent, LE.le.trans, Singleton.singleton, 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
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
simp : (∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v) ↔ ∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W
⊢ Module.rank K ↥W ≤ 1 ↔ W.IsPrincipal

Tactic:
simp only [rank_le_one_iff, Submodule.isPrincipal_iff, le_antisymm_iff, le_span_singleton_iff,
    span_singleton_le_iff_mem]

Premises used: Submodule.isPrincipal_iff, Submodule.le_span_singleton_iff, le_antisymm_iff, Submodule.span_singleton_le_iff_mem, 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
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
mpr : (∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W) → ∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v
⊢ (∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v) ↔ ∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W

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
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
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
⊢ ∃ (a : V), (∀ v ∈ W, ∃ (r : K), r • a = v) ∧ a ∈ W

Tactic:
choose f hf using hm'
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
m : V
hm : m ∈ W
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:
⟨m, ⟨fun v hv => ⟨f ⟨v, hv⟩, congr_arg ((↑) : W → V) (hf ⟨v, hv⟩)⟩, hm⟩⟩

Premises used: Subtype.mk, congr_arg, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
m : V
hm : m ∈ W
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:
exact ⟨m, ⟨fun v hv => ⟨f ⟨v, hv⟩, congr_arg ((↑) : W → V) (hf ⟨v, hv⟩)⟩, hm⟩⟩
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
a : V
h : ∀ v ∈ W, ∃ (r : K), r • a = v
ha : a ∈ W
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
⊢ ∃ (v₀ : ↥W), ∀ (v : ↥W), ∃ (r : K), r • v₀ = v

Tactic:
choose f hf using h
-- Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Goal:
K : Type u
V : Type v
inst : Ring K
inst_1 : StrongRankCondition K
inst_2 : AddCommGroup V
inst_3 : Module K V
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
a : V
ha : a ∈ W
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:
⟨⟨a, ha⟩, fun v => ⟨f v.1 v.2, Subtype.ext (hf v.1 v.2)⟩⟩

Premises used: Subtype.mk, Exists.intro, Subtype.val, Subtype.property, Subtype.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
W : Submodule K V
inst_4 : Free.{u, v} K ↥W
a : V
ha : a ∈ W
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:
exact ⟨⟨a, ha⟩, fun v => ⟨f v.1 v.2, Subtype.ext (hf v.1 v.2)⟩⟩
-- 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
⊢ Free.{u, v} K ↥⊤

Tactic:
haveI := Module.Free.of_equiv (topEquiv (R := K) (M := V)).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
this : Free.{u, v} K ↥⊤
rw : Module.rank K V ≤ 1 ↔ Module.rank K ↥⊤ ≤ 1
rw₁ rw₂ : Module.rank K V ≤ 1 ↔ Module.rank K V ≤ 1
⊢ Module.rank K V ≤ 1 ↔ Submodule.IsPrincipal.{u, v} (R := K) (M := V) ⊤

Tactic:
rw [← Submodule.rank_le_one_iff_isPrincipal, rank_top]

Premises used: Submodule.rank_le_one_iff_isPrincipal, 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 u_1
inst_5 : Unique ι
mp : finrank K V = 1 → Nonempty (Basis ι K V)
mpr : Nonempty (Basis ι K V) → finrank K V = 1
⊢ finrank K V = 1 ↔ Nonempty (Basis ι K 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 u_1
inst_5 : Unique ι
h : finrank K V = 1
⊢ Nonempty (Basis ι K V)

Tactic:
⟨Module.basisUnique ι h⟩

Premises used: Nonempty.intro, Module.basisUnique
-- 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 u_1
inst_5 : Unique ι
h : finrank K V = 1
⊢ Nonempty (Basis ι K V)

Tactic:
exact ⟨Module.basisUnique ι h⟩
-- 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 u_1
inst_5 : Unique ι
b : Basis ι K V
⊢ finrank K V = 1

Tactic:
simpa using finrank_eq_card_basis b

Premises used: Module.finrank_eq_card_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
rw : finrank K V = 1 ↔ Module.rank K V = 1
⊢ finrank K V = 1 ↔ ∃ (v : V), v ≠ 0 ∧ ∀ (w : V), ∃ (c : K), c • v = w

Tactic:
rw [← rank_eq_one_iff]

Premises used: rank_eq_one_iff