awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ (b : R),
      Membership.mem (γ := Multiset R)
          (if h : a = 0 then ∅
          else Classical.choose (p := fun (x : Multiset R) ↦ (∀ b ∈ x, Irreducible b) ∧ Associated x.prod a) ⋯)
          b →
        Irreducible b) ∧
    Associated
      (Multiset.prod
        (if h : a = 0 then ∅
        else Classical.choose (p := fun (x : Multiset R) ↦ (∀ b ∈ x, Irreducible b) ∧ Associated x.prod a) ⋯))
      a
have rw : (∀ b ∈ Classical.choose (p := fun (x : Multiset R) ↦ (∀ b ∈ x, Irreducible b) ∧ Associated x.prod a) sorry, Irreducible b) ∧
  Associated (Classical.choose (p := fun (x : Multiset R) ↦ (∀ b ∈ x, Irreducible b) ∧ Associated x.prod a) sorry).prod a
Tactic: rw [dif_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ b ∈ factors a, b ∈ s
hunit : ∀ (c : Rˣ), (↑c : R) ∈ s
⊢ a ∈ s
have rcases : ∀ (c : Rˣ) (hc : (factors a).prod * (↑c : R) = a), a ∈ s
Tactic: rcases (factors_spec a ha).2 with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ b ∈ factors a, b ∈ s
hunit : ∀ (c : Rˣ), (↑c : R) ∈ s
c : Rˣ
hc : (factors a).prod * (↑c : R) = a
⊢ a ∈ s
have rw : (factors a).prod * (↑c : R) ∈ s
Tactic: rw [← hc]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
N : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M →ₗ[R] N
S : Submodule R M
hI : S.IsPrincipal
⊢ Submodule.map f S = span R (singleton (α := N) ((f : (a : M) → N) (generator S) : N))
have rw : Submodule.map f S = span R (image (α := M) (⇑f : (a : M) → N) {generator S})
Tactic: rw [← Set.image_singleton, ← map_span, span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
N : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M →ₗ[R] N
S : Submodule R M
hI : S.IsPrincipal
rw : Submodule.map f S = span R (image (α := M) (⇑f : (a : M) → N) {generator S})
⊢ Submodule.map f S = span R (singleton (α := N) ((f : (a : M) → N) (generator S) : N))
have rw₁ : Submodule.map f S = Submodule.map f (R ∙ generator S)
Tactic: rw [← Set.image_singleton, ← map_span, span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
N : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M →ₗ[R] N
S : Submodule R M
hI : S.IsPrincipal
rw : Submodule.map f S = span R (image (α := M) (⇑f : (a : M) → N) {generator S})
rw₁ : Submodule.map f S = Submodule.map f (R ∙ generator S)
⊢ Submodule.map f S = span R (singleton (α := N) ((f : (a : M) → N) (generator S) : N))
have rw₂ : Submodule.map f S = Submodule.map f S
Tactic: rw [← Set.image_singleton, ← map_span, span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
M : Type v
N : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : M →ₗ[R] N
hf : Surjective.{v + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
S : Submodule R N
hI : (comap f S).IsPrincipal
⊢ S.IsPrincipal
have rw : (Submodule.map f (comap f S)).IsPrincipal
Tactic: rw [← Submodule.map_comap_eq_of_surjective hf S]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
S : Type u_1
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
I : Ideal R
hI : IsPrincipal I
⊢ Eq (α := Submodule S S) (Ideal.map f I) (span S (singleton (α := S) ((f : (a : R) → S) (generator I) : S)))
have rw : Eq (α := Submodule S S) (Ideal.map f I) (Ideal.span (singleton (α := S) ((f : (a : R) → S) (generator I) : S)))
Tactic: rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span,
      Ideal.span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
S : Type u_1
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
I : Ideal R
hI : IsPrincipal I
rw : Eq (α := Submodule S S) (Ideal.map f I) (Ideal.span (singleton (α := S) ((f : (a : R) → S) (generator I) : S)))
⊢ Eq (α := Submodule S S) (Ideal.map f I) (span S (singleton (α := S) ((f : (a : R) → S) (generator I) : S)))
have rw₁ : Eq.{u_1 + 1} (α := Submodule S S) (Ideal.map f I) (Ideal.span (image (α := R) (⇑f : (a : R) → S) {generator I}))
Tactic: rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span,
      Ideal.span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
S : Type u_1
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
I : Ideal R
hI : IsPrincipal I
rw : Eq (α := Submodule S S) (Ideal.map f I) (Ideal.span (singleton (α := S) ((f : (a : R) → S) (generator I) : S)))
rw₁ : Eq.{u_1 + 1} (α := Submodule S S) (Ideal.map f I) (Ideal.span (image (α := R) (⇑f : (a : R) → S) {generator I}))
⊢ Eq (α := Submodule S S) (Ideal.map f I) (span S (singleton (α := S) ((f : (a : R) → S) (generator I) : S)))
have rw₂ : Eq.{u_1 + 1} (α := Submodule S S) (Ideal.map f I) (Ideal.map (R := R) f (Ideal.span {generator I}))
Tactic: rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span,
      Ideal.span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
S : Type u_1
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
I : Ideal R
hI : IsPrincipal I
rw : Eq (α := Submodule S S) (Ideal.map f I) (Ideal.span (singleton (α := S) ((f : (a : R) → S) (generator I) : S)))
rw₁ : Eq.{u_1 + 1} (α := Submodule S S) (Ideal.map f I) (Ideal.span (image (α := R) (⇑f : (a : R) → S) {generator I}))
rw₂ : Eq.{u_1 + 1} (α := Submodule S S) (Ideal.map f I) (Ideal.map (R := R) f (Ideal.span {generator I}))
⊢ Eq (α := Submodule S S) (Ideal.map f I) (span S (singleton (α := S) ((f : (a : R) → S) (generator I) : S)))
have rw₃ : Eq.{u_1 + 1} (α := Submodule S S) (Ideal.map f I) (Ideal.map f I)
Tactic: rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span,
      Ideal.span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
S : Type u_1
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ IsPrincipal I
have rw : IsPrincipal.{u_1, u_1} (R := S) (map f (comap f I))
Tactic: rw [← map_comap_of_surjective f hf I]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
p n : R
hp : Irreducible p
⊢ IsCoprime p n ↔ ¬p ∣ n
have rw : IsRelPrime p n ↔ ¬p ∣ n
Tactic: rw [← isRelPrime_iff_isCoprime, hp.isRelPrime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
p n : R
hp : Irreducible p
rw : IsRelPrime p n ↔ ¬p ∣ n
⊢ IsCoprime p n ↔ ¬p ∣ n
have rw₁ : ¬p ∣ n ↔ ¬p ∣ n
Tactic: rw [← isRelPrime_iff_isCoprime, hp.isRelPrime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
x y : R
⊢ Eq (α := Ideal R) (Ideal.span {@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ x y}) (Ideal.span {gcd x y})
have rw : Associated (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ x y) (gcd x y)
Tactic: rw [Ideal.span_singleton_eq_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
x y : R
⊢ Eq (α := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) (Ideal.span {x, y})
have rw : Eq (α := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) (Ideal.span {IsBezout.gcd x y})
Tactic: rw [← IsBezout.span_gcd, IsBezout.span_gcd_eq_span_gcd]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
x y : R
rw : Eq (α := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) (Ideal.span {IsBezout.gcd x y})
⊢ Eq (α := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) (Ideal.span {x, y})
have rw₁ : Eq (α := Ideal R) (Ideal.span {IsBezout.gcd x y}) (Ideal.span {IsBezout.gcd x y})
Tactic: rw [← IsBezout.span_gcd, IsBezout.span_gcd_eq_span_gcd]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
a b z : R
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = a * x + b * y
have simp_rw : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = x * a + b * y
Tactic: simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd,
    Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
a b z : R
simp_rw : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = x * a + b * y
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = a * x + b * y
have simp_rw₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = x * a + y * b
Tactic: simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd,
    Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
a b z : R
simp_rw : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = x * a + b * y
simp_rw₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = x * a + y * b
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = a * x + b * y
have simp_rw₂ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), x * a + y * b = z
Tactic: simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd,
    Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
a b z : R
simp_rw : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = x * a + b * y
simp_rw₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = x * a + y * b
simp_rw₂ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), x * a + y * b = z
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = a * x + b * y
have simp_rw₃ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ Membership.mem (γ := Ideal R) (Ideal.span {a, b}) z
Tactic: simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd,
    Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
a b z : R
simp_rw : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = x * a + b * y
simp_rw₁ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = x * a + y * b
simp_rw₂ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), x * a + y * b = z
simp_rw₃ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ Membership.mem (γ := Ideal R) (Ideal.span {a, b}) z
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = a * x + b * y
have simp_rw₄ : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔
  Membership.mem (γ := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ a b}) z
Tactic: simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd,
    Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
a b : R
⊢ ∃ (x : R) (y : R), @gcd _ CommSemiring.toCommMonoidWithZero _ a b = a * x + b * y
have rw : @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ @gcd _ CommSemiring.toCommMonoidWithZero _ a b
Tactic: rw [← gcd_dvd_iff_exists]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
inst_2 : IsDomain R
inst_3 : GCDMonoid R
x y : R
⊢ IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔ IsCoprime x y
have rw : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔ ∃ (a : R) (b : R), a * x + b * y = 1
Tactic: rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
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
⊢ IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔ IsCoprime x y
have rw₁ : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔ Membership.mem (γ := Ideal R) (Ideal.span {x, y}) 1
Tactic: rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
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
⊢ IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔ IsCoprime x y
have rw₂ : IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔
  Membership.mem (γ := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) 1
Tactic: rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
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
⊢ IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔ IsCoprime x y
have rw₃ : Eq (α := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) ⊤ ↔
  Membership.mem (γ := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) 1
Tactic: rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
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
⊢ IsUnit (@gcd _ CommSemiring.toCommMonoidWithZero _ x y) ↔ IsCoprime x y
have 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
Tactic: rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
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)
⊢ ∃ (d : R), Associated (d ^ k) a
have obtain : ∀ (u : Rˣ) (hu : a * b * (↑u : R) = c ^ k), ∃ (d : R), Associated (d ^ k) a
Tactic: obtain ⟨u, hu⟩ := h.symm
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
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
⊢ ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I
have pos : ∀ (H : c.Nonempty), ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I
Tactic: by_cases H : c.Nonempty
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
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
⊢ ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I
have neg : ∀ (H : ¬c.Nonempty), ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I
Tactic: by_cases H : c.Nonempty
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
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
have pos : ∀ (K : Ideal R) (hKmem : K ∈ c),
  ∃ (I : Ideal R), Membership.mem (γ := Set (Ideal R)) (nonPrincipals R) I ∧ ∀ J ∈ c, J ≤ I
Tactic: obtain ⟨K, hKmem⟩ := Set.nonempty_def.1 H
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
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
have pos : IsPrincipal (sSup c) → ∀ (x : R) (hx : sSup c = R ∙ x), False
Tactic: refine ⟨sSup c, fun ⟨x, hx⟩ ↦ ?_, fun _ ↦ le_sSup⟩
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (hypothesis)
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
⊢ False
have hxmem : x ∈ sSup c
Tactic: have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
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
⊢ False
have pos : ∀ (J : Submodule R R) (hJc : J ∈ c) (hxJ : x ∈ J), False
Tactic: obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (hypothesis)
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
⊢ False
have hsSupJ : sSup c = J
Tactic: have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : GCDMonoid R
n m : R
⊢ Eq (α := Ideal R) (Ideal.span {n} ⊓ Ideal.span {m}) (Ideal.span {@lcm _ CommSemiring.toCommMonoidWithZero _ n m})
have 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
Tactic: rw [Ideal.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomain (goal)
Goal:
R : Type u
inst : EuclideanDomain R
inst_1 : GCDMonoid R
n m x : R
⊢ 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
have simp : n ∣ x ∧ m ∣ x ↔ @lcm _ CommSemiring.toCommMonoidWithZero _ n m ∣ x
Tactic: simp only [Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = R ∙ x
⊢ Submodule.IsPrincipal (Submodule.colon I (↑(span {a}) : Set R)) → Submodule.IsPrincipal I
have this : ∀ (y : R) (hy : Submodule.colon I (↑(span {a}) : Set R) = R ∙ y), Submodule.IsPrincipal I
Tactic: ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
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
have refine_1 : I ≤ R ∙ x * y
Tactic: refine ⟨x * y, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
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
⊢ Submodule.IsPrincipal I
have refine_2 : R ∙ x * y ≤ I
Tactic: refine ⟨x * y, le_antisymm ?_ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
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
⊢ I ≤ R ∙ x * y
have refine_1 : ∀ (hx : I ⊔ span {a} = span {x}) (y : R) (hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}), I ≤ span {x * y}
Tactic: rw [submodule_span_eq] at *
Cleared hypotheses: hx, y, hy
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (goal)
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
⊢ R ∙ x * y ≤ I
have refine_2 : ∀ (hx : I ⊔ span {a} = span {x}) (y : R) (hy : Submodule.colon I (↑(span {a}) : Set R) = span {y}), span {x * y} ≤ I
Tactic: rw [submodule_span_eq] at *
Cleared hypotheses: hx, y, hy
-- Lean 4 proof step from Mathlib.RingTheory.PrincipalIdealDomainOfPrime (hypothesis)
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
⊢ Membership.mem (γ := Submodule R R) (span {x * y}) i
have hisup : i ∈ I ⊔ span {a}
Tactic: have hisup : i ∈ I ⊔ span {a} := mem_sup_left hi