awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
H : IsFiniteLength R M
s : CompositionSeries (Submodule R M)
hs₁ :
  RelSeries.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs₂ :
  RelSeries.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
⊢ length R M ≠ ⊤
have refine_2 : Ne (α := ℕ∞)
  (↑(s.length (r :=
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})) :
    ℕ∞)
  ⊤
Tactic: rw [← length_compositionSeries s hs₁ 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
inst_3 : IsArtinian R M
inst_4 : IsNoetherian R M
⊢ length R M ≠ ⊤
have rw : IsNoetherian R M ∧ IsArtinian R M
Tactic: rw [length_ne_top_iff, isFiniteLength_iff_isNoetherian_isArtinian]
-- 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
⊢ FiniteDimensionalOrder.{u_2} (Submodule R M) ↔ IsFiniteLength R M
have rw : length R M ≠ ⊤ ↔ IsFiniteLength R M
Tactic: rw [← Module.length_ne_top_iff_finiteDimensionalOrder, Module.length_ne_top_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
rw : length R M ≠ ⊤ ↔ IsFiniteLength R M
⊢ FiniteDimensionalOrder.{u_2} (Submodule R M) ↔ IsFiniteLength R M
have rw₁ : IsFiniteLength R M ↔ IsFiniteLength R M
Tactic: rw [← Module.length_ne_top_iff_finiteDimensionalOrder, Module.length_ne_top_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
inst_3 : IsArtinian R M
inst_4 : IsNoetherian R M
⊢ FiniteDimensionalOrder.{u_2} (Submodule R M)
have rw : IsNoetherian R M ∧ IsArtinian R M
Tactic: rw [Module.finiteDimensionalOrder_submodule_iff, isFiniteLength_iff_isNoetherian_isArtinian]
-- 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 : Submodule R M
⊢ length.{u_1, u_2} R ↥N = Order.height N
have a : (↑(length.{u_1, u_2} R ↥N) : WithBot ℕ∞) = (↑(Order.height N) : WithBot ℕ∞)
Tactic: apply WithBot.coe_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
N : Submodule R M
⊢ (↑(length.{u_1, u_2} R ↥N) : WithBot ℕ∞) = (↑(Order.height N) : WithBot ℕ∞)
have a : (↑(length.{u_1, u_2} R ↥N) : WithBot ℕ∞) = Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2)
Tactic: rw [Order.height_eq_krullDim_Iic, coe_length, Order.krullDim_eq_of_orderIso (Submodule.mapIic _)]
-- 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 : Submodule R M
a : (↑(length.{u_1, u_2} R ↥N) : WithBot ℕ∞) = Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2)
⊢ (↑(length.{u_1, u_2} R ↥N) : WithBot ℕ∞) = (↑(Order.height N) : WithBot ℕ∞)
have a₁ : Order.krullDim.{u_2} (Submodule R ↥N) = Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2)
Tactic: rw [Order.height_eq_krullDim_Iic, coe_length, Order.krullDim_eq_of_orderIso (Submodule.mapIic _)]
-- 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 : Submodule R M
a : (↑(length.{u_1, u_2} R ↥N) : WithBot ℕ∞) = Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2)
a₁ : Order.krullDim.{u_2} (Submodule R ↥N) = Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2)
⊢ (↑(length.{u_1, u_2} R ↥N) : WithBot ℕ∞) = (↑(Order.height N) : WithBot ℕ∞)
have a₂ : Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2) = Order.krullDim.{u_2} (↑(Set.Iic N) : Type u_2)
Tactic: rw [Order.height_eq_krullDim_Iic, coe_length, Order.krullDim_eq_of_orderIso (Submodule.mapIic _)]
-- 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 : Submodule R M
⊢ length.{u_1, u_2} R (M ⧸ N) = Order.coheight N
have a : (↑(length.{u_1, u_2} R (M ⧸ N)) : WithBot ℕ∞) = (↑(Order.coheight N) : WithBot ℕ∞)
Tactic: apply WithBot.coe_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
N : Submodule R M
⊢ (↑(length.{u_1, u_2} R (M ⧸ N)) : WithBot ℕ∞) = (↑(Order.coheight N) : WithBot ℕ∞)
have a : (↑(length.{u_1, u_2} R (M ⧸ N)) : WithBot ℕ∞) = Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2)
Tactic: rw [Order.coheight_eq_krullDim_Ici, coe_length,
    Order.krullDim_eq_of_orderIso (Submodule.comapMkQRelIso N)]
-- 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 : Submodule R M
a : (↑(length.{u_1, u_2} R (M ⧸ N)) : WithBot ℕ∞) = Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2)
⊢ (↑(length.{u_1, u_2} R (M ⧸ N)) : WithBot ℕ∞) = (↑(Order.coheight N) : WithBot ℕ∞)
have a₁ : Order.krullDim.{u_2} (Submodule R (M ⧸ N)) = Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2)
Tactic: rw [Order.coheight_eq_krullDim_Ici, coe_length,
    Order.krullDim_eq_of_orderIso (Submodule.comapMkQRelIso N)]
-- 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 : Submodule R M
a : (↑(length.{u_1, u_2} R (M ⧸ N)) : WithBot ℕ∞) = Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2)
a₁ : Order.krullDim.{u_2} (Submodule R (M ⧸ N)) = Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2)
⊢ (↑(length.{u_1, u_2} R (M ⧸ N)) : WithBot ℕ∞) = (↑(Order.coheight N) : WithBot ℕ∞)
have a₂ : Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2) = Order.krullDim.{u_2} (↑(Set.Ici N) : Type u_2)
Tactic: rw [Order.coheight_eq_krullDim_Ici, coe_length,
    Order.krullDim_eq_of_orderIso (Submodule.comapMkQRelIso N)]
-- 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
e : M ≃ₗ[R] N
⊢ Module.length R M = Module.length R N
have a : (↑(Module.length R M) : WithBot ℕ∞) = (↑(Module.length R N) : WithBot ℕ∞)
Tactic: apply WithBot.coe_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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
⊢ (↑(Module.length R M) : WithBot ℕ∞) = (↑(Module.length R N) : WithBot ℕ∞)
have a : Order.krullDim.{u_2} (Submodule R M) = (↑(Module.length R N) : WithBot ℕ∞)
Tactic: rw [Module.coe_length, Module.coe_length,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComap e)]
-- 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
e : M ≃ₗ[R] N
a : Order.krullDim.{u_2} (Submodule R M) = (↑(Module.length R N) : WithBot ℕ∞)
⊢ (↑(Module.length R M) : WithBot ℕ∞) = (↑(Module.length R N) : WithBot ℕ∞)
have a₁ : Order.krullDim.{u_2} (Submodule R M) = Order.krullDim.{u_3} (Submodule R N)
Tactic: rw [Module.coe_length, Module.coe_length,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComap e)]
-- 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
e : M ≃ₗ[R] N
a : Order.krullDim.{u_2} (Submodule R M) = (↑(Module.length R N) : WithBot ℕ∞)
a₁ : Order.krullDim.{u_2} (Submodule R M) = Order.krullDim.{u_3} (Submodule R N)
⊢ (↑(Module.length R M) : WithBot ℕ∞) = (↑(Module.length R N) : WithBot ℕ∞)
have a₂ : Order.krullDim.{u_3} (Submodule R N) = Order.krullDim.{u_3} (Submodule R N)
Tactic: rw [Module.coe_length, Module.coe_length,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComap e)]
-- 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
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
h : Function.Surjective.{u_3 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
⊢ length S M = length R M
have this : RingHomSurjective (algebraMap S R)
Tactic: have : RingHomSurjective (algebraMap S R) := ⟨h⟩
-- 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
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
h : Function.Surjective.{u_3 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
this : RingHomSurjective (algebraMap S R)
f : M →ₛₗ[algebraMap S R] M := { toAddHom := AddHom.id M, map_smul' := ⋯ }
⊢ length S M = length R M
have rw : (Order.krullDim.{u_2} (Submodule S M)).unbot sorry = length R M
Tactic: rw [Module.length, Module.length, WithBot.unbot_inj,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective f Function.bijective_id)]
-- 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
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
h : Function.Surjective.{u_3 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
this : RingHomSurjective (algebraMap S R)
f : M →ₛₗ[algebraMap S R] M := { toAddHom := AddHom.id M, map_smul' := ⋯ }
rw : (Order.krullDim.{u_2} (Submodule S M)).unbot ⋯ = length R M
⊢ length S M = length R M
have rw₁ : (Order.krullDim.{u_2} (Submodule S M)).unbot sorry = (Order.krullDim.{u_2} (Submodule R M)).unbot sorry
Tactic: rw [Module.length, Module.length, WithBot.unbot_inj,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective f Function.bijective_id)]
-- 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
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
h : Function.Surjective.{u_3 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
this : RingHomSurjective (algebraMap S R)
f : M →ₛₗ[algebraMap S R] M := { toAddHom := AddHom.id M, map_smul' := ⋯ }
rw : (Order.krullDim.{u_2} (Submodule S M)).unbot ⋯ = length R M
rw₁ : (Order.krullDim.{u_2} (Submodule S M)).unbot ⋯ = (Order.krullDim.{u_2} (Submodule R M)).unbot ⋯
⊢ length S M = length R M
have rw₂ : Order.krullDim.{u_2} (Submodule S M) = Order.krullDim.{u_2} (Submodule R M)
Tactic: rw [Module.length, Module.length, WithBot.unbot_inj,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective f Function.bijective_id)]
-- 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
S : Type u_3
inst_3 : CommRing S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
h : Function.Surjective.{u_3 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
this : RingHomSurjective (algebraMap S R)
f : M →ₛₗ[algebraMap S R] M := { toAddHom := AddHom.id M, map_smul' := ⋯ }
rw : (Order.krullDim.{u_2} (Submodule S M)).unbot ⋯ = length R M
rw₁ : (Order.krullDim.{u_2} (Submodule S M)).unbot ⋯ = (Order.krullDim.{u_2} (Submodule R M)).unbot ⋯
rw₂ : Order.krullDim.{u_2} (Submodule S M) = Order.krullDim.{u_2} (Submodule R M)
⊢ length S M = length R M
have rw₃ : Order.krullDim.{u_2} (Submodule R M) = Order.krullDim.{u_2} (Submodule R M)
Tactic: rw [Module.length, Module.length, WithBot.unbot_inj,
    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective f Function.bijective_id)]
-- 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
⊢ length.{u_1, u_2} R ↥⊤ = length R M
have rw : Order.height.{u_2} (α := Submodule R M) ⊤ = length R M
Tactic: rw [Module.length_submodule, Module.length_eq_height]
-- 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
rw : Order.height.{u_2} (α := Submodule R M) ⊤ = length R M
⊢ length.{u_1, u_2} R ↥⊤ = length R M
have rw₁ : Order.height.{u_2} (α := Submodule R M) ⊤ = Order.height.{u_2} (α := Submodule R M) ⊤
Tactic: rw [Module.length_submodule, Module.length_eq_height]
-- 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)
⊢ length R M = length R N + length R P
have pos : ∀ (hP : IsFiniteLength R P), length R M = length R N + length R P
Tactic: by_cases hP : IsFiniteLength R P
-- 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)
pos : ∀ (hP : IsFiniteLength R P), length R M = length R N + length R P
⊢ length R M = length R N + length R P
have neg : ∀ (hP : ¬IsFiniteLength R P), length R M = length R N + length R P
Tactic: by_cases hP : IsFiniteLength R P
-- 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 : IsFiniteLength R P
⊢ length R M = length R N + length R P
have pos : ∀ (hN : IsFiniteLength R N), length R M = length R N + length R P
Tactic: by_cases hN : IsFiniteLength R N
-- 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 : IsFiniteLength R P
pos : ∀ (hN : IsFiniteLength R N), length R M = length R N + length R P
⊢ length R M = length R N + length R P
have neg : ∀ (hN : ¬IsFiniteLength R N), length R M = length R N + length R P
Tactic: by_cases hN : IsFiniteLength R N
-- 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 : IsFiniteLength R P
hN : IsFiniteLength R N
⊢ length R M = length R N + length R P
have pos : ∀ (s : CompositionSeries (Submodule R P))
  (hs₁ :
    RelSeries.head (r :=
        {x : Submodule R P × Submodule R P |
          match (motive := Submodule R P × Submodule R P → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        s =
      ⊥)
  (hs₂ :
    RelSeries.last (r :=
        {x : Submodule R P × Submodule R P |
          match (motive := Submodule R P × Submodule R P → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        s =
      ⊤),
  length R M = length R N + length R P
Tactic: obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hP
-- 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 : IsFiniteLength R P
hN : IsFiniteLength R N
s : CompositionSeries (Submodule R P)
hs₁ :
  RelSeries.head (r :=
      {x : Submodule R P × Submodule R P |
        match (motive := Submodule R P × Submodule R P → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
hs₂ :
  RelSeries.last (r :=
      {x : Submodule R P × Submodule R P |
        match (motive := Submodule R P × Submodule R P → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
⊢ length R M = length R N + length R P
have pos : ∀ (t : CompositionSeries (Submodule R N))
  (ht₁ :
    RelSeries.head (r :=
        {x : Submodule R N × Submodule R N |
          match (motive := Submodule R N × Submodule R N → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        t =
      ⊥)
  (ht₂ :
    RelSeries.last (r :=
        {x : Submodule R N × Submodule R N |
          match (motive := Submodule R N × Submodule R N → Prop) x with
          | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
        t =
      ⊤),
  length R M = length R N + length R P
Tactic: obtain ⟨t, ht₁, ht₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hN
-- 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
hN : ¬IsFiniteLength R N
⊢ length R M = length R N + length R P
have this : ¬IsFiniteLength R M
Tactic: have := mt (IsFiniteLength.of_injective · hf) hN
-- 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
hN : ¬IsFiniteLength R N
this : ¬IsFiniteLength R M
⊢ length R M = length R N + length R P
have hN₁ : length R N = ⊤
Tactic: rw [← Module.length_ne_top_iff, ne_eq, not_not] at hN this
Cleared hypotheses: hN, 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
hN : ¬IsFiniteLength R N
this : ¬IsFiniteLength R M
hN₁ : length R N = ⊤
⊢ 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 hN this
Cleared hypotheses: hN, 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 : IsFiniteLength R P
hN : length R N = ⊤
this : length R M = ⊤
⊢ length R M = length R N + length R P
have neg : length R M = ⊤ + length R P
Tactic: rw [hN, this, top_add]
-- 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 : IsFiniteLength R P
hN : length R N = ⊤
this : length R M = ⊤
neg : length R M = ⊤ + length R P
⊢ length R M = length R N + length R P
have neg₁ : ⊤ = ⊤ + length R P
Tactic: rw [hN, this, top_add]
-- 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 : IsFiniteLength R P
hN : length R N = ⊤
this : length R M = ⊤
neg : length R M = ⊤ + length R P
neg₁ : ⊤ = ⊤ + length R P
⊢ length R M = length R N + length R P
have neg₂ : Eq (α := ℕ∞) ⊤ ⊤
Tactic: rw [hN, this, top_add]