awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Module.Finite R M
inst_4 : StrongRankCondition R
t : Finset M
h : finrank R M + 1 < #t
x₀ : M
x₀_mem : x₀ ∈ t
shift : M ↪ M := { toFun := fun (x : M) ↦ x - x₀, inj' := ⋯ }
t' : Finset M := Finset.map shift (t.erase x₀)
h' : finrank R M < #t'
g : M → R
gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0
f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
x₁ : M
x₁_mem' : x₁ ∈ t.erase x₀
x₁_mem : Membership.mem (α := M) t' ((shift : (a : M) → M) x₁ : M)
nz : g ((shift : (a : M) → M) x₁) ≠ 0
this : x₁ ≠ x₀ ∧ x₁ ∈ t
⊢ ∃ x ∈ t, f x ≠ 0

Tactic:
exact ⟨x₁, by
      simpa only [f, Embedding.coeFn_mk, sub_add_cancel, this.2, true_and, if_neg this.1]⟩
-- 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
inst_4 : Subsingleton M
rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) (0 : ℕ)
rw₁ : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) 0 : ℕ) (0 : ℕ)
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ finrank R M = 0

Tactic:
rw [finrank, rank_subsingleton', map_zero]

Premises used: rank_subsingleton', map_zero, 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
inst_3 : Nontrivial R
ι : Type u_1
inst_4 : Infinite ι
v : ι → M
hv : LinearIndependent R v
⊢ finrank R M = 0

Tactic:
toNat_eq_zero.mpr <| .inr hv.aleph0_le_rank

Premises used: Iff.mpr, LinearIndependent.aleph0_le_rank, Cardinal.toNat_eq_zero, Module.finrank, Or.inr
-- 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
h : 0 < finrank R M
contrapose! : ∀ (h : Subsingleton M), finrank R M ≤ 0
⊢ Nontrivial M

Tactic:
contrapose! 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
inst_3 : Nontrivial R
h : Subsingleton M
⊢ finrank R M ≤ 0

Tactic:
finrank_zero_of_subsingleton.le

Premises used: Eq.le, Module.finrank_zero_of_subsingleton
-- 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
h : Subsingleton M
⊢ finrank R M ≤ 0

Tactic:
exact finrank_zero_of_subsingleton.le

Premises used: Eq.le, Module.finrank_zero_of_subsingleton
-- 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 : ℕ
hn : finrank R M = n.succ
rw : 0 < n.succ
⊢ 0 < finrank R M

Tactic:
rw [hn]
-- 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 : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ

Tactic:
n.succ_pos

Premises used: Nat.succ_pos
-- 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 : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ

Tactic:
exact n.succ_pos

Premises used: Nat.succ_pos
-- 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
⊢ finrank.{u, v} R ↥⊥ = 0

Tactic:
finrank_eq_of_rank_eq (rank_bot _ _)

Premises used: rank_bot, Module.finrank_eq_of_rank_eq
-- 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 : StrongRankCondition R
inst_4 : Module.Finite R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
rw : 0 < finrank R M ↔ LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 (↑(finrank R M) : Cardinal.{u_2})
⊢ 0 < finrank R M ↔ ∃ (x : M), x ≠ 0

Tactic:
rw [← @rank_pos_iff_exists_ne_zero R M, ← finrank_eq_rank]

Premises used: Module.finrank_eq_rank, rank_pos_iff_exists_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
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < finrank R M ↔ 0 < finrank R M
⊢ 0 < finrank R M ↔ LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 (↑(finrank R M) : Cardinal.{u_2})

Tactic:
norm_cast
-- 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 : StrongRankCondition R
inst_4 : Module.Finite R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
rw : 0 < finrank R M ↔ LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 (↑(finrank R M) : Cardinal.{u_2})
⊢ 0 < finrank R M ↔ Nontrivial M

Tactic:
rw [← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank]

Premises used: rank_pos_iff_nontrivial, Module.finrank_eq_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
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
h : Nontrivial M
⊢ 0 < finrank R M

Tactic:
finrank_pos_iff.mpr h

Premises used: Iff.mpr, Module.finrank_pos_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 : StrongRankCondition R
inst_4 : Module.Finite R M
rw : finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0
⊢ finrank R M = 0 ↔ ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0

Tactic:
rw [← rank_eq_zero_iff (R := R), ← finrank_eq_rank]

Premises used: Module.finrank_eq_rank, rank_eq_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 : StrongRankCondition R
inst_4 : Module.Finite R M
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : finrank R M = 0 ↔ finrank R M = 0
⊢ finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0

Tactic:
norm_cast
-- 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 : StrongRankCondition R
inst_4 : Module.Finite R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
rw : finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0
⊢ finrank R M = 0 ↔ Subsingleton M

Tactic:
rw [← rank_zero_iff (R := R), ← finrank_eq_rank]

Premises used: Module.finrank_eq_rank, 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 : StrongRankCondition R
inst_4 : Module.Finite R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : finrank R M = 0 ↔ finrank R M = 0
⊢ finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0

Tactic:
norm_cast
-- 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 : StrongRankCondition R
inst_4 : Module.Finite R M
N : Submodule R M
⊢ Nontrivial R

Tactic:
haveI := nontrivial_of_invariantBasisNumber 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 : StrongRankCondition R
inst_4 : Module.Finite R M
N : Submodule R M
this : Nontrivial R
⊢ Module.rank R (M ⧸ N) + Module.rank R ↥N ≤ Module.rank R M

Tactic:
have := rank_quotient_add_rank_le N
-- 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 : StrongRankCondition R
inst_4 : Module.Finite R M
N : Submodule R M
this_1 : Nontrivial R
this : Module.rank R (M ⧸ N) + Module.rank R ↥N ≤ Module.rank R M
⊢ HAdd.hAdd (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} R (M ⧸ N)) : Cardinal.{u_2})
      (↑(finrank.{u_1, u_2} R ↥N) : Cardinal.{u_2}) ≤
    (↑(finrank R M) : Cardinal.{u_2})

Tactic:
rw [← finrank_eq_rank R M, ← finrank_eq_rank R, ← N.finrank_eq_rank] at this

Premises used: Module.finrank_eq_rank, Submodule.finrank_eq_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
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
N : Submodule R M
this_1 : Nontrivial R
this :
  HAdd.hAdd (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} R (M ⧸ N)) : Cardinal.{u_2})
      (↑(finrank.{u_1, u_2} R ↥N) : Cardinal.{u_2}) ≤
    (↑(finrank R M) : Cardinal.{u_2})
⊢ finrank.{u_1, u_2} R (M ⧸ N) + finrank.{u_1, u_2} R ↥N ≤ finrank R M

Tactic:
mod_cast this

Premises used: congrArg, Nat.cast_add._simp_1, cast, Membership.mem, Subtype, Nat.cast_le._simp_1, LE.le, Nat.cast, HasQuotient.Quotient, congrFun', Module.finrank, Eq.trans
-- 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 : StrongRankCondition R
inst_4 : Module.Finite R M
N : Submodule R M
this_1 : Nontrivial R
this :
  HAdd.hAdd (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} R (M ⧸ N)) : Cardinal.{u_2})
      (↑(finrank.{u_1, u_2} R ↥N) : Cardinal.{u_2}) ≤
    (↑(finrank R M) : Cardinal.{u_2})
⊢ finrank.{u_1, u_2} R (M ⧸ N) + finrank.{u_1, u_2} R ↥N ≤ finrank R M

Tactic:
exact mod_cast this
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Module.rank R M = 0
rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) 0 : ℕ) (0 : ℕ)
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) (0 : ℕ)

Tactic:
rw [h, zero_toNat]

Premises used: Cardinal.zero_toNat
-- 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
⊢ Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊤

Tactic:
subsingleton
-- 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
S : Submodule R M
h : S = ⊥
rw : Module.rank R ↥⊥ = 0
rw₁ rw₂ : Eq.{u_2 + 2} (α := Cardinal.{u_2}) 0 0
⊢ Module.rank R ↥S = 0

Tactic:
rw [h, rank_bot]

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 : IsDomain R
inst_4 : IsTorsionFree R M
inst_5 : StrongRankCondition R
S : Submodule R M
inst_6 : Module.Finite.{u_1, u_2} R ↥S
rw : finrank.{u_1, u_2} R ↥S = 0 ↔ Module.rank R ↥S = 0
rw₁ : finrank.{u_1, u_2} R ↥S = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} R ↥S) : Cardinal.{u_2}) 0
rw₂ :
  finrank.{u_1, u_2} R ↥S = 0 ↔
    Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank.{u_1, u_2} R ↥S) : Cardinal.{u_2}) (↑0 : Cardinal.{u_2})
rw₃ rw₄ : finrank.{u_1, u_2} R ↥S = 0 ↔ finrank.{u_1, u_2} R ↥S = 0
⊢ finrank.{u_1, u_2} R ↥S = 0 ↔ S = ⊥

Tactic:
rw [← Submodule.rank_eq_zero, ← finrank_eq_rank, ← @Nat.cast_zero Cardinal, Nat.cast_inj]

Premises used: Nat.cast_inj, Submodule.rank_eq_zero, Module.finrank_eq_rank, Nat.cast_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
inst_5 : StrongRankCondition R
S : Submodule R M
inst_6 : Module.Finite.{u_1, u_2} R ↥S
contrapose! : finrank.{u_1, u_2} R ↥S < 1 ↔ S = ⊥
⊢ 1 ≤ finrank.{u_1, u_2} R ↥S ↔ S ≠ ⊥

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
inst_5 : StrongRankCondition R
S : Submodule R M
inst_6 : Module.Finite.{u_1, u_2} R ↥S
rw : finrank.{u_1, u_2} R ↥S = 0 ↔ S = ⊥
rw₁ rw₂ : S = ⊥ ↔ S = ⊥
⊢ finrank.{u_1, u_2} R ↥S < 1 ↔ S = ⊥

Tactic:
rw [Nat.lt_one_iff, finrank_eq_zero]

Premises used: Submodule.finrank_eq_zero, Nat.lt_one_iff
-- 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
rw : finrank.{u, v} R ↥(span R ∅) = 0
rw₁ : finrank.{u, v} R ↥⊥ = 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ Set.finrank.{u, v} R (M := M) ∅ = 0

Tactic:
rw [Set.finrank, span_empty, finrank_bot]

Premises used: Set.finrank, Submodule.span_empty, finrank_bot
-- 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 : ∀ (s : Set M) (a : Basis (↑s : Type v) R M), ¬s.Finite
inl : Subsingleton R → finrank R M = 0
inr : Nontrivial R → finrank R M = 0
⊢ finrank R M = 0

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- 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 : ∀ (s : Set M) (a : Basis (↑s : Type v) R M), ¬s.Finite
h_1 : Subsingleton R
⊢ Subsingleton M

Tactic:
have := Module.subsingleton R M
-- 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 : ∀ (s : Set M) (a : Basis (↑s : Type v) R M), ¬s.Finite
h_1 : Subsingleton R
this : Subsingleton M
⊢ finrank R M = 0

Tactic:
(h ∅ ⟨LinearEquiv.ofSubsingleton _ _⟩ Set.finite_empty).elim

Premises used: Set.finite_empty, Module.Basis.ofRepr, False.elim, LinearEquiv.ofSubsingleton, EmptyCollection.emptyCollection
-- 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 : ∀ (s : Set M) (a : Basis (↑s : Type v) R M), ¬s.Finite
h_1 : Subsingleton R
this : Subsingleton M
⊢ finrank R M = 0

Tactic:
exact (h ∅ ⟨LinearEquiv.ofSubsingleton _ _⟩ Set.finite_empty).elim

Premises used: Set.finite_empty, Module.Basis.ofRepr, False.elim, LinearEquiv.ofSubsingleton, EmptyCollection.emptyCollection
-- 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 : ∀ (s : Set M) (a : Basis (↑s : Type v) R M), ¬s.Finite
h_1 : Nontrivial R
inr : ∀ (w : Set M) (b : Basis (↑w : Type v) R M), finrank R M = 0
⊢ finrank R M = 0

Tactic:
obtain ⟨_, ⟨b⟩⟩ := (Module.free_iff_set R M).mp ‹_›

Premises used: Module.free_iff_set, 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 : Free R M
h : ∀ (s : Set M) (a : Basis (↑s : Type v) R M), ¬s.Finite
h_1 : Nontrivial R
w : Set M
b : Basis (↑w : Type v) R M
⊢ Infinite.{v + 1} (↑w : Type v)

Tactic:
have := Set.Infinite.to_subtype (h _ b)
-- 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 : ∀ (s : Set M) (a : Basis (↑s : Type v) R M), ¬s.Finite
h_1 : Nontrivial R
w : Set M
b : Basis (↑w : Type v) R M
this : Infinite.{v + 1} (↑w : Type v)
⊢ finrank R M = 0

Tactic:
b.linearIndependent.finrank_eq_zero_of_infinite

Premises used: LinearIndependent.finrank_eq_zero_of_infinite, Module.Basis.linearIndependent
-- 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 : ∀ (s : Set M) (a : Basis (↑s : Type v) R M), ¬s.Finite
h_1 : Nontrivial R
w : Set M
b : Basis (↑w : Type v) R M
this : Infinite.{v + 1} (↑w : Type v)
⊢ finrank R M = 0

Tactic:
exact b.linearIndependent.finrank_eq_zero_of_infinite

Premises used: LinearIndependent.finrank_eq_zero_of_infinite, Module.Basis.linearIndependent
-- 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 : ∀ (s : Finset M) (a : Basis (↑(↑s : Set M) : Type v) R M), False
s : Set M
b : Basis (↑s : Type v) R M
hs : s.Finite
h₁ : (↑(hs.toFinset (s := s)) : Set M) = s
⊢ Basis (↑(↑(hs.toFinset (s := s)) : Set M) : Type v) R M

Tactic:
convert! b
-- 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 : ∀ (s : Finset M) (a : Basis (↑(↑s : Set M) : Type v) R M), False
s : Set M
b : Basis (↑s : Type v) R M
hs : s.Finite
⊢ (↑(hs.toFinset (s := s)) : Set M) = s

Tactic:
simp
-- 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 : ¬∃ (s : Finset M), Nonempty (Basis (↑(↑s : Set M) : Type v) R M)
⊢ finrank R M = 0

Tactic:
finrank_eq_zero_of_basis_imp_false fun s b => h ⟨s, ⟨b⟩⟩

Premises used: Nonempty.intro, Exists.intro, finrank_eq_zero_of_basis_imp_false
-- 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 : ¬∃ (s : Set M) (x : Basis (↑s : Type v) R M), s.Finite
⊢ finrank R M = 0

Tactic:
finrank_eq_zero_of_basis_imp_not_finite fun s b hs => h ⟨s, b, hs⟩

Premises used: finrank_eq_zero_of_basis_imp_not_finite, Exists.intro
-- 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 : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
⊢ finrank R M = 0

Tactic:
finrank_eq_zero_of_basis_imp_false fun s b => h ⟨s, ⟨b⟩⟩

Premises used: Nonempty.intro, Exists.intro, finrank_eq_zero_of_basis_imp_false
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
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 : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ (c : R), c • v = w
⊢ Nontrivial R

Tactic:
haveI := nontrivial_of_invariantBasisNumber R
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
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 : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ (c : R), c • v = w
this : Nontrivial R
obtain : ∀ (b : Basis PUnit.{u + 1} R M), Module.rank R M = 1
⊢ Module.rank R M = 1

Tactic:
obtain ⟨b⟩ := (Basis.basis_singleton_iff.{_, _, u} PUnit).mpr ⟨v, n, h⟩
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
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 : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ (c : R), c • v = w
this : Nontrivial R
b : Basis PUnit.{u + 1} R M
rw : Eq.{v + 2} (α := Cardinal.{v}) (↑(Fintype.card PUnit.{u + 1}) : Cardinal.{v}) 1
rw₁ : Eq.{v + 2} (α := Cardinal.{v}) (↑1 : Cardinal.{v}) 1
rw₂ rw₃ : Eq.{v + 2} (α := Cardinal.{v}) 1 1
⊢ Module.rank R M = 1

Tactic:
rw [rank_eq_card_basis b, Fintype.card_punit, Nat.cast_one]

Premises used: rank_eq_card_basis, Fintype.card_punit, Nat.cast_one
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
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 : StrongRankCondition R
v : M
n : v ≠ 0
h : ∀ (w : M), ∃ (c : R), c • v = w
⊢ finrank R M = 1

Tactic:
finrank_eq_of_rank_eq (rank_eq_one v n h)

Premises used: rank_eq_one, Module.finrank_eq_of_rank_eq
-- 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
v : M
h : ∀ (w : M), ∃ (c : R), c • v = w
⊢ Module.rank R M ≤ 1

Tactic:
simpa using LinearMap.lift_rank_le_of_surjective _
    (id h : Surjective (LinearMap.toSpanSingleton R M v))

Premises used: LinearMap.lift_rank_le_of_surjective, 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
inst_3 : StrongRankCondition R
v : M
h : ∀ (w : M), ∃ (c : R), c • v = w
rw : LE.le (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) 1 : ℕ)
⊢ finrank R M ≤ 1

Tactic:
rw [← map_one toNat, finrank]

Premises used: Cardinal.toNat, map_one, 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
inst_3 : StrongRankCondition R
v : M
h : ∀ (w : M), ∃ (c : R), c • v = w
⊢ LE.le (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) 1 : ℕ)

Tactic:
toNat_le_toNat (rank_le_one v h) one_lt_aleph0

Premises used: rank_le_one, Cardinal.one_lt_aleph0, Cardinal.toNat_le_toNat
-- 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
v : M
h : ∀ (w : M), ∃ (c : R), c • v = w
⊢ LE.le (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) 1 : ℕ)

Tactic:
exact toNat_le_toNat (rank_le_one v h) one_lt_aleph0

Premises used: rank_le_one, Cardinal.one_lt_aleph0, Cardinal.toNat_le_toNat
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
simp : Module.Finite R (ι →₀ M) → Nonempty ι → Nontrivial M → Module.Finite R M ∧ Finite ι
⊢ Module.Finite R (ι →₀ M) → IsEmpty ι ∨ Subsingleton M ∨ Module.Finite R M ∧ Finite ι

Tactic:
simp only [or_iff_not_imp_left, not_subsingleton_iff_nontrivial, not_isEmpty_iff]

Premises used: Classical.or_iff_not_imp_left, not_isEmpty_iff, not_subsingleton_iff_nontrivial
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
h : Module.Finite R (ι →₀ M)
i : ι
h_1 : Nontrivial M
obtain :
  ∀ (s : Finset (ι →₀ M)) (hs : Eq (α := Submodule R (ι →₀ M)) (span R (↑s : Set (ι →₀ M))) ⊤),
    Module.Finite R M ∧ Finite ι
⊢ Module.Finite R M ∧ Finite ι

Tactic:
obtain ⟨s, hs⟩ := id h

Premises used: 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
ι : Type u_1
h : Module.Finite R (ι →₀ M)
i : ι
h_1 : Nontrivial M
s : Finset (ι →₀ M)
hs : Eq (α := Submodule R (ι →₀ M)) (span R (↑s : Set (ι →₀ M))) ⊤
⊢ Module.Finite R M ∧ Finite ι

Tactic:
⟨.of_surjective (Finsupp.lapply (R := R) (M := M) i) (Finsupp.apply_surjective i),
       finite_of_span_finite_eq_top_finsupp s.finite_toSet hs⟩

Premises used: Module.Finite.of_surjective, Finsupp.apply_surjective, finite_of_span_finite_eq_top_finsupp, And.intro, Finset.finite_toSet, Finsupp.lapply
-- Module: Mathlib.LinearAlgebra.Dimension.Finite
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
h : Module.Finite R (ι →₀ M)
i : ι
h_1 : Nontrivial M
s : Finset (ι →₀ M)
hs : Eq (α := Submodule R (ι →₀ M)) (span R (↑s : Set (ι →₀ M))) ⊤
⊢ Module.Finite R M ∧ Finite ι

Tactic:
exact ⟨.of_surjective (Finsupp.lapply (R := R) (M := M) i) (Finsupp.apply_surjective i),
       finite_of_span_finite_eq_top_finsupp s.finite_toSet 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
ι : Type u_1
h : Module.Finite R M ∧ Finite ι
⊢ Module.Finite R M

Tactic:
cases 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
ι : Type u_1
h : Module.Finite R M ∧ Finite ι
left : Module.Finite R M
⊢ Finite ι

Tactic:
cases h