awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
b : Finset M
h : LinearIndependent R (M := M) fun (x : ↥b) ↦ (↑x : M)
⊢ Fintype.card.{v} ↥b ≤ finrank R M

Tactic:
exact h.fintype_card_le_finrank

Premises used: LinearIndependent.fintype_card_le_finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Module.Finite R M
v : ι → M
h : LinearIndependent R v
apply : lift.{v, w} #ι < lift.{v, w} ℵ₀
⊢ #ι < ℵ₀

Tactic:
apply Cardinal.lift_lt.1

Premises used: Cardinal.lift_lt, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Module.Finite R M
v : ι → M
h : LinearIndependent R v
hab : lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)
hbc : lift.{w, v} (Module.rank R M) < lift.{v, w} ℵ₀
b : Cardinal.{max w v}
⊢ lift.{v, w} #ι < lift.{v, w} ℵ₀

Tactic:
apply lt_of_le_of_lt

Premises used: lt_of_le_of_lt
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ lift.{v, w} #ι ≤ lift.{w, v} (Module.rank R M)

Tactic:
apply h.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Module.Finite R M
v : ι → M
h : LinearIndependent R v
hbc : (↑(finrank R M) : Cardinal.{max v w}) < ℵ₀
⊢ lift.{w, v} (Module.rank R M) < lift.{v, w} ℵ₀

Tactic:
rw [← finrank_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_natCast]

Premises used: Module.finrank_eq_rank, Cardinal.lift_natCast, Cardinal.lift_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type w
inst_4 : Module.Finite R M
v : ι → M
h : LinearIndependent R v
⊢ (↑(finrank R M) : Cardinal.{max v w}) < ℵ₀

Tactic:
apply Cardinal.natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
ι : Type u_1
f : ι → M
h : LinearIndependent R f
⊢ Finite ι

Tactic:
Cardinal.lt_aleph0_iff_finite.1 <| h.lt_aleph0_of_finite

Premises used: Cardinal.lt_aleph0_iff_finite, LinearIndependent.lt_aleph0_of_finite, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
b : Set M
h : LinearIndependent R (M := M) fun (x : (↑b : Type v)) ↦ (↑x : M)
⊢ b.Finite

Tactic:
Cardinal.lt_aleph0_iff_set_finite.mp h.lt_aleph0_of_finite

Premises used: LinearIndependent.lt_aleph0_of_finite, Iff.mp, Cardinal.lt_aleph0_iff_set_finite
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
inl : ∀ (h : (↑n : Cardinal.{v}) = Module.rank R M), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
inr : ∀ (h : (↑n : Cardinal.{v}) < Module.rank R M), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
rcases hn.eq_or_lt with h | h

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
inl :
  ∀ (s : Set M) (hs : LinearIndepOn R id s)
    (hs' :
      #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) =
        ⨆ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v)),
    ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
obtain ⟨⟨s, hs⟩, hs'⟩ := exists_eq_ciSup_of_not_isSuccLimit
      Cardinal.bddAbove_of_small (h.trans (Module.rank_def R M) ▸ not_isSuccLimit_natCast n)

Premises used: exists_eq_ciSup_of_not_isSuccLimit, Cardinal.bddAbove_of_small
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' :
  #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) =
    ⨆ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v)
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) = (↑n : Cardinal.{v})

Tactic:
rw [← Module.rank_def, ← h] at hs'

Premises used: Module.rank_def
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) = (↑n : Cardinal.{v})
⊢ Finite.{v + 1} (↑s : Type v)

Tactic:
have : Finite s := lt_aleph0_iff_finite.mp (hs' ▸ natCast_lt_aleph0)
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) = (↑n : Cardinal.{v})
this : Finite.{v + 1} (↑s : Type v)
inl : ∀ (val : Fintype (↑s : Type v)), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
cases nonempty_fintype s

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) = (↑n : Cardinal.{v})
this : Finite.{v + 1} (↑s : Type v)
val : Fintype (↑s : Type v)
⊢ s.toFinset.card = n

Tactic:
simpa using hs'
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) = (↑n : Cardinal.{v})
this : Finite.{v + 1} (↑s : Type v)
val : Fintype (↑s : Type v)
⊢ LinearIndepOn R id (↑s.toFinset : Set M)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type v) = (↑n : Cardinal.{v})
this : Finite.{v + 1} (↑s : Type v)
val : Fintype (↑s : Type v)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
refine ⟨s.toFinset, by simpa using hs', by simpa⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) < Module.rank R M
inr :
  ∀ (s : Set M) (hs : #(↑s : Type v) = (↑n : Cardinal.{v})) (hs' : LinearIndepOn R id s),
    ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_set_linearIndependent_of_lt_rank h

Premises used: Module.exists_set_linearIndependent_of_lt_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) < Module.rank R M
s : Set M
hs : #(↑s : Type v) = (↑n : Cardinal.{v})
hs' : LinearIndepOn R id s
⊢ Finite.{v + 1} (↑s : Type v)

Tactic:
have : Finite s := lt_aleph0_iff_finite.mp (hs ▸ natCast_lt_aleph0)
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) < Module.rank R M
s : Set M
hs : #(↑s : Type v) = (↑n : Cardinal.{v})
hs' : LinearIndepOn R id s
this : Finite.{v + 1} (↑s : Type v)
inr : ∀ (val : Fintype (↑s : Type v)), ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
cases nonempty_fintype s

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) < Module.rank R M
s : Set M
hs : #(↑s : Type v) = (↑n : Cardinal.{v})
hs' : LinearIndepOn R id s
this : Finite.{v + 1} (↑s : Type v)
val : Fintype (↑s : Type v)
⊢ s.toFinset.card = n

Tactic:
simpa using hs
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) < Module.rank R M
s : Set M
hs : #(↑s : Type v) = (↑n : Cardinal.{v})
hs' : LinearIndepOn R id s
this : Finite.{v + 1} (↑s : Type v)
val : Fintype (↑s : Type v)
⊢ LinearIndepOn R id (↑s.toFinset : Set M)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
h : (↑n : Cardinal.{v}) < Module.rank R M
s : Set M
hs : #(↑s : Type v) = (↑n : Cardinal.{v})
hs' : LinearIndepOn R id s
this : Finite.{v + 1} (↑s : Type v)
val : Fintype (↑s : Type v)
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndepOn R id (↑s : Set M)

Tactic:
exact ⟨s.toFinset, by simpa using hs, by simpa⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : (↑n : Cardinal.{v}) ≤ Module.rank R M
⊢ ∃ (f : Fin n → M), LinearIndependent R f

Tactic:
have ⟨_, hs, hs'⟩ := exists_finset_linearIndependent_of_le_rank hn
  ⟨_, (linearIndependent_equiv (Finset.equivFinOfCardEq hs).symm).mpr hs'⟩

Premises used: Iff.mpr, Function.comp, Exists, id, linearIndependent_equiv, exists_finset_linearIndependent_of_le_rank, Finset.equivFinOfCardEq, LinearIndependent, Exists.intro, Equiv.symm, _private.0.exists_linearIndependent_of_le_rank.match_1, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
H : ∃ (f : Fin n → M), LinearIndependent R f
⊢ (↑n : Cardinal.{v}) ≤ Module.rank R M

Tactic:
simpa using H.choose_spec.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank, Exists.choose_spec
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
n : ℕ
h : ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
s : Finset M
h₁ : s.card = n
h₂ : LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ (↑n : Cardinal.{v}) ≤ Module.rank R M

Tactic:
simpa [h₁] using h₂.cardinal_le_rank

Premises used: LinearIndependent.cardinal_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
pos :
  ∀ (h : finrank R M = 0),
    ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
neg :
  ∀ (h : ¬finrank R M = 0),
    ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
by_cases h : finrank R M = 0

Premises used: Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
pos : ∃ (s : Finset M), s.card = 0 ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
rw [le_zero_iff.mp (hn.trans_eq h)]

Premises used: LE.le.trans_eq, le_zero_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ LinearIndependent R (M := M) fun (x : (↑∅ : Type v)) ↦ (↑x : M)

Tactic:
linearIndependent_empty R M

Premises used: linearIndependent_empty
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
h₁ : Eq.{v + 1} (α := M → Prop) (fun (x : M) ↦ Membership.mem (γ := Finset M) ∅ x) ∅
h₂ :
  ↥∅ = (↑∅ : Type v) →
    Eq.{v + 1} (α := M → Prop) (fun (x : M) ↦ Membership.mem (γ := Finset M) ∅ x) fun (x : M) ↦
      Membership.mem (γ := Set M) ∅ x
⊢ LinearIndependent.{v, u, v} (ι := ↥∅) R (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Finset M) ∅ x))

Tactic:
convert! linearIndependent_empty R M using 2

Premises used: linearIndependent_empty
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ Eq.{v + 1} (α := M → Prop) (fun (x : M) ↦ Membership.mem (γ := Finset M) ∅ x) ∅

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
e_1 : ↥∅ = (↑∅ : Type v)
⊢ Eq.{v + 1} (α := M → Prop) (fun (x : M) ↦ Membership.mem (γ := Finset M) ∅ x) fun (x : M) ↦
    Membership.mem (γ := Set M) ∅ x

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : finrank R M = 0
⊢ ∃ (s : Finset M), s.card = 0 ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
exact ⟨∅, rfl, by convert! linearIndependent_empty R M using 2 <;> aesop⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : ¬finrank R M = 0
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
exists_finset_linearIndependent_of_le_rank
    ((Nat.cast_le.mpr hn).trans_eq (cast_toNat_of_lt_aleph0 (toNat_ne_zero.mp h).2))

Premises used: Iff.mpr, LE.le.trans_eq, exists_finset_linearIndependent_of_le_rank, And.right, Iff.mp, Cardinal.cast_toNat_of_lt_aleph0, Nat.cast_le, Cardinal.toNat_ne_zero, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
h : ¬finrank R M = 0
⊢ ∃ (s : Finset M), s.card = n ∧ LinearIndependent.{v, u, v} (ι := ↥s) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))

Tactic:
exact exists_finset_linearIndependent_of_le_rank
    ((Nat.cast_le.mpr hn).trans_eq (cast_toNat_of_lt_aleph0 (toNat_ne_zero.mp h).2))

Premises used: Iff.mpr, LE.le.trans_eq, exists_finset_linearIndependent_of_le_rank, And.right, Iff.mp, Cardinal.cast_toNat_of_lt_aleph0, Nat.cast_le, Cardinal.toNat_ne_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
hn : n ≤ finrank R M
⊢ ∃ (f : Fin n → M), LinearIndependent R f

Tactic:
have ⟨_, hs, hs'⟩ := exists_finset_linearIndependent_of_le_finrank hn
  ⟨_, (linearIndependent_equiv (Finset.equivFinOfCardEq hs).symm).mpr hs'⟩

Premises used: Iff.mpr, Function.comp, Exists, exists_finset_linearIndependent_of_le_finrank, linearIndependent_equiv, Finset.equivFinOfCardEq, LinearIndependent, Exists.intro, _private.0.exists_linearIndependent_of_le_finrank.match_1, Equiv.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : StrongRankCondition R
ι : Type u_1
inst_5 : Infinite ι
v : ι → M
⊢ ¬LinearIndependent R v

Tactic:
mt LinearIndependent.finite <| @not_finite _ _

Premises used: mt, LinearIndependent.finite, not_finite
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
set :
  let I := { i : ι // V i ≠ ⊥ };
  lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
⊢ lift.{v, w} #{ i : ι // V i ≠ ⊥ } ≤ lift.{w, v} (Module.rank R M)

Tactic:
set I := { i : ι // V i ≠ ⊥ }
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
i : I
rw : V (↑i : ι) ≠ ⊥
⊢ ∃ v ∈ V (↑i : ι), v ≠ 0

Tactic:
rw [← Submodule.ne_bot_iff]

Premises used: Submodule.ne_bot_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
i : I
⊢ V (↑i : ι) ≠ ⊥

Tactic:
i.prop

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
i : I
⊢ V (↑i : ι) ≠ ⊥

Tactic:
exact i.prop

Premises used: Subtype.prop
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
⊢ ∀ (i : I), ∃ v ∈ V (↑i : ι), v ≠ 0

Tactic:
have hI : ∀ i : I, ∃ v ∈ V i, v ≠ (0 : M) := by
    intro i
    rw [← Submodule.ne_bot_iff]
    exact i.prop
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
hI : ∀ (i : I), ∃ v ∈ V (↑i : ι), v ≠ 0
choose :
  ∀ (v : (i : I) → M) (hvV : ∀ (i : I), v i ∈ V (↑i : ι)) (hv : ∀ (i : I), v i ≠ 0),
    lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Tactic:
choose v hvV hv using hI
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
v : (i : I) → M
hvV : ∀ (i : I), v i ∈ V (↑i : ι)
hv : ∀ (i : I), v i ≠ 0
⊢ LinearIndependent R v

Tactic:
have : LinearIndependent R v := (hV.comp Subtype.coe_injective).linearIndependent _ hvV hv
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
v : (i : I) → M
hvV : ∀ (i : I), v i ∈ V (↑i : ι)
hv : ∀ (i : I), v i ≠ 0
this : LinearIndependent R v
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Tactic:
this.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
V : ι → Submodule R M
hV : iSupIndep V
I : Type w := { i : ι // V i ≠ ⊥ }
v : (i : I) → M
hvV : ∀ (i : I), v i ∈ V (↑i : ι)
hv : ∀ (i : I), v i ≠ 0
this : LinearIndependent R v
⊢ lift.{v, w} #I ≤ lift.{w, v} (Module.rank R M)

Tactic:
exact this.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
this : lift.{v, w} #{ i : ι // p i ≠ ⊥ } ≤ lift.{v, w} (↑(finrank R M) : Cardinal.{w})
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : #{ i : ι // p i ≠ ⊥ } ≤ (↑(finrank R M) : Cardinal.{w})),
    #{ i : ι // p i ≠ ⊥ } ≤ (↑(finrank R M) : Cardinal.{w})
⊢ #{ i : ι // p i ≠ ⊥ } ≤ (↑(finrank R M) : Cardinal.{w})

Tactic:
rwa [Cardinal.lift_le] at this

Premises used: Cardinal.lift_le
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
suffices : lift.{v, w} #{ i : ι // p i ≠ ⊥ } ≤ lift.{v, w} (↑(finrank R M) : Cardinal.{w})
⊢ #{ i : ι // p i ≠ ⊥ } ≤ (↑(finrank R M) : Cardinal.{w})

Tactic:
suffices Cardinal.lift.{v} #{ i // p i ≠ ⊥ } ≤ Cardinal.lift.{v} (finrank R M : Cardinal.{w}) by
    rwa [Cardinal.lift_le] at this
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
⊢ lift.{v, w} #{ i : ι // p i ≠ ⊥ } ≤ lift.{w, v} (Module.rank R M)

Tactic:
hp.subtype_ne_bot_le_rank

Premises used: iSupIndep.subtype_ne_bot_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
ι : Type w
R : Type u
M : Type v
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Module.Finite R M
inst_6 : StrongRankCondition R
p : ι → Submodule R M
hp : iSupIndep p
rw rw₁ : lift.{w, v} (Module.rank R M) = lift.{w, v} (Module.rank R M)
⊢ lift.{w, v} (Module.rank R M) = lift.{w, v} (↑(finrank R M) : Cardinal.{v})

Tactic:
rw [finrank_eq_rank]

Premises used: Module.finrank_eq_rank