awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Artinian.Module
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

Tactic:
(RelEmbedding.natGT (LinearMap.range <| f ^ ·) ?_).not_wellFounded

Premises used: RelEmbedding.natGT, LinearMap.range, RelEmbedding.not_wellFounded, HPow.hPow
-- Module: Mathlib.RingTheory.Artinian.Module
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)
refine :
  ∀ (n : ℕ), LT.lt.{u_2} (α := Submodule R M) ((fun (x : ℕ) ↦ (f ^ x).range) (n + 1)) ((fun (x : ℕ) ↦ (f ^ x).range) n)
⊢ ¬WellFounded fun (x1 x2 : Submodule R M) ↦ x1 < x2

Tactic:
refine (RelEmbedding.natGT (LinearMap.range <| f ^ ·) ?_).not_wellFounded

Premises used: RelEmbedding.natGT, LinearMap.range, RelEmbedding.not_wellFounded, HPow.hPow
-- Module: Mathlib.RingTheory.Artinian.Module
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 : ℕ
simp_rw : Submodule.map (f ^ n) f.range < Submodule.map (f ^ n) ⊤
⊢ LT.lt.{u_2} (α := Submodule R M) ((fun (x : ℕ) ↦ (f ^ x).range) (n + 1)) ((fun (x : ℕ) ↦ (f ^ x).range) n)

Tactic:
simp_rw [pow_succ, Module.End.mul_eq_comp, LinearMap.range_comp, ← Submodule.map_top (f ^ n)]

Premises used: Module.End.mul_eq_comp, pow_succ, Submodule.map_top, LinearMap.range_comp, HPow.hPow
-- Module: Mathlib.RingTheory.Artinian.Module
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) ⊤

Tactic:
Submodule.map_strictMono_of_injective (Module.End.iterate_injective s n) (Ne.lt_top ?_)

Premises used: Submodule.map_strictMono_of_injective, Ne.lt_top, Module.End.iterate_injective
-- Module: Mathlib.RingTheory.Artinian.Module
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 : ℕ
refine : f.range ≠ ⊤
⊢ Submodule.map (f ^ n) f.range < Submodule.map (f ^ n) ⊤

Tactic:
refine Submodule.map_strictMono_of_injective (Module.End.iterate_injective s n) (Ne.lt_top ?_)

Premises used: Submodule.map_strictMono_of_injective, Ne.lt_top, Module.End.iterate_injective
-- Module: Mathlib.RingTheory.Artinian.Module
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 : ℕ
rwa : ¬f.range = ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : ¬Surjective (α := M) (β := M) (⇑f : (a : M) → M)
⊢ f.range ≠ ⊤

Tactic:
rwa [Ne, LinearMap.range_eq_top]

Premises used: Ne, LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.Artinian.Module
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)
⊢ Bijective (α := M) (β := M) (⇑f : (a : M) → M)

Tactic:
⟨s, surjective_of_injective_endomorphism f s⟩

Premises used: IsArtinian.surjective_of_injective_endomorphism, And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.Artinian.Module
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 = ⊤
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)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊤

Tactic:
rsuffices ⟨n, w⟩ : ∃ n : ℕ, ∀ m, n ≤ m → OrderDual.toDual f (m + 1) = ⊤
-- Module: Mathlib.RingTheory.Artinian.Module
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)
h₁ : ∀ (m : ℕ), n + 1 ≤ m → f m = ⊤
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊤

Tactic:
use n + 1
-- Module: Mathlib.RingTheory.Artinian.Module
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)
p : n + 1 ≤ 0
⊢ f 0 = ⊤

Tactic:
cases p
-- Module: Mathlib.RingTheory.Artinian.Module
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
h₁ : n ≤ m
⊢ f (m + 1) = ⊤

Tactic:
apply w
-- Module: Mathlib.RingTheory.Artinian.Module
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
⊢ n ≤ m

Tactic:
Nat.succ_le_succ_iff.mp p

Premises used: Nat.succ_le_succ_iff, Iff.mp
-- Module: Mathlib.RingTheory.Artinian.Module
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
⊢ n ≤ m

Tactic:
exact Nat.succ_le_succ_iff.mp p

Premises used: Nat.succ_le_succ_iff, Iff.mp
-- Module: Mathlib.RingTheory.Artinian.Module
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)ᵒᵈ)
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)
⊢ ∃ (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))

Premises used: OrderDual.toDual, Function.comp, partialSups, IsArtinian.monotone_stabilizes, DFunLike.coe
-- Module: Mathlib.RingTheory.Artinian.Module
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)

Tactic:
⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩

Premises used: Disjoint.eq_bot_of_ge, sup_eq_left, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Artinian.Module
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)ᵒᵈ)
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)ᵒᵈ)
⊢ ∃ (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:
refine ⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩
-- Module: Mathlib.RingTheory.Artinian.Module
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)ᵒᵈ)
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:
simpa only [partialSups_add_one] using (w (m + 1) <| le_add_right p).symm.trans <| w m p

Premises used: partialSups_add_one, HAdd.hAdd, OfNat.ofNat, Eq.symm, Eq.trans, le_add_right
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
P : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid P
inst_2 : AddCommMonoid N
inst_3 : Module R P
inst_4 : Module R N
inst_5 : IsArtinian R N
f : P × N →ₗ[R] N
inj : Function.Injective (α := P × N) (β := N) (⇑f : (a : P × N) → N)
⊢ Subsingleton P

Tactic:
subsingleton_of_forall_eq 0 fun p ↦
    have ⟨_, eq⟩ := IsArtinian.surjective_of_injective_endomorphism (f ∘ₗ .inr ..)
      (inj.comp (Prod.mk_right_injective _)) (f (p, 0))
    congr($(inj eq).1).symm

Premises used: subsingleton_of_forall_eq, congrArg, Zero.zero, id, Prod.mk, Prod.fst, IsArtinian.surjective_of_injective_endomorphism, AddZero.toZero, LinearMap.comp, Function.Injective.comp, Prod.mk_right_injective, _private.0.IsArtinian.subsingleton_of_injective.match_1, OfNat.ofNat, Eq.symm, LinearMap.inr, Eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Artinian.Module
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
obtain :
  ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)),
    ∀ᶠ (n : ℕ) in atTop, ⨅ (m : ℕ), (f ^ m).range = (f ^ n).range
⊢ ∀ᶠ (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

Premises used: LinearMap.iterateRange, IsArtinian.monotone_stabilizes
-- Module: Mathlib.RingTheory.Artinian.Module
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

Tactic:
eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩

Premises used: Iff.mpr, le_iInf, LinearMap.range, le_antisymm, HPow.hPow, Exists.intro, Filter.eventually_atTop, iInf_le
-- Module: Mathlib.RingTheory.Artinian.Module
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)
refine : ∀ (l : ℕ) (hl : l ≥ n) (m : ℕ), (f ^ l).range ≤ (f ^ m).range
⊢ ∀ᶠ (n : ℕ) in atTop, ⨅ (m : ℕ), (f ^ m).range = (f ^ n).range

Tactic:
refine eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩

Premises used: Iff.mpr, le_iInf, le_antisymm, Exists.intro, Filter.eventually_atTop, iInf_le
-- Module: Mathlib.RingTheory.Artinian.Module
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
inr : ∀ (h : m < l), (f ^ l).range ≤ (f ^ m).range
⊢ (f ^ l).range ≤ (f ^ m).range

Tactic:
rcases le_or_gt l m with h | h

Premises used: le_or_gt
-- Module: Mathlib.RingTheory.Artinian.Module
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)
inl₁ inl₂ : (f ^ l).range ≤ (f ^ l).range
⊢ (f ^ l).range ≤ (f ^ m).range

Tactic:
rw [← hn _ (hl.trans h), hn _ hl]

Premises used: LE.le.trans
-- Module: Mathlib.RingTheory.Artinian.Module
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 : m < l
⊢ (f ^ l).range ≤ (f ^ m).range

Tactic:
f.iterateRange.monotone h.le

Premises used: OrderHom.monotone, Set.Mem, LinearMap.iterateRange, LT.lt.le
-- Module: Mathlib.RingTheory.Artinian.Module
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 : m < l
⊢ (f ^ l).range ≤ (f ^ m).range

Tactic:
exact f.iterateRange.monotone h.le

Premises used: OrderHom.monotone, LinearMap.iterateRange, LT.lt.le
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
N_1 : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup P
inst_3 : AddCommGroup N_1
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R N_1
N : Submodule R M
inst_7 : IsArtinian R M
⊢ IsArtinian.{u_1, u_2} R (M ⧸ N)

Tactic:
isArtinian_of_surjective M (Submodule.mkQ N) (Submodule.Quotient.mk_surjective N)

Premises used: Submodule.Quotient.mk_surjective, isArtinian_of_surjective, Submodule.mkQ
-- Module: Mathlib.RingTheory.Artinian.Module
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
inst_7 : IsArtinian R M
inst_8 : IsArtinian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range = g.ker
⊢ ∀ (a : Submodule R N), Submodule.map (f.ker.liftQ f ⋯) (Submodule.comap (f.ker.liftQ f ⋯) a) = a ⊓ f.range

Tactic:
simp [Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ]

Premises used: Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ
-- Module: Mathlib.RingTheory.Artinian.Module
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
inst_7 : IsArtinian R M
inst_8 : IsArtinian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range = g.ker
⊢ ∀ (a : Submodule R N),
    Submodule.comap (M₂ := ↥g.range) g.rangeRestrict (Submodule.map g.rangeRestrict a) = a ⊔ f.range

Tactic:
simp [Submodule.comap_map_eq, h]

Premises used: Submodule.comap_map_eq
-- Module: Mathlib.RingTheory.Artinian.Module
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)

Tactic:
⟨fun h ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩

Premises used: _private.0.isArtinian_iff_submodule_quotient.match_1, inferInstance, IsArtinian, And.intro, Iff.intro
-- Module: Mathlib.RingTheory.Artinian.Module
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
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
⊢ IsArtinian R P ↔ IsArtinian.{u_1, u_3} R ↥S ∧ IsArtinian.{u_1, u_3} R (P ⧸ S)

Tactic:
refine ⟨fun h ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.Artinian.Module
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)
apply : S.subtype.range = S.mkQ.ker
⊢ IsArtinian R P

Tactic:
apply isArtinian_of_range_eq_ker S.subtype S.mkQ

Premises used: isArtinian_of_range_eq_ker, Submodule.subtype, Submodule.mkQ
-- Module: Mathlib.RingTheory.Artinian.Module
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
rw₁ rw₂ : S = S
⊢ S.subtype.range = S.mkQ.ker

Tactic:
rw [Submodule.ker_mkQ, Submodule.range_subtype]

Premises used: Submodule.ker_mkQ, Submodule.range_subtype
-- Module: Mathlib.RingTheory.Artinian.Module
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
inst_7 : IsArtinian R M
inst_8 : IsArtinian R P
⊢ IsArtinian R (M × P)

Tactic:
isArtinian_of_range_eq_ker (LinearMap.inl R M P) (LinearMap.snd R M P) (LinearMap.range_inl R M P)

Premises used: LinearMap.inl, LinearMap.snd, LinearMap.range_inl, isArtinian_of_range_eq_ker
-- Module: Mathlib.RingTheory.Artinian.Module
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₁.subtype.coprod M₂.subtype).range

Tactic:
have := isArtinian_range (M₁.subtype.coprod M₂.subtype)