awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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' := ⋯ }
let let₁ let₂ :
  ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
let₃ :
  let t' := Finset.map shift (t.erase x₀);
  ∀ (h' : finrank R M < #t'),
    ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
let₄ let₅ :
  let t' := Finset.map shift (t.erase x₀);
  ∀ (h' : finrank R M < #t') (g : M → R) (gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0) (x₁ : M) (x₁_mem : x₁ ∈ t')
    (nz : g x₁ ≠ 0),
    ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
refine_1 :
  let t' := Finset.map shift (t.erase x₀);
  ∀ (h' : finrank R M < #t') (g : M → R) (gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0) (x₁ : M) (x₁_mem : x₁ ∈ t')
    (nz : g x₁ ≠ 0),
    let f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀);
    Eq (α := M) (∑ e ∈ t, f e • e) 0
⊢ ∃ (f : M → R), Eq (α := M) (∑ e ∈ t, f e • e) 0 ∧ Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0 ∧ ∃ x ∈ t, f x ≠ 0
have refine_2 : let t' := Finset.map shift (t.erase x₀);
∀ (h' : finrank R M < #t') (g : M → R) (gsum : Eq (α := M) (∑ e ∈ t', g e • e) 0) (x₁ : M) (x₁_mem : x₁ ∈ t')
  (nz : g x₁ ≠ 0),
  let f : M → R := fun (z : M) ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀);
  Eq.{u_1 + 1} (α := R) (∑ e ∈ t, f e) 0
Tactic: classical
  let t' := (t.erase x₀).map shift
  have h' : finrank R M < t'.card := by
    rw [card_map, card_erase_of_mem x₀_mem]
    exact Nat.lt_pred_iff.mpr h
  -- to obtain a function `g`.
  obtain ⟨g, gsum, x₁, x₁_mem, nz⟩ := exists_nontrivial_relation_of_finrank_lt_card h'
  -- Then obtain `f` by translating back by `x₀`,
  -- and setting the value of `f` at `x₀` to ensure `∑ e ∈ t, f e = 0`.
  let f : M → R := fun z ↦ if z = x₀ then -∑ z ∈ t.erase x₀, g (z - x₀) else g (z - x₀)
  refine ⟨f, ?_, ?_, ?_⟩
  -- After this, it's a matter of verifying the properties,
  -- based on the corresponding properties for `g`.
  · rw [sum_map, Embedding.coeFn_mk] at gsum
    simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, neg_smul, sum_smul,
             ← sub_eq_add_neg, ← sum_sub_distrib, ← gsum, smul_sub]
    refine sum_congr rfl fun x x_mem ↦ ?_
    rw [if_neg (mem_erase.mp x_mem).1]
  · simp_rw [f, ← t.sum_erase_add _ x₀_mem, if_pos, add_neg_eq_zero]
    exact sum_congr rfl fun x x_mem ↦ if_neg (mem_erase.mp x_mem).1
  · obtain ⟨x₁, x₁_mem', rfl⟩ := Finset.mem_map.mp x₁_mem
    have := mem_erase.mp x₁_mem'
    exact ⟨x₁, by
      simpa only [f, Embedding.coeFn_mk, sub_add_cancel, this.2, true_and, if_neg this.1]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank R M = 0
have rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) (0 : ℕ)
Tactic: rw [finrank, rank_subsingleton', map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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 : ℕ)
⊢ finrank R M = 0
have rw₁ : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) 0 : ℕ) (0 : ℕ)
Tactic: rw [finrank, rank_subsingleton', map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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 : ℕ)
⊢ finrank R M = 0
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [finrank, rank_subsingleton', map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Nontrivial M
have contrapose! : ∀ (h : Subsingleton M), finrank R M ≤ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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 < finrank R M
have rw : 0 < n.succ
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ 0 < finrank R M ↔ ∃ (x : M), x ≠ 0
have rw : 0 < finrank R M ↔ LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 (↑(finrank R M) : Cardinal.{u_2})
Tactic: rw [← @rank_pos_iff_exists_ne_zero R M, ← finrank_eq_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ 0 < finrank R M ↔ LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 (↑(finrank R M) : Cardinal.{u_2})
have norm_cast : 0 < finrank R M ↔ 0 < finrank R M
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ 0 < finrank R M ↔ Nontrivial M
have rw : 0 < finrank R M ↔ LT.lt.{u_2 + 1} (α := Cardinal.{u_2}) 0 (↑(finrank R M) : Cardinal.{u_2})
Tactic: rw [← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank R M = 0 ↔ ∀ (x : M), ∃ (a : R), a ≠ 0 ∧ a • x = 0
have rw : finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0
Tactic: rw [← rank_eq_zero_iff (R := R), ← finrank_eq_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0
have norm_cast : finrank R M = 0 ↔ finrank R M = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank R M = 0 ↔ Subsingleton M
have rw : finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0
Tactic: rw [← rank_zero_iff (R := R), ← finrank_eq_rank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank R M = 0 ↔ Eq.{u_2 + 2} (α := Cardinal.{u_2}) (↑(finrank R M) : Cardinal.{u_2}) 0
have norm_cast : finrank R M = 0 ↔ finrank R M = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
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
⊢ finrank.{u_1, u_2} R (M ⧸ N) + finrank.{u_1, u_2} R ↥N ≤ finrank R M
have this : Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
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
⊢ finrank.{u_1, u_2} R (M ⧸ N) + finrank.{u_1, u_2} R ↥N ≤ finrank R M
have this₁ : Module.rank R (M ⧸ N) + Module.rank R ↥N ≤ Module.rank R M
Tactic: have := rank_quotient_add_rank_le N
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
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
⊢ finrank.{u_1, u_2} R (M ⧸ N) + finrank.{u_1, u_2} R ↥N ≤ finrank R M
have 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})
Tactic: rw [← finrank_eq_rank R M, ← finrank_eq_rank R, ← N.finrank_eq_rank] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) (0 : ℕ)
have rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) 0 : ℕ) (0 : ℕ)
Tactic: rw [h, zero_toNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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 : ℕ)
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) (0 : ℕ)
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [h, zero_toNat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊤
have inst : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊤
have h₁ : Subsingleton M
Tactic: rw [rank_zero_iff] at h
Cleared hypotheses: h, inst_5
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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 = ⊥
⊢ Module.rank R ↥S = 0
have rw : Module.rank R ↥⊥ = 0
Tactic: rw [h, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Module.rank R ↥S = 0
have rw₁ : Eq.{u_2 + 2} (α := Cardinal.{u_2}) 0 0
Tactic: rw [h, rank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank.{u_1, u_2} R ↥S = 0 ↔ S = ⊥
have rw : finrank.{u_1, u_2} R ↥S = 0 ↔ Module.rank R ↥S = 0
Tactic: rw [← Submodule.rank_eq_zero, ← finrank_eq_rank, ← @Nat.cast_zero Cardinal, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank.{u_1, u_2} R ↥S = 0 ↔ S = ⊥
have 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
Tactic: rw [← Submodule.rank_eq_zero, ← finrank_eq_rank, ← @Nat.cast_zero Cardinal, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank.{u_1, u_2} R ↥S = 0 ↔ S = ⊥
have 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})
Tactic: rw [← Submodule.rank_eq_zero, ← finrank_eq_rank, ← @Nat.cast_zero Cardinal, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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})
⊢ finrank.{u_1, u_2} R ↥S = 0 ↔ S = ⊥
have rw₃ : finrank.{u_1, u_2} R ↥S = 0 ↔ finrank.{u_1, u_2} R ↥S = 0
Tactic: rw [← Submodule.rank_eq_zero, ← finrank_eq_rank, ← @Nat.cast_zero Cardinal, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ 1 ≤ finrank.{u_1, u_2} R ↥S ↔ S ≠ ⊥
have contrapose! : finrank.{u_1, u_2} R ↥S < 1 ↔ S = ⊥
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank.{u_1, u_2} R ↥S < 1 ↔ S = ⊥
have rw : finrank.{u_1, u_2} R ↥S = 0 ↔ S = ⊥
Tactic: rw [Nat.lt_one_iff, finrank_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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 = ⊥
⊢ finrank.{u_1, u_2} R ↥S < 1 ↔ S = ⊥
have rw₁ : S = ⊥ ↔ S = ⊥
Tactic: rw [Nat.lt_one_iff, finrank_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
⊢ Set.finrank.{u, v} R (M := M) ∅ = 0
have rw : finrank.{u, v} R ↥(span R ∅) = 0
Tactic: rw [Set.finrank, span_empty, finrank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Set.finrank.{u, v} R (M := M) ∅ = 0
have rw₁ : finrank.{u, v} R ↥⊥ = 0
Tactic: rw [Set.finrank, span_empty, finrank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Set.finrank.{u, v} R (M := M) ∅ = 0
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [Set.finrank, span_empty, finrank_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank R M = 0
have inl : Subsingleton R → finrank R M = 0
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank R M = 0
have inr : Nontrivial R → finrank R M = 0
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
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
⊢ finrank R M = 0
have this : Subsingleton M
Tactic: have := Module.subsingleton R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank R M = 0
have inr : ∀ (w : Set M) (b : Basis (↑w : Type v) R M), finrank R M = 0
Tactic: obtain ⟨_, ⟨b⟩⟩ := (Module.free_iff_set R M).mp ‹_›
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
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
⊢ finrank R M = 0
have this : Infinite.{v + 1} (↑w : Type v)
Tactic: have := Set.Infinite.to_subtype (h _ b)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Basis (↑(↑(hs.toFinset (s := s)) : Set M) : Type v) R M
have h₁ : (↑(hs.toFinset (s := s)) : Set M) = s
Tactic: convert! b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
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
⊢ Module.rank R M = 1
have this : Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Module.rank R M = 1
have obtain : ∀ (b : Basis PUnit.{u + 1} R M), Module.rank R M = 1
Tactic: obtain ⟨b⟩ := (Basis.basis_singleton_iff.{_, _, u} PUnit).mpr ⟨v, n, h⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Module.rank R M = 1
have rw : Eq.{v + 2} (α := Cardinal.{v}) (↑(Fintype.card PUnit.{u + 1}) : Cardinal.{v}) 1
Tactic: rw [rank_eq_card_basis b, Fintype.card_punit, Nat.cast_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Module.rank R M = 1
have rw₁ : Eq.{v + 2} (α := Cardinal.{v}) (↑1 : Cardinal.{v}) 1
Tactic: rw [rank_eq_card_basis b, Fintype.card_punit, Nat.cast_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Module.rank R M = 1
have rw₂ : Eq.{v + 2} (α := Cardinal.{v}) 1 1
Tactic: rw [rank_eq_card_basis b, Fintype.card_punit, Nat.cast_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ finrank R M ≤ 1
have rw : LE.le (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) 1 : ℕ)
Tactic: rw [← map_one toNat, finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
⊢ Module.Finite R (ι →₀ M) → IsEmpty ι ∨ Subsingleton M ∨ Module.Finite R M ∧ Finite ι
have simp : Module.Finite R (ι →₀ M) → Nonempty ι → Nontrivial M → Module.Finite R M ∧ Finite ι
Tactic: simp only [or_iff_not_imp_left, not_subsingleton_iff_nontrivial, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
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
⊢ Module.Finite R M ∧ Finite ι
have obtain : ∀ (s : Finset (ι →₀ M)) (hs : Eq (α := Submodule R (ι →₀ M)) (span R (↑s : Set (ι →₀ M))) ⊤),
  Module.Finite R M ∧ Finite ι
Tactic: obtain ⟨s, hs⟩ := id h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
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)
have left : Module.Finite R M
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (hypothesis)
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
⊢ Module.Finite R (ι →₀ M)
have right : Finite ι
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finite (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
⊢ Module.Finite R (ι →₀ R) ↔ Subsingleton R ∨ Finite ι
have simp : IsEmpty ι → Subsingleton R ∨ Finite ι
Tactic: simp only [finite_finsupp_iff, Finite.self, true_and, or_iff_right_iff_imp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton R
⊢ finrank R M = 1
have rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) (1 : ℕ)
Tactic: rw [finrank, rank_subsingleton, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dimension.Finrank (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Subsingleton R
rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) (Module.rank R M) : ℕ) (1 : ℕ)
⊢ finrank R M = 1
have rw₁ : Eq (α := ℕ) ((toNat : (a : Cardinal.{v}) → ℕ) 1 : ℕ) (1 : ℕ)
Tactic: rw [finrank, rank_subsingleton, map_one]