awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
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₂)
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : IsArtinian.{u_1, u_3} R ↥(M₁ ⊔ M₂)), 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

Premises used: LinearMap.range_coprod, 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
ι : 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)
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)
⊢ ∀ {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 _ _ _ ι

Premises used: Finite.induction_empty_option
-- 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
ι : Type u_5
inst_7 : Finite ι
α β : 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:
fun e h ↦ isArtinian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)

Premises used: LinearEquiv.piCongrLeft, isArtinian_of_linearEquiv
-- 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
ι : Type u_5
inst_7 : Finite ι
⊢ ∀ {α β : 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:
exact fun e h ↦ isArtinian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)

Premises used: LinearEquiv.piCongrLeft, isArtinian_of_linearEquiv
-- 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
ι : Type u_5
inst_7 : Finite ι
⊢ ∀ {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:
infer_instance
-- 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
ι : Type u_5
inst_7 : Finite ι
α : Type u_5
inst_8 : 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:
fun ih ↦ isArtinian_of_linearEquiv (LinearEquiv.piOptionEquivProd R).symm

Premises used: LinearEquiv.symm, LinearEquiv.piOptionEquivProd, isArtinian_of_linearEquiv
-- 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
ι : Type u_5
inst_7 : Finite ι
⊢ ∀ {α : 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:
exact fun ih ↦ isArtinian_of_linearEquiv (LinearEquiv.piOptionEquivProd R).symm

Premises used: LinearEquiv.symm, LinearEquiv.piOptionEquivProd, isArtinian_of_linearEquiv
-- 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
ι : Type u_5
inst_7 : Finite ι
inst_8 : IsArtinian R M
⊢ IsArtinian R (ι → M)

Tactic:
isArtinian_pi

Premises used: isArtinian_pi
-- 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
ι : Type u_5
inst_7 : Finite ι
inst_8 : IsArtinian R M
⊢ IsArtinian R (ι →₀ M)

Tactic:
isArtinian_of_linearEquiv (Finsupp.linearEquivFunOnFinite _ _ _).symm

Premises used: LinearEquiv.symm, Finsupp.linearEquivFunOnFinite, isArtinian_of_linearEquiv
-- 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
ι : 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)
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)
⊢ ∀ {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 _ _ _ ι

Premises used: Finite.induction_empty_option
-- 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
ι : Type u_5
inst_7 : Finite ι
α : Type u_5
_ :
  ∀ {β : 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)
⊢ ∀ {β : 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:
_
-- 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
ι : 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 : β → 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:
_
-- 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
ι : 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
_ : ∀ [∀ (i : β), IsArtinian.{u_1, u_3} R ↥(M_1 i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : β), M_1 i)
⊢ ∀ [∀ (i : β), IsArtinian.{u_1, u_3} R ↥(M_1 i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : β), M_1 i)

Tactic:
_
-- 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
ι : 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)
rw : IsArtinian.{u_1, u_3} R ↥(⨆ (x : α), M_1 ((e : (a : α) → β) x))
⊢ IsArtinian.{u_1, u_3} R ↥(⨆ (i : β), M_1 i)

Tactic:
rw [← e.iSup_comp]

Premises used: Equiv.iSup_comp
-- 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
ι : 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 ↥(⨆ (x : α), M_1 ((e : (a : α) → β) x))

Tactic:
apply h
-- 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
ι : 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)
rw : IsArtinian.{u_1, u_3} R ↥⊥
⊢ IsArtinian.{u_1, u_3} R ↥(⨆ (i : PEmpty.{u_5 + 1}), M_1 i)

Tactic:
rw [iSup_of_empty]

Premises used: iSup_of_empty
-- 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
ι : 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 ↥⊥

Tactic:
infer_instance
-- 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
ι : Type u_5
inst_7 : Finite ι
α : 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)
⊢ ∀ [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:
_
-- 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
ι : 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 : Option α → Submodule R P} [∀ (i : Option α), IsArtinian.{u_1, u_3} R ↥(M i)],
    IsArtinian.{u_1, u_3} R ↥(⨆ (i : Option α), 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:
_
-- 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
ι : 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
_ : ∀ [∀ (i : Option α), IsArtinian.{u_1, u_3} R ↥(M_1 i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : Option α), M_1 i)
⊢ ∀ [∀ (i : Option α), IsArtinian.{u_1, u_3} R ↥(M_1 i)], IsArtinian.{u_1, u_3} R ↥(⨆ (i : Option α), M_1 i)

Tactic:
_
-- 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
ι : 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)
rw : IsArtinian.{u_1, u_3} R ↥(M_1 none ⊔ ⨆ (b : α), M_1 (some b))
⊢ IsArtinian.{u_1, u_3} R ↥(⨆ (i : Option α), M_1 i)

Tactic:
rw [iSup_option]

Premises used: iSup_option
-- 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
ι : 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 ↥(M_1 none ⊔ ⨆ (b : α), M_1 (some b))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Artinian.Module
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
rw : ∀ (p : Submodule R M), Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | IsCoatom m} p → x ∈ p
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
rw [← h, Module.jacobson, Submodule.mem_sInf]

Premises used: Module.jacobson, Submodule.mem_sInf
-- Module: Mathlib.RingTheory.Artinian.Module
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
⊢ ∀ (p : Submodule R M), Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | IsCoatom m} p → x ∈ p

Tactic:
fun m hm ↦ hs ⟨m, hm⟩ <| Submodule.mem_finsetInf.mpr fun i hi ↦
        (Submodule.Quotient.mk_eq_zero i.1).mp <| congr_fun hx ⟨i, hi⟩

Premises used: Iff.mpr, Set.Mem, Subtype.mk, Iff.mp, Submodule.mem_finsetInf, congr_fun, Subtype.val, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Artinian.Module
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
⊢ ∀ (p : Submodule R M), Membership.mem (γ := Set (Submodule R M)) {m : Submodule R M | IsCoatom m} p → x ∈ p

Tactic:
exact fun m hm ↦ hs ⟨m, hm⟩ <| Submodule.mem_finsetInf.mpr fun i hi ↦
        (Submodule.Quotient.mk_eq_zero i.1).mp <| congr_fun hx ⟨i, hi⟩

Premises used: Iff.mpr, Subtype.mk, Iff.mp, Submodule.mem_finsetInf, congr_fun, Subtype.val, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Artinian.Module
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
obtain :
  ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → range (f ^ n) = range (f ^ m)),
    ∀ᶠ (n : ℕ) in atTop, Codisjoint (f ^ n).ker (f ^ n).range
⊢ ∀ᶠ (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

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

Tactic:
eventually_atTop.mpr ⟨n, fun m hm ↦ codisjoint_iff.mpr ?_⟩

Premises used: Iff.mpr, codisjoint_iff, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.RingTheory.Artinian.Module
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)
refine : ∀ (m : ℕ) (hm : m ≥ n), (f ^ m).ker ⊔ (f ^ m).range = ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, Codisjoint (f ^ n).ker (f ^ n).range

Tactic:
refine eventually_atTop.mpr ⟨n, fun m hm ↦ codisjoint_iff.mpr ?_⟩

Premises used: Iff.mpr, codisjoint_iff, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.RingTheory.Artinian.Module
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
simp_rw : ∀ (x : M), ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x
⊢ (f ^ m).ker ⊔ (f ^ m).range = ⊤

Tactic:
simp_rw [← hn _ hm, Submodule.eq_top_iff', Submodule.mem_sup]

Premises used: Submodule.eq_top_iff', Submodule.mem_sup
-- Module: Mathlib.RingTheory.Artinian.Module
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
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)
⊢ ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x

Tactic:
rsuffices ⟨y, hy⟩ : ∃ y, (f ^ m) ((f ^ n) y) = (f ^ m) x

Premises used: HPow.hPow, DFunLike.coe
-- Module: Mathlib.RingTheory.Artinian.Module
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 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)
⊢ HSub.hSub (β := M) x ((f ^ n : (a : M) → M) y : M) ∈ (f ^ m).ker

Tactic:
simp [hy]
-- Module: Mathlib.RingTheory.Artinian.Module
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 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)
⊢ Membership.mem (α := M) (range (f ^ n)) ((f ^ n : (a : M) → M) y : M) ∧
    HAdd.hAdd (β := M) (HSub.hSub (β := M) x ((f ^ n : (a : M) → M) y : M)) ((f ^ n : (a : M) → M) y : M) = x

Tactic:
simp