awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
a b : R
rw rw₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a b
⊢ ∃ (x : R) (y : R), @gcd _ CommSemiring.toCommMonoidWithZero _ a b = a * x + b * y

Tactic:
rw [← gcd_dvd_iff_exists]

Premises used: gcd_dvd_iff_exists
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
x y : R
rw : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔ ∃ (a : R) (b : R), a * x + b * y = 1
rw₁ : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔ Membership.mem (γ := Ideal R) (Ideal.span {x, y}) 1
rw₂ :
  IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔
    Membership.mem (γ := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) 1
rw₃ :
  Eq (α := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) ⊤ ↔
    Membership.mem (γ := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) 1
rw₄ rw₅ :
  Membership.mem (γ := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) 1 ↔
    Membership.mem (γ := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) 1
⊢ IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔ IsCoprime x y

Tactic:
rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]

Premises used: span_gcd, Ideal.span_singleton_eq_top, Ideal.eq_top_iff_one, Ideal.mem_span_pair, IsCoprime
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
p n : R
hp : Prime p
⊢ IsCoprime p n ↔ ¬p ∣ n

Tactic:
hp.irreducible.coprime_iff_not_dvd

Premises used: Prime.irreducible, Irreducible.coprime_iff_not_dvd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ k
this : GCDMonoid R := IsBezout.toGCDDomain R
⊢ ∃ (d : R), Associated (d ^ k) a

Tactic:
exists_associated_pow_of_mul_eq_pow ((gcd_isUnit_iff _ _).mpr hab) h

Premises used: Iff.mpr, gcd_isUnit_iff, exists_associated_pow_of_mul_eq_pow
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ k
this : GCDMonoid R := IsBezout.toGCDDomain R
⊢ ∃ (d : R), Associated (d ^ k) a

Tactic:
exact exists_associated_pow_of_mul_eq_pow ((gcd_isUnit_iff _ _).mpr hab) h

Premises used: Iff.mpr, gcd_isUnit_iff, exists_associated_pow_of_mul_eq_pow
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ k
letI letI₁ letI₂ : ∃ (d : R), Associated (d ^ k) a
⊢ ∃ (d : R), Associated (d ^ k) a

Tactic:
classical
  letI := IsBezout.toGCDDomain R
  exact exists_associated_pow_of_mul_eq_pow ((gcd_isUnit_iff _ _).mpr hab) h
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : Associated (c ^ k) (a * b)
obtain : ∀ (u : Rˣ) (hu : a * b * (↑u : R) = c ^ k), ∃ (d : R), Associated (d ^ k) a
⊢ ∃ (d : R), Associated (d ^ k) a

Tactic:
obtain ⟨u, hu⟩ := h.symm

Premises used: Associated.symm
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : Associated (c ^ k) (a * b)
u : Rˣ
hu : a * b * (↑u : R) = c ^ k
⊢ ∃ (d : R), Associated (d ^ k) a

Tactic:
exists_associated_pow_of_mul_eq_pow'
    ((isCoprime_mul_unit_right_right u.isUnit a b).mpr hab) <| mul_assoc a _ _ ▸ hu

Premises used: Iff.mpr, isCoprime_mul_unit_right_right, exists_associated_pow_of_mul_eq_pow', Units.isUnit
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : Associated (c ^ k) (a * b)
u : Rˣ
hu : a * b * (↑u : R) = c ^ k
⊢ ∃ (d : R), Associated (d ^ k) a

Tactic:
exact exists_associated_pow_of_mul_eq_pow'
    ((isCoprime_mul_unit_right_right u.isUnit a b).mpr hab) <| mul_assoc a _ _ ▸ hu

Premises used: Iff.mpr, isCoprime_mul_unit_right_right, exists_associated_pow_of_mul_eq_pow', Units.isUnit
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
⊢ IsCoprime x y

Tactic:
(WfDvdMonoid.isRelPrime_of_no_irreducible_factors nonzero H).isCoprime

Premises used: WfDvdMonoid.isRelPrime_of_no_irreducible_factors, IsRelPrime.isCoprime
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Prime z → z ∣ x → ¬z ∣ y
⊢ IsCoprime x y

Tactic:
isCoprime_of_irreducible_dvd nonzero fun z zi ↦ H z zi.prime

Premises used: isCoprime_of_irreducible_dvd, Irreducible.prime
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
⊢ Eq (α := Set (Ideal R)) (nonPrincipals R) ∅ ↔ IsPrincipalIdealRing R

Tactic:
simp [Set.eq_empty_iff_forall_notMem, isPrincipalIdealRing_iff]

Premises used: isPrincipalIdealRing_iff, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
pos : ∀ (H : c.Nonempty), ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I
neg : ∀ (H : ¬c.Nonempty), ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I
⊢ ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I

Tactic:
by_cases H : c.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
H : c.Nonempty
pos :
  ∀ (K : Ideal R) (hKmem : K ∈ c),
    ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I
⊢ ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I

Tactic:
obtain ⟨K, hKmem⟩ := Set.nonempty_def.1 H

Premises used: Set.nonempty_def, Iff.mp
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
⊢ ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I

Tactic:
⟨sSup c, fun ⟨x, hx⟩ ↦ ?_, fun _ ↦ le_sSup⟩

Premises used: False, _private.0.Ideal.nonPrincipals_zorn.match_1, And.intro, Exists.intro, le_sSup, SupSet.sSup
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
pos : IsPrincipal (sSup c) → ∀ (x : R) (hx : sSup c = R ∙ x), False
⊢ ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I

Tactic:
refine ⟨sSup c, fun ⟨x, hx⟩ ↦ ?_, fun _ ↦ le_sSup⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
h : IsPrincipal (sSup c)
x : R
hx : sSup c = R ∙ x
⊢ x ∈ sSup c

Tactic:
have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
h : IsPrincipal (sSup c)
x : R
hx : sSup c = R ∙ x
hxmem : x ∈ sSup c
pos : ∀ (J : Submodule R R) (hJc : J ∈ c) (hxJ : x ∈ J), False
⊢ False

Tactic:
obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem

Premises used: IsChain.directedOn, Exists.intro, Iff.mp, Submodule.mem_sSup_of_directed
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
h : IsPrincipal (sSup c)
x : R
hx : sSup c = R ∙ x
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
⊢ sSup c ≤ J

Tactic:
simp [hx, Ideal.span_le, hxJ]

Premises used: Ideal.span_le
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
h : IsPrincipal (sSup c)
x : R
hx : sSup c = R ∙ x
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
⊢ sSup c = J

Tactic:
have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
h : IsPrincipal (sSup c)
x : R
hx : sSup c = R ∙ x
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
⊢ False

Tactic:
hs hJc ⟨hsSupJ ▸ ⟨x, hx⟩⟩

Premises used: Eq.rec, Submodule.IsPrincipal.mk, Exists.intro
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
H : c.Nonempty
K : Ideal R
hKmem : K ∈ c
h : IsPrincipal (sSup c)
x : R
hx : sSup c = R ∙ x
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
⊢ False

Tactic:
exact hs hJc ⟨hsSupJ ▸ ⟨x, hx⟩⟩

Premises used: Eq.rec, Submodule.IsPrincipal.mk, Exists.intro
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) c
H : ¬c.Nonempty
⊢ ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I

Tactic:
simpa [Set.not_nonempty_iff_eq_empty.1 H, isPrincipalIdealRing_iff] using hR

Premises used: Set.not_nonempty_iff_eq_empty, isPrincipalIdealRing_iff, Iff.mp
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
hR : ¬IsPrincipalIdealRing R
⊢ ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬IsPrincipal x) I

Tactic:
zorn_le₀ _ (nonPrincipals_zorn hR)

Premises used: Set.Mem, Ideal.nonPrincipals_zorn, zorn_le₀, Not
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : GCDMonoid R
n m : R
rw :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (Ideal.span {n} ⊓ Ideal.span {m}) x ↔
      Membership.mem (γ := Ideal R) (Ideal.span {@lcm _ CommSemiring.toCommMonoidWithZero _ n m}) x
⊢ Eq (α := Ideal R) (Ideal.span {n} ⊓ Ideal.span {m}) (Ideal.span {@lcm _ CommSemiring.toCommMonoidWithZero _ n m})

Tactic:
rw [Ideal.ext_iff]

Premises used: Ideal.ext_iff
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : GCDMonoid R
n m x : R
simp : n ∣ x ∧ m ∣ x ↔ @lcm _ CommSemiring.toCommMonoidWithZero _ n m ∣ x
⊢ Membership.mem (γ := Ideal R) (Ideal.span {n}) x ∧ Membership.mem (γ := Ideal R) (Ideal.span {m}) x ↔
    Membership.mem (γ := Ideal R) (Ideal.span {@lcm _ CommSemiring.toCommMonoidWithZero _ n m}) x

Tactic:
simp only [Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : GCDMonoid R
n m x : R
⊢ n ∣ x ∧ m ∣ x ↔ @lcm _ CommSemiring.toCommMonoidWithZero _ n m ∣ x

Tactic:
lcm_dvd_iff.symm

Premises used: lcm_dvd_iff, Iff.symm
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : GCDMonoid R
n m x : R
⊢ n ∣ x ∧ m ∣ x ↔ @lcm _ CommSemiring.toCommMonoidWithZero _ n m ∣ x

Tactic:
exact lcm_dvd_iff.symm

Premises used: lcm_dvd_iff, Iff.symm
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = R ∙ x
this : ∀ (y : R) (hy : Submodule.colon I (↑(span {a}) : Set R) = R ∙ y), Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal (Submodule.colon I (↑(span {a}) : Set R)) → Submodule.IsPrincipal I

Tactic:
⟨y, hy⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = R ∙ x
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = R ∙ y
⊢ Submodule.IsPrincipal I

Tactic:
⟨x * y, le_antisymm ?_ ?_⟩

Premises used: HMul.hMul, Submodule.IsPrincipal.mk, le_antisymm, Exists.intro
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = R ∙ x
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = R ∙ y
refine_1 : I ≤ R ∙ x * y
refine_2 : R ∙ x * y ≤ I
⊢ Submodule.IsPrincipal I

Tactic:
refine ⟨x * y, le_antisymm ?_ ?_⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = R ∙ x
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = R ∙ y
refine_1 :
  ∀ (hx : I ⊔ span {a} = span {x}) (y : R) (hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}), I ≤ span {x * y}
⊢ I ≤ R ∙ x * y

Tactic:
rw [submodule_span_eq] at *

Premises used: Ideal.submodule_span_eq
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = R ∙ x
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = R ∙ y
refine_2 :
  ∀ (hx : I ⊔ span {a} = span {x}) (y : R) (hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}), span {x * y} ≤ I
⊢ R ∙ x * y ≤ I

Tactic:
rw [submodule_span_eq] at *

Premises used: Ideal.submodule_span_eq
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
i : R
hi : i ∈ I
⊢ i ∈ I ⊔ span {a}

Tactic:
have hisup : i ∈ I ⊔ span {a} := mem_sup_left hi
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {a}
⊢ a ∈ I ⊔ span {a}

Tactic:
have hasup : a ∈ I ⊔ span {a} := mem_sup_right (mem_span_singleton_self a)
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {a}
hasup : a ∈ I ⊔ span {a}
⊢ ∃ (a : R), a * x = i

Tactic:
rw [hx, mem_span_singleton'] at hisup hasup

Premises used: Ideal.mem_span_singleton'
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {a}
hasup : a ∈ I ⊔ span {a}
hisup₁ : ∃ (a : R), a * x = i
⊢ ∃ (a_1 : R), a_1 * x = a

Tactic:
rw [hx, mem_span_singleton'] at hisup hasup

Premises used: Ideal.mem_span_singleton'
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
i : R
hi : i ∈ I
hisup : ∃ (a : R), a * x = i
hasup : ∃ (a_1 : R), a_1 * x = a
refine_1 : ∀ (u : R) (hi : u * x ∈ I), Membership.mem (γ := Submodule R R) (span {x * y}) (u * x)
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) i

Tactic:
obtain ⟨u, rfl⟩ := hisup

Premises used: rfl
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
hasup : ∃ (a_1 : R), a_1 * x = a
u : R
hi : u * x ∈ I
refine_1 :
  ∀ (v : R) (hx : I ⊔ span {v * x} = span {x}) (hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}),
    Membership.mem (γ := Submodule R R) (span {x * y}) (u * x)
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) (u * x)

Tactic:
obtain ⟨v, rfl⟩ := hasup

Premises used: rfl
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}
rw : u * x * v ∈ I
⊢ ∃ (z : R), z * y = u

Tactic:
rw [← mem_span_singleton', ← hy, mem_colon_span_singleton, mul_comm v, ← mul_assoc]

Premises used: Ideal.mem_span_singleton', Ideal.mem_colon_span_singleton, mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}
⊢ u * x * v ∈ I

Tactic:
mul_mem_right _ _ hi

Premises used: Set.Mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}
⊢ u * x * v ∈ I

Tactic:
exact mul_mem_right _ _ hi

Premises used: Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y u : R
hi : u * x ∈ I
v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}
refine_1 : ∀ (z : R) (hi : z * y * x ∈ I), Membership.mem (γ := Submodule R R) (span {x * y}) (z * y * x)
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) (u * x)

Tactic:
obtain ⟨z, rfl⟩ : ∃ z, z * y = u := by
        rw [← mem_span_singleton', ← hy, mem_colon_span_singleton, mul_comm v, ← mul_assoc]
        exact mul_mem_right _ _ hi

Premises used: rfl
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}
z : R
hi : z * y * x ∈ I
rw : z * (x * y) = z * (y * x)
rw₁ rw₂ : z * (x * y) = z * (x * y)
⊢ z * (x * y) = z * y * x

Tactic:
rw [mul_assoc, mul_comm y]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
x y v : R
hx : I ⊔ span {v * x} = span {x}
hy : Submodule.colon I (↑(span {v * x}) : Set R) = span {y}
z : R
hi : z * y * x ∈ I
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) (z * y * x)

Tactic:
exact mem_span_singleton'.2 ⟨z, by rw [mul_assoc, mul_comm y]⟩

Premises used: Iff.mpr, Ideal.mem_span_singleton', Exists.intro
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
refine_2 : I * span {y} ≤ I ∧ y * a ∈ I
⊢ span {x * y} ≤ I

Tactic:
rw [← span_singleton_mul_span_singleton, ← hx, Ideal.sup_mul, sup_le_iff,
        span_singleton_mul_span_singleton, mul_comm a, span_singleton_le_iff_mem]

Premises used: Ideal.span_singleton_le_iff_mem, Ideal.span_singleton_mul_span_singleton, sup_le_iff, mul_comm, Ideal.sup_mul
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
⊢ I * span {y} ≤ I ∧ y * a ∈ I

Tactic:
⟨mul_le_right, mem_colon_span_singleton.1 <| hy ▸ mem_span_singleton_self y⟩

Premises used: Ideal.mul_le_right, Ideal.mem_colon_span_singleton, Eq.rec, And.intro, Iff.mp, Eq.symm, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}
⊢ I * span {y} ≤ I ∧ y * a ∈ I

Tactic:
exact ⟨mul_le_right, mem_colon_span_singleton.1 <| hy ▸ mem_span_singleton_self y⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
⊢ IsPrincipalIdealRing R

Tactic:
⟨isOka_isPrincipal.forall_of_forall_prime (fun I hI ↦ exists_maximal_not_isPrincipal ?_) H⟩

Premises used: Ideal.IsOka.forall_of_forall_prime, Ideal.exists_maximal_not_isPrincipal, IsPrincipalIdealRing.mk, Ideal.isOka_isPrincipal
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
refine : ∀ (I : Ideal R) (hI : ¬Submodule.IsPrincipal I), ¬IsPrincipalIdealRing R
⊢ IsPrincipalIdealRing R

Tactic:
refine ⟨isOka_isPrincipal.forall_of_forall_prime (fun I hI ↦ exists_maximal_not_isPrincipal ?_) H⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
I : Ideal R
hI : ¬Submodule.IsPrincipal I
rw : ∃ (x : Ideal R), ¬Submodule.IsPrincipal x
⊢ ¬IsPrincipalIdealRing R

Tactic:
rw [isPrincipalIdealRing_iff, not_forall]

Premises used: isPrincipalIdealRing_iff, Classical.not_forall
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
I : Ideal R
hI : ¬Submodule.IsPrincipal I
⊢ ∃ (x : Ideal R), ¬Submodule.IsPrincipal x

Tactic:
⟨I, hI⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
I : Ideal R
hI : ¬Submodule.IsPrincipal I
⊢ ∃ (x : Ideal R), ¬Submodule.IsPrincipal x

Tactic:
exact ⟨I, hI⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime
Goal:
R : Type u_1
inst : CommSemiring R
H : ∀ (P : Ideal R), P.IsPrime → P ≠ ⊥ → Submodule.IsPrincipal P
⊢ IsPrincipalIdealRing R

Tactic:
.of_prime fun P hp ↦ (eq_or_ne P ⊥).elim (· ▸ inferInstance) <| H _ hp

Premises used: Eq.rec, inferInstance, Bot.bot, eq_or_ne, IsPrincipalIdealRing.of_prime, Or.elim, Eq.symm
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : QuasiFinite R S
P : Ideal R
inst_8 : P.IsPrime
⊢ IsArtinianRing (P.Fiber S)

Tactic:
.of_finite P.ResidueField _

Premises used: Ideal.ResidueField, IsArtinianRing.of_finite
-- Module: Mathlib.RingTheory.QuasiFinite.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : QuasiFinite R S
P : PrimeSpectrum R
⊢ Set.Finite (α := PrimeSpectrum S) (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S)) {P})

Tactic:
(PrimeSpectrum.preimageEquivFiber R S P).finite_iff.mpr finite_of_compact_of_discrete

Premises used: Iff.mpr, finite_of_compact_of_discrete, Equiv.finite_iff, Set.Finite, PrimeSpectrum.preimageEquivFiber