awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R : Type u_2
M_1 : Type u
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : IsSemiprimaryRing R
M : Type u
x : AddCommGroup M
x_1 x_2 : Module R M
h_1 : IsScalarTower R R M
h :
  (fun (M : Type u) [AddCommGroup M] [Module R M] [Module R M] ↦ IsNoetherian R M ↔ IsArtinian R M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h' :
  (fun (M : Type u) [AddCommGroup M] [Module R M] [Module R M] ↦ IsNoetherian R M ↔ IsArtinian R M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
N : Submodule R M := HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤
simp_rw simp_rw₁ : IsNoetherian R M ↔ IsArtinian R M
simp_rw₂ : IsNoetherian.{u_2, u} R ↥N ∧ IsNoetherian.{u_2, u} R (M ⧸ N) ↔ IsArtinian R M
⊢ IsNoetherian R M ↔ IsArtinian R M
have simp_rw₃ : IsNoetherian.{u_2, u} R ↥N ∧ IsNoetherian.{u_2, u} R (M ⧸ N) ↔ IsArtinian.{u_2, u} R ↥N ∧ IsArtinian.{u_2, u} R (M ⧸ N)
Tactic: simp_rw [isNoetherian_iff_submodule_quotient N, isArtinian_iff_submodule_quotient N, N, h, h']
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R : Type u_2
M_1 : Type u
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : IsSemiprimaryRing R
M : Type u
x : AddCommGroup M
x_1 x_2 : Module R M
h_1 : IsScalarTower R R M
h :
  (fun (M : Type u) [AddCommGroup M] [Module R M] [Module R M] ↦ IsNoetherian R M ↔ IsArtinian R M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h' :
  (fun (M : Type u) [AddCommGroup M] [Module R M] [Module R M] ↦ IsNoetherian R M ↔ IsArtinian R M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
N : Submodule R M := HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤
simp_rw simp_rw₁ : IsNoetherian R M ↔ IsArtinian R M
simp_rw₂ : IsNoetherian.{u_2, u} R ↥N ∧ IsNoetherian.{u_2, u} R (M ⧸ N) ↔ IsArtinian R M
simp_rw₃ :
  IsNoetherian.{u_2, u} R ↥N ∧ IsNoetherian.{u_2, u} R (M ⧸ N) ↔
    IsArtinian.{u_2, u} R ↥N ∧ IsArtinian.{u_2, u} R (M ⧸ N)
simp_rw₄ :
  IsNoetherian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ∧
      IsNoetherian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ↔
    IsArtinian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ∧
      IsArtinian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
⊢ IsNoetherian R M ↔ IsArtinian R M
have simp_rw₅ : IsArtinian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ∧
    IsNoetherian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ↔
  IsArtinian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ∧
    IsArtinian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
Tactic: simp_rw [isNoetherian_iff_submodule_quotient N, isArtinian_iff_submodule_quotient N, N, h, h']
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE
have tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
Tactic: tfae_have 2 ↔ 3 := IsSemiprimaryRing.isNoetherian_iff_isArtinian
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE
have tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
Tactic: tfae_have 2 → 1 := fun _ ↦ inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE
have tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
Tactic: tfae_have 1 → 3 := fun _ ↦ inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE
have rw : [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M].TFAE
Tactic: rw [isFiniteLength_iff_isNoetherian_isArtinian]
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M].TFAE
have tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
Tactic: tfae_have 4 → 2 := And.left
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M].TFAE
have tfae_2_to_4 : ∀ (a : IsNoetherian R M), IsNoetherian R M ∧ IsArtinian R M
Tactic: tfae_have 2 → 4 := fun h ↦ ⟨h, tfae_2_iff_3.mp h⟩
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
⊢ IsNoetherian R M
have obtain : ∀ (s : Set M) (fin : s.Finite) (span : Eq (α := Submodule R M) (Submodule.span R s) ⊤), IsNoetherian R M
Tactic: obtain ⟨s, fin, span⟩ := Submodule.fg_def.mp (Module.finite_def.mp ‹_›)
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : s.Finite
span : Eq (α := Submodule R M) (Submodule.span R s) ⊤
⊢ IsNoetherian R M
have span₁ : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
Tactic: rw [← s.iUnion_of_singleton_coe, Submodule.span_iUnion] at span
Cleared hypotheses: span
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : s.Finite
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
⊢ IsNoetherian R M
have fin₁ : Finite.{u + 1} (↑s : Type u)
Tactic: rw [← Set.finite_coe_iff] at fin
Cleared hypotheses: fin, span
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
⊢ IsNoetherian R M
have rw : IsNoetherian.{u_3, u} R ↥(⨆ (i : (↑s : Type u)), R ∙ (↑i : M))
Tactic: rw [← isNoetherian_top_iff, ← span]
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
i : M
⊢ IsNoetherian.{u_3, u} R ↥(R ∙ i)
have rw : IsNoetherian R (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
Tactic: rw [LinearMap.span_singleton_eq_range, ← (LinearMap.quotKerEquivRange _).isNoetherian_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I :=
  fun (I : Ideal R) ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsNoetherian R (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
have rw : IsNoetherian.{u_3, u_3} (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
  (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
Tactic: rw [(e _).isNoetherian_iff_of_bijective Function.bijective_id]
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I :=
  fun (I : Ideal R) ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsNoetherian.{u_3, u_3} (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
    (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
have refine : IsArtinianRing.{u_3} (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
Tactic: refine @instIsNoetherianRingOfIsArtinianRing _ _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I :=
  fun (I : Ideal R) ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsArtinianRing.{u_3} (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
have rw : IsArtinian.{u_3, u} R ↥(LinearMap.range (LinearMap.toSpanSingleton R M i))
Tactic: rw [IsArtinianRing, ← (e _).isArtinian_iff_of_bijective Function.bijective_id,
      (LinearMap.quotKerEquivRange _).isArtinian_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (hypothesis)
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
⊢ IsNoetherian.{u_3, u} R ↥(⨆ (i : (↑s : Type u)), R ∙ (↑i : M))
have x : ∀ (i : M), IsNoetherian.{u_3, u} R ↥(R ∙ i)
Tactic: have _ (i : M) : IsNoetherian R (Submodule.span R {i}) := by
    rw [LinearMap.span_singleton_eq_range, ← (LinearMap.quotKerEquivRange _).isNoetherian_iff]
    let e (I : Ideal R) : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := ⟨.id _, fun _ _ ↦ rfl⟩
    rw [(e _).isNoetherian_iff_of_bijective Function.bijective_id]
    refine @instIsNoetherianRingOfIsArtinianRing _ _ ?_
    rw [IsArtinianRing, ← (e _).isArtinian_iff_of_bijective Function.bijective_id,
      (LinearMap.quotKerEquivRange _).isArtinian_iff]
    infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : Ring.KrullDimLE 0 R
eq : Eq (α := Ideal R) (Ring.jacobson R) (nilradical R)
Spec : Set (Ideal R) := {I : Ideal R | I.IsPrime}
this_1 : Finite.{u_3 + 1} (↑Spec : Type u_3)
this_2 : ∀ (I : (↑Spec : Type u_3)), (↑I : Ideal R).IsPrime
this : ∀ (I : (↑Spec : Type u_3)), IsSemisimpleRing.{u_3} (R ⧸ (↑I : Ideal R))
⊢ IsSemisimpleRing.{u_3} (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
have rw : IsSemisimpleRing.{u_3}
  (HasQuotient.Quotient R (B := Ideal R) (⨅ (a : (↑{J : Ideal R | J.IsPrime} : Type u_3)), (↑a : Ideal R)))
Tactic: rw [eq, nilradical_eq_sInf, sInf_eq_iInf']
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ IsArtinianRing R ↔ Ring.KrullDimLE 0 R
have rwa : IsNoetherianRing R ∧ Ring.KrullDimLE 0 R ↔ Ring.KrullDimLE 0 R
Tactic: rwa [isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, and_iff_right]
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
rwa : IsNoetherianRing R ∧ Ring.KrullDimLE 0 R ↔ Ring.KrullDimLE 0 R
⊢ IsArtinianRing R ↔ Ring.KrullDimLE 0 R
have rwa₁ : Ring.KrullDimLE 0 R ↔ Ring.KrullDimLE 0 R
Tactic: rwa [isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, and_iff_right]
-- Lean 4 proof step from Mathlib.RingTheory.HopkinsLevitzki (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ IsArtinianRing R ↔ IsNilpotent (R := Ideal R) (IsLocalRing.maximalIdeal R)
have rw : LE.le (α := Ideal R) (nilradical R) (IsLocalRing.maximalIdeal R)
Tactic: rw [isArtinianRing_iff_krullDimLE_zero,
    Ideal.FG.isNilpotent_iff_le_nilradical (IsNoetherian.noetherian _),
    ← and_iff_left (a := Ring.KrullDimLE 0 R) ‹IsLocalRing R›,
    (Ring.krullDimLE_zero_and_isLocalRing_tfae R).out 0 3 rfl rfl,
    IsLocalRing.isMaximal_iff, le_antisymm_iff, and_iff_right]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
I : Ideal R
inst_3 : IsNoetherianRing R
⊢ N.IsAssociatedPrime I ↔ I.IsPrime ∧ ∃ (x : M), I = N.colon {x}
have mp : N.IsAssociatedPrime I → I.IsPrime ∧ ∃ (x : M), I = N.colon {x}
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
I : Ideal R
inst_3 : IsNoetherianRing R
mp : N.IsAssociatedPrime I → I.IsPrime ∧ ∃ (x : M), I = N.colon {x}
⊢ N.IsAssociatedPrime I ↔ I.IsPrime ∧ ∃ (x : M), I = N.colon {x}
have mpr : (I.IsPrime ∧ ∃ (x : M), I = N.colon {x}) → N.IsAssociatedPrime I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
⊢ (N.colon {x}).radical.IsPrime ∧ ∃ (x_1 : M), (N.colon {x}).radical = N.colon {x_1}
have mp : (N.colon {x}).radical ∈ (N.colon {x}).minimalPrimes
Tactic: refine ⟨hx, exists_eq_colon_of_mem_minimalPrimes (x := x) ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
⊢ (N.colon {x}).radical ∈ (N.colon {x}).minimalPrimes
have mp : (N.colon {x}).radical ∈ (N.colon {x}).radical.minimalPrimes
Tactic: rw [← Ideal.radical_minimalPrimes, Ideal.minimalPrimes_eq_subsingleton_self,
      Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
mp : (N.colon {x}).radical ∈ (N.colon {x}).radical.minimalPrimes
⊢ (N.colon {x}).radical ∈ (N.colon {x}).minimalPrimes
have mp₁ : Membership.mem (γ := Set (Ideal R)) {(N.colon {x}).radical} (N.colon {x}).radical
Tactic: rw [← Ideal.radical_minimalPrimes, Ideal.minimalPrimes_eq_subsingleton_self,
      Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsNoetherianRing R
x : M
hx : (N.colon {x}).radical.IsPrime
mp : (N.colon {x}).radical ∈ (N.colon {x}).radical.minimalPrimes
mp₁ : Membership.mem (γ := Set (Ideal R)) {(N.colon {x}).radical} (N.colon {x}).radical
⊢ (N.colon {x}).radical ∈ (N.colon {x}).minimalPrimes
have mp₂ : (N.colon {x}).radical = (N.colon {x}).radical
Tactic: rw [← Ideal.radical_minimalPrimes, Ideal.minimalPrimes_eq_subsingleton_self,
      Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
h : IsAssociatedPrime I M
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
⊢ IsAssociatedPrime I M'
have obtain : ∀ (x : M) (h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M),
  IsAssociatedPrime.{u_1, u_3} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M'
Tactic: obtain ⟨x, rfl⟩ := h.2
Cleared hypotheses: I, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : M
h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M
⊢ IsAssociatedPrime.{u_1, u_3} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M'
have refine : Eq.{u_1 + 1} (α := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x}))
  (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
Tactic: refine ⟨h.1, ⟨f x, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : M
h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M
⊢ Eq.{u_1 + 1} (α := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x}))
    (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
have h₁ : ∀ (r : R),
  Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) r ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      r
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : M
h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M
r : R
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) r ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      r
have h₁ : (∃ (n : ℕ), Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {x}) (r ^ n)) ↔
  ∃ (n : ℕ), Membership.mem (γ := Ideal R) (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))) (r ^ n)
Tactic: simp_rw [Ideal.mem_radical_iff, mem_colon_singleton, mem_bot, ← map_smul, map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : M
h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M
r : R
h₁ :
  (∃ (n : ℕ), Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {x}) (r ^ n)) ↔
    ∃ (n : ℕ),
      Membership.mem (γ := Ideal R) (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))) (r ^ n)
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) r ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      r
have h₂ : (∃ (n : ℕ), Membership.mem (γ := Submodule R M) ⊥ (r ^ n • x)) ↔
  ∃ (n : ℕ), Membership.mem (γ := Submodule R M') ⊥ (HSMul.hSMul (β := M') (r ^ n) ((f : (a : M) → M') x : M'))
Tactic: simp_rw [Ideal.mem_radical_iff, mem_colon_singleton, mem_bot, ← map_smul, map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : M
h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M
r : R
h₁ :
  (∃ (n : ℕ), Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {x}) (r ^ n)) ↔
    ∃ (n : ℕ),
      Membership.mem (γ := Ideal R) (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))) (r ^ n)
h₂ :
  (∃ (n : ℕ), Membership.mem (γ := Submodule R M) ⊥ (r ^ n • x)) ↔
    ∃ (n : ℕ), Membership.mem (γ := Submodule R M') ⊥ (HSMul.hSMul (β := M') (r ^ n) ((f : (a : M) → M') x : M'))
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) r ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      r
have h₃ : (∃ (n : ℕ), r ^ n • x = 0) ↔ ∃ (n : ℕ), HSMul.hSMul (β := M') (r ^ n) ((f : (a : M) → M') x : M') = 0
Tactic: simp_rw [Ideal.mem_radical_iff, mem_colon_singleton, mem_bot, ← map_smul, map_eq_zero_iff f hf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.AssociatedPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : M
h : IsAssociatedPrime.{u_1, u_2} (R := R) (Ideal.radical (colon (M := M) ⊥ {x})) M
r : R
h₁ :
  (∃ (n : ℕ), Membership.mem (γ := Ideal R) (colon (M := M) ⊥ {x}) (r ^ n)) ↔
    ∃ (n : ℕ),
      Membership.mem (γ := Ideal R) (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))) (r ^ n)
h₂ :
  (∃ (n : ℕ), Membership.mem (γ := Submodule R M) ⊥ (r ^ n • x)) ↔
    ∃ (n : ℕ), Membership.mem (γ := Submodule R M') ⊥ (HSMul.hSMul (β := M') (r ^ n) ((f : (a : M) → M') x : M'))
h₃ : (∃ (n : ℕ), r ^ n • x = 0) ↔ ∃ (n : ℕ), HSMul.hSMul (β := M') (r ^ n) ((f : (a : M) → M') x : M') = 0
⊢ Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M) ⊥ {x})) r ↔
    Membership.mem (γ := Ideal R) (Ideal.radical (colon (M := M') ⊥ (singleton (α := M') ((f : (a : M) → M') x : M'))))
      r
have h₄ : (∃ (n : ℕ), r ^ n • x = 0) ↔ ∃ (n : ℕ), Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (r ^ n • x) : M') (0 : M')
Tactic: simp_rw [Ideal.mem_radical_iff, mem_colon_singleton, mem_bot, ← map_smul, map_eq_zero_iff f hf]