awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup P
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R N
ι : Type u_5
inst_7 : Finite ι
apply :
  ∀ {α β : Type u_5} (a : α ≃ β),
    (∀ {M : α → Submodule R P} [∀ (i : α), IsArtinian.{u_1, u_3} R ↥(M i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : α), M i)) →
      ∀ {M : β → Submodule R P} [∀ (i : β), IsArtinian.{u_1, u_3} R ↥(M i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : β), M i)
⊢ ∀ {M : ι → Submodule R P} [∀ (i : ι), IsArtinian.{u_1, u_3} R ↥(M i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : ι), M i)
have apply₁ : ∀ {M : PEmpty.{u_5 + 1} → Submodule R P} [∀ (i : PEmpty.{u_5 + 1}), IsArtinian.{u_1, u_3} R ↥(M i)],
  IsArtinian.{u_1, u_3} R ↥(⨆ (i : PEmpty.{u_5 + 1}), M i)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup P
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R N
ι : Type u_5
inst_7 : Finite ι
apply :
  ∀ {α β : Type u_5} (a : α ≃ β),
    (∀ {M : α → Submodule R P} [∀ (i : α), IsArtinian.{u_1, u_3} R ↥(M i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : α), M i)) →
      ∀ {M : β → Submodule R P} [∀ (i : β), IsArtinian.{u_1, u_3} R ↥(M i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : β), M i)
apply₁ :
  ∀ {M : PEmpty.{u_5 + 1} → Submodule R P} [∀ (i : PEmpty.{u_5 + 1}), IsArtinian.{u_1, u_3} R ↥(M i)],
    IsArtinian.{u_1, u_3} R ↥(⨆ (i : PEmpty.{u_5 + 1}), M i)
⊢ ∀ {M : ι → Submodule R P} [∀ (i : ι), IsArtinian.{u_1, u_3} R ↥(M i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : ι), M i)
have apply₂ : ∀ {α : Type u_5} [Fintype α],
  (∀ {M : α → Submodule R P} [∀ (i : α), IsArtinian.{u_1, u_3} R ↥(M i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : α), M i)) →
    ∀ {M : Option α → Submodule R P} [∀ (i : Option α), IsArtinian.{u_1, u_3} R ↥(M i)],
      IsArtinian.{u_1, u_3} R ↥(⨆ (i : Option α), M i)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup P
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R N
ι : Type u_5
inst_7 : Finite ι
α β : Type u_5
e : α ≃ β
h : ∀ {M : α → Submodule R P} [∀ (i : α), IsArtinian.{u_1, u_3} R ↥(M i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : α), M i)
M_1 : β → Submodule R P
inst_8 : ∀ (i : β), IsArtinian.{u_1, u_3} R ↥(M_1 i)
⊢ IsArtinian.{u_1, u_3} R ↥(⨆ (i : β), M_1 i)
have rw : IsArtinian.{u_1, u_3} R ↥(⨆ (x : α), M_1 ((e : (a : α) → β) x))
Tactic: rw [← e.iSup_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup P
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R N
ι : Type u_5
inst_7 : Finite ι
M_1 : PEmpty.{u_5 + 1} → Submodule R P
inst_8 : ∀ (i : PEmpty.{u_5 + 1}), IsArtinian.{u_1, u_3} R ↥(M_1 i)
⊢ IsArtinian.{u_1, u_3} R ↥(⨆ (i : PEmpty.{u_5 + 1}), M_1 i)
have rw : IsArtinian.{u_1, u_3} R ↥⊥
Tactic: rw [iSup_of_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup P
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R N
ι : Type u_5
inst_7 : Finite ι
α : Type u_5
inst_8 : Fintype α
ih : ∀ {M : α → Submodule R P} [∀ (i : α), IsArtinian.{u_1, u_3} R ↥(M i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : α), M i)
M_1 : Option α → Submodule R P
inst_9 : ∀ (i : Option α), IsArtinian.{u_1, u_3} R ↥(M_1 i)
⊢ IsArtinian.{u_1, u_3} R ↥(⨆ (i : Option α), M_1 i)
have rw : IsArtinian.{u_1, u_3} R ↥(M_1 none ⊔ ⨆ (b : α), M_1 (some b))
Tactic: rw [iSup_option]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (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
h : Eq (α := Submodule R M) (Module.jacobson R M) ⊥
s : Finset { m : Submodule R M // IsCoatom m }
hs :
  ∀ (a : { m : Submodule R M // IsCoatom m }),
    s.inf (Subtype.val (p := fun (m : Submodule R M) ↦ IsCoatom m)) ≤ (↑a : Submodule R M)
h_1 : ∀ (m : ↥s), IsSimpleModule.{u_1, u_2} R (M ⧸ (↑(↑m : { m : Submodule R M // IsCoatom m }) : Submodule R M))
f : M →ₗ[R] (m : ↥s) → M ⧸ (↑(↑m : { m : Submodule R M // IsCoatom m }) : Submodule R M) :=
  LinearMap.pi (φ := fun (m : ↥s) ↦ M ⧸ (↑(↑m : { m : Submodule R M // IsCoatom m }) : Submodule R M)) fun (m : ↥s) ↦
    (↑(↑m : { m : Submodule R M // IsCoatom m }) : Submodule R M).mkQ
x : M
hx : x ∈ f.ker
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have rw : ∀ (p : Submodule R M), Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | IsCoatom m} p → x ∈ p
Tactic: rw [← h, Module.jacobson, Submodule.mem_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (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
f : Module.End R M
⊢ ∀ᶠ (n : ℕ) in atTop, Codisjoint (f ^ n).ker (f ^ n).range
have obtain : ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)),
  ∀ᶠ (n : ℕ) in atTop, Codisjoint (f ^ n).ker (f ^ n).range
Tactic: obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.range (f ^ n) = LinearMap.range (f ^ m)⟩ :=
    IsArtinian.monotone_stabilizes f.iterateRange
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (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
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
⊢ ∀ᶠ (n : ℕ) in atTop, Codisjoint (f ^ n).ker (f ^ n).range
have refine : ∀ (m : ℕ) (hm : m ≥ n), (f ^ m).ker ⊔ (f ^ m).range = ⊤
Tactic: refine eventually_atTop.mpr ⟨n, fun m hm ↦ codisjoint_iff.mpr ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (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
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : m ≥ n
⊢ (f ^ m).ker ⊔ (f ^ m).range = ⊤
have simp_rw : ∀ (x : M), ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x
Tactic: simp_rw [← hn _ hm, Submodule.eq_top_iff', Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (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
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : m ≥ n
x : M
⊢ ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x
have rsuffices : ∀ (y : M) (hy : Eq (α := M) ((f ^ m : (a : M) → M) ((f ^ n : (a : M) → M) y : M) : M) ((f ^ m : (a : M) → M) x : M)),
  ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x
Tactic: rsuffices ⟨y, hy⟩ : ∃ y, (f ^ m) ((f ^ n) y) = (f ^ m) x
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (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
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : m ≥ n
x : M
rsuffices :
  ∀ (y : M) (hy : Eq (α := M) ((f ^ m : (a : M) → M) ((f ^ n : (a : M) → M) y : M) : M) ((f ^ m : (a : M) → M) x : M)),
    ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x
⊢ ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x
have rsuffices₁ : ∃ (y : M), Eq (α := M) ((f ^ m : (a : M) → M) ((f ^ n : (a : M) → M) y : M) : M) ((f ^ m : (a : M) → M) x : M)
Tactic: rsuffices ⟨y, hy⟩ : ∃ y, (f ^ m) ((f ^ n) y) = (f ^ m) x
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (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
f : Module.End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)
m : ℕ
hm : m ≥ n
x : M
⊢ ∃ (y : M), Eq (α := M) ((f ^ m : (a : M) → M) ((f ^ n : (a : M) → M) y : M) : M) ((f ^ m : (a : M) → M) x : M)
have simp_rw : Membership.mem (α := M) (range (f ^ m)) ((f ^ m : (a : M) → M) x : M)
Tactic: simp_rw [f.pow_apply n, f.pow_apply m, ← iterate_add_apply, ← f.pow_apply (m + n),
    ← f.pow_apply m, ← mem_range (f := _), ← hn _ (n.le_add_left m), hn _ hm]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (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
f : Module.End R M
⊢ ∀ᶠ (n : ℕ) in atTop, IsCompl (f ^ n).ker (f ^ n).range
have h : ∀ (n : ℕ) (hn : Disjoint (f ^ n).ker (f ^ n).range ∧ Codisjoint (f ^ n).ker (f ^ n).range),
  IsCompl (f ^ n).ker (f ^ n).range
Tactic: filter_upwards [f.eventually_disjoint_ker_pow_range_pow.and
    f.eventually_codisjoint_ker_pow_range_pow] with n hn
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (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
f : M →ₗ[R] M
⊢ IsCompl.{u_2} (α := Submodule R M) (⨆ (n : ℕ), (f ^ n).ker) (⨅ (n : ℕ), (f ^ n).range)
have obtain : ∀ (k : ℕ)
  (hk :
    ∀ b ≥ k,
      IsCompl (f ^ b).ker (f ^ b).range ∧
        ⨅ (m : ℕ), (f ^ m).range = (f ^ b).range ∧ ⨆ (m : ℕ), (f ^ m).ker = (f ^ b).ker),
  IsCompl.{u_2} (α := Submodule R M) (⨆ (n : ℕ), (f ^ n).ker) (⨅ (n : ℕ), (f ^ n).range)
Tactic: obtain ⟨k, hk⟩ := eventually_atTop.mp <| f.eventually_isCompl_ker_pow_range_pow.and <|
    f.eventually_iInf_range_pow_eq.and f.eventually_iSup_ker_pow_eq
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
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
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ b ≥ k,
    IsCompl (f ^ b).ker (f ^ b).range ∧ ⨅ (m : ℕ), (f ^ m).range = (f ^ b).range ∧ ⨆ (m : ℕ), (f ^ m).ker = (f ^ b).ker
⊢ IsCompl.{u_2} (α := Submodule R M) (⨆ (n : ℕ), (f ^ n).ker) (⨅ (n : ℕ), (f ^ n).range)
have h₁ : IsCompl (f ^ k).ker (f ^ k).range
Tactic: obtain ⟨h₁, h₂, h₃⟩ := hk k (le_refl k)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
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
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ b ≥ k,
    IsCompl (f ^ b).ker (f ^ b).range ∧ ⨅ (m : ℕ), (f ^ m).range = (f ^ b).range ∧ ⨆ (m : ℕ), (f ^ m).ker = (f ^ b).ker
h₁ : IsCompl (f ^ k).ker (f ^ k).range
⊢ IsCompl.{u_2} (α := Submodule R M) (⨆ (n : ℕ), (f ^ n).ker) (⨅ (n : ℕ), (f ^ n).range)
have h₂ : ⨅ (m : ℕ), (f ^ m).range = (f ^ k).range
Tactic: obtain ⟨h₁, h₂, h₃⟩ := hk k (le_refl k)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
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
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ b ≥ k,
    IsCompl (f ^ b).ker (f ^ b).range ∧ ⨅ (m : ℕ), (f ^ m).range = (f ^ b).range ∧ ⨆ (m : ℕ), (f ^ m).ker = (f ^ b).ker
h₁ : IsCompl (f ^ k).ker (f ^ k).range
h₂ : ⨅ (m : ℕ), (f ^ m).range = (f ^ k).range
⊢ IsCompl.{u_2} (α := Submodule R M) (⨆ (n : ℕ), (f ^ n).ker) (⨅ (n : ℕ), (f ^ n).range)
have h₃ : ⨆ (m : ℕ), (f ^ m).ker = (f ^ k).ker
Tactic: obtain ⟨h₁, h₂, h₃⟩ := hk k (le_refl k)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (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
f : M →ₗ[R] M
k : ℕ
hk :
  ∀ b ≥ k,
    IsCompl (f ^ b).ker (f ^ b).range ∧ ⨅ (m : ℕ), (f ^ m).range = (f ^ b).range ∧ ⨆ (m : ℕ), (f ^ m).ker = (f ^ b).ker
h₁ : IsCompl (f ^ k).ker (f ^ k).range
h₂ : ⨅ (m : ℕ), (f ^ m).range = (f ^ k).range
h₃ : ⨆ (m : ℕ), (f ^ m).ker = (f ^ k).ker
⊢ IsCompl.{u_2} (α := Submodule R M) (⨆ (n : ℕ), (f ^ n).ker) (⨅ (n : ℕ), (f ^ n).range)
have rwa : IsCompl (⨆ (n : ℕ), (f ^ n).ker) (f ^ k).range
Tactic: rwa [h₂, h₃]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
h_1 :
  Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range) m) x
y : M
hy : (HSMul.hSMul (β := M →ₗ[R] M) (r ^ m) LinearMap.id : (a : M) → M) y = x
⊢ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id : (a : M) → M) (r ^ (m - n) • y) = x
have dsimp : r ^ n • r ^ (m - n) • y = x
Tactic: dsimp at hy ⊢
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
h_1 :
  Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range) m) x
y : M
hy : r ^ m • y = x
⊢ r ^ n • r ^ (m - n) • y = x
have rw : (r ^ n • r ^ (m - n)) • y = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
h_1 :
  Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range) m) x
y : M
hy : r ^ m • y = x
rw : (r ^ n • r ^ (m - n)) • y = x
⊢ r ^ n • r ^ (m - n) • y = x
have rw₁ : (r ^ n * r ^ (m - n)) • y = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
h_1 :
  Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range) m) x
y : M
hy : r ^ m • y = x
rw : (r ^ n • r ^ (m - n)) • y = x
rw₁ : (r ^ n * r ^ (m - n)) • y = x
⊢ r ^ n • r ^ (m - n) • y = x
have rw₂ : r ^ (n + (m - n)) • y = x
Tactic: rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
h_1 :
  Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range) m) x
y : M
hy : r ^ m • y = x
rw : (r ^ n • r ^ (m - n)) • y = x
rw₁ : (r ^ n * r ^ (m - n)) • y = x
rw₂ : r ^ (n + (m - n)) • y = x
⊢ r ^ n • r ^ (m - n) • y = x
have rw₃ : r ^ (n + (m - n)) • y = r ^ m • y
Tactic: rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
r : R
n m : ℕ
h : n ≤ m
x : M
h_1 :
  Membership.mem (γ := Submodule R M) ((fun (n : ℕ) ↦ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range) m) x
y : M
hy : r ^ m • y = x
rw : (r ^ n • r ^ (m - n)) • y = x
rw₁ : (r ^ n * r ^ (m - n)) • y = x
rw₂ : r ^ (n + (m - n)) • y = x
rw₃ : r ^ (n + (m - n)) • y = r ^ m • y
⊢ r ^ n • r ^ (m - n) • y = x
have rw₄ : r ^ m • y = r ^ m • y
Tactic: rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
r : R
x : M
⊢ ∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x
have obtain : ∀ (n : ℕ)
  (hn :
    ∀ (m : ℕ),
      n ≤ m →
        (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range =
          (HSMul.hSMul (β := M →ₗ[R] M) (r ^ m) LinearMap.id).range),
  ∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x
Tactic: obtain ⟨n, hn⟩ := IsArtinian.range_smul_pow_stabilizes M r
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
r : R
x : M
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range =
        (HSMul.hSMul (β := M →ₗ[R] M) (r ^ m) LinearMap.id).range
⊢ ∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x
have hn₁ : ∀ (m : ℕ),
  n ≤ m →
    ∀ (x : M),
      x ∈ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range ↔
        x ∈ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ m) LinearMap.id).range
Tactic: simp_rw [SetLike.ext_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing R
a b : R
hab : a * b = 1
⊢ b * a = 1
have have : ∀ (c : R) (hca : Eq (α := R) ((LinearMap.toSpanSingleton R R a : (a : R) → R) c : R) (1 : R)), b * a = 1
Tactic: have ⟨c, hca⟩ := IsArtinian.surjective_of_injective_endomorphism
      (.toSpanSingleton R R a) (isRightRegular_of_mul_eq_one hab) 1
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing R
a b : R
hab : a * b = 1
c : R
hca : Eq (α := R) ((LinearMap.toSpanSingleton R R a : (a : R) → R) c : R) (1 : R)
⊢ b * a = 1
have rwa : HMul.hMul (α := R) ((LinearMap.id : (a : R) → R) c : R) a = 1
Tactic: rwa [← left_inv_eq_right_inv hca hab]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
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
inst_3 : IsArtinianRing R
hN : N.FG
⊢ IsArtinian.{u_1, u_2} R ↥N
have hN₁ : Module.Finite.{u_1, u_2} R ↥N
Tactic: rw [← Module.Finite.iff_fg] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
F : Type u_3
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
H : IsArtinianRing R
⊢ IsArtinianRing S
have H₁ : IsArtinian R R
Tactic: rw [isArtinianRing_iff] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
ι : Type u_2
inst : Finite ι
⊢ ∀ {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsArtinianRing.{u_1} (R i)],
    IsArtinianRing ((i : ι) → R i)
have apply : ∀ {α β : Type u_2} (a : α ≃ β),
  (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsArtinianRing.{u_1} (R i)],
      IsArtinianRing ((i : α) → R i)) →
    ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsArtinianRing.{u_1} (R i)],
      IsArtinianRing ((i : β) → R i)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
ι : Type u_2
inst : Finite ι
apply :
  ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsArtinianRing.{u_1} (R i)],
        IsArtinianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsArtinianRing.{u_1} (R i)],
        IsArtinianRing ((i : β) → R i)
⊢ ∀ {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsArtinianRing.{u_1} (R i)],
    IsArtinianRing ((i : ι) → R i)
have apply₁ : ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
  [∀ (i : PEmpty.{u_2 + 1}), IsArtinianRing.{u_1} (R i)], IsArtinianRing ((i : PEmpty.{u_2 + 1}) → R i)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
ι : Type u_2
inst : Finite ι
apply :
  ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsArtinianRing.{u_1} (R i)],
        IsArtinianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsArtinianRing.{u_1} (R i)],
        IsArtinianRing ((i : β) → R i)
apply₁ :
  ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsArtinianRing.{u_1} (R i)], IsArtinianRing ((i : PEmpty.{u_2 + 1}) → R i)
⊢ ∀ {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsArtinianRing.{u_1} (R i)],
    IsArtinianRing ((i : ι) → R i)
have apply₂ : ∀ {α : Type u_2} [Fintype α],
  (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsArtinianRing.{u_1} (R i)],
      IsArtinianRing ((i : α) → R i)) →
    ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)] [∀ (i : Option α), IsArtinianRing.{u_1} (R i)],
      IsArtinianRing ((i : Option α) → R i)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing R
x : R
⊢ IsUnit x ↔ IsRightRegular x
have rw : (Injective (β := R) fun (x_1 : R) ↦ x_1 * x) → Surjective (β := R) fun (x_1 : R) ↦ x_1 * x
Tactic: rw [IsRightRegular, IsUnit.isUnit_iff_mulRight_bijective, Bijective, and_iff_left_of_imp]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing R
x : R
⊢ IsUnit x ↔ IsRegular x
have rw : IsUnit x ↔ IsLeftRegular x ∧ IsRightRegular x
Tactic: rw [isRegular_iff, ← isUnit_iff_isRightRegular, and_iff_right_of_imp (·.isRegular.1)]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing R
x : R
rw : IsUnit x ↔ IsLeftRegular x ∧ IsRightRegular x
⊢ IsUnit x ↔ IsRegular x
have rw₁ : IsUnit x ↔ IsLeftRegular x ∧ IsUnit x
Tactic: rw [isRegular_iff, ← isUnit_iff_isRightRegular, and_iff_right_of_imp (·.isRegular.1)]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing R
x : R
rw : IsUnit x ↔ IsLeftRegular x ∧ IsRightRegular x
rw₁ : IsUnit x ↔ IsLeftRegular x ∧ IsUnit x
⊢ IsUnit x ↔ IsRegular x
have rw₂ : IsUnit x ↔ IsUnit x
Tactic: rw [isRegular_iff, ← isUnit_iff_isRightRegular, and_iff_right_of_imp (·.isRegular.1)]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
⊢ IsUnit x ↔ IsLeftRegular x
have rw : IsUnit x ↔ IsRightRegular (MulOpposite.op x)
Tactic: rw [← isRightRegular_op, ← isUnit_op, isUnit_iff_isRightRegular]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
rw : IsUnit x ↔ IsRightRegular (MulOpposite.op x)
⊢ IsUnit x ↔ IsLeftRegular x
have rw₁ : IsUnit (MulOpposite.op x) ↔ IsRightRegular (MulOpposite.op x)
Tactic: rw [← isRightRegular_op, ← isUnit_op, isUnit_iff_isRightRegular]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
rw : IsUnit x ↔ IsRightRegular (MulOpposite.op x)
rw₁ : IsUnit (MulOpposite.op x) ↔ IsRightRegular (MulOpposite.op x)
⊢ IsUnit x ↔ IsLeftRegular x
have rw₂ : IsRightRegular (MulOpposite.op x) ↔ IsRightRegular (MulOpposite.op x)
Tactic: rw [← isRightRegular_op, ← isUnit_op, isUnit_iff_isRightRegular]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
⊢ IsUnit x ↔ IsRegular x
have rw : IsUnit x ↔ IsLeftRegular x ∧ IsRightRegular x
Tactic: rw [isRegular_iff, ← isUnit_iff_isLeftRegular, and_iff_left_of_imp (·.isRegular.2)]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
rw : IsUnit x ↔ IsLeftRegular x ∧ IsRightRegular x
⊢ IsUnit x ↔ IsRegular x
have rw₁ : IsUnit x ↔ IsUnit x ∧ IsRightRegular x
Tactic: rw [isRegular_iff, ← isUnit_iff_isLeftRegular, and_iff_left_of_imp (·.isRegular.2)]