awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Finite.{u_2 + 1} (S ⧸ I)
this : Fintype (S ⧸ I)
h_main : ∀ {d : ℕ}, (↑d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
inl : AddMonoid.exponent.{u_2} (S ⧸ I) ∣ Fintype.card.{u_2} (S ⧸ I)
⊢ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ Fintype.card.{u_2} (S ⧸ I)

Tactic:
simp_rw [absNorm_under_eq_sInf, h_main, ← AddMonoid.exponent_eq_sInf]

Premises used: AddMonoid.exponent_eq_sInf, Int.absNorm_under_eq_sInf
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Finite.{u_2 + 1} (S ⧸ I)
this : Fintype (S ⧸ I)
h_main : ∀ {d : ℕ}, (↑d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
⊢ AddMonoid.exponent.{u_2} (S ⧸ I) ∣ Fintype.card.{u_2} (S ⧸ I)

Tactic:
AddGroup.exponent_dvd_card (G := S ⧸ I)

Premises used: AddGroup.exponent_dvd_card
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Finite.{u_2 + 1} (S ⧸ I)
this : Fintype (S ⧸ I)
h_main : ∀ {d : ℕ}, (↑d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0
⊢ AddMonoid.exponent.{u_2} (S ⧸ I) ∣ Fintype.card.{u_2} (S ⧸ I)

Tactic:
exact AddGroup.exponent_dvd_card (G := S ⧸ I)

Premises used: AddGroup.exponent_dvd_card
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Infinite.{u_2 + 1} (S ⧸ I)
inr : Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)

Tactic:
rw [absNorm_apply I, Submodule.cardQuot_apply, Nat.card_eq_zero_of_infinite]

Premises used: Nat.card_eq_zero_of_infinite, Ideal.absNorm_apply, Submodule.cardQuot_apply
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Infinite.{u_2 + 1} (S ⧸ I)
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)

Tactic:
Nat.dvd_zero _

Premises used: Nat.dvd_zero
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Module.Free ℤ S
I : Ideal S
h : Infinite.{u_2 + 1} (S ⧸ I)
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) : ℕ) (0 : ℕ)

Tactic:
exact Nat.dvd_zero _

Premises used: Nat.dvd_zero
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
⊢ ringChar.{u_2} (S ⧸ I) = (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)

Tactic:
ringChar.eq_iff.mpr <| (charP_iff _ _).mpr fun x ↦ ?_

Premises used: Iff.mpr, charP_iff, ringChar.eq_iff
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
refine : ∀ (x : ℕ), Eq.{u_2 + 1} (α := S ⧸ I) (↑x : S ⧸ I) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
⊢ ringChar.{u_2} (S ⧸ I) = (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)

Tactic:
refine ringChar.eq_iff.mpr <| (charP_iff _ _).mpr fun x ↦ ?_

Premises used: Iff.mpr, charP_iff, ringChar.eq_iff
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
x : ℕ
change :
  Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑x : S)) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
⊢ Eq.{u_2 + 1} (α := S ⧸ I) (↑x : S ⧸ I) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x

Tactic:
change Ideal.Quotient.mk I x = 0 ↔ _

Premises used: Ideal.Quotient.mk, Nat.cast, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
S : Type u_2
inst : CommRing S
I : Ideal S
x : ℕ
rw : (↑x : S) ∈ I ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
rw₁ : (↑(↑x : ℤ) : S) ∈ I ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
rw₂ :
  Dvd.dvd (α := ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I)) : ℤ) (↑x : ℤ) ↔
    (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
rw₃ rw₄ : (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x
⊢ Eq (α := S ⧸ I) ((Ideal.Quotient.mk I : (a : S) → S ⧸ I) (↑x : S)) 0 ↔ (absNorm : (a : Ideal ℤ) → ℕ) (under ℤ I) ∣ x

Tactic:
rw [Quotient.eq_zero_iff_mem, ← Int.cast_natCast, cast_mem_ideal_iff, natCast_dvd_natCast]

Premises used: Int.cast_natCast, Ideal.Quotient.eq_zero_iff_mem, Int.cast_mem_ideal_iff, Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
rw : IsPrime (under ℤ P)
rw₁ : Ne (α := ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)) : ℤ) 0
⊢ Prime ((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P))

Tactic:
rw [Nat.prime_iff_prime_int, ← span_singleton_prime, Int.ideal_span_absNorm_eq_self]

Premises used: Nat.prime_iff_prime_int, Ideal.span_singleton_prime, Int.ideal_span_absNorm_eq_self
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
⊢ IsPrime (under ℤ P)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
⊢ Ne (α := ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)) : ℤ) 0

Tactic:
Int.natCast_ne_zero.mpr <| absNorm_eq_zero_iff.not.mpr ?_

Premises used: Iff.mpr, Int.natCast_ne_zero, Iff.not, Ideal.absNorm_eq_zero_iff
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
refine : ¬Eq (α := Ideal ℤ) (under ℤ P) ⊥
⊢ Ne (α := ℤ) (↑((absNorm : (a : Ideal ℤ) → ℕ) (under ℤ P)) : ℤ) 0

Tactic:
refine Int.natCast_ne_zero.mpr <| absNorm_eq_zero_iff.not.mpr ?_

Premises used: Iff.mpr, Int.natCast_ne_zero, Iff.not, Ideal.absNorm_eq_zero_iff
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
⊢ P ≠ ⊥

Tactic:
have : P ≠ ⊥ := NeZero.ne _
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
this : P ≠ ⊥
contrapose : ∀ (this : Eq (α := Ideal ℤ) (under ℤ P) ⊥), P = ⊥
⊢ ¬Eq (α := Ideal ℤ) (under ℤ P) ⊥

Tactic:
contrapose this
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
this : Eq (α := Ideal ℤ) (under ℤ P) ⊥
⊢ P = ⊥

Tactic:
eq_bot_of_comap_eq_bot this

Premises used: Ideal.eq_bot_of_comap_eq_bot
-- Module: Mathlib.RingTheory.Ideal.Int
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Algebra.IsIntegral ℤ R
P : Ideal R
inst_3 : P.IsPrime
inst_4 : NeZero P
this : Eq (α := Ideal ℤ) (under ℤ P) ⊥
⊢ P = ⊥

Tactic:
exact eq_bot_of_comap_eq_bot this

Premises used: Ideal.eq_bot_of_comap_eq_bot
-- Module: Mathlib.RingTheory.Ideal.IsAugmentation
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
I : Ideal A
⊢ IsAugmentation R I ↔ IsCompl (α := Submodule R A) 1 (Submodule.restrictScalars R I)

Tactic:
Iff.rfl

Premises used: Ideal.IsAugmentation, Iff.rfl
-- Module: Mathlib.RingTheory.Ideal.IsAugmentation
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
I : Ideal A
⊢ IsAugmentation (↥S) I ↔
    IsCompl (α := Submodule R A) ((toSubmodule : (a : Subalgebra R A) → Submodule R A) S : Submodule R A)
      (Submodule.restrictScalars R I : Submodule R A)

Tactic:
simp [Ideal.IsAugmentation, ← Submodule.isCompl_restrictScalars_iff R]

Premises used: Ideal.IsAugmentation, Submodule.isCompl_restrictScalars_iff
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
rw :
  (I ≠ ⊤ ∧ ∀ (b a : R), a • b ∈ I → b ∈ I ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R R) (a ^ n) ⊤ ≤ I) ↔
    I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
⊢ I.IsPrimary ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
rw [IsPrimary, Submodule.IsPrimary, forall_comm]

Premises used: Submodule.IsPrimary, forall_comm, Ideal.IsPrimary
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
⊢ (I ≠ ⊤ ∧ ∀ (b a : R), a • b ∈ I → b ∈ I ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R R) (a ^ n) ⊤ ≤ I) ↔
    I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
simp only [mul_comm, mem_radical_iff,
    ← Submodule.ideal_span_singleton_smul, smul_eq_mul, mul_top, span_singleton_le_iff_mem]

Premises used: Submodule.ideal_span_singleton_smul, Ideal.span_singleton_le_iff_mem, mul_comm, Ideal.mem_radical_iff, smul_eq_mul, Ideal.mul_top
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.IsPrime
⊢ I.IsPrimary

Tactic:
isPrimary_iff.mpr
  ⟨hi.1, fun {_ _} hxy => (hi.mem_or_mem hxy).imp id fun hyi => le_radical hyi⟩

Premises used: Iff.mpr, Ideal.le_radical, id, Ideal.IsPrime.mem_or_mem, And.intro, Ideal.isPrimary_iff, Or.imp, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.IsPrimary
⊢ I.radical.IsPrime

Tactic:
I.colon_univ ▸ hi.isPrime_radical_colon

Premises used: Submodule.IsPrimary.isPrime_radical_colon, Eq.rec, Submodule.colon_univ
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
rw : I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
⊢ I.IsPrimary

Tactic:
rw [isPrimary_iff]

Premises used: Ideal.isPrimary_iff
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
left : I ≠ ⊤
right : ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
⊢ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
hi : IsMaximal.{u_1} (α := R) (radical ⊤)
⊢ False

Tactic:
exact (radical_top R ▸ hi).ne_top rfl
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
pos : ∀ (h : I + span {y} = ⊤), x ∈ I ∨ y ∈ I.radical
neg : ∀ (h : ¬I + span {y} = ⊤), x ∈ I ∨ y ∈ I.radical
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
by_cases h : I + span {y} = ⊤

Premises used: Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : I + span {y} = ⊤
pos : span {x} * I ≤ I ∧ x * y ∈ I ∨ y ∈ I.radical
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
rw [← span_singleton_le_iff_mem, ← mul_top (span {x}), ← h, mul_add,
        span_singleton_mul_span_singleton, add_le_iff, span_singleton_le_iff_mem]

Premises used: add_le_iff, Ideal.span_singleton_le_iff_mem, Ideal.span_singleton_mul_span_singleton, Ideal.span, mul_add, Ideal.mul_top, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : I + span {y} = ⊤
⊢ span {x} * I ≤ I ∧ x * y ∈ I ∨ y ∈ I.radical

Tactic:
Or.inl ⟨mul_le_left, hxy⟩

Premises used: Ideal.mul_le_left, And.intro, Or.inl
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : I + span {y} = ⊤
⊢ span {x} * I ≤ I ∧ x * y ∈ I ∨ y ∈ I.radical

Tactic:
exact Or.inl ⟨mul_le_left, hxy⟩

Premises used: Or.inl
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
neg : ∀ (m : Ideal R) (hm : m.IsMaximal) (hy : I + span {y} ≤ m), x ∈ I ∨ y ∈ I.radical
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
obtain ⟨m, hm, hy⟩ := exists_le_maximal (I + span {y}) h

Premises used: HAdd.hAdd, Ideal.exists_le_maximal, Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
m : Ideal R
hm : m.IsMaximal
hy : I + span {y} ≤ m
⊢ I.radical ≤ m ∧ y ∈ m

Tactic:
rw [add_le_iff, span_singleton_le_iff_mem, ← hm.isPrime.radical_le_iff] at hy

Premises used: Ideal.IsMaximal.isPrime, add_le_iff, Ideal.span_singleton_le_iff_mem, Ideal.IsPrime.radical_le_iff
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
m : Ideal R
hm : m.IsMaximal
hy : I.radical ≤ m ∧ y ∈ m
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
Or.inr (hi.eq_of_le hm.ne_top hy.1 ▸ hy.2)

Premises used: Eq.rec, And.right, And.left, Ideal.IsMaximal.eq_of_le, Ideal.IsMaximal.ne_top, Eq.symm, Or.inr
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hi : I.radical.IsMaximal
x y : R
hxy : x * y ∈ I
h : ¬I + span {y} = ⊤
m : Ideal R
hm : m.IsMaximal
hy : I.radical ≤ m ∧ y ∈ m
⊢ x ∈ I ∨ y ∈ I.radical

Tactic:
exact Or.inr (hi.eq_of_le hm.ne_top hy.1 ▸ hy.2)

Premises used: Or.inr
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
I J : Ideal R
hi : I.IsPrimary
hj : J.IsPrimary
hij : I.radical = J.radical
⊢ (Submodule.colon I Set.univ).radical = (Submodule.colon J Set.univ).radical

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
inst : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ ∀ ⦃y : ι⦄, y ∈ s → (Submodule.colon (f y) Set.univ).radical = (Submodule.colon (f i) Set.univ).radical

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
hI : I.IsPrimary
φ : R →+* S
rw :
  ∀ (hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical) (φ : R →+* S),
    Ne (α := Ideal R) (Ideal.comap φ I) ⊤ ∧
      ∀ {x y : R},
        Membership.mem (γ := Ideal R) (Ideal.comap φ I) (x * y) →
          Membership.mem (γ := Ideal R) (Ideal.comap φ I) x ∨
            Membership.mem (γ := Ideal R) (radical (Ideal.comap φ I)) y
⊢ IsPrimary (Ideal.comap φ I)

Tactic:
rw [isPrimary_iff] at hI ⊢

Premises used: Ideal.isPrimary_iff
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
⊢ Ne (α := Ideal R) (Ideal.comap φ I) ⊤ ∧
    ∀ {x y : R},
      Membership.mem (γ := Ideal R) (Ideal.comap φ I) (x * y) →
        Membership.mem (γ := Ideal R) (Ideal.comap φ I) x ∨ Membership.mem (γ := Ideal R) (radical (Ideal.comap φ I)) y

Tactic:
hI.imp (comap_ne_top φ) fun h ↦ ?_

Premises used: And.imp, Ideal.comap_ne_top
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
refine :
  ∀ (h : ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical) {x y : R},
    Membership.mem (γ := Ideal R) (Ideal.comap φ I) (x * y) →
      Membership.mem (γ := Ideal R) (Ideal.comap φ I) x ∨ Membership.mem (γ := Ideal R) (radical (Ideal.comap φ I)) y
⊢ Ne (α := Ideal R) (Ideal.comap φ I) ⊤ ∧
    ∀ {x y : R},
      Membership.mem (γ := Ideal R) (Ideal.comap φ I) (x * y) →
        Membership.mem (γ := Ideal R) (Ideal.comap φ I) x ∨ Membership.mem (γ := Ideal R) (radical (Ideal.comap φ I)) y

Tactic:
refine hI.imp (comap_ne_top φ) fun h ↦ ?_

Premises used: And.imp, Ideal.comap_ne_top
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
h : ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
simp :
  ∀ {x y : R},
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) x : S) ((φ : (a : R) → S) y : S) ∈ I →
      Membership.mem (α := S) I ((φ : (a : R) → S) x : S) ∨ Membership.mem (α := S) I.radical ((φ : (a : R) → S) y : S)
⊢ ∀ {x y : R},
    Membership.mem (γ := Ideal R) (Ideal.comap φ I) (x * y) →
      Membership.mem (γ := Ideal R) (Ideal.comap φ I) x ∨ Membership.mem (γ := Ideal R) (radical (Ideal.comap φ I)) y

Tactic:
simp only [mem_comap, map_mul, ← comap_radical]

Premises used: map_mul, Ideal.comap_radical, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
h : ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
x y : R
⊢ HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) x : S) ((φ : (a : R) → S) y : S) ∈ I →
    Membership.mem (α := S) I ((φ : (a : R) → S) x : S) ∨ Membership.mem (α := S) I.radical ((φ : (a : R) → S) y : S)

Tactic:
h
-- Module: Mathlib.RingTheory.Ideal.IsPrimary
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
I : Ideal S
hI : I ≠ ⊤ ∧ ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
φ : R →+* S
h : ∀ {x y : S}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
⊢ ∀ {x y : R},
    HMul.hMul (α := S) (β := S) ((φ : (a : R) → S) x : S) ((φ : (a : R) → S) y : S) ∈ I →
      Membership.mem (α := S) I ((φ : (a : R) → S) x : S) ∨ Membership.mem (α := S) I.radical ((φ : (a : R) → S) y : S)

Tactic:
exact h
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ Membership.mem (γ := Set (Ideal R)) {I : Ideal R | IsPrincipal I} (HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y))

Tactic:
⟨x * y, span_singleton_mul_span_singleton x y⟩

Premises used: HMul.hMul, Set.Mem, setOf, Ideal.span_singleton_mul_span_singleton, Submodule.IsPrincipal.mk, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ Membership.mem (γ := Set (Ideal R)) {I : Ideal R | IsPrincipal I} (HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y))

Tactic:
exact ⟨x * y, span_singleton_mul_span_singleton x y⟩
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ Membership.mem (γ := Submonoid (Ideal R)) (isPrincipalSubmonoid R) I ↔ IsPrincipal I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
a : R
⊢ Membership.mem (γ := Submonoid (Ideal R)) (isPrincipalSubmonoid R) (span {a})

Tactic:
mem_isPrincipalSubmonoid_iff.mpr ⟨a, rfl⟩

Premises used: Iff.mpr, Submodule.IsPrincipal.mk, Exists.intro, Ideal.mem_isPrincipalSubmonoid_iff, rfl
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
x : R
property : Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (R ∙ x)
y : R
property_1 : Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (R ∙ y)
simp_rw : HMul.hMul (α := Ideal R) (R ∙ x) (R ∙ y) = R ∙ x * y
simp_rw₁ : HMul.hMul (α := Ideal R) (span {x}) (span {y}) = span {x * y}
⊢ (↑(Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x) (R ∙ x) property *
          Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x) (R ∙ y)
            property_1) :
      Ideal R) =
    R ∙ x * y

Tactic:
simp_rw [Submonoid.mk_mul_mk, submodule_span_eq, span_singleton_mul_span_singleton]

Premises used: Ideal.submodule_span_eq, Submonoid.mk_mul_mk, Ideal.span_singleton_mul_span_singleton
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
x : R
property : Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (R ∙ x)
y : R
property_1 : Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ (R ∙ y)
⊢ Membership.mem (γ := Set ↥(Ideal R)⁰) {I : ↥(Ideal R)⁰ | IsPrincipal (↑I : Ideal R)}
    (Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x) (R ∙ x) property *
      Subtype.mk (p := fun (x : Ideal R) ↦ Membership.mem (γ := Submonoid (Ideal R)) (Ideal R)⁰ x) (R ∙ y) property_1)

Tactic:
exact ⟨x * y, by
      simp_rw [Submonoid.mk_mul_mk, submodule_span_eq, span_singleton_mul_span_singleton]⟩
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := Submodule R R) (↑1 : Ideal R) (R ∙ 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x x_1 : R
h : x ≈ x_1
⊢ Eq.{u_1 + 1} (α := { I : Ideal R // IsPrincipal I })
    ((fun (x : R) ↦ Subtype.mk (p := fun (I : Ideal R) ↦ IsPrincipal I) (span {x}) ⋯) x)
    ((fun (x : R) ↦ Subtype.mk (p := fun (I : Ideal R) ↦ IsPrincipal I) (span {x}) ⋯) x_1)

Tactic:
simpa [span_singleton_eq_span_singleton]

Premises used: Ideal.span_singleton_eq_span_singleton
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x : R
⊢ (fun (I : { I : Ideal R // IsPrincipal I }) ↦ (Associates.mk (IsPrincipal.generator (↑I : Ideal R)) : Associates R))
      (Quotient.lift (fun (x : R) ↦ Subtype.mk (p := fun (I : Ideal R) ↦ IsPrincipal I) (span {x}) ⋯) ⋯ ⟦x⟧) =
    ⟦x⟧

Tactic:
simpa [Quotient.eq] using
    Ideal.span_singleton_eq_span_singleton.mp (@Ideal.span_singleton_generator _ _ _ ⟨_, rfl⟩)

Premises used: Ideal.span_singleton_eq_span_singleton, Ideal.span_singleton_generator, Iff.mp, Quotient.eq
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : { I : Ideal R // IsPrincipal I }
⊢ Quotient.lift (s := Associated.setoid R)
      (fun (x : R) ↦ Subtype.mk (p := fun (I : Ideal R) ↦ IsPrincipal I) (span {x}) ⋯) ⋯
      ((fun (I : { I : Ideal R // IsPrincipal I }) ↦
          (Associates.mk (IsPrincipal.generator (↑I : Ideal R)) : Associates R))
        I) =
    I

Tactic:
simp only [_root_.Quotient.lift_mk, span_singleton_generator, Subtype.coe_eta]

Premises used: Quotient.lift_mk, Ideal.span_singleton_generator, Subtype.coe_eta
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
x : R
⊢ Eq (α := Ideal R)
    (↑((associatesEquivIsPrincipal R : (a : Associates R) → { I : Ideal R // IsPrincipal I }) (Associates.mk x)) :
      Ideal R)
    (span {x})

Tactic:
rfl

Premises used: Submodule.span, rfl
-- Module: Mathlib.RingTheory.Ideal.IsPrincipal
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
I : Ideal R
hI : IsPrincipal I
⊢ Eq (α := Associates R)
    ((Equiv.symm (associatesEquivIsPrincipal R) : (a : { I : Ideal R // IsPrincipal I }) → Associates R)
        (Subtype.mk (p := fun (I : Ideal R) ↦ IsPrincipal I) I hI) :
      Associates R)
    (Associates.mk (IsPrincipal.generator I) : Associates R)

Tactic:
rfl

Premises used: rfl