awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ ∃ y ∈ (f ^ m).ker, ∃ z ∈ range (f ^ n), y + z = x

Tactic:
exact ⟨x - (f ^ n) y, by simp [hy], (f ^ n) y, by simp⟩
-- 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
simp_rw : Membership.mem (α := M) (range (f ^ m)) ((f ^ m : (a : M) → M) 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)

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]

Premises used: Function.iterate_add_apply, Nat.le_add_left, Module.End.pow_apply, HAdd.hAdd, LinearMap.mem_range
-- 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
⊢ Membership.mem (α := M) (range (f ^ m)) ((f ^ m : (a : M) → M) x : M)

Tactic:
LinearMap.mem_range_self (f ^ m) x

Premises used: Set.Mem, LinearMap.mem_range_self, HPow.hPow
-- 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
⊢ Membership.mem (α := M) (range (f ^ m)) ((f ^ m : (a : M) → M) x : M)

Tactic:
exact LinearMap.mem_range_self (f ^ m) x

Premises used: LinearMap.mem_range_self, HPow.hPow
-- 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
inst_4 : IsNoetherian R M
f : Module.End R M
h :
  ∀ (n : ℕ) (hn : Disjoint (f ^ n).ker (f ^ n).range ∧ Codisjoint (f ^ n).ker (f ^ n).range),
    IsCompl (f ^ n).ker (f ^ n).range
⊢ ∀ᶠ (n : ℕ) in atTop, 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

Premises used: Filter.Eventually.and, Module.End.eventually_disjoint_ker_pow_range_pow, LinearMap.eventually_codisjoint_ker_pow_range_pow
-- 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
inst_4 : IsNoetherian R M
f : Module.End R M
n : ℕ
hn : Disjoint (f ^ n).ker (f ^ n).range ∧ Codisjoint (f ^ n).ker (f ^ n).range
⊢ IsCompl (f ^ n).ker (f ^ n).range

Tactic:
simpa only [isCompl_iff]

Premises used: isCompl_iff
-- 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
inst_4 : IsNoetherian R M
f : M →ₗ[R] M
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)
⊢ 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

Premises used: LinearMap.eventually_iSup_ker_pow_eq, Filter.Eventually.and, LinearMap.eventually_isCompl_ker_pow_range_pow, LinearMap.eventually_iInf_range_pow_eq, Iff.mp, 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
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 (f ^ k).ker (f ^ k).range

Tactic:
obtain ⟨h₁, h₂, h₃⟩ := hk k (le_refl k)

Premises used: le_refl
-- 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
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
⊢ ⨅ (m : ℕ), (f ^ m).range = (f ^ k).range

Tactic:
obtain ⟨h₁, h₂, h₃⟩ := hk k (le_refl k)

Premises used: le_refl
-- 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
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
⊢ ⨆ (m : ℕ), (f ^ m).ker = (f ^ k).ker

Tactic:
obtain ⟨h₁, h₂, h₃⟩ := hk k (le_refl k)

Premises used: le_refl
-- 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
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
rwa : IsCompl (⨆ (n : ℕ), (f ^ n).ker) (f ^ k).range
rwa₁ rwa₂ rwa₃ rwa₄ : IsCompl (f ^ k).ker (f ^ k).range
⊢ IsCompl.{u_2} (α := Submodule R M) (⨆ (n : ℕ), (f ^ n).ker) (⨅ (n : ℕ), (f ^ n).range)

Tactic:
rwa [h₂, h₃]
-- Module: Mathlib.RingTheory.Artinian.Module
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
dsimp : r ^ n • r ^ (m - n) • y = x
⊢ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id : (a : M) → M) (r ^ (m - n) • y) = x

Tactic:
dsimp at hy ⊢
-- Module: Mathlib.RingTheory.Artinian.Module
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
rw₄ rw₅ : r ^ m • y = r ^ m • y
⊢ r ^ n • r ^ (m - n) • y = x

Tactic:
rw [← smul_assoc, smul_eq_mul, ← pow_add, ← hy, add_tsub_cancel_of_le h]

Premises used: smul_assoc, pow_add, smul_eq_mul, add_tsub_cancel_of_le
-- Module: Mathlib.RingTheory.Artinian.Module
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
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
⊢ ∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x

Tactic:
obtain ⟨n, hn⟩ := IsArtinian.range_smul_pow_stabilizes M r

Premises used: IsArtinian.range_smul_pow_stabilizes
-- Module: Mathlib.RingTheory.Artinian.Module
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
⊢ ∀ (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

Premises used: SetLike.ext_iff
-- Module: Mathlib.RingTheory.Artinian.Module
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 →
      ∀ (x : M),
        x ∈ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range ↔
          x ∈ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ m) LinearMap.id).range
⊢ ∃ (y : M), r ^ n.succ • y = r ^ n • x

Tactic:
simpa using hn n.succ n.le_succ (r ^ n • x)

Premises used: Nat.le_succ, HPow.hPow, HSMul.hSMul, Nat.succ
-- Module: Mathlib.RingTheory.Artinian.Module
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 →
      ∀ (x : M),
        x ∈ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ n) LinearMap.id).range ↔
          x ∈ (HSMul.hSMul (β := M →ₗ[R] M) (r ^ m) LinearMap.id).range
⊢ ∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x

Tactic:
exact ⟨n, by simpa using hn n.succ n.le_succ (r ^ n • x)⟩
-- 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
N : Submodule R M
h : IsArtinian R M
⊢ IsArtinian.{u_1, u_2} R ↥N

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : SMul R S
inst_4 : Module S M
inst_5 : Module R M
inst_6 : IsScalarTower R S M
h : IsArtinian R M
⊢ IsArtinian S M

Tactic:
⟨(Submodule.restrictScalarsEmbedding R S M).wellFounded h.wf⟩

Premises used: IsWellFounded.mk, Submodule.restrictScalarsEmbedding, IsWellFounded.wf, OrderEmbedding.wellFounded
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
K : Type u_1
inst : DivisionSemiring K
⊢ IsArtinianRing K

Tactic:
⟨Finite.wellFounded_of_trans_of_irrefl _⟩

Premises used: IsWellFounded.mk, Finite.wellFounded_of_trans_of_irrefl
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
K : Type u_1
inst : DivisionRing K
⊢ IsArtinianRing K

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Semiring R
h01 : Eq.{u_1 + 1} (α := R) 0 1
⊢ IsArtinianRing R

Tactic:
have := subsingleton_of_zero_eq_one h01
  inferInstance

Premises used: inferInstance, subsingleton_of_zero_eq_one
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
I : Ideal R
inst_2 : I.IsTwoSided
⊢ IsArtinianRing.{u_1} (R ⧸ I)

Tactic:
isArtinian_of_tower R inferInstance

Premises used: inferInstance, isArtinian_of_tower
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing R
a b : R
hab : a * b = 1
have : ∀ (c : R) (hca : Eq (α := R) ((LinearMap.toSpanSingleton R R a : (a : R) → R) c : R) (1 : R)), b * a = 1
⊢ b * a = 1

Tactic:
have ⟨c, hca⟩ := IsArtinian.surjective_of_injective_endomorphism
      (.toSpanSingleton R R a) (isRightRegular_of_mul_eq_one hab) 1
-- Module: Mathlib.RingTheory.Artinian.Module
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)
rwa rwa₁ rwa₂ rwa₃ : HMul.hMul (α := R) ((LinearMap.id : (a : R) → R) c : R) a = 1
⊢ b * a = 1

Tactic:
rwa [← left_inv_eq_right_inv hca hab]

Premises used: left_inv_eq_right_inv
-- 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 : IsArtinianRing R
inst_4 : Module.Finite R M
⊢ IsArtinian R M

Tactic:
have ⟨_, _, h⟩ := Module.Finite.exists_fin' R M
  isArtinian_of_surjective _ _ h

Premises used: _private.0.isArtinian_of_fg_of_artinian'.match_1, IsArtinian, isArtinian_of_surjective, Module.Finite.exists_fin'
-- 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
N : Submodule R M
inst_3 : IsArtinianRing R
hN : N.FG
⊢ Module.Finite.{u_1, u_2} R ↥N

Tactic:
rw [← Module.Finite.iff_fg] at hN

Premises used: Module.Finite.iff_fg
-- 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
N : Submodule R M
inst_3 : IsArtinianRing R
hN : Module.Finite.{u_1, u_2} R ↥N
⊢ IsArtinian.{u_1, u_2} R ↥N

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : IsArtinianRing R
inst_5 : Module.Finite R S
⊢ IsArtinianRing S

Tactic:
isArtinian_of_tower R isArtinian_of_fg_of_artinian'

Premises used: isArtinian_of_fg_of_artinian', isArtinian_of_tower
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Ring R
inst_3 : IsNoetherianRing R
⊢ IsNoetherianRing (Matrix n n R)

Tactic:
.of_finite R _

Premises used: IsNoetherianRing.of_finite
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
n : Type u_1
R : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : Ring R
inst_3 : IsArtinianRing R
⊢ IsArtinianRing (Matrix n n R)

Tactic:
.of_finite R _

Premises used: IsArtinianRing.of_finite
-- 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 : IsArtinianRing R
A : Set M
hA : A.Finite
⊢ IsArtinian.{u_1, u_2} R ↥(span R A)

Tactic:
isArtinian_of_fg_of_artinian _ (Submodule.fg_def.mpr ⟨A, hA, rfl⟩)

Premises used: Iff.mpr, Submodule.fg_def, isArtinian_of_fg_of_artinian, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Artinian.Module
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
⊢ IsArtinian R R

Tactic:
rw [isArtinianRing_iff] at H ⊢

Premises used: isArtinianRing_iff
-- Module: Mathlib.RingTheory.Artinian.Module
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 : IsArtinian R R
⊢ IsArtinian S S

Tactic:
⟨(Ideal.orderEmbeddingOfSurjective f hf).wellFounded H.wf⟩

Premises used: Ideal.orderEmbeddingOfSurjective, IsWellFounded.mk, IsWellFounded.wf, OrderEmbedding.wellFounded
-- Module: Mathlib.RingTheory.Artinian.Module
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 : IsArtinian R R
⊢ IsArtinian S S

Tactic:
exact ⟨(Ideal.orderEmbeddingOfSurjective f hf).wellFounded H.wf⟩
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
inst_2 : IsArtinianRing R
⊢ IsArtinianRing.{u_2} ↥f.rangeS

Tactic:
f.rangeSRestrict_surjective.isArtinianRing

Premises used: Function.Surjective.isArtinianRing, RingHom.rangeSRestrict_surjective
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : Ring S
f : R →+* S
inst_2 : IsArtinianRing R
⊢ IsArtinianRing.{u_2} ↥(RingHom.range.{u_1, u_2} (R := R) f)

Tactic:
isArtinianRing_rangeS f

Premises used: Set.Mem, isArtinianRing_rangeS, Subring.copy, RingHom.range, Subsemiring.copy, RingHom.rangeS
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R ≃+* S
inst_2 : IsArtinianRing R
⊢ IsArtinianRing S

Tactic:
f.surjective.isArtinianRing

Premises used: RingEquiv.surjective, Function.Surjective.isArtinianRing
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsArtinianRing R
inst_3 : IsArtinianRing S
⊢ IsArtinianRing (R × S)

Tactic:
Ideal.idealProdEquiv.toOrderEmbedding.wellFoundedLT

Premises used: OrderIso.toOrderEmbedding, Ideal.idealProdEquiv, OrderEmbedding.wellFoundedLT
-- Module: Mathlib.RingTheory.Artinian.Module
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)
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)
⊢ ∀ {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 _ _ _ ι

Premises used: Finite.induction_empty_option
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
ι : Type u_2
inst : Finite ι
α β : 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:
fun e h ↦ RingEquiv.isArtinianRing (.piCongrLeft _ e)

Premises used: RingEquiv.piCongrLeft, RingEquiv.isArtinianRing
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
ι : Type u_2
inst : Finite ι
⊢ ∀ {α β : 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:
exact fun e h ↦ RingEquiv.isArtinianRing (.piCongrLeft _ e)

Premises used: RingEquiv.isArtinianRing
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
ι : Type u_2
inst : Finite ι
⊢ ∀ {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:
infer_instance
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
ι : Type u_2
inst : Finite ι
α : Type u_2
inst_1 : 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:
fun ih ↦ RingEquiv.isArtinianRing (.symm .piOptionEquivProd)

Premises used: RingEquiv.piOptionEquivProd, RingEquiv.isArtinianRing, RingEquiv.symm
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
ι : Type u_2
inst : Finite ι
⊢ ∀ {α : 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:
exact fun ih ↦ RingEquiv.isArtinianRing (.symm .piOptionEquivProd)

Premises used: RingEquiv.isArtinianRing, RingEquiv.symm
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing R
x : R
rw : (Injective (β := R) fun (x_1 : R) ↦ x_1 * x) → Surjective (β := R) fun (x_1 : R) ↦ x_1 * x
⊢ IsUnit x ↔ IsRightRegular x

Tactic:
rw [IsRightRegular, IsUnit.isUnit_iff_mulRight_bijective, Bijective, and_iff_left_of_imp]

Premises used: and_iff_left_of_imp, IsRightRegular, Function.Bijective, IsUnit.isUnit_iff_mulRight_bijective
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing R
x : R
⊢ (Injective (β := R) fun (x_1 : R) ↦ x_1 * x) → Surjective (β := R) fun (x_1 : R) ↦ x_1 * x

Tactic:
IsArtinian.surjective_of_injective_endomorphism (.toSpanSingleton R R x)

Premises used: IsArtinian.surjective_of_injective_endomorphism, LinearMap.toSpanSingleton
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing R
x : R
⊢ (Injective (β := R) fun (x_1 : R) ↦ x_1 * x) → Surjective (β := R) fun (x_1 : R) ↦ x_1 * x

Tactic:
exact IsArtinian.surjective_of_injective_endomorphism (.toSpanSingleton R R x)

Premises used: IsArtinian.surjective_of_injective_endomorphism, LinearMap.toSpanSingleton
-- Module: Mathlib.RingTheory.Artinian.Module
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
rw₂ rw₃ : IsUnit x ↔ IsUnit x
⊢ IsUnit x ↔ IsRegular x

Tactic:
rw [isRegular_iff, ← isUnit_iff_isRightRegular, and_iff_right_of_imp (·.isRegular.1)]

Premises used: isRegular_iff, IsArtinianRing.isUnit_iff_isRightRegular, and_iff_right_of_imp
-- Module: Mathlib.RingTheory.Artinian.Module
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)
rw₂ rw₃ : IsRightRegular (MulOpposite.op x) ↔ IsRightRegular (MulOpposite.op x)
⊢ IsUnit x ↔ IsLeftRegular x

Tactic:
rw [← isRightRegular_op, ← isUnit_op, isUnit_iff_isRightRegular]

Premises used: isUnit_op, isRightRegular_op, IsArtinianRing.isUnit_iff_isRightRegular
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
x : R
rw : IsUnit x ↔ IsLeftRegular x ∧ IsRightRegular x
rw₁ : IsUnit x ↔ IsUnit x ∧ IsRightRegular x
rw₂ rw₃ : IsUnit x ↔ IsUnit x
⊢ IsUnit x ↔ IsRegular x

Tactic:
rw [isRegular_iff, ← isUnit_iff_isLeftRegular, and_iff_left_of_imp (·.isRegular.2)]

Premises used: and_iff_left_of_imp, isRegular_iff, IsArtinianRing.isUnit_iff_isLeftRegular
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing R
a : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
rwa : IsRegular a
rwa₁ rwa₂ rwa₃ rwa₄ : Membership.mem (γ := Submonoid R) R⁰ a
⊢ IsUnit a

Tactic:
rwa [isUnit_iff_isRegular, isRegular_iff_mem_nonZeroDivisors]

Premises used: isRegular_iff_mem_nonZeroDivisors, IsArtinianRing.isUnit_iff_isRegular
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsArtinianRing.{u_1} Rᵐᵒᵖ
a : R
ha : Membership.mem (γ := Submonoid R) R⁰ a
rwa : IsRegular a
rwa₁ rwa₂ rwa₃ rwa₄ : Membership.mem (γ := Submonoid R) R⁰ a
⊢ IsUnit a

Tactic:
rwa [isUnit_iff_isRegular_of_mulOpposite, isRegular_iff_mem_nonZeroDivisors]

Premises used: IsArtinianRing.isUnit_iff_isRegular_of_mulOpposite, isRegular_iff_mem_nonZeroDivisors