awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
h : Set.Nonempty.{u} (α := R) {x : R | x ∈ S ∧ x ≠ 0}
wf : WellFounded.{u + 1} (α := R) EuclideanDomain.r
hmin :
  wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∈ S ∧
    wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this :
  x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∉ S ∨
    x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h = 0
⊢ x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h = 0

Tactic:
exact this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx

Premises used: Iff.mpr, mod_mem_iff, And.left, Or.neg_resolve_left
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
h : Set.Nonempty.{u} (α := R) {x : R | x ∈ S ∧ x ≠ 0}
wf : WellFounded.{u + 1} (α := R) EuclideanDomain.r
hmin :
  wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∈ S ∧
    wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this : x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∉ {x : R | x ∈ S ∧ x ≠ 0}
⊢ x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h = 0

Tactic:
have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h = 0 := by
                  simp only [not_and_or, Set.mem_setOf_eq, not_ne_iff] at this
                  exact this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
h : Set.Nonempty.{u} (α := R) {x : R | x ∈ S ∧ x ≠ 0}
wf : WellFounded.{u + 1} (α := R) EuclideanDomain.r
hmin :
  wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∈ S ∧
    wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this_1 : x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∉ {x : R | x ∈ S ∧ x ≠ 0}
this : x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h = 0
⊢ wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∣
    x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
h : ¬Set.Nonempty.{u} (α := R) {x : R | x ∈ S ∧ x ≠ 0}
a : R
rw : a ∈ S ↔ a = 0
⊢ a ∈ S ↔ Membership.mem (γ := Submodule R R) (R ∙ 0) a

Tactic:
rw [← @Submodule.bot_coe R R _ _ _, span_eq, Submodule.mem_bot]

Premises used: Submodule.bot_coe, Submodule.mem_bot, Submodule.span_eq
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
h : ¬Set.Nonempty.{u} (α := R) {x : R | x ∈ S ∧ x ≠ 0}
a : R
⊢ a ∈ S ↔ a = 0

Tactic:
⟨fun haS => by_contra fun ha0 => h ⟨a, ⟨haS, ha0⟩⟩,
              fun h₁ => h₁.symm ▸ S.zero_mem⟩

Premises used: Eq.rec, Ideal.zero_mem, And.intro, Iff.intro, Exists.intro, by_contra, Eq.symm
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
h : ¬Set.Nonempty.{u} (α := R) {x : R | x ∈ S ∧ x ≠ 0}
a : R
⊢ a ∈ S ↔ a = 0

Tactic:
exact ⟨fun haS => by_contra fun ha0 => h ⟨a, ⟨haS, ha0⟩⟩,
              fun h₁ => h₁.symm ▸ S.zero_mem⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
⊢ IsPrincipal S

Tactic:
exact
    ⟨if h : { x : R | x ∈ S ∧ x ≠ 0 }.Nonempty then
        have wf : WellFounded (EuclideanDomain.r : R → R → Prop) := EuclideanDomain.r_wellFounded
        have hmin : WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ∈ S ∧
            WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ≠ 0 :=
          WellFounded.min_mem wf { x : R | x ∈ S ∧ x ≠ 0 } h
        ⟨WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h,
          Submodule.ext fun x => ⟨fun hx =>
            div_add_mod x (WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h) ▸
              (Ideal.mem_span_singleton.2 <| dvd_add (dvd_mul_right _ _) <| by
                have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ∉
                    { x : R | x ∈ S ∧ x ≠ 0 } :=
                  fun h₁ => WellFounded.not_lt_min wf _ h₁ (mod_lt x hmin.2)
                have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h = 0 := by
                  simp only [not_and_or, Set.mem_setOf_eq, not_ne_iff] at this
                  exact this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx
                simp [*]),
              fun hx =>
                let ⟨y, hy⟩ := Ideal.mem_span_singleton.1 hx
                hy.symm ▸ S.mul_mem_right _ hmin.1⟩⟩
      else ⟨0, Submodule.ext fun a => by
            rw [← @Submodule.bot_coe R R _ _ _, span_eq, Submodule.mem_bot]
            exact ⟨fun haS => by_contra fun ha0 => h ⟨a, ⟨haS, ha0⟩⟩,
              fun h₁ => h₁.symm ▸ S.zero_mem⟩⟩⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : EuclideanDomain R
S : Ideal R
⊢ IsPrincipal S

Tactic:
classical exact
    ⟨if h : { x : R | x ∈ S ∧ x ≠ 0 }.Nonempty then
        have wf : WellFounded (EuclideanDomain.r : R → R → Prop) := EuclideanDomain.r_wellFounded
        have hmin : WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ∈ S ∧
            WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ≠ 0 :=
          WellFounded.min_mem wf { x : R | x ∈ S ∧ x ≠ 0 } h
        ⟨WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h,
          Submodule.ext fun x => ⟨fun hx =>
            div_add_mod x (WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h) ▸
              (Ideal.mem_span_singleton.2 <| dvd_add (dvd_mul_right _ _) <| by
                have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h ∉
                    { x : R | x ∈ S ∧ x ≠ 0 } :=
                  fun h₁ => WellFounded.not_lt_min wf _ h₁ (mod_lt x hmin.2)
                have : x % WellFounded.min wf { x : R | x ∈ S ∧ x ≠ 0 } h = 0 := by
                  simp only [not_and_or, Set.mem_setOf_eq, not_ne_iff] at this
                  exact this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx
                simp [*]),
              fun hx =>
                let ⟨y, hy⟩ := Ideal.mem_span_singleton.1 hx
                hy.symm ▸ S.mul_mem_right _ hmin.1⟩⟩
      else ⟨0, Submodule.ext fun a => by
            rw [← @Submodule.bot_coe R R _ _ _, span_eq, Submodule.mem_bot]
            exact ⟨fun haS => by_contra fun ha0 => h ⟨a, ⟨haS, ha0⟩⟩,
              fun h₁ => h₁.symm ▸ S.zero_mem⟩⟩⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u_1
inst : Ring R
h : IsField R
⊢ IsPrincipalIdealRing R

Tactic:
@EuclideanDomain.to_principal_ideal_domain R (@Field.toEuclideanDomain R h.toField)

Premises used: EuclideanDomain.to_principal_ideal_domain
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
hI : R ∙ p < I
rcases : ∀ (a : R) (hI : LT.lt (α := Ideal R) (R ∙ p) (R ∙ a)), Eq (α := Ideal R) (R ∙ a) ⊤
⊢ I = ⊤

Tactic:
rcases principal I with ⟨a, rfl⟩

Premises used: IsPrincipalIdealRing.principal, rfl
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : LT.lt (α := Ideal R) (R ∙ p) (R ∙ a)
rw : IsUnit a
⊢ Eq (α := Ideal R) (R ∙ a) ⊤

Tactic:
rw [Ideal.submodule_span_eq, Ideal.span_singleton_eq_top]

Premises used: Ideal.submodule_span_eq, Ideal.span_singleton_eq_top
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : LT.lt (α := Ideal R) (R ∙ p) (R ∙ a)
rcases : ∀ (b : R) (hp : Irreducible (a * b)) (hI : LT.lt (α := Ideal R) (R ∙ a * b) (R ∙ a)), IsUnit a
⊢ IsUnit a

Tactic:
rcases Ideal.span_singleton_le_span_singleton.1 (le_of_lt hI) with ⟨b, rfl⟩

Premises used: Ideal.span_singleton_le_span_singleton, le_of_lt, Iff.mp, rfl
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : LT.lt (α := Ideal R) (R ∙ a * b) (R ∙ a)
⊢ IsUnit a

Tactic:
(of_irreducible_mul hp).resolve_right (mt (fun hb => ?_) (not_le_of_gt hI))

Premises used: mt, of_irreducible_mul, Or.resolve_right, not_le_of_gt
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : LT.lt (α := Ideal R) (R ∙ a * b) (R ∙ a)
refine : ∀ (hb : IsUnit b), LE.le (α := Ideal R) (R ∙ a) (R ∙ a * b)
⊢ IsUnit a

Tactic:
refine (of_irreducible_mul hp).resolve_right (mt (fun hb => ?_) (not_le_of_gt hI))

Premises used: mt, of_irreducible_mul, Or.resolve_right, not_le_of_gt
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : LT.lt (α := Ideal R) (R ∙ a * b) (R ∙ a)
hb : IsUnit b
rw : LE.le (α := Ideal R) (Ideal.span {a}) (R ∙ a * b)
rw₁ : LE.le (α := Ideal R) (Ideal.span {a}) (Ideal.span {a * b})
rw₂ : a * b ∣ a
rw₃ rw₄ : a ∣ a
⊢ LE.le (α := Ideal R) (R ∙ a) (R ∙ a * b)

Tactic:
rw [Ideal.submodule_span_eq, Ideal.submodule_span_eq,
        Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]

Premises used: Ideal.submodule_span_eq, Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
h : a ≠ 0
rw :
  (∀ b ∈ Classical.choose (p := fun (x : Multiset R) ↦ (∀ b ∈ x, Irreducible b) ∧ Associated x.prod a) ⋯,
      Irreducible b) ∧
    Associated (Classical.choose (p := fun (x : Multiset R) ↦ (∀ b ∈ x, Irreducible b) ∧ Associated x.prod a) ⋯).prod a
⊢ (∀ (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

Tactic:
rw [dif_neg h]

Premises used: dif_neg
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ Classical.choose (p := fun (x : Multiset R) ↦ (∀ b ∈ x, Irreducible b) ∧ Associated x.prod a) ⋯,
      Irreducible b) ∧
    Associated (Classical.choose (p := fun (x : Multiset R) ↦ (∀ b ∈ x, Irreducible b) ∧ Associated x.prod a) ⋯).prod a

Tactic:
Classical.choose_spec (WfDvdMonoid.exists_factors a h)

Premises used: Classical.choose_spec, WfDvdMonoid.exists_factors
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ Classical.choose (p := fun (x : Multiset R) ↦ (∀ b ∈ x, Irreducible b) ∧ Associated x.prod a) ⋯,
      Irreducible b) ∧
    Associated (Classical.choose (p := fun (x : Multiset R) ↦ (∀ b ∈ x, Irreducible b) ∧ Associated x.prod a) ⋯).prod a

Tactic:
exact Classical.choose_spec (WfDvdMonoid.exists_factors a h)

Premises used: Classical.choose_spec, WfDvdMonoid.exists_factors
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
a b : R
ha : a ≠ 0
hb : b ∈ factors a
⊢ b ≠ 0

Tactic:
Irreducible.ne_zero ((factors_spec a ha).1 b hb)

Premises used: And.left, PrincipalIdealRing.factors_spec, Irreducible.ne_zero
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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
rcases : ∀ (c : Rˣ) (hc : (factors a).prod * (↑c : R) = a), a ∈ s
⊢ a ∈ s

Tactic:
rcases (factors_spec a ha).2 with ⟨c, hc⟩

Premises used: And.right, PrincipalIdealRing.factors_spec
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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
rw : (factors a).prod * (↑c : R) ∈ s
⊢ a ∈ s

Tactic:
rw [← hc]
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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
⊢ (factors a).prod * (↑c : R) ∈ s

Tactic:
mul_mem (multiset_prod_mem _ hfac) (hunit _)

Premises used: multiset_prod_mem, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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
⊢ (factors a).prod * (↑c : R) ∈ s

Tactic:
exact mul_mem (multiset_prod_mem _ hfac) (hunit _)

Premises used: multiset_prod_mem, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : NonAssocSemiring S
f : R →+* S
s : Submonoid S
a : R
ha : a ≠ 0
h : ∀ b ∈ factors a, Membership.mem (α := S) s ((f : (a : R) → S) b : S)
hf : ∀ (c : Rˣ), Membership.mem (α := S) s ((f : (a : R) → S) (↑c : R) : S)
⊢ Membership.mem (α := S) s ((f : (a : R) → S) a : S)

Tactic:
mem_submonoid_of_factors_subset_of_units_subset (s.comap f.toMonoidHom) ha h hf

Premises used: PrincipalIdealRing.mem_submonoid_of_factors_subset_of_units_subset, Set.Mem, setOf, Submonoid.comap, Set.preimage, RingHom.toMonoidHom
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
⊢ UniqueFactorizationMonoid R

Tactic:
{ (IsNoetherianRing.wfDvdMonoid : WfDvdMonoid R) with
    irreducible_iff_prime := irreducible_iff_prime }

Premises used: IsNoetherianRing.wfDvdMonoid, irreducible_iff_prime, UniqueFactorizationMonoid.mk
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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)
rw₂ rw₃ : Submodule.map f S = Submodule.map f S
⊢ Submodule.map f S = span R (singleton (α := N) ((f : (a : M) → N) (generator S) : N))

Tactic:
rw [← Set.image_singleton, ← map_span, span_singleton_generator]

Premises used: Set.image_singleton, Submodule.IsPrincipal.span_singleton_generator, Submodule.map_span
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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
rw : (Submodule.map f (comap f S)).IsPrincipal
⊢ S.IsPrincipal

Tactic:
rw [← Submodule.map_comap_eq_of_surjective hf S]

Premises used: Submodule.map_comap_eq_of_surjective
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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
⊢ (Submodule.map f (comap f S)).IsPrincipal

Tactic:
hI.map f

Premises used: Submodule.IsPrincipal.map
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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
⊢ (Submodule.map f (comap f S)).IsPrincipal

Tactic:
exact hI.map f

Premises used: Submodule.IsPrincipal.map
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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}))
rw₃ rw₄ : Eq.{u_1 + 1} (α := Submodule S S) (Ideal.map f I) (Ideal.map f I)
⊢ Eq (α := Submodule S S) (Ideal.map f I) (span S (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]

Premises used: Ideal.submodule_span_eq, Set.image_singleton, Ideal.map_span, Ideal.span_singleton_generator
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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)
rw : IsPrincipal.{u_1, u_1} (R := S) (map f (comap f I))
⊢ IsPrincipal I

Tactic:
rw [← map_comap_of_surjective f hf I]

Premises used: Ideal.map_comap_of_surjective
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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.{u_1, u_1} (R := S) (map f (comap f I))

Tactic:
hI.map_ringHom f

Premises used: Submodule.IsPrincipal.map_ringHom
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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.{u_1, u_1} (R := S) (map f (comap f I))

Tactic:
exact hI.map_ringHom f

Premises used: Submodule.IsPrincipal.map_ringHom
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
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
inst_4 : IsPrincipalIdealRing R
f : F
hf : Surjective.{u + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ IsPrincipalIdealRing S

Tactic:
⟨fun I => Ideal.IsPrincipal.of_comap f hf I⟩

Premises used: IsPrincipalIdealRing.mk, Ideal.IsPrincipal.of_comap
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ z ∈ nonunits R, z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsCoprime x y

Tactic:
(isRelPrime_of_no_nonunits_factors nonzero H).isCoprime

Premises used: IsRelPrime.isCoprime, isRelPrime_of_no_nonunits_factors
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
x y : R
h : Irreducible x
⊢ x ∣ y ∨ IsCoprime x y

Tactic:
h.dvd_or_isRelPrime.imp_right IsRelPrime.isCoprime

Premises used: IsRelPrime.isCoprime, Irreducible.dvd_or_isRelPrime, Or.imp_right
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
p n : R
hp : Irreducible p
rw : IsRelPrime p n ↔ ¬p ∣ n
rw₁ rw₂ : ¬p ∣ n ↔ ¬p ∣ n
⊢ IsCoprime p n ↔ ¬p ∣ n

Tactic:
rw [← isRelPrime_iff_isCoprime, hp.isRelPrime_iff_not_dvd]

Premises used: Irreducible.isRelPrime_iff_not_dvd, isRelPrime_iff_isCoprime
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
p n : R
hp : Irreducible p
⊢ p ∣ n ↔ ¬IsCoprime p n

Tactic:
iff_not_comm.2 hp.coprime_iff_not_dvd

Premises used: Iff.mpr, iff_not_comm, Irreducible.coprime_iff_not_dvd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
p a : R
m : ℕ
hp : Irreducible p
h : ¬p ∣ a
⊢ IsCoprime a (p ^ m)

Tactic:
(hp.coprime_iff_not_dvd.2 h).symm.pow_right

Premises used: Iff.mpr, IsCoprime.symm, IsCoprime.pow_right, Irreducible.coprime_iff_not_dvd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsBezout R
p : R
hp : Irreducible p
i : R
⊢ IsCoprime p i ∨ p ∣ i

Tactic:
(_root_.em _).imp_right hp.dvd_iff_not_isCoprime.2

Premises used: Iff.mpr, em, Irreducible.dvd_iff_not_isCoprime, Or.imp_right
-- 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 : Associated (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ x y) (gcd x y)
⊢ Eq (α := Ideal R) (Ideal.span {@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ x y}) (Ideal.span {gcd x y})

Tactic:
rw [Ideal.span_singleton_eq_span_singleton]

Premises used: Ideal.span_singleton_eq_span_singleton
-- 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
⊢ Associated (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ x y) (gcd x y)

Tactic:
associated_of_dvd_dvd
    (IsBezout.dvd_gcd (GCDMonoid.gcd_dvd_left _ _) <| GCDMonoid.gcd_dvd_right _ _)
    (GCDMonoid.dvd_gcd (IsBezout.gcd_dvd_left _ _) <| IsBezout.gcd_dvd_right _ _)

Premises used: associated_of_dvd_dvd, GCDMonoid.dvd_gcd, IsBezout.gcd_dvd_left, IsBezout.dvd_gcd, GCDMonoid.gcd_dvd_left, GCDMonoid.gcd_dvd_right, IsBezout.gcd_dvd_right
-- 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
⊢ Associated (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ x y) (gcd x y)

Tactic:
exact associated_of_dvd_dvd
    (IsBezout.dvd_gcd (GCDMonoid.gcd_dvd_left _ _) <| GCDMonoid.gcd_dvd_right _ _)
    (GCDMonoid.dvd_gcd (IsBezout.gcd_dvd_left _ _) <| IsBezout.gcd_dvd_right _ _)

Premises used: associated_of_dvd_dvd, GCDMonoid.dvd_gcd
-- 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 : Eq (α := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) (Ideal.span {IsBezout.gcd x y})
rw₁ rw₂ : Eq (α := Ideal R) (Ideal.span {IsBezout.gcd x y}) (Ideal.span {IsBezout.gcd x y})
⊢ Eq (α := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ x y}) (Ideal.span {x, y})

Tactic:
rw [← IsBezout.span_gcd, IsBezout.span_gcd_eq_span_gcd]

Premises used: IsBezout.span_gcd_eq_span_gcd, IsBezout.span_gcd
-- 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 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
simp_rw₄ :
  @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔
    Membership.mem (γ := Ideal R) (Ideal.span {@gcd _ CommSemiring.toCommMonoidWithZero _ a b}) z
⊢ @gcd _ CommSemiring.toCommMonoidWithZero _ a b ∣ z ↔ ∃ (x : R) (y : R), z = a * x + b * y

Tactic:
simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd,
    Ideal.mem_span_singleton]

Premises used: span_gcd, eq_comm, mul_comm, Ideal.mem_span_pair, Ideal.mem_span_singleton