awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x_1 : ι
h : Eq (α := Polynomial R →ₐ[R] A) (Polynomial.aeval (x x_1)) (AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)))
⊢ Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) (f x_1) : A)
    ((AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)) : (a : Polynomial R) → A) (f x_1) : A)

Tactic:
congr 1
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x_1 : ι
h :
  Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) Polynomial.X : A)
    ((AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)) : (a : Polynomial R) → A) Polynomial.X : A)
⊢ Eq (α := Polynomial R →ₐ[R] A) (Polynomial.aeval (x x_1)) (AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)))

Tactic:
ext1
-- Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Goal:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
hx : AlgebraicIndependent R x
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x_1 : ι
⊢ Eq.{v + 1} (α := A) ((Polynomial.aeval (x x_1) : (a : Polynomial R) → A) Polynomial.X : A)
    ((AlgHom.comp (aeval x) (Polynomial.aeval (X x_1)) : (a : Polynomial R) → A) Polynomial.X : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.Artinian.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : Ring A
inst_3 : Algebra R A
a : A
hi : IsIntegral R a
ha : Membership.mem (γ := Submonoid A) A⁰ a
⊢ IsUnit a

Tactic:
let B := Algebra.adjoin R {a}
  let b : B := ⟨a, Algebra.self_mem_adjoin_singleton R a⟩
  haveI : Module.Finite R B := Algebra.finite_adjoin_simple_of_isIntegral hi
  haveI : IsArtinianRing B := isArtinian_of_tower R inferInstance
  have hinj : Function.Injective B.subtype := Subtype.val_injective
  have hb : b ∈ B⁰ := comap_nonZeroDivisors_le_of_injective hinj ha
  (isUnit_of_mem_nonZeroDivisors hb).map B.subtype

Premises used: IsArtinianRing.isUnit_of_mem_nonZeroDivisors, Subsemiring.subtype, Subtype.val_injective, Algebra.adjoin, Subalgebra.toSubsemiring, Subtype.mk, IsUnit.map, Singleton.singleton, comap_nonZeroDivisors_le_of_injective, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.Artinian.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : Ring A
inst_3 : Algebra R A
a : A
hi : IsIntegral R a
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid A) A⁰ a

Tactic:
⟨IsUnit.mem_nonZeroDivisors, isUnit_of_isIntegral_of_nonZeroDivisor hi⟩

Premises used: Iff.intro, IsUnit.mem_nonZeroDivisors, IsArtinianRing.isUnit_of_isIntegral_of_nonZeroDivisor
-- Module: Mathlib.RingTheory.Artinian.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : Ring A
inst_3 : Algebra R A
inst_4 : Algebra.IsIntegral R A
a : A
ha : Membership.mem (γ := Submonoid A) A⁰ a
⊢ IsUnit a

Tactic:
isUnit_of_isIntegral_of_nonZeroDivisor (R := R) (Algebra.IsIntegral.isIntegral a) ha

Premises used: Algebra.IsIntegral.isIntegral, IsArtinianRing.isUnit_of_isIntegral_of_nonZeroDivisor
-- Module: Mathlib.RingTheory.Artinian.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : Ring A
inst_3 : Algebra R A
inst_4 : Algebra.IsIntegral R A
a : A
⊢ IsUnit a ↔ Membership.mem (γ := Submonoid A) A⁰ a

Tactic:
isUnit_iff_nonZeroDivisor_of_isIntegral (R := R) (Algebra.IsIntegral.isIntegral a)

Premises used: Algebra.IsIntegral.isIntegral, IsArtinianRing.isUnit_iff_nonZeroDivisor_of_isIntegral
-- Module: Mathlib.RingTheory.Artinian.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : Ring A
inst_3 : Algebra R A
inst_4 : Algebra.IsIntegral R A
h :
  ∀ (x : A),
    Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ↔ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x
⊢ Eq (α := Submonoid A) (IsUnit.submonoid A : Submonoid A) (A⁰ : Submonoid A)

Tactic:
ext
-- Module: Mathlib.RingTheory.Artinian.Algebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : Ring A
inst_3 : Algebra R A
inst_4 : Algebra.IsIntegral R A
x : A
⊢ Membership.mem (γ := Submonoid A) (IsUnit.submonoid A) x ↔ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x

Tactic:
simpa [IsUnit.mem_submonoid_iff] using isUnit_iff_nonZeroDivisor_of_isIntegral' (R := R)

Premises used: IsUnit.mem_submonoid_iff, IsArtinianRing.isUnit_iff_nonZeroDivisor_of_isIntegral'
-- Module: Mathlib.RingTheory.Artinian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsArtinian R M ↔ WellFounded fun (x1 x2 : Submodule R M) ↦ x1 < x2

Tactic:
isWellFounded_iff _ _

Premises used: isWellFounded_iff
-- Module: Mathlib.RingTheory.Artinian.Defs
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
P : Submodule R M → Prop
hgt : ∀ (I : Submodule R M), (∀ J < I, P J) → P I
I : Submodule R M
⊢ P I

Tactic:
WellFoundedLT.induction I hgt

Premises used: WellFoundedLT.induction
-- Module: Mathlib.RingTheory.Artinian.Defs
Goal:
R : Type u_1
inst : Semiring R
⊢ IsArtinianRing R ↔ IsArtinian R R

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Artinian.Instances
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
inst_2 : ∀ (n : ℕ), IsArtinian R (Fin n → R)
⊢ StrongRankCondition R

Tactic:
(strongRankCondition_iff_succ R).2 fun n f hf ↦
    have e := LinearEquiv.piCongrLeft R (fun _ ↦ R) (finSuccEquiv n) ≪≫ₗ .piOptionEquivProd _
    not_subsingleton R <| IsArtinian.subsingleton_of_injective
      (f := f ∘ₗ e.symm.toLinearMap) (hf.comp e.symm.injective)

Premises used: Iff.mpr, LinearEquiv.symm, IsArtinian.subsingleton_of_injective, LinearEquiv.piCongrLeft, finSuccEquiv, Function.Injective.comp, LinearEquiv.piOptionEquivProd, not_subsingleton, LinearEquiv.injective, LinearEquiv.trans, strongRankCondition_iff_succ
-- Module: Mathlib.RingTheory.Artinian.Instances
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsReduced R
⊢ DecompositionMonoid R

Tactic:
MulEquiv.decompositionMonoid (equivPi R)

Premises used: IsArtinianRing.equivPi, MulEquiv.decompositionMonoid
-- Module: Mathlib.RingTheory.Artinian.Instances
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
inst_2 : IsReduced R
⊢ DecompositionMonoid.{u_1} (Polynomial R)

Tactic:
MulEquiv.decompositionMonoid <|
    (Polynomial.mapEquiv <| (equivPi R).toRingEquiv).trans (Polynomial.piEquiv _)

Premises used: IsArtinianRing.equivPi, AlgEquiv.toRingEquiv, Polynomial.piEquiv, RingEquiv.trans, MulEquiv.decompositionMonoid, Polynomial.mapEquiv
-- 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
S : Type u_5
P : Type u_6
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Function.Bijective.{u_2 + 1, u_6 + 1} (α := M) (β := P) (⇑l : (a : M) → P)
⊢ IsArtinian R M ↔ IsArtinian S P

Tactic:
let e := Submodule.orderIsoMapComapOfBijective l hl
  ⟨fun _ ↦ e.symm.strictMono.wellFoundedLT, fun _ ↦ e.strictMono.wellFoundedLT⟩

Premises used: OrderIso.strictMono, OrderIso.symm, Iff.intro, StrictMono.wellFoundedLT, Submodule.orderIsoMapComapOfBijective
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : Module R M
inst_4 : Module R P
f : M →ₗ[R] P
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
inst_5 : IsArtinian R P
⊢ IsArtinian R M

Tactic:
⟨Subrelation.wf
    (fun {A B} hAB => show A.map f < B.map f from Submodule.map_strictMono_of_injective h hAB)
    (InvImage.wf (Submodule.map f) IsWellFounded.wf)⟩

Premises used: IsWellFounded.mk, Submodule.map_strictMono_of_injective, IsWellFounded.wf, Subrelation.wf, InvImage.wf, Submodule.map
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
N_1 : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid N_1
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R N_1
inst_7 : IsArtinian R M
N : Submodule R M
⊢ IsArtinian.{u_1, u_2} R ↥N

Tactic:
isArtinian_of_injective N.subtype Subtype.val_injective

Premises used: Subtype.val_injective, isArtinian_of_injective, Submodule.subtype
-- 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
s t : Submodule R M
inst_3 : IsArtinian.{u_1, u_2} R ↥t
h : s ≤ t
⊢ IsArtinian.{u_1, u_2} R ↥s

Tactic:
isArtinian_of_injective (Submodule.inclusion h) (Submodule.inclusion_injective h)

Premises used: Submodule.inclusion, isArtinian_of_injective, Submodule.inclusion_injective
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : Module R M
inst_4 : Module R P
f : M →ₗ[R] P
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
inst_5 : IsArtinian R M
⊢ IsArtinian R P

Tactic:
⟨Subrelation.wf
    (fun {A B} hAB =>
      show A.comap f < B.comap f from Submodule.comap_strictMono_of_surjective hf hAB)
    (InvImage.wf (Submodule.comap f) IsWellFounded.wf)⟩

Premises used: IsWellFounded.mk, Submodule.comap_strictMono_of_surjective, IsWellFounded.wf, Subrelation.wf, Submodule.comap, InvImage.wf
-- 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
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
apply : Submodule S M ↪o Submodule R M
⊢ IsArtinian S M

Tactic:
apply (OrderEmbedding.wellFoundedLT (β := Submodule R M))

Premises used: OrderEmbedding.wellFoundedLT
-- 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
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
refine_1 : Submodule S M → Submodule R M
refine_2 :
  Function.Injective (β := Submodule R M) fun (N : Submodule S M) ↦
    let __AddSubmonoid := N.toAddSubmonoid;
    { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ }
refine_3 :
  ∀ {a b : Submodule S M},
    LE.le (α := Submodule R M)
        (({
                toFun := fun (N : Submodule S M) ↦
                  let __AddSubmonoid := N.toAddSubmonoid;
                  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
                inj' := ⋯ } :
              (a : Submodule S M) → Submodule R M)
            a :
          Submodule R M)
        (({
                toFun := fun (N : Submodule S M) ↦
                  let __AddSubmonoid := N.toAddSubmonoid;
                  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
                inj' := ⋯ } :
              (a : Submodule S M) → Submodule R M)
            b :
          Submodule R M) ↔
      a ≤ b
⊢ Submodule S M ↪o Submodule R M

Tactic:
refine ⟨⟨?_, ?_⟩, ?_⟩
-- 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
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N : Submodule S M
refine_1 : ∀ (c : R) {x : M}, x ∈ N.carrier → c • x ∈ N.carrier
⊢ Submodule R M

Tactic:
refine { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ?_ }
-- 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
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N : Submodule S M
c : R
x : M
hx : x ∈ N.carrier
refine_1 : ∀ (r : S), HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x ∈ N.carrier
⊢ c • x ∈ N.carrier

Tactic:
obtain ⟨r, rfl⟩ := H c

Premises used: rfl
-- 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
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N : Submodule S M
x : M
hx : x ∈ N.carrier
r : S
this : r • x ∈ N
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x ∈ N.carrier

Tactic:
simpa [Algebra.algebraMap_eq_smul_one, smul_assoc]

Premises used: smul_assoc, Algebra.algebraMap_eq_smul_one
-- 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
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N : Submodule S M
x : M
hx : x ∈ N.carrier
r : S
refine_1 : r • x ∈ N
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x ∈ N.carrier

Tactic:
suffices r • x ∈ N by simpa [Algebra.algebraMap_eq_smul_one, smul_assoc]
-- 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
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N : Submodule S M
x : M
hx : x ∈ N.carrier
r : S
⊢ r • x ∈ N

Tactic:
apply N.smul_mem _ hx

Premises used: Submodule.smul_mem
-- 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
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N1 N2 : Submodule S M
h :
  Eq.{u_2 + 1} (α := Submodule R M)
    ((fun (N : Submodule S M) ↦
        let __AddSubmonoid := N.toAddSubmonoid;
        ({ toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ } : Submodule R M))
      N1)
    ((fun (N : Submodule S M) ↦
        let __AddSubmonoid := N.toAddSubmonoid;
        ({ toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ } : Submodule R M))
      N2)
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  ∀
    (h :
      ∀ (x : M),
        Membership.mem (γ := Submodule R M)
            ((fun (N : Submodule S M) ↦
                let __AddSubmonoid := N.toAddSubmonoid;
                ({ toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ } : Submodule R M))
              N1)
            x ↔
          Membership.mem (γ := Submodule R M)
            ((fun (N : Submodule S M) ↦
                let __AddSubmonoid := N.toAddSubmonoid;
                ({ toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ } : Submodule R M))
              N2)
            x)
    (x : M), x ∈ N1 ↔ x ∈ N2
⊢ N1 = N2

Tactic:
rwa [Submodule.ext_iff] at h ⊢

Premises used: Submodule.ext_iff
-- 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
S : Type u_5
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsArtinian R M
inst_7 : IsScalarTower S R M
H : Function.Surjective.{u_5 + 1, u_1 + 1} (α := S) (β := R) (⇑(algebraMap S R) : (a : S) → R)
N1 N2 : Submodule S M
⊢ LE.le (α := Submodule R M)
      (({
              toFun := fun (N : Submodule S M) ↦
                let __AddSubmonoid := N.toAddSubmonoid;
                { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
              inj' := ⋯ } :
            (a : Submodule S M) → Submodule R M)
          N1 :
        Submodule R M)
      (({
              toFun := fun (N : Submodule S M) ↦
                let __AddSubmonoid := N.toAddSubmonoid;
                { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
              inj' := ⋯ } :
            (a : Submodule S M) → Submodule R M)
          N2 :
        Submodule R M) ↔
    N1 ≤ N2

Tactic:
rfl
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R N
f : M →ₗ[R] P
inst_7 : IsArtinian R M
⊢ IsArtinian.{u_1, u_3} R ↥f.range

Tactic:
isArtinian_of_surjective _ _ f.surjective_rangeRestrict

Premises used: isArtinian_of_surjective, LinearMap.surjective_rangeRestrict
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : Module R M
inst_4 : Module R P
f : M ≃ₗ[R] P
inst_5 : IsArtinian R M
⊢ IsArtinian R P

Tactic:
isArtinian_of_surjective _ f.toLinearMap f.toEquiv.surjective

Premises used: LinearEquiv.toLinearMap, LinearEquiv.toEquiv, isArtinian_of_surjective, Equiv.surjective
-- Module: Mathlib.RingTheory.Artinian.Module
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : Module R M
inst_4 : Module R P
f : M ≃ₗ[R] P
⊢ IsArtinian R M ↔ IsArtinian R P

Tactic:
⟨fun _ ↦ isArtinian_of_linearEquiv f, fun _ ↦ isArtinian_of_linearEquiv f.symm⟩

Premises used: LinearEquiv.symm, Iff.intro, isArtinian_of_linearEquiv
-- 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 : Finite M
⊢ IsArtinian R M

Tactic:
⟨Finite.wellFounded_of_trans_of_irrefl _⟩

Premises used: IsWellFounded.mk, Finite.wellFounded_of_trans_of_irrefl
-- 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 : Nontrivial R
h : IsArtinian R M
s : Set M
hs : LinearIndependent.{u_2, u_1, u_2} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
i : (↑s : Type u_2)
h_1 : Eq (α := Submodule R M) (R ∙ (↑i : M)) ⊥
⊢ (↑i : M) = 0

Tactic:
simp_all
-- 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
rw :
  (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔
    WellFounded fun (x1 x2 : Submodule R M) ↦ x1 < x2
rw₁ 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
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M

Tactic:
rw [isArtinian_iff, WellFounded.wellFounded_iff_has_min]

Premises used: isArtinian_iff, WellFounded.wellFounded_iff_has_min
-- 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
a : Set (Submodule R M)
ha : a.Nonempty
⊢ ∃ M' ∈ a, ∀ I ∈ a, ¬I < M'

Tactic:
set_has_minimal_iff_artinian.mpr ‹_› a ha

Premises used: Iff.mpr, set_has_minimal_iff_artinian
-- 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
⊢ (∀ (f : ℕ →o (Submodule R M)ᵒᵈ),
      ∃ (n : ℕ),
        ∀ (m : ℕ),
          n ≤ m →
            Eq (α := (Submodule R M)ᵒᵈ) ((f : (a : ℕ) → (Submodule R M)ᵒᵈ) n : (Submodule R M)ᵒᵈ)
              ((f : (a : ℕ) → (Submodule R M)ᵒᵈ) m : (Submodule R M)ᵒᵈ)) ↔
    IsArtinian R M

Tactic:
wellFoundedGT_iff_monotone_chain_condition.symm

Premises used: wellFoundedGT_iff_monotone_chain_condition, OrderDual, Iff.symm
-- 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 : ℕ →o (Submodule R M)ᵒᵈ
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := (Submodule R M)ᵒᵈ) ((f : (a : ℕ) → (Submodule R M)ᵒᵈ) n : (Submodule R M)ᵒᵈ)
          ((f : (a : ℕ) → (Submodule R M)ᵒᵈ) m : (Submodule R M)ᵒᵈ)

Tactic:
monotone_stabilizes_iff_artinian.mpr ‹_› f

Premises used: Iff.mpr, monotone_stabilizes_iff_artinian
-- 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 : ℕ →o (Submodule R M)ᵒᵈ
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)ᵒᵈ)
⊢ EventuallyConst (α := ℕ) (β := (Submodule R M)ᵒᵈ) (⇑f : (a : ℕ) → (Submodule R M)ᵒᵈ) atTop

Tactic:
simp_rw [eventuallyConst_atTop, eq_comm]

Premises used: Filter.eventuallyConst_atTop, eq_comm
-- 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 : ℕ →o (Submodule R M)ᵒᵈ
⊢ ∃ (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:
monotone_stabilizes f

Premises used: 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 : ℕ →o (Submodule R M)ᵒᵈ
⊢ ∃ (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:
exact monotone_stabilizes f

Premises used: 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 : M →ₗ[R] M
s : Injective (α := M) (β := M) (⇑f : (a : M) → M)
⊢ IsArtinian R M

Tactic:
have h := ‹IsArtinian R M›
-- 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 : IsArtinian R M
contrapose : ∀ (h : ¬Surjective (α := M) (β := M) (⇑f : (a : M) → M)), ¬IsArtinian R M
⊢ Surjective (α := M) (β := M) (⇑f : (a : M) → M)

Tactic:
contrapose h
-- 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)
rw : ¬WellFounded fun (x1 x2 : Submodule R M) ↦ x1 < x2
⊢ ¬IsArtinian R M

Tactic:
rw [IsArtinian, WellFoundedLT, isWellFounded_iff]

Premises used: WellFoundedLT, isWellFounded_iff, IsArtinian