awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
⊢ N ≤ I • N
have this : I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (k + 1)
Tactic: have := hk k (le_refl _)
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
this : I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (k + 1)
⊢ N ≤ I • N
have this₁ : I • N = N
Tactic: rw [hN, hN] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x →
    ∃ (r : ↥I), (↑r : R) • x = x
have mp : ∀ (r : R) (hr₁ : r ∈ I) (hr₂ : ∀ n ∈ N, r • n = n),
  Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x →
    ∃ (r : ↥I), (↑r : R) • x = x
Tactic: obtain ⟨r, hr₁, hr₂⟩ :=
      Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I N (IsNoetherian.noetherian N) (by
        obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)
        have := hk k (le_refl _)
        rw [hN, hN] at this
        exact le_of_eq this.symm)
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : (↑r : R) • x = x
⊢ Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
have mpr : ∀ (i : ℕ), x ∈ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
Tactic: rw [Submodule.mem_iInf]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : (↑r : R) • x = x
i : ℕ
hi : x ∈ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
⊢ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ (i + 1)) ⊤
have mpr : (↑r : R) • x ∈ I • HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
Tactic: rw [add_comm, pow_add, ← smul_smul, pow_one, ← eq]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : (↑r : R) • x = x
i : ℕ
⊢ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
have mpr : x ∈ HSMul.hSMul (β := Submodule R M) (HPow.hPow (β := ℕ) I 0) ⊤
Tactic: induction i with
    | zero => simp
    | succ i hi =>
      rw [add_comm, pow_add, ← smul_smul, pow_one, ← eq]
      exact Submodule.smul_mem_smul r.prop hi
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : (↑r : R) • x = x
i : ℕ
mpr : x ∈ HSMul.hSMul (β := Submodule R M) (HPow.hPow (β := ℕ) I 0) ⊤
⊢ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤
have mpr₁ : ∀ (i : ℕ) (hi : x ∈ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤), x ∈ HSMul.hSMul (β := Submodule R M) (I ^ (i + 1)) ⊤
Tactic: induction i with
    | zero => simp
    | succ i hi =>
      rw [add_comm, pow_add, ← smul_smul, pow_one, ← eq]
      exact Submodule.smul_mem_smul r.prop hi
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ jacobson ⊥
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) ⊥
have rw : LE.le.{u_2} (α := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ jacobson ⊥
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have obtain : ∀ (r : ↥I) (hr : (↑r : R) • x = x), Membership.mem (γ := Submodule R M) ⊥ x
Tactic: obtain ⟨r, hr⟩ := (I.mem_iInf_smul_pow_eq_bot_iff x).mp hx
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ jacobson ⊥
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
r : ↥I
hr : (↑r : R) • x = x
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have this : IsUnit (1 - (↑r : R))
Tactic: have := isUnit_of_sub_one_mem_jacobson_bot (1 - r.1) (by simpa using h r.2)
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
h : I ≤ jacobson ⊥
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
r : ↥I
hr : (↑r : R) • x = x
this : IsUnit (1 - (↑r : R))
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have apply : (1 - (↑r : R)) • x = HSMul.hSMul (β := M) (1 - (↑r : R)) 0
Tactic: apply this.smul_left_cancel.mp
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
h : I ≠ ⊤
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : ℕ), I ^ i) ⊥
have h₁ : ∀ (x : ℕ), I ^ x = HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤
Tactic: convert! I.iInf_pow_smul_eq_bot_of_isLocalRing (M := R) h
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
h : I ≠ ⊤
x : ℕ
⊢ I ^ x = HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤
have h₁ : ∀ (i : R), i ∈ I ^ x ↔ i ∈ HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
h : I ≠ ⊤
x : ℕ
i : R
⊢ i ∈ I ^ x ↔ i ∈ HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤
have h₁ : i ∈ I ^ x ↔ i ∈ I ^ x * ⊤
Tactic: rw [smul_eq_mul, ← Ideal.one_eq_top, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
h : I ≠ ⊤
x : ℕ
i : R
h₁ : i ∈ I ^ x ↔ i ∈ I ^ x * ⊤
⊢ i ∈ I ^ x ↔ i ∈ HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤
have h₂ : i ∈ I ^ x ↔ i ∈ I ^ x * 1
Tactic: rw [smul_eq_mul, ← Ideal.one_eq_top, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
h : I ≠ ⊤
x : ℕ
i : R
h₁ : i ∈ I ^ x ↔ i ∈ I ^ x * ⊤
h₂ : i ∈ I ^ x ↔ i ∈ I ^ x * 1
⊢ i ∈ I ^ x ↔ i ∈ HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤
have h₃ : i ∈ I ^ x ↔ i ∈ I ^ x
Tactic: rw [smul_eq_mul, ← Ideal.one_eq_top, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
have mp : IsIdempotentElem I → I = ⊥ ∨ I = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
mp : IsIdempotentElem I → I = ⊥ ∨ I = ⊤
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
have mpr : I = ⊥ ∨ I = ⊤ → IsIdempotentElem I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤
have pos : I = ⊤ → I = ⊥ ∨ I = ⊤
Tactic: by_cases I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
pos : I = ⊤ → I = ⊥ ∨ I = ⊤
⊢ I = ⊥ ∨ I = ⊤
have neg : ¬I = ⊤ → I = ⊥ ∨ I = ⊤
Tactic: by_cases I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : ¬I = ⊤
⊢ I = ⊥ ∨ I = ⊤
have neg : I ≤ ⊥
Tactic: refine Or.inl (eq_bot_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : ¬I = ⊤
⊢ I ≤ ⊥
have neg : I ≤ ⨅ (i : ℕ), I ^ i
Tactic: rw [← Ideal.iInf_pow_eq_bot_of_isLocalRing I ‹_›]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h : ¬I = ⊤
⊢ I ≤ ⨅ (i : ℕ), I ^ i
have neg : ∀ (i : ℕ), I ≤ I ^ i
Tactic: apply le_iInf
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
⊢ Eq.{u_2 + 1} (α := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) ⊥
have rw : LE.le.{u_2} (α := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have by_contra : ∀ (hx' : x ∉ ⊥), False
Tactic: by_contra hx'
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
hx' : x ∉ ⊥
⊢ False
have this : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
  ∃ (r : ↥I), (↑r : R) • x = x
Tactic: have := Ideal.mem_iInf_smul_pow_eq_bot_iff I x
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
hx' : x ∉ ⊥
this :
  Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x
⊢ False
have obtain : ∀ (r : ↥I) (hr : (↑r : R) • x = x), False
Tactic: obtain ⟨r, hr⟩ := this.mp hx
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
inst_3 : IsDomain R
inst_4 : IsNoetherianRing R
inst_5 : Module.IsTorsionFree R M
inst_6 : Module.Finite R M
h : I ≠ ⊤
x : M
hx : Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x
hx' : x ∉ ⊥
this :
  Membership.mem (γ := Submodule R M) (⨅ (i : ℕ), HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) x ↔
    ∃ (r : ↥I), (↑r : R) • x = x
r : ↥I
hr : (↑r : R) • x = x
⊢ False
have this₁ : (↑r : R) = 1
Tactic: have := smul_left_injective _ hx' (hr.trans (one_smul _ x).symm)
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
inst_2 : IsDomain R
h : I ≠ ⊤
⊢ Eq.{u_1 + 1} (α := Ideal R) (⨅ (i : ℕ), I ^ i) ⊥
have h₁ : ∀ (x : ℕ), I ^ x = HSMul.hSMul (β := Submodule R R) (I ^ x) ⊤
Tactic: convert! I.iInf_pow_smul_eq_bot_of_isTorsionFree (M := R) h
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M_1 : Type u_2
inst_3 : AddCommGroup M_1
inst_4 : Module R M_1
inst_5 : Subsingleton M_1
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
e : M_1 ≃ₗ[R] N
⊢ IsFiniteLength R N
have this : Subsingleton N
Tactic: have := e.symm.toEquiv.subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
S : Submodule R M
inst_5 : IsSimpleModule.{u_1, u_2} R (M ⧸ S)
h : IsFiniteLength.{u_1, u_2} R ↥S
ih :
  ∀ {N : Type u_3} [inst_8 : AddCommGroup N] [inst_9 : Module R N]
    (e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥S) N), IsFiniteLength R N
N : Type u_3
inst_6 : AddCommGroup N
inst_7 : Module R N
e : M ≃ₗ[R] N
⊢ IsFiniteLength R N
have this : IsSimpleModule.{u_1, u_3} R (N ⧸ Submodule.map (↑e : M →ₗ[R] N) S)
Tactic: have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
      IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
h : IsFiniteLength R M
⊢ IsFiniteLength R N
have of_subsingleton : ∀ {M : Type u_2} [inst_5 : AddCommGroup M] [inst_6 : Module R M] [Subsingleton M] {N : Type u_3}
  [inst_8 : AddCommGroup N] [inst_9 : Module R N] (e : M ≃ₗ[R] N), IsFiniteLength R N
Tactic: induction h generalizing N with
  | of_subsingleton =>
    have := e.symm.toEquiv.subsingleton; exact .of_subsingleton
  | @of_simple_quotient M _ _ S _ _ ih =>
    have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
      IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
    exact .of_simple_quotient (ih <| e.submoduleMap S)
Cleared hypotheses: N, inst_3, inst_4, e, h
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
h : IsFiniteLength R M
of_subsingleton :
  ∀ {M : Type u_2} [inst_5 : AddCommGroup M] [inst_6 : Module R M] [Subsingleton M] {N : Type u_3}
    [inst_8 : AddCommGroup N] [inst_9 : Module R N] (e : M ≃ₗ[R] N), IsFiniteLength R N
⊢ IsFiniteLength R N
have of_simple_quotient : ∀ {M : Type u_2} [inst_5 : AddCommGroup M] [inst_6 : Module R M] {S : Submodule R M}
  [IsSimpleModule.{u_1, u_2} R (M ⧸ S)],
  IsFiniteLength.{u_1, u_2} R ↥S →
    ∀
      (ih :
        ∀ {N : Type u_3} [inst_8 : AddCommGroup N] [inst_9 : Module R N]
          (e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥S) N), IsFiniteLength R N)
      {N : Type u_3} [inst_8 : AddCommGroup N] [inst_9 : Module R N] (e : M ≃ₗ[R] N), IsFiniteLength R N
Tactic: induction h generalizing N with
  | of_subsingleton =>
    have := e.symm.toEquiv.subsingleton; exact .of_subsingleton
  | @of_simple_quotient M _ _ S _ _ ih =>
    have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
      IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
    exact .of_simple_quotient (ih <| e.submoduleMap S)
Cleared hypotheses: N, inst_3, inst_4, e, h
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
inst_4 : IsArtinian R M
⊢ ∃ (s : CompositionSeries (Submodule R M)),
    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 =
        ⊥ ∧
      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 =
        ⊤
have obtain : ∀ (f : ℕ → Submodule R M) (f0 : IsMin (f 0)) (n : ℕ) (hn : IsMax (f n) ∧ ∀ i < n, f i ⋖ f (i + 1)),
  ∃ (s : CompositionSeries (Submodule R M)),
    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 =
        ⊥ ∧
      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 =
        ⊤
Tactic: obtain ⟨f, f0, n, hn⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (Submodule R M)
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  ∃ (s : CompositionSeries (Submodule R M)),
    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 =
        ⊥ ∧
      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 =
        ⊤
⊢ IsFiniteLength.{u_1, u_2} R ↥⊤
have obtain : ∀ (s : CompositionSeries (Submodule R M))
  (s_head :
    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 =
      ⊥)
  (s_last :
    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 =
      ⊤),
  IsFiniteLength.{u_1, u_2} R ↥⊤
Tactic: obtain ⟨s, s_head, s_last⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
s_head :
  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 =
    ⊥
s_last :
  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 =
    ⊤
⊢ IsFiniteLength.{u_1, u_2} R ↥⊤
have rw : IsFiniteLength.{u_1, u_2} R
  ↥(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)
Tactic: rw [← s_last]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
s_head :
  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 =
    ⊥
s_last :
  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 =
    ⊤
⊢ IsFiniteLength.{u_1, u_2} R
    ↥(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)
have suffices : ∀
  (i :
    Fin
      (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}) +
        1)),
  IsFiniteLength.{u_1, u_2} R
    ↥(s.toFun (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})
        i)
Tactic: suffices ∀ i, IsFiniteLength R (s i) from this (Fin.last _)