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
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M
have rw : (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔
  WellFounded fun (x1 x2 : Submodule R M) ↦ x1 < x2
Tactic: rw [isArtinian_iff, WellFounded.wellFounded_iff_has_min]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔
    WellFounded fun (x1 x2 : Submodule R M) ↦ x1 < x2
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M
have rw₁ : (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔
  ∀ (s : Set (Submodule R M)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
Tactic: rw [isArtinian_iff, WellFounded.wellFounded_iff_has_min]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : ℕ →o (Submodule R M)ᵒᵈ
⊢ EventuallyConst (α := ℕ) (β := (Submodule R M)ᵒᵈ) (⇑f : (a : ℕ) → (Submodule R M)ᵒᵈ) atTop
have simp_rw : ∃ (i : ℕ),
  ∀ (j : ℕ),
    i ≤ j →
      Eq (α := (Submodule R M)ᵒᵈ) ((f : (a : ℕ) → (Submodule R M)ᵒᵈ) i : (Submodule R M)ᵒᵈ)
        ((f : (a : ℕ) → (Submodule R M)ᵒᵈ) j : (Submodule R M)ᵒᵈ)
Tactic: simp_rw [eventuallyConst_atTop, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : M →ₗ[R] M
s : Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : IsArtinian R M
⊢ Surjective (α := M) (β := M) (⇑f : (a : M) → M)
have contrapose : ∀ (h : ¬Surjective (α := M) (β := M) (⇑f : (a : M) → M)), ¬IsArtinian R M
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : M →ₗ[R] M
s : Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : ¬Surjective (α := M) (β := M) (⇑f : (a : M) → M)
⊢ ¬IsArtinian R M
have rw : ¬WellFounded fun (x1 x2 : Submodule R M) ↦ x1 < x2
Tactic: rw [IsArtinian, WellFoundedLT, isWellFounded_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : M →ₗ[R] M
s : Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : ¬Surjective (α := M) (β := M) (⇑f : (a : M) → M)
⊢ ¬WellFounded fun (x1 x2 : Submodule R M) ↦ x1 < x2
have refine : ∀ (n : ℕ), LT.lt.{u_2} (α := Submodule R M) ((fun (x : ℕ) ↦ (f ^ x).range) (n + 1)) ((fun (x : ℕ) ↦ (f ^ x).range) n)
Tactic: refine (RelEmbedding.natGT (LinearMap.range <| f ^ ·) ?_).not_wellFounded
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : M →ₗ[R] M
s : Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : ¬Surjective (α := M) (β := M) (⇑f : (a : M) → M)
n : ℕ
⊢ LT.lt.{u_2} (α := Submodule R M) ((fun (x : ℕ) ↦ (f ^ x).range) (n + 1)) ((fun (x : ℕ) ↦ (f ^ x).range) n)
have simp_rw : Submodule.map (f ^ n) f.range < Submodule.map (f ^ n) ⊤
Tactic: simp_rw [pow_succ, Module.End.mul_eq_comp, LinearMap.range_comp, ← Submodule.map_top (f ^ n)]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : M →ₗ[R] M
s : Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : ¬Surjective (α := M) (β := M) (⇑f : (a : M) → M)
n : ℕ
⊢ Submodule.map (f ^ n) f.range < Submodule.map (f ^ n) ⊤
have refine : f.range ≠ ⊤
Tactic: refine Submodule.map_strictMono_of_injective (Module.End.iterate_injective s n) (Ne.lt_top ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : M →ₗ[R] M
s : Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : ¬Surjective (α := M) (β := M) (⇑f : (a : M) → M)
n : ℕ
⊢ f.range ≠ ⊤
have rwa : ¬f.range = ⊤
Tactic: rwa [Ne, LinearMap.range_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : ℕ → Submodule R M
h :
  ∀ (n : ℕ),
    Disjoint (α := (Submodule R M)ᵒᵈ)
      ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) : (a : ℕ) → (Submodule R M)ᵒᵈ)
          n :
        (Submodule R M)ᵒᵈ)
      ((OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) (f (n + 1)) : (Submodule R M)ᵒᵈ)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊤
have rsuffices : ∀ (n : ℕ)
  (w :
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Submodule R M)
          ((OrderDual.toDual : (a : ℕ → Submodule R M) → (ℕ → Submodule R M)ᵒᵈ) f (m + 1) : Submodule R M)
          (⊤ : Submodule R M)),
  ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊤
Tactic: rsuffices ⟨n, w⟩ : ∃ n : ℕ, ∀ m, n ≤ m → OrderDual.toDual f (m + 1) = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : ℕ → Submodule R M
h :
  ∀ (n : ℕ),
    Disjoint (α := (Submodule R M)ᵒᵈ)
      ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) : (a : ℕ) → (Submodule R M)ᵒᵈ)
          n :
        (Submodule R M)ᵒᵈ)
      ((OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) (f (n + 1)) : (Submodule R M)ᵒᵈ)
rsuffices :
  ∀ (n : ℕ)
    (w :
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Submodule R M)
            ((OrderDual.toDual : (a : ℕ → Submodule R M) → (ℕ → Submodule R M)ᵒᵈ) f (m + 1) : Submodule R M)
            (⊤ : Submodule R M)),
    ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊤
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊤
have rsuffices₁ : ∃ (n : ℕ),
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        ((OrderDual.toDual : (a : ℕ → Submodule R M) → (ℕ → Submodule R M)ᵒᵈ) f (m + 1) : Submodule R M)
        (⊤ : Submodule R M)
Tactic: rsuffices ⟨n, w⟩ : ∃ n : ℕ, ∀ m, n ≤ m → OrderDual.toDual f (m + 1) = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : ℕ → Submodule R M
h :
  ∀ (n : ℕ),
    Disjoint (α := (Submodule R M)ᵒᵈ)
      ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) : (a : ℕ) → (Submodule R M)ᵒᵈ)
          n :
        (Submodule R M)ᵒᵈ)
      ((OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) (f (n + 1)) : (Submodule R M)ᵒᵈ)
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        ((OrderDual.toDual : (a : ℕ → Submodule R M) → (ℕ → Submodule R M)ᵒᵈ) f (m + 1) : Submodule R M)
        (⊤ : Submodule R M)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊤
have h₁ : ∀ (m : ℕ), n + 1 ≤ m → f m = ⊤
Tactic: use n + 1
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : ℕ → Submodule R M
h :
  ∀ (n : ℕ),
    Disjoint (α := (Submodule R M)ᵒᵈ)
      ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) : (a : ℕ) → (Submodule R M)ᵒᵈ)
          n :
        (Submodule R M)ᵒᵈ)
      ((OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) (f (n + 1)) : (Submodule R M)ᵒᵈ)
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M)
        ((OrderDual.toDual : (a : ℕ → Submodule R M) → (ℕ → Submodule R M)ᵒᵈ) f (m + 1) : Submodule R M)
        (⊤ : Submodule R M)
m : ℕ
p : n + 1 ≤ m + 1
⊢ f (m + 1) = ⊤
have h₁ : n ≤ m
Tactic: apply w
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : ℕ → Submodule R M
h :
  ∀ (n : ℕ),
    Disjoint (α := (Submodule R M)ᵒᵈ)
      ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) : (a : ℕ) → (Submodule R M)ᵒᵈ)
          n :
        (Submodule R M)ᵒᵈ)
      ((OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) (f (n + 1)) : (Submodule R M)ᵒᵈ)
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Submodule R M)
          ((OrderDual.toDual : (a : ℕ → Submodule R M) → (ℕ → Submodule R M)ᵒᵈ) f (m + 1) : Submodule R M)
          (⊤ : Submodule R M)
have obtain : ∀ (n : ℕ)
  (w :
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Submodule R M)ᵒᵈ)
          ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) :
                (a : ℕ) → (Submodule R M)ᵒᵈ)
              n :
            (Submodule R M)ᵒᵈ)
          ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) :
                (a : ℕ) → (Submodule R M)ᵒᵈ)
              m :
            (Submodule R M)ᵒᵈ)),
  ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Submodule R M)
          ((OrderDual.toDual : (a : ℕ → Submodule R M) → (ℕ → Submodule R M)ᵒᵈ) f (m + 1) : Submodule R M)
          (⊤ : Submodule R M)
Tactic: obtain ⟨n, w⟩ := monotone_stabilizes (partialSups (OrderDual.toDual ∘ f))
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : ℕ → Submodule R M
h :
  ∀ (n : ℕ),
    Disjoint (α := (Submodule R M)ᵒᵈ)
      ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) : (a : ℕ) → (Submodule R M)ᵒᵈ)
          n :
        (Submodule R M)ᵒᵈ)
      ((OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) (f (n + 1)) : (Submodule R M)ᵒᵈ)
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule R M)ᵒᵈ)
        ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) : (a : ℕ) → (Submodule R M)ᵒᵈ)
            n :
          (Submodule R M)ᵒᵈ)
        ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) : (a : ℕ) → (Submodule R M)ᵒᵈ)
            m :
          (Submodule R M)ᵒᵈ)
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Submodule R M)
          ((OrderDual.toDual : (a : ℕ → Submodule R M) → (ℕ → Submodule R M)ᵒᵈ) f (m + 1) : Submodule R M)
          (⊤ : Submodule R M)
have refine : ∀ (m : ℕ) (p : n ≤ m),
  Eq (α := (Submodule R M)ᵒᵈ)
    ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) : (a : ℕ) → (Submodule R M)ᵒᵈ) m ⊔
        (OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) (f (m + 1)) :
      (Submodule R M)ᵒᵈ)
    ((partialSups ((⇑OrderDual.toDual : (a : Submodule R M) → (Submodule R M)ᵒᵈ) ∘ f) : (a : ℕ) → (Submodule R M)ᵒᵈ) m :
      (Submodule R M)ᵒᵈ)
Tactic: refine ⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsArtinian R M
f : Module.End R M
⊢ ∀ᶠ (n : ℕ) in atTop, ⨅ (m : ℕ), (f ^ m).range = (f ^ n).range
have obtain : ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)),
  ∀ᶠ (n : ℕ) in atTop, ⨅ (m : ℕ), (f ^ m).range = (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 : Semiring R
inst_1 : AddCommMonoid 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, ⨅ (m : ℕ), (f ^ m).range = (f ^ n).range
have refine : ∀ (l : ℕ) (hl : l ≥ n) (m : ℕ), (f ^ l).range ≤ (f ^ m).range
Tactic: refine eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid 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)
l : ℕ
hl : l ≥ n
m : ℕ
⊢ (f ^ l).range ≤ (f ^ m).range
have inl : ∀ (h : l ≤ m), (f ^ l).range ≤ (f ^ m).range
Tactic: rcases le_or_gt l m with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid 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)
l : ℕ
hl : l ≥ n
m : ℕ
inl : ∀ (h : l ≤ m), (f ^ l).range ≤ (f ^ m).range
⊢ (f ^ l).range ≤ (f ^ m).range
have inr : ∀ (h : m < l), (f ^ l).range ≤ (f ^ m).range
Tactic: rcases le_or_gt l m with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid 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)
l : ℕ
hl : l ≥ n
m : ℕ
h : l ≤ m
⊢ (f ^ l).range ≤ (f ^ m).range
have inl : (f ^ l).range ≤ range (f ^ n)
Tactic: rw [← hn _ (hl.trans h), hn _ hl]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid 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)
l : ℕ
hl : l ≥ n
m : ℕ
h : l ≤ m
inl : (f ^ l).range ≤ range (f ^ n)
⊢ (f ^ l).range ≤ (f ^ m).range
have inl₁ : (f ^ l).range ≤ (f ^ l).range
Tactic: rw [← hn _ (hl.trans h), hn _ hl]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup P
inst_2 : Module R P
S : Submodule R P
⊢ IsArtinian R P ↔ IsArtinian.{u_1, u_3} R ↥S ∧ IsArtinian.{u_1, u_3} R (P ⧸ S)
have refine : IsArtinian.{u_1, u_3} R ↥S ∧ IsArtinian.{u_1, u_3} R (P ⧸ S) →
  IsArtinian.{u_1, u_3} R ↥S → IsArtinian.{u_1, u_3} R (P ⧸ S) → IsArtinian R P
Tactic: refine ⟨fun h ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup P
inst_2 : Module R P
S : Submodule R P
h : IsArtinian.{u_1, u_3} R ↥S ∧ IsArtinian.{u_1, u_3} R (P ⧸ S)
left : IsArtinian.{u_1, u_3} R ↥S
right : IsArtinian.{u_1, u_3} R (P ⧸ S)
⊢ IsArtinian R P
have apply : S.subtype.range = S.mkQ.ker
Tactic: apply isArtinian_of_range_eq_ker S.subtype S.mkQ
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup P
inst_2 : Module R P
S : Submodule R P
h : IsArtinian.{u_1, u_3} R ↥S ∧ IsArtinian.{u_1, u_3} R (P ⧸ S)
left : IsArtinian.{u_1, u_3} R ↥S
right : IsArtinian.{u_1, u_3} R (P ⧸ S)
⊢ S.subtype.range = S.mkQ.ker
have rw : S.subtype.range = S
Tactic: rw [Submodule.ker_mkQ, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (goal)
Goal:
R : Type u_1
P : Type u_3
inst : Ring R
inst_1 : AddCommGroup P
inst_2 : Module R P
S : Submodule R P
h : IsArtinian.{u_1, u_3} R ↥S ∧ IsArtinian.{u_1, u_3} R (P ⧸ S)
left : IsArtinian.{u_1, u_3} R ↥S
right : IsArtinian.{u_1, u_3} R (P ⧸ S)
rw : S.subtype.range = S
⊢ S.subtype.range = S.mkQ.ker
have rw₁ : S = S
Tactic: rw [Submodule.ker_mkQ, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Artinian.Module (hypothesis)
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
M₁ M₂ : Submodule R P
inst_7 : IsArtinian.{u_1, u_3} R ↥M₁
inst_8 : IsArtinian.{u_1, u_3} R ↥M₂
⊢ IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)
have this : IsArtinian.{u_1, u_3} R ↥(M₁.subtype.coprod M₂.subtype).range
Tactic: have := isArtinian_range (M₁.subtype.coprod M₂.subtype)
-- 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
M₁ M₂ : Submodule R P
inst_7 : IsArtinian.{u_1, u_3} R ↥M₁
inst_8 : IsArtinian.{u_1, u_3} R ↥M₂
this : IsArtinian.{u_1, u_3} R ↥(M₁.subtype.coprod M₂.subtype).range
⊢ IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)
have rwa : ∀ (this : IsArtinian.{u_1, u_3} R ↥(M₁.subtype.range ⊔ M₂.subtype.range)), IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)
Tactic: rwa [LinearMap.range_coprod, Submodule.range_subtype, Submodule.range_subtype] at this
Cleared hypotheses: this
-- 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
M₁ M₂ : Submodule R P
inst_7 : IsArtinian.{u_1, u_3} R ↥M₁
inst_8 : IsArtinian.{u_1, u_3} R ↥M₂
this : IsArtinian.{u_1, u_3} R ↥(M₁.subtype.coprod M₂.subtype).range
rwa : ∀ (this : IsArtinian.{u_1, u_3} R ↥(M₁.subtype.range ⊔ M₂.subtype.range)), IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)
⊢ IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)
have rwa₁ : ∀ (this : IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂.subtype.range)), IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)
Tactic: rwa [LinearMap.range_coprod, Submodule.range_subtype, Submodule.range_subtype] at this
Cleared hypotheses: this
-- 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
M₁ M₂ : Submodule R P
inst_7 : IsArtinian.{u_1, u_3} R ↥M₁
inst_8 : IsArtinian.{u_1, u_3} R ↥M₂
this : IsArtinian.{u_1, u_3} R ↥(M₁.subtype.coprod M₂.subtype).range
rwa : ∀ (this : IsArtinian.{u_1, u_3} R ↥(M₁.subtype.range ⊔ M₂.subtype.range)), IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)
rwa₁ : ∀ (this : IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂.subtype.range)), IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)
⊢ IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)
have rwa₂ : ∀ (this : IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)), IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)
Tactic: rwa [LinearMap.range_coprod, Submodule.range_subtype, Submodule.range_subtype] at this
Cleared hypotheses: this
-- 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 : ι → Type u_6} [inst_8 : (i : ι) → AddCommGroup (M i)] [inst_9 : (i : ι) → Module.{u_1, u_6} R (M i)]
    [∀ (i : ι), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : ι) → M i)
have apply : ∀ {α β : Type u_5} (a : α ≃ β),
  (∀ {M : α → Type u_6} [inst_8 : (i : α) → AddCommGroup (M i)] [inst_9 : (i : α) → Module.{u_1, u_6} R (M i)]
      [∀ (i : α), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : α) → M i)) →
    ∀ {M : β → Type u_6} [inst_8 : (i : β) → AddCommGroup (M i)] [inst_9 : (i : β) → Module.{u_1, u_6} R (M i)]
      [∀ (i : β), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : β) → 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 : α → Type u_6} [inst_8 : (i : α) → AddCommGroup (M i)] [inst_9 : (i : α) → Module.{u_1, u_6} R (M i)]
        [∀ (i : α), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : α) → M i)) →
      ∀ {M : β → Type u_6} [inst_8 : (i : β) → AddCommGroup (M i)] [inst_9 : (i : β) → Module.{u_1, u_6} R (M i)]
        [∀ (i : β), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : β) → M i)
⊢ ∀ {M : ι → Type u_6} [inst_8 : (i : ι) → AddCommGroup (M i)] [inst_9 : (i : ι) → Module.{u_1, u_6} R (M i)]
    [∀ (i : ι), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : ι) → M i)
have apply₁ : ∀ {M : PEmpty.{u_5 + 1} → Type u_6} [inst_8 : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)]
  [inst_9 : (i : PEmpty.{u_5 + 1}) → Module.{u_1, u_6} R (M i)]
  [∀ (i : PEmpty.{u_5 + 1}), IsArtinian.{u_1, u_6} R (M i)], IsArtinian 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 : α → Type u_6} [inst_8 : (i : α) → AddCommGroup (M i)] [inst_9 : (i : α) → Module.{u_1, u_6} R (M i)]
        [∀ (i : α), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : α) → M i)) →
      ∀ {M : β → Type u_6} [inst_8 : (i : β) → AddCommGroup (M i)] [inst_9 : (i : β) → Module.{u_1, u_6} R (M i)]
        [∀ (i : β), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : β) → M i)
apply₁ :
  ∀ {M : PEmpty.{u_5 + 1} → Type u_6} [inst_8 : (i : PEmpty.{u_5 + 1}) → AddCommGroup (M i)]
    [inst_9 : (i : PEmpty.{u_5 + 1}) → Module.{u_1, u_6} R (M i)]
    [∀ (i : PEmpty.{u_5 + 1}), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : PEmpty.{u_5 + 1}) → M i)
⊢ ∀ {M : ι → Type u_6} [inst_8 : (i : ι) → AddCommGroup (M i)] [inst_9 : (i : ι) → Module.{u_1, u_6} R (M i)]
    [∀ (i : ι), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : ι) → M i)
have apply₂ : ∀ {α : Type u_5} [Fintype α],
  (∀ {M : α → Type u_6} [inst_9 : (i : α) → AddCommGroup (M i)] [inst_10 : (i : α) → Module.{u_1, u_6} R (M i)]
      [∀ (i : α), IsArtinian.{u_1, u_6} R (M i)], IsArtinian R ((i : α) → M i)) →
    ∀ {M : Option α → Type u_6} [inst_9 : (i : Option α) → AddCommGroup (M i)]
      [inst_10 : (i : Option α) → Module.{u_1, u_6} R (M i)] [∀ (i : Option α), IsArtinian.{u_1, u_6} R (M i)],
      IsArtinian 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 ι
⊢ ∀ {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} (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)
Tactic: apply Finite.induction_empty_option _ _ _ ι