awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : N →ₗ[R] M
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
rw : length R N ≤ length R N + length.{u_1, u_2} R (M ⧸ f.range)
⊢ length R N ≤ length R M

Tactic:
rw [Module.length_eq_add_of_exact f (LinearMap.range f).mkQ hf
    (Submodule.mkQ_surjective _) (LinearMap.exact_map_mkQ_range f)]

Premises used: LinearMap.range, LinearMap.exact_map_mkQ_range, Module.length_eq_add_of_exact, Submodule.mkQ, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : N →ₗ[R] M
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
⊢ length R N ≤ length R N + length.{u_1, u_2} R (M ⧸ f.range)

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : N →ₗ[R] M
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
⊢ length R N ≤ length R N + length.{u_1, u_2} R (M ⧸ f.range)

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
P : Type u_4
inst_3 : AddCommGroup P
inst_4 : Module R P
g : M →ₗ[R] P
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
rw : length R P ≤ length.{u_1, u_2} R ↥g.ker + length R P
⊢ length R P ≤ length R M

Tactic:
rw [Module.length_eq_add_of_exact (LinearMap.ker g).subtype g (Submodule.subtype_injective _) hg
    (LinearMap.exact_subtype_ker_map g)]

Premises used: LinearMap.ker, LinearMap.exact_subtype_ker_map, Module.length_eq_add_of_exact, Submodule.subtype, Submodule.subtype_injective
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
P : Type u_4
inst_3 : AddCommGroup P
inst_4 : Module R P
g : M →ₗ[R] P
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
⊢ length R P ≤ length.{u_1, u_2} R ↥g.ker + length R P

Tactic:
le_add_self

Premises used: le_add_self
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
P : Type u_4
inst_3 : AddCommGroup P
inst_4 : Module R P
g : M →ₗ[R] P
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
⊢ length R P ≤ length.{u_1, u_2} R ↥g.ker + length R P

Tactic:
exact le_add_self

Premises used: le_add_self
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
⊢ length R (M × N) = length R M + length R N

Tactic:
Module.length_eq_add_of_exact _ _ LinearMap.inl_injective LinearMap.snd_surjective .inl_snd

Premises used: LinearMap.inl_injective, Module.length_eq_add_of_exact, LinearMap.snd_surjective, Function.Exact.inl_snd
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
of_equiv :
  ∀ (α β : Type u_5) [inst_1 : Fintype β] (e : α ≃ β),
    (∀ (M : α → Type u_6) [inst_2 : (i : α) → AddCommGroup (M i)] [inst_3 : (i : α) → Module.{u_1, u_6} R (M i)],
        length R ((i : α) → M i) = ∑ i : α, length.{u_1, u_6} R (M i)) →
      ∀ (M : β → Type u_6) [inst_2 : (i : β) → AddCommGroup (M i)] [inst_3 : (i : β) → Module.{u_1, u_6} R (M i)],
        length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)
h_empty :
  ∀ (M : PEmpty.{u_5 + 1} → Type u_6) [inst_1 : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)]
    [inst_2 : (i : PEmpty.{u_5 + 1}) → Module.{u_1, u_6} R (M i)],
    length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i : PEmpty.{u_5 + 1}, length.{u_1, u_6} R (M i)
h_option :
  ∀ (α : Type u_5) [inst_1 : Fintype α],
    (∀ (M : α → Type u_6) [inst_2 : (i : α) → AddCommGroup (M i)] [inst_3 : (i : α) → Module.{u_1, u_6} R (M i)],
        length R ((i : α) → M i) = ∑ i : α, length.{u_1, u_6} R (M i)) →
      ∀ (M : Option α → Type u_6) [inst_2 : (i : Option α) → AddCommGroup (M i)]
        [inst_3 : (i : Option α) → Module.{u_1, u_6} R (M i)],
        length R ((i : Option α) → M i) = ∑ i : Option α, length.{u_1, u_6} R (M i)
⊢ ∀ {ι : Type u_5} [inst_1 : Fintype ι] (M : ι → Type u_6) [inst_2 : (i : ι) → AddCommGroup (M i)]
    [inst_3 : (i : ι) → Module.{u_1, u_6} R (M i)], length R ((i : ι) → M i) = ∑ i : ι, length.{u_1, u_6} R (M i)

Tactic:
apply Fintype.induction_empty_option
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
α β : Type u_5
of_equiv :
  ∀ [inst_1 : Fintype β] (e : α ≃ β),
    (∀ (M : α → Type u_6) [inst_2 : (i : α) → AddCommGroup (M i)] [inst_3 : (i : α) → Module.{u_1, u_6} R (M i)],
        length R ((i : α) → M i) = ∑ i : α, length.{u_1, u_6} R (M i)) →
      ∀ (M : β → Type u_6) [inst_2 : (i : β) → AddCommGroup (M i)] [inst_3 : (i : β) → Module.{u_1, u_6} R (M i)],
        length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)
⊢ ∀ [inst_1 : Fintype β] (e : α ≃ β),
    (∀ (M : α → Type u_6) [inst_2 : (i : α) → AddCommGroup (M i)] [inst_3 : (i : α) → Module.{u_1, u_6} R (M i)],
        length R ((i : α) → M i) = ∑ i : α, length.{u_1, u_6} R (M i)) →
      ∀ (M : β → Type u_6) [inst_2 : (i : β) → AddCommGroup (M i)] [inst_3 : (i : β) → Module.{u_1, u_6} R (M i)],
        length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
α β : Type u_5
inst_1 : Fintype β
e : α ≃ β
IH :
  ∀ (M : α → Type u_6) [inst_2 : (i : α) → AddCommGroup (M i)] [inst_3 : (i : α) → Module.{u_1, u_6} R (M i)],
    length R ((i : α) → M i) = ∑ i : α, length.{u_1, u_6} R (M i)
M : β → Type u_6
of_equiv :
  ∀ [inst_2 : (i : β) → AddCommGroup (M i)] [inst_3 : (i : β) → Module.{u_1, u_6} R (M i)],
    length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)
⊢ ∀ [inst_2 : (i : β) → AddCommGroup (M i)] [inst_3 : (i : β) → Module.{u_1, u_6} R (M i)],
    length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
α β : Type u_5
inst_1 : Fintype β
e : α ≃ β
IH :
  ∀ (M : α → Type u_6) [inst_3 : (i : α) → AddCommGroup (M i)] [inst_4 : (i : α) → Module.{u_1, u_6} R (M i)],
    length R ((i : α) → M i) = ∑ i : α, length.{u_1, u_6} R (M i)
M : β → Type u_6
inst_2 : (i : β) → AddCommGroup (M i)
of_equiv :
  ∀ [inst_3 : (i : β) → Module.{u_1, u_6} R (M i)], length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)
⊢ ∀ [inst_3 : (i : β) → Module.{u_1, u_6} R (M i)], length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
α β : Type u_5
inst_1 : Fintype β
e : α ≃ β
IH :
  ∀ (M : α → Type u_6) [inst_4 : (i : α) → AddCommGroup (M i)] [inst_5 : (i : α) → Module.{u_1, u_6} R (M i)],
    length R ((i : α) → M i) = ∑ i : α, length.{u_1, u_6} R (M i)
M : β → Type u_6
inst_2 : (i : β) → AddCommGroup (M i)
inst_3 : (i : β) → Module.{u_1, u_6} R (M i)
x : Fintype α := Fintype.ofEquiv β e.symm
of_equiv : length R ((i' : α) → M ((e : (a : α) → β) i')) = ∑ i : β, length.{u_1, u_6} R (M i)
of_equiv₁ : Eq (α := ℕ∞) (∑ i : α, length.{u_1, u_6} R (M ((e : (a : α) → β) i))) (∑ i : β, length.{u_1, u_6} R (M i))
of_equiv₂ of_equiv₃ : Eq (α := ℕ∞) (∑ i : β, length.{u_1, u_6} R (M i)) (∑ i : β, length.{u_1, u_6} R (M i))
⊢ length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)

Tactic:
rw [← (LinearEquiv.piCongrLeft R M e).length_eq, IH, e.sum_comp (length R <| M ·)]

Premises used: Equiv.sum_comp, LinearEquiv.length_eq, LinearEquiv.piCongrLeft, Module.length
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
M : PEmpty.{u_5 + 1} → Type u_6
h_empty :
  ∀ [inst_1 : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)]
    [inst_2 : (i : PEmpty.{u_5 + 1}) → Module.{u_1, u_6} R (M i)],
    length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i : PEmpty.{u_5 + 1}, length.{u_1, u_6} R (M i)
⊢ ∀ [inst_1 : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)]
    [inst_2 : (i : PEmpty.{u_5 + 1}) → Module.{u_1, u_6} R (M i)],
    length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i : PEmpty.{u_5 + 1}, length.{u_1, u_6} R (M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
M : PEmpty.{u_5 + 1} → Type u_6
inst_1 : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)
h_empty :
  ∀ [inst_2 : (i : PEmpty.{u_5 + 1}) → Module.{u_1, u_6} R (M i)],
    length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i : PEmpty.{u_5 + 1}, length.{u_1, u_6} R (M i)
⊢ ∀ [inst_2 : (i : PEmpty.{u_5 + 1}) → Module.{u_1, u_6} R (M i)],
    length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i : PEmpty.{u_5 + 1}, length.{u_1, u_6} R (M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
M : PEmpty.{u_5 + 1} → Type u_6
inst_1 : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)
inst_2 : (i : PEmpty.{u_5 + 1}) → Module.{u_1, u_6} R (M i)
⊢ length R ((i : PEmpty.{u_5 + 1}) → M i) = ∑ i : PEmpty.{u_5 + 1}, length.{u_1, u_6} R (M i)

Tactic:
simp [Module.length_eq_zero]

Premises used: Module.length_eq_zero
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
ι : Type u_5
h_option :
  ∀ [inst_1 : Fintype ι],
    (∀ (M : ι → Type u_6) [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module.{u_1, u_6} R (M i)],
        length R ((i : ι) → M i) = ∑ i : ι, length.{u_1, u_6} R (M i)) →
      ∀ (M : Option ι → Type u_6) [inst_2 : (i : Option ι) → AddCommGroup (M i)]
        [inst_3 : (i : Option ι) → Module.{u_1, u_6} R (M i)],
        length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
⊢ ∀ [inst_1 : Fintype ι],
    (∀ (M : ι → Type u_6) [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module.{u_1, u_6} R (M i)],
        length R ((i : ι) → M i) = ∑ i : ι, length.{u_1, u_6} R (M i)) →
      ∀ (M : Option ι → Type u_6) [inst_2 : (i : Option ι) → AddCommGroup (M i)]
        [inst_3 : (i : Option ι) → Module.{u_1, u_6} R (M i)],
        length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
ι : Type u_5
inst_1 : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst_2 : (i : ι) → AddCommGroup (M i)] [inst_3 : (i : ι) → Module.{u_1, u_6} R (M i)],
    length R ((i : ι) → M i) = ∑ i : ι, length.{u_1, u_6} R (M i)
M : Option ι → Type u_6
h_option :
  ∀ [inst_2 : (i : Option ι) → AddCommGroup (M i)] [inst_3 : (i : Option ι) → Module.{u_1, u_6} R (M i)],
    length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
⊢ ∀ [inst_2 : (i : Option ι) → AddCommGroup (M i)] [inst_3 : (i : Option ι) → Module.{u_1, u_6} R (M i)],
    length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
ι : Type u_5
inst_1 : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst_3 : (i : ι) → AddCommGroup (M i)] [inst_4 : (i : ι) → Module.{u_1, u_6} R (M i)],
    length R ((i : ι) → M i) = ∑ i : ι, length.{u_1, u_6} R (M i)
M : Option ι → Type u_6
inst_2 : (i : Option ι) → AddCommGroup (M i)
h_option :
  ∀ [inst_3 : (i : Option ι) → Module.{u_1, u_6} R (M i)],
    length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
⊢ ∀ [inst_3 : (i : Option ι) → Module.{u_1, u_6} R (M i)],
    length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
inst : Ring R
ι : Type u_5
inst_1 : Fintype ι
IH :
  ∀ (M : ι → Type u_6) [inst_4 : (i : ι) → AddCommGroup (M i)] [inst_5 : (i : ι) → Module.{u_1, u_6} R (M i)],
    length R ((i : ι) → M i) = ∑ i : ι, length.{u_1, u_6} R (M i)
M : Option ι → Type u_6
inst_2 : (i : Option ι) → AddCommGroup (M i)
inst_3 : (i : Option ι) → Module.{u_1, u_6} R (M i)
h_option : length R (M none × ((i : ι) → M (some i))) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
h_option₁ : length.{u_1, u_6} R (M none) + length R ((i : ι) → M (some i)) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
h_option₂ :
  length.{u_1, u_6} R (M none) + ∑ i : ι, length.{u_1, u_6} R (M (some i)) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
h_option₃ :
  ∑ i : ι, length.{u_1, u_6} R (M (some i)) + length.{u_1, u_6} R (M none) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
h_option₄ :
  ∑ i : ι, length.{u_1, u_6} R (M (some i)) + length.{u_1, u_6} R (M none) =
    length.{u_1, u_6} R (M none) + ∑ i : ι, length.{u_1, u_6} R (M (some i))
h_option₅ h_option₆ :
  length.{u_1, u_6} R (M none) + ∑ i : ι, length.{u_1, u_6} R (M (some i)) =
    length.{u_1, u_6} R (M none) + ∑ i : ι, length.{u_1, u_6} R (M (some i))
⊢ length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)

Tactic:
rw [(LinearEquiv.piOptionEquivProd _).length_eq, Module.length_prod, IH, add_comm,
      Fintype.sum_option, add_comm]

Premises used: Fintype.sum_option, LinearEquiv.length_eq, add_comm, Module.length_prod
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inl : Finite ι → length R (ι →₀ M) = ENat.card ι * length R M
inr : Infinite ι → length R (ι →₀ M) = ENat.card ι * length R M
⊢ length R (ι →₀ M) = ENat.card ι * length R M

Tactic:
cases finite_or_infinite ι

Premises used: finite_or_infinite
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Finite ι
inl : ∀ (val : Fintype ι), length R (ι →₀ M) = ENat.card ι * length R M
⊢ length R (ι →₀ M) = ENat.card ι * length R M

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Finite ι
val : Fintype ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M

Tactic:
simp [(Finsupp.linearEquivFunOnFinite R M ι).length_eq]

Premises used: Finsupp.linearEquivFunOnFinite, LinearEquiv.length_eq
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
⊢ Nontrivial M

Tactic:
nontriviality M
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
rw : ∀ (m : ℕ), (↑m : ℕ∞) ≤ length R (ι →₀ M)
⊢ length R (ι →₀ M) = ENat.card ι * length R M

Tactic:
rw [ENat.card_eq_top_of_infinite, ENat.top_mul length_pos.ne', ENat.eq_top_iff_forall_ge]

Premises used: ENat.card_eq_top_of_infinite, LT.lt.ne', Module.length_pos, ENat.top_mul, ENat.eq_top_iff_forall_ge
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
m : ℕ
obtain : ∀ (s : Finset ι) (hs : s.card = m), (↑m : ℕ∞) ≤ length R (ι →₀ M)
⊢ (↑m : ℕ∞) ≤ length R (ι →₀ M)

Tactic:
obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq ι m

Premises used: Infinite.exists_subset_card_eq
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
⊢ length R (Finsupp.{u_5, u_2} (↥s) M) = (↑m : ℕ∞) * length R M

Tactic:
simp [(Finsupp.linearEquivFunOnFinite R M _).length_eq, hs]

Premises used: Finsupp.linearEquivFunOnFinite, LinearEquiv.length_eq
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
⊢ length R (Finsupp.{u_5, u_2} (↥s) M) = (↑m : ℕ∞) * length R M

Tactic:
have : length R (s →₀ M) = ↑m * length R M := by
    simp [(Finsupp.linearEquivFunOnFinite R M _).length_eq, hs]
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
this : length R (Finsupp.{u_5, u_2} (↥s) M) = (↑m : ℕ∞) * length R M
⊢ (↑m : ℕ∞) ≤ length R (ι →₀ M)

Tactic:
le_trans ?_ (Module.length_le_of_injective (Finsupp.lmapDomain M R ((↑) : s → ι))
    (Finsupp.mapDomain_injective Subtype.val_injective))

Premises used: Subtype.val_injective, Finsupp.lmapDomain, Module.length_le_of_injective, Subtype.val, Finsupp.mapDomain_injective, le_trans
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
this : length R (Finsupp.{u_5, u_2} (↥s) M) = (↑m : ℕ∞) * length R M
refine : (↑m : ℕ∞) ≤ length R (Finsupp.{u_5, u_2} (↥s) M)
⊢ (↑m : ℕ∞) ≤ length R (ι →₀ M)

Tactic:
refine le_trans ?_ (Module.length_le_of_injective (Finsupp.lmapDomain M R ((↑) : s → ι))
    (Finsupp.mapDomain_injective Subtype.val_injective))

Premises used: Subtype.val_injective, Finsupp.lmapDomain, Module.length_le_of_injective, Subtype.val, Finsupp.mapDomain_injective, le_trans
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
this : length R (Finsupp.{u_5, u_2} (↥s) M) = (↑m : ℕ∞) * length R M
rw : (↑m : ℕ∞) ≤ (↑m : ℕ∞) * length R M
⊢ (↑m : ℕ∞) ≤ length R (Finsupp.{u_5, u_2} (↥s) M)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
this : length R (Finsupp.{u_5, u_2} (↥s) M) = (↑m : ℕ∞) * length R M
⊢ (↑m : ℕ∞) ≤ (↑m : ℕ∞) * length R M

Tactic:
ENat.self_le_mul_right _ length_pos.ne'

Premises used: LT.lt.ne', Module.length_pos, ENat.self_le_mul_right
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
m : ℕ
s : Finset ι
hs : s.card = m
this : length R (Finsupp.{u_5, u_2} (↥s) M) = (↑m : ℕ∞) * length R M
⊢ (↑m : ℕ∞) ≤ (↑m : ℕ∞) * length R M

Tactic:
exact ENat.self_le_mul_right _ length_pos.ne'

Premises used: LT.lt.ne', Module.length_pos, ENat.self_le_mul_right
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inl : Finite ι → length R (ι → M) = ENat.card ι * length R M
inr : Infinite ι → length R (ι → M) = ENat.card ι * length R M
⊢ length R (ι → M) = ENat.card ι * length R M

Tactic:
cases finite_or_infinite ι

Premises used: finite_or_infinite
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Finite ι
inl : ∀ (val : Fintype ι), length R (ι → M) = ENat.card ι * length R M
⊢ length R (ι → M) = ENat.card ι * length R M

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Finite ι
val : Fintype ι
⊢ length R (ι → M) = ENat.card ι * length R M

Tactic:
simp
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
rw : ⊤ ≤ length R (ι → M)
⊢ length R (ι → M) = ENat.card ι * length R M

Tactic:
rw [ENat.card_eq_top_of_infinite, ENat.top_mul length_pos.ne', ← top_le_iff]

Premises used: ENat.card_eq_top_of_infinite, LT.lt.ne', Module.length_pos, top_le_iff, ENat.top_mul
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
⊢ ⊤ ≤ length R (ι → M)

Tactic:
le_trans ?_ (Module.length_le_of_injective Finsupp.lcoeFun DFunLike.coe_injective)

Premises used: Module.length_le_of_injective, DFunLike.coe_injective, Finsupp.lcoeFun, le_trans
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
refine : ⊤ ≤ length R (ι →₀ M)
⊢ ⊤ ≤ length R (ι → M)

Tactic:
refine le_trans ?_ (Module.length_le_of_injective Finsupp.lcoeFun DFunLike.coe_injective)

Premises used: Module.length_le_of_injective, le_trans
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
h : Infinite ι
h_1 : Nontrivial M
⊢ ⊤ ≤ length R (ι →₀ M)

Tactic:
simp [ENat.top_mul length_pos.ne']

Premises used: LT.lt.ne', Module.length_pos, ENat.top_mul
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
⊢ Nontrivial M

Tactic:
nontriviality M
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
pos :
  ∀ (H : length R R = ⊤),
    length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
neg :
  ∀ (H : ¬length R R = ⊤),
    length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)

Tactic:
by_cases H : Module.length R R = ⊤

Premises used: Module.length
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : length R R = ⊤
pos :
  Eq (α := ℕ∞) (if ENat.card.{u_2} (Free.ChooseBasisIndex R M) = 0 then 0 else ⊤)
    (if Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (0 : ℕ∞) then 0 else ⊤)
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)

Tactic:
rw [b.repr.length_eq, Module.length_finsupp, H, ENat.mul_top', ENat.mul_top']

Premises used: LinearEquiv.length_eq, ENat.mul_top', Module.Basis.repr, Module.length_finsupp
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
h : Nontrivial R
h_1 : Nontrivial M
H : length R R = ⊤
pos :
  (ENat.card.{u_2} (Free.ChooseBasisIndex R M) = 0) =
    Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (0 : ℕ∞)
⊢ Eq (α := ℕ∞) (if ENat.card.{u_2} (Free.ChooseBasisIndex R M) = 0 then 0 else ⊤)
    (if Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (0 : ℕ∞) then 0 else ⊤)

Tactic:
congr 1