awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
V : Type v
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
rw : lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)
⊢ lift.{u, v} (Module.rank K V) < Module.rank K (V →ₗ[K] K)

Tactic:
rw [rank_dual_eq_card_dual_of_aleph0_le_rank h, ← rank_dual_eq_card_dual_of_aleph0_le_rank' h]

Premises used: rank_dual_eq_card_dual_of_aleph0_le_rank', rank_dual_eq_card_dual_of_aleph0_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
V : Type v
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
lift_rank_lt_rank_dual' h

Premises used: lift_rank_lt_rank_dual'
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
V : Type v
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
exact lift_rank_lt_rank_dual' h

Premises used: lift_rank_lt_rank_dual'
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, u} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
lift_rank_lt_rank_dual' h

Premises used: lift_rank_lt_rank_dual'
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
h₁ : Module.rank K V = lift.{u, u} (Module.rank K V)
⊢ Module.rank K V < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
convert! lift_rank_lt_rank_dual' h

Premises used: lift_rank_lt_rank_dual'
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K : Type u
inst : DivisionRing K
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
h₁ h₂ : Module.rank K V = Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)

Tactic:
rw [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K V : Type u
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, u} (Module.rank K V) < Module.rank K (V →ₗ[K] K)

Tactic:
lift_rank_lt_rank_dual h

Premises used: lift_rank_lt_rank_dual
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K V : Type u
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
h₁ : Module.rank K V = lift.{u, u} (Module.rank K V)
⊢ Module.rank K V < Module.rank K (V →ₗ[K] K)

Tactic:
convert! lift_rank_lt_rank_dual h

Premises used: lift_rank_lt_rank_dual
-- Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
Goal:
K V : Type u
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ℵ₀ ≤ Module.rank K V
h₁ h₂ : Module.rank K V = Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)

Tactic:
rw [lift_id]

Premises used: Cardinal.lift_id
-- 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 : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
s : Set M
li : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
H₁ : ∀ (s_1 : Finset (↑s : Type v)), s_1.card ≤ n
⊢ #(↑s : Type v) ≤ (↑n : Cardinal.{v})

Tactic:
apply Cardinal.card_le_of

Premises used: Cardinal.card_le_of
-- 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 : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
s : Set M
li : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
t : Finset (↑s : Type v)
H₁ : (Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t).card ≤ n
⊢ t.card ≤ n

Tactic:
rw [← Finset.card_map (Embedding.subtype (· ∈ s))]

Premises used: Finset.card_map, Membership.mem, Function.Embedding.subtype
-- 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 : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
s : Set M
li : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
t : Finset (↑s : Type v)
H₁ : LinearIndependent R (M := M) fun (i : ↥(Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t)) ↦ (↑i : M)
⊢ (Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t).card ≤ n

Tactic:
apply H
-- 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 : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
s : Set M
li : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
t : Finset (↑s : Type v)
⊢ LinearIndependent R (M := M) fun (i : ↥(Finset.map (Embedding.subtype fun (x : M) ↦ x ∈ s) t)) ↦ (↑i : M)

Tactic:
apply linearIndependent_finset_map_embedding_subtype _ li

Premises used: linearIndependent_finset_map_embedding_subtype
-- 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 : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
rw :
  LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
    (↑n : Cardinal.{v})
⊢ Module.rank R M ≤ (↑n : Cardinal.{v})

Tactic:
rw [Module.rank_def]

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 : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
h : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type v) ≤ (↑n : Cardinal.{v})
⊢ LE.le.{v + 1} (α := Cardinal.{v}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type v))
    (↑n : Cardinal.{v})

Tactic:
apply ciSup_le'

Premises used: ciSup_le'
-- 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 : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
s : Set M
li : LinearIndepOn R id s
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s li) : Set M) : Type v) ≤ (↑n : Cardinal.{v})

Tactic:
linearIndependent_bounded_of_finset_linearIndependent_bounded H _ li

Premises used: linearIndependent_bounded_of_finset_linearIndependent_bounded
-- 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 : ℕ
H : ∀ (s : Finset M), (LinearIndependent R (M := M) fun (i : ↥s) ↦ (↑i : M)) → s.card ≤ n
s : Set M
li : LinearIndepOn R id s
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s li) : Set M) : Type v) ≤ (↑n : Cardinal.{v})

Tactic:
exact linearIndependent_bounded_of_finset_linearIndependent_bounded H _ li

Premises used: linearIndependent_bounded_of_finset_linearIndependent_bounded
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Nontrivial R
mp : Module.rank R M = 0 → ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
mpr : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) → Module.rank R M = 0
⊢ Module.rank R M = 0 ↔ ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Nontrivial R
mp : (∃ (x : M), ∀ (a : R) (_ : a ≠ 0), a • x ≠ 0) → Module.rank R M ≠ 0
⊢ Module.rank R M = 0 → ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0

Tactic:
contrapose!
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Nontrivial R
x : M
hx : ∀ (a : R) (_ : a ≠ 0), a • x ≠ 0
mp : 1 ≤ Module.rank R M
⊢ Module.rank R M ≠ 0

Tactic:
rw [← Cardinal.one_le_iff_ne_zero]

Premises used: Cardinal.one_le_iff_ne_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Nontrivial R
x : M
hx : ∀ (a : R) (_ : a ≠ 0), a • x ≠ 0
⊢ LinearIndependent.{0, u_1, u_2} R (M := M) fun (x_1 : Unit) ↦ x

Tactic:
have : LinearIndependent R (fun _ : Unit ↦ x) :=
      linearIndependent_iff.mpr (fun l hl ↦ Finsupp.unique_ext <| not_not.mp fun H ↦
        hx _ H ((Finsupp.linearCombination_unique _ _ _).symm.trans hl))
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Nontrivial R
x : M
hx : ∀ (a : R) (_ : a ≠ 0), a • x ≠ 0
this : LinearIndependent.{0, u_1, u_2} R (M := M) fun (x_1 : Unit) ↦ x
⊢ 1 ≤ Module.rank R M

Tactic:
simpa using this.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
mpr :
  LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type u_2)) 0
⊢ Module.rank R M = 0

Tactic:
rw [← nonpos_iff_eq_zero, Module.rank_def]

Premises used: Module.rank_def, nonpos_iff_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
mpr : ∀ (i : { s : Set M // LinearIndepOn R id s }), #(↑(↑i : Set M) : Type u_2) ≤ 0
⊢ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type u_2)) 0

Tactic:
apply ciSup_le'

Premises used: ciSup_le'
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
mpr : ¬Nonempty.{u_2 + 1} (↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type u_2)
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ LinearIndepOn R id s) s hs) : Set M) : Type u_2) ≤ 0

Tactic:
rw [nonpos_iff_eq_zero, Cardinal.mk_eq_zero_iff, ← not_nonempty_iff]

Premises used: Cardinal.mk_eq_zero_iff, not_nonempty_iff, nonpos_iff_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : (↑s : Type u_2)
mpr : ∀ (a : R) (ha : a ≠ 0) (ha' : a • (↑i : M) = 0), False
⊢ False

Tactic:
obtain ⟨a, ha, ha'⟩ := h i

Premises used: Subtype.val
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : (↑s : Type u_2)
a : R
ha : a ≠ 0
ha' : a • (↑i : M) = 0
mpr : a = 0
⊢ False

Tactic:
apply ha
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : (↑s : Type u_2)
a : R
ha : a ≠ 0
ha' : a • (↑i : M) = 0
⊢ Eq.{u_2 + 1} (α := M)
    ((Finsupp.linearCombination R fun (x : (↑s : Type u_2)) ↦ id (↑x : M) : (a : (↑s : Type u_2) →₀ R) → M)
        (Finsupp.single i a) :
      M)
    (0 : M)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Nontrivial R
h : ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
s : Set M
hs : LinearIndepOn R id s
i : (↑s : Type u_2)
a : R
ha : a ≠ 0
ha' : a • (↑i : M) = 0
⊢ a = 0

Tactic:
simpa using DFunLike.congr_fun (linearIndependent_iff.mp hs (Finsupp.single i a) (by simpa)) i

Premises used: DFunLike.congr_fun, linearIndependent_iff, Iff.mp, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
simp_rw : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0) ↔ ∀ (x : M), x = 0
simp_rw₁ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ (a = 0 ∨ x = 0)) ↔ ∀ (x : M), x = 0
simp_rw₂ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a = 0 ∨ a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
simp_rw₃ : (∀ (x : M), ∃ (a : R), False ∨ a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
simp_rw₄ : (∀ (x : M), ∃ (a : R), a ≠ 0 ∧ x = 0) ↔ ∀ (x : M), x = 0
simp_rw₅ : (∀ (x : M), (∃ (x : R), x ≠ 0) ∧ x = 0) ↔ ∀ (x : M), x = 0
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0

Tactic:
simp_rw [rank_eq_zero_iff, smul_eq_zero, and_or_left, not_and_self_iff, false_or,
    exists_and_right, and_iff_right (exists_ne (0 : R))]

Premises used: and_or_left, exists_ne, false_or, and_iff_right, exists_and_right, rank_eq_zero_iff, OfNat.ofNat, not_and_self_iff, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
⊢ Module.rank R M = 0 ↔ Subsingleton M

Tactic:
rank_zero_iff_forall_zero.trans (subsingleton_iff_forall_eq 0).symm

Premises used: rank_zero_iff_forall_zero, subsingleton_iff_forall_eq, Iff.trans, OfNat.ofNat, Iff.symm
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
contrapose! : Module.rank R M ≤ 0 ↔ ∀ (x : M), x = 0
⊢ 0 < Module.rank R M ↔ ∃ (x : M), x ≠ 0

Tactic:
contrapose!
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
rw : Module.rank R M = 0 ↔ ∀ (x : M), x = 0
⊢ Module.rank R M ≤ 0 ↔ ∀ (x : M), x = 0

Tactic:
rw [nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0

Tactic:
rank_zero_iff_forall_zero

Premises used: rank_zero_iff_forall_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0

Tactic:
exact rank_zero_iff_forall_zero

Premises used: rank_zero_iff_forall_zero
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
⊢ 0 < Module.rank R M ↔ Nontrivial M

Tactic:
rank_pos_iff_exists_ne_zero.trans (nontrivial_iff_exists_ne 0).symm

Premises used: nontrivial_iff_exists_ne, Iff.trans, rank_pos_iff_exists_ne_zero, OfNat.ofNat, Iff.symm
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : Nontrivial M
⊢ 0 < Module.rank R M

Tactic:
rank_pos_iff_nontrivial.mpr ‹_›

Premises used: Iff.mpr, rank_pos_iff_nontrivial
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h : Module.rank R M = 0
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h : Module.rank R M = 0
inst_5 : Nontrivial R
⊢ Subsingleton M

Tactic:
rw [rank_zero_iff] at h

Premises used: rank_zero_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h : Module.rank R M = 0
inst_5 : Nontrivial R
h₁ : Subsingleton M
⊢ Nontrivial R

Tactic:
rw [rank_zero_iff] at h

Premises used: rank_zero_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
h : Subsingleton M
inst_5 : Nontrivial R
⊢ Module.Finite R M

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
s : Submodule R M
h : 0 < Module.rank R ↥s
eq : s = ⊥
⊢ LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 0

Tactic:
rw [eq, rank_bot] at h

Premises used: rank_bot
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
s : Submodule R M
h : 0 < Module.rank R ↥s
eq : s = ⊥
h₁ : LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 0
⊢ s = ⊥

Tactic:
rw [eq, rank_bot] at h

Premises used: rank_bot
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
s : Submodule R M
h : LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 0
eq : s = ⊥
⊢ False

Tactic:
lt_irrefl _ h

Premises used: lt_irrefl
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial R
s : Submodule R M
h : LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 0
eq : s = ⊥
⊢ False

Tactic:
exact lt_irrefl _ h

Premises used: lt_irrefl
-- 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 : Free R M
n : ℕ
h : Module.rank R M = (↑n : Cardinal.{v})
⊢ Nontrivial R

Tactic:
nontriviality R
-- 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 : Free R M
n : ℕ
h : Module.rank R M = (↑n : Cardinal.{v})
h_1 : Nontrivial R
obtain : ∀ (ι : Type v) (b : Basis ι R M), Module.Finite R M
⊢ Module.Finite R M

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

Premises used: Module.Free.exists_basis
-- 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 : Free R M
n : ℕ
h : Module.rank R M = (↑n : Cardinal.{v})
h_1 : Nontrivial R
ι : Type v
b : Basis ι R M
⊢ Finite ι

Tactic:
have := mk_lt_aleph0_iff.mp <|
    b.linearIndependent.cardinal_le_rank |>.trans_eq h |>.trans_lt 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 : Free R M
n : ℕ
h : Module.rank R M = (↑n : Cardinal.{v})
h_1 : Nontrivial R
ι : Type v
b : Basis ι R M
this : Finite ι
⊢ Module.Finite R M

Tactic:
Module.Finite.of_basis b

Premises used: Module.Finite.of_basis
-- 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 : Free R M
n : ℕ
h : Module.rank R M = (↑n : Cardinal.{v})
h_1 : Nontrivial R
ι : Type v
b : Basis ι R M
this : Finite ι
⊢ Module.Finite R M

Tactic:
exact Module.Finite.of_basis b

Premises used: Module.Finite.of_basis
-- 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 : Free R M
h : Module.rank R M = 1
⊢ Module.Finite R M

Tactic:
Module.finite_of_rank_eq_nat <| h.trans Nat.cast_one.symm

Premises used: Module.finite_of_rank_eq_nat, Eq.symm, Nat.cast_one, Eq.trans
-- 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 u_1
b : Basis ι R M
h : Module.rank R M < ℵ₀
rwa : ∀ (h : lift.{u_1, v} (Module.rank R M) < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
rwa₁ : ∀ (h : lift.{v, u_1} #ι < lift.{u_1, v} ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
rwa₂ : ∀ (h : lift.{v, u_1} #ι < ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
rwa₃ : ∀ (h : #ι < ℵ₀), Nonempty.{u_1 + 1} (Fintype ι)
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (h : Nonempty.{u_1 + 1} (Fintype ι)), Nonempty.{u_1 + 1} (Fintype ι)
⊢ Nonempty.{u_1 + 1} (Fintype ι)

Tactic:
rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
    Cardinal.lt_aleph0_iff_fintype] at h

Premises used: Module.Basis.mk_eq_rank, Cardinal.lift_lt, Cardinal.lift_lt_aleph0, Cardinal.lift_aleph0, Cardinal.lt_aleph0_iff_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
inst_3 : StrongRankCondition R
ι : Type u_1
s : Set ι
b : Basis.{u_1, u, v} (↑s : Type u_1) R M
h : Module.rank R M < ℵ₀
⊢ s.Finite

Tactic:
Set.finite_def.2 (b.nonempty_fintype_index_of_rank_lt_aleph0 h)

Premises used: Iff.mpr, Module.Basis.nonempty_fintype_index_of_rank_lt_aleph0, Set.finite_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
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
ι : Type w
b : ι → M
h : LinearIndependent R b
rw : lift.{max v w, w} #ι ≤ lift.{max v w, w} (↑(finrank R M) : Cardinal.{w})
⊢ #ι ≤ (↑(finrank R M) : Cardinal.{w})

Tactic:
rw [← lift_le.{max v w}]
-- 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 w
b : ι → M
h : LinearIndependent R b
⊢ lift.{max v w, w} #ι ≤ lift.{max v w, w} (↑(finrank R M) : Cardinal.{w})

Tactic:
simpa only [← finrank_eq_rank, lift_natCast, lift_le_nat_iff] using h.cardinal_lift_le_rank

Premises used: LinearIndependent.cardinal_lift_le_rank, Cardinal.lift_le_nat_iff, Module.finrank_eq_rank, Cardinal.lift_natCast
-- 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
inst_5 : Fintype ι
b : ι → M
h : LinearIndependent R b
⊢ Fintype.card ι ≤ finrank R M

Tactic:
simpa using h.cardinalMk_le_finrank

Premises used: LinearIndependent.cardinalMk_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
inst_4 : Module.Finite R M
b : Finset M
h : LinearIndependent R (M := M) fun (x : ↥b) ↦ (↑x : M)
rw : Fintype.card.{v} ↥b ≤ finrank R M
⊢ b.card ≤ finrank R M

Tactic:
rw [← Fintype.card_coe]

Premises used: Fintype.card_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 : 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:
h.fintype_card_le_finrank

Premises used: LinearIndependent.fintype_card_le_finrank