awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
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
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : ¬IsFiniteLength R P
⊢ length R M = length R N + length R P
have this : ¬IsFiniteLength R M
Tactic: have := mt (IsFiniteLength.of_surjective · hg) hP
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
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
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : ¬IsFiniteLength R P
this : ¬IsFiniteLength R M
⊢ length R M = length R N + length R P
have hP₁ : length R P = ⊤
Tactic: rw [← Module.length_ne_top_iff, ne_eq, not_not] at hP this
Cleared hypotheses: hP, this
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
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
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : ¬IsFiniteLength R P
this : ¬IsFiniteLength R M
hP₁ : length R P = ⊤
⊢ length R M = length R N + length R P
have this₁ : length R M = ⊤
Tactic: rw [← Module.length_ne_top_iff, ne_eq, not_not] at hP this
Cleared hypotheses: hP, this
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : length R P = ⊤
this : length R M = ⊤
⊢ length R M = length R N + length R P
have neg : length R M = length R N + ⊤
Tactic: rw [hP, this, add_top]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : length R P = ⊤
this : length R M = ⊤
neg : length R M = length R N + ⊤
⊢ length R M = length R N + length R P
have neg₁ : ⊤ = length R N + ⊤
Tactic: rw [hP, this, add_top]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R N
inst_6 : Module R P
f : N →ₗ[R] M
g : M →ₗ[R] P
hf : Function.Injective.{u_3 + 1, u_2 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑g : (a : M) → P)
H : Function.Exact.{u_3, u_2, u_4} (M := N) (N := M) (P := P) (⇑f : (a : N) → M) (⇑g : (a : M) → P)
hP : length R P = ⊤
this : length R M = ⊤
neg : length R M = length R N + ⊤
neg₁ : ⊤ = length R N + ⊤
⊢ length R M = length R N + length R P
have neg₂ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [hP, this, add_top]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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 M
have rw : length R N ≤ length R N + length.{u_1, u_2} R (M ⧸ f.range)
Tactic: rw [Module.length_eq_add_of_exact f (LinearMap.range f).mkQ hf
    (Submodule.mkQ_surjective _) (LinearMap.exact_map_mkQ_range f)]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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 R M
have rw : length R P ≤ length.{u_1, u_2} R ↥g.ker + length R P
Tactic: rw [Module.length_eq_add_of_exact (LinearMap.ker g).subtype g (Submodule.subtype_injective _) hg
    (LinearMap.exact_subtype_ker_map g)]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
inst : Ring R
⊢ ∀ {ι : 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)
have 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)
Tactic: apply Fintype.induction_empty_option
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
⊢ ∀ {ι : 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)
have 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)
Tactic: apply Fintype.induction_empty_option
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
⊢ ∀ {ι : 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)
have 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)
Tactic: apply Fintype.induction_empty_option
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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
⊢ length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)
have of_equiv : length R ((i' : α) → M ((e : (a : α) → β) 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 ·)]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
⊢ length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)
have of_equiv₁ : Eq (α := ℕ∞) (∑ i : α, length.{u_1, u_6} R (M ((e : (a : α) → β) 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 ·)]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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))
⊢ length R ((i : β) → M i) = ∑ i : β, length.{u_1, u_6} R (M i)
have of_equiv₂ : Eq (α := ℕ∞) (∑ i : β, length.{u_1, u_6} R (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 ·)]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
⊢ length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
have h_option : length R (M none × ((i : ι) → M (some 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]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
⊢ length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
have 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)
Tactic: rw [(LinearEquiv.piOptionEquivProd _).length_eq, Module.length_prod, IH, add_comm,
      Fintype.sum_option, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
⊢ length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
have 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)
Tactic: rw [(LinearEquiv.piOptionEquivProd _).length_eq, Module.length_prod, IH, add_comm,
      Fintype.sum_option, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
⊢ length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
have 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)
Tactic: rw [(LinearEquiv.piOptionEquivProd _).length_eq, Module.length_prod, IH, add_comm,
      Fintype.sum_option, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
⊢ length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
have 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))
Tactic: rw [(LinearEquiv.piOptionEquivProd _).length_eq, Module.length_prod, IH, add_comm,
      Fintype.sum_option, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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))
⊢ length R ((i : Option ι) → M i) = ∑ i : Option ι, length.{u_1, u_6} R (M i)
have 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))
Tactic: rw [(LinearEquiv.piOptionEquivProd _).length_eq, Module.length_prod, IH, add_comm,
      Fintype.sum_option, add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
⊢ length R (ι →₀ M) = ENat.card ι * length R M
have inl : Finite ι → length R (ι →₀ M) = ENat.card ι * length R M
Tactic: cases finite_or_infinite ι
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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
⊢ length R (ι →₀ M) = ENat.card ι * length R M
have inr : Infinite ι → length R (ι →₀ M) = ENat.card ι * length R M
Tactic: cases finite_or_infinite ι
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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 ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M
have inl : ∀ (val : Fintype ι), length R (ι →₀ M) = ENat.card ι * length R M
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
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 ι
⊢ length R (ι →₀ M) = ENat.card ι * length R M
have a : Nontrivial M
Tactic: nontriviality M
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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) = ENat.card ι * length R M
have rw : ∀ (m : ℕ), (↑m : ℕ∞) ≤ length R (ι →₀ M)
Tactic: rw [ENat.card_eq_top_of_infinite, ENat.top_mul length_pos.ne', ENat.eq_top_iff_forall_ge]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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 : ℕ
⊢ (↑m : ℕ∞) ≤ length R (ι →₀ M)
have obtain : ∀ (s : Finset ι) (hs : s.card = m), (↑m : ℕ∞) ≤ length R (ι →₀ M)
Tactic: obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq ι m
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
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
⊢ (↑m : ℕ∞) ≤ length R (ι →₀ M)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
have refine : (↑m : ℕ∞) ≤ length R (Finsupp.{u_5, u_2} (↥s) M)
Tactic: refine le_trans ?_ (Module.length_le_of_injective (Finsupp.lmapDomain M R ((↑) : s → ι))
    (Finsupp.mapDomain_injective Subtype.val_injective))
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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 (Finsupp.{u_5, u_2} (↥s) M)
have rw : (↑m : ℕ∞) ≤ (↑m : ℕ∞) * length R M
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
⊢ length R (ι → M) = ENat.card ι * length R M
have inl : Finite ι → length R (ι → M) = ENat.card ι * length R M
Tactic: cases finite_or_infinite ι
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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
⊢ length R (ι → M) = ENat.card ι * length R M
have inr : Infinite ι → length R (ι → M) = ENat.card ι * length R M
Tactic: cases finite_or_infinite ι
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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 ι
⊢ length R (ι → M) = ENat.card ι * length R M
have inl : ∀ (val : Fintype ι), length R (ι → M) = ENat.card ι * length R M
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
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 ι
⊢ length R (ι → M) = ENat.card ι * length R M
have a : Nontrivial M
Tactic: nontriviality M
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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) = ENat.card ι * length R M
have rw : ⊤ ≤ length R (ι → M)
Tactic: rw [ENat.card_eq_top_of_infinite, ENat.top_mul length_pos.ne', ← top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
have refine : ⊤ ≤ length R (ι →₀ M)
Tactic: refine le_trans ?_ (Module.length_le_of_injective Finsupp.lcoeFun DFunLike.coe_injective)
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
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
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Length (hypothesis)
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
⊢ length R M = HMul.hMul (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_2}) → ℕ∞) (Module.rank R M) : ℕ∞) (length R R)
have a : Nontrivial M
Tactic: nontriviality M