awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y z : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
hx : z ∣ x
hy : z ∣ y
rw :
  ∀ (hx : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {z}))
    (hy : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {z})),
    LE.le (α := Ideal R) (Ideal.span {gcd x y}) (Ideal.span {z})
⊢ z ∣ gcd x y

Tactic:
rw [← Ideal.span_singleton_le_span_singleton] at hx hy ⊢

Premises used: Ideal.span_singleton_le_span_singleton
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y z : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
hx : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {z})
hy : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {z})
rw : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {z}) ∧ LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {z})
⊢ LE.le (α := Ideal R) (Ideal.span {gcd x y}) (Ideal.span {z})

Tactic:
rw [span_gcd, Ideal.span_insert, sup_le_iff]

Premises used: sup_le_iff, IsBezout.span_gcd, Ideal.span_insert
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y z : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
hx : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {z})
hy : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {z})
⊢ LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {z}) ∧ LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {z})

Tactic:
⟨hx, hy⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y z : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
hx : LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {z})
hy : LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {z})
⊢ LE.le (α := Ideal R) (Ideal.span {x}) (Ideal.span {z}) ∧ LE.le (α := Ideal R) (Ideal.span {y}) (Ideal.span {z})

Tactic:
exact ⟨hx, hy⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
rw : Membership.mem (γ := Ideal R) (Ideal.span {gcd x y}) (gcd x y)
⊢ Membership.mem (γ := Ideal R) (Ideal.span {x, y}) (gcd x y)

Tactic:
rw [← span_gcd]

Premises used: IsBezout.span_gcd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
a : Membership.mem (γ := Set R) {gcd x y} (gcd x y)
⊢ Membership.mem (γ := Ideal R) (Ideal.span {gcd x y}) (gcd x y)

Tactic:
apply Ideal.subset_span

Premises used: Ideal.subset_span
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
⊢ Membership.mem (γ := Set R) {gcd x y} (gcd x y)

Tactic:
simp
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
h : IsRelPrime x y
rw : IsUnit (gcd x y)
⊢ IsCoprime x y

Tactic:
rw [← Ideal.isCoprime_span_singleton_iff, Ideal.isCoprime_iff_sup_eq, ← Ideal.span_union,
    Set.singleton_union, ← span_gcd, Ideal.span_singleton_eq_top]

Premises used: Set.singleton_union, Ideal.span_singleton_eq_top, Ideal.isCoprime_span_singleton_iff, Ideal.span_union, Ideal.isCoprime_iff_sup_eq, IsBezout.span_gcd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
h : IsRelPrime x y
⊢ IsUnit (gcd x y)

Tactic:
h (gcd_dvd_left x y) (gcd_dvd_right x y)

Premises used: IsBezout.gcd_dvd_left, IsBezout.gcd_dvd_right
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
h : IsRelPrime x y
⊢ IsUnit (gcd x y)

Tactic:
exact h (gcd_dvd_left x y) (gcd_dvd_right x y)

Premises used: IsBezout.gcd_dvd_left, IsBezout.gcd_dvd_right
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
⊢ IsRelPrime x y ↔ IsCoprime x y

Tactic:
⟨IsRelPrime.isCoprime, IsCoprime.isRelPrime⟩

Premises used: IsRelPrime.isCoprime, Iff.intro, IsCoprime.isRelPrime
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : CommRing R
x y z : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
inst_2 : IsBezout R
inst_3 : IsDomain R
⊢ Nonempty.{u + 1} (GCDMonoid R)

Tactic:
⟨toGCDDomain R⟩

Premises used: IsBezout.toGCDDomain, Nonempty.intro
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : CommRing R
x y z : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
inst_2 : IsBezout R
inst_3 : IsDomain R
⊢ Nonempty.{u + 1} (GCDMonoid R)

Tactic:
exact ⟨toGCDDomain R⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : CommRing R
x y z : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
inst_2 : IsBezout R
inst_3 : IsDomain R
⊢ Nonempty.{u + 1} (GCDMonoid R)

Tactic:
classical exact ⟨toGCDDomain R⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
inst_2 : GCDMonoid R
⊢ Associated (gcd x y) (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ x y)

Tactic:
gcd_greatest_associated (gcd_dvd_left _ _) (gcd_dvd_right _ _) (fun _ => dvd_gcd)

Premises used: IsBezout.gcd_dvd_left, IsBezout.dvd_gcd, gcd_greatest_associated, IsBezout.gcd_dvd_right
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
⊢ ∃ (g : α → R), gcd ∅ f = ∑ a ∈ ∅, f a * g a

Tactic:
simp
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
insert :
  ∀ (x y : R) (hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)),
    ∃ (g : α → R), (Insert.insert a s).gcd f = ∑ a ∈ Insert.insert a s, f a * g a
⊢ ∃ (g : α → R), (Insert.insert a s).gcd f = ∑ a ∈ Insert.insert a s, f a * g a

Tactic:
obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)

Premises used: Finset.gcd, IsBezout.gcd_eq_sum
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
insert :
  ∀ (u : Rˣ)
    (hu :
      IsBezout.gcd (f a) (s.gcd f) * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)),
    ∃ (g : α → R), (Insert.insert a s).gcd f = ∑ a ∈ Insert.insert a s, f a * g a
⊢ ∃ (g : α → R), (Insert.insert a s).gcd f = ∑ a ∈ Insert.insert a s, f a * g a

Tactic:
obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)

Premises used: IsBezout.associated_gcd_gcd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : IsBezout.gcd (f a) (s.gcd f) * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
⊢ f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)

Tactic:
rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu

Premises used: add_mul, mul_comm
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
insert :
  ∀ (g : α → R) (hg : s.gcd f = ∑ a ∈ s, f a * g a),
    ∃ (g : α → R), (Insert.insert a s).gcd f = ∑ a ∈ Insert.insert a s, f a * g a
⊢ ∃ (g : α → R), (Insert.insert a s).gcd f = ∑ a ∈ Insert.insert a s, f a * g a

Tactic:
obtain ⟨g, hg⟩ := ih
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ ∃ (g : α → R), (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a

Tactic:
⟨Function.update (g · * (y * u)) a (x * u), ?_⟩

Premises used: Units.val, Function.update, HMul.hMul, Exists.intro
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
insert :
  (Insert.insert a s).gcd f =
    ∑ a_1 ∈ Insert.insert a s,
      HMul.hMul (β := R) (f a_1)
        (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) a_1 : R)
⊢ ∃ (g : α → R), (Insert.insert a s).gcd f = ∑ a ∈ Insert.insert a s, f a * g a

Tactic:
refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
insert :
  f a * x * (↑u : R) + (∑ a ∈ s, f a * g a) * y * (↑u : R) =
    HMul.hMul (β := R) (f a)
        (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) a : R) +
      ∑ x_1 ∈ s,
        HMul.hMul (β := R) (f x_1)
          (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) x_1 : R)
⊢ (Insert.insert a s).gcd f =
    ∑ a_1 ∈ Insert.insert a s,
      HMul.hMul (β := R) (f a_1)
        (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) a_1 : R)

Tactic:
rw [gcd_insert, sum_insert ha, ← hu, hg]

Premises used: Finset.gcd_insert, Finset.sum_insert
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
insert :
  Eq.{u + 1} (α := R) (∑ x ∈ s, f x * (g x * (y * (↑u : R))))
    (∑ x_1 ∈ s,
      HMul.hMul (β := R) (f x_1)
        (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) x_1 : R))
⊢ f a * x * (↑u : R) + (∑ a ∈ s, f a * g a) * y * (↑u : R) =
    HMul.hMul (β := R) (f a)
        (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) a : R) +
      ∑ x_1 ∈ s,
        HMul.hMul (β := R) (f x_1)
          (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) x_1 : R)

Tactic:
simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]

Premises used: mul_assoc, Function.update_self, add_right_inj, Finset.sum_mul
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
b : α
hb : b ∈ s
⊢ b ≠ a

Tactic:
grind
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * (↑u : R) + s.gcd f * y * (↑u : R) = @GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ (f a) (s.gcd f)
g : α → R
hg : s.gcd f = ∑ a ∈ s, f a * g a
⊢ Eq.{u + 1} (α := R) (∑ x ∈ s, f x * (g x * (y * (↑u : R))))
    (∑ x_1 ∈ s,
      HMul.hMul (β := R) (f x_1)
        (update (β := fun (a : α) ↦ R) (fun (x : α) ↦ g x * (y * (↑u : R))) a (x * (↑u : R)) x_1 : R))

Tactic:
exact sum_congr rfl fun b hb ↦ congrArg (f b * ·) <|
      (Function.update_of_ne (show b ≠ a by grind) (x * u) (g · * (y * u))).symm

Premises used: HMul.hMul, congrArg, Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
s : Finset α
f : α → R
empty : ∃ (g : α → R), gcd ∅ f = ∑ a ∈ ∅, f a * g a
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a),
    ∃ (g : α → R), (Insert.insert a s).gcd f = ∑ a ∈ Insert.insert a s, f a * g a
⊢ ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)
    obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)
    rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu
    obtain ⟨g, hg⟩ := ih
    refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
    rw [gcd_insert, sum_insert ha, ← hu, hg]
    simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]
    exact sum_congr rfl fun b hb ↦ congrArg (f b * ·) <|
      (Function.update_of_ne (show b ≠ a by grind) (x * u) (g · * (y * u))).symm

Premises used: add_mul, mul_assoc, Insert.insert, Finset.gcd_insert, Function.update_self, add_right_inj, Finset.sum_mul
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
α : Type u_1
inst : CommRing R
inst_1 : IsBezout R
inst_2 : NormalizedGCDMonoid R
s : Finset α
f : α → R
empty : ∃ (g : α → R), gcd ∅ f = ∑ a ∈ ∅, f a * g a
insert :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s) (ih : ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a),
    ∃ (g : α → R), (Insert.insert a s).gcd f = ∑ a ∈ Insert.insert a s, f a * g a
⊢ ∃ (g : α → R), s.gcd f = ∑ a ∈ s, f a * g a

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    obtain ⟨x, y, hxy⟩ := IsBezout.gcd_eq_sum (f a) (s.gcd f)
    obtain ⟨u, hu⟩ := IsBezout.associated_gcd_gcd R (x := f a) (y := s.gcd f)
    rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu
    obtain ⟨g, hg⟩ := ih
    refine ⟨Function.update (g · * (y * u)) a (x * u), ?_⟩
    rw [gcd_insert, sum_insert ha, ← hu, hg]
    simp only [Function.update_self, add_right_inj, sum_mul, mul_assoc]
    exact sum_congr rfl fun b hb ↦ congrArg (f b * ·) <|
      (Function.update_of_ne (show b ≠ a by grind) (x * u) (g · * (y * u))).symm

Premises used: add_mul, mul_assoc, Insert.insert, Finset.gcd_insert, Function.update_self, add_right_inj, Finset.sum_mul
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
obtain : ∀ (z : R) (hz : generator S = generator T * z), 1 ∈ T
⊢ 1 ∈ T

Tactic:
obtain ⟨z, hz⟩ := (mem_iff_generator_dvd _).1 (hST <| generator_mem S)

Premises used: Submodule.IsPrincipal.generator_mem, Iff.mp, Submodule.IsPrincipal.mem_iff_generator_dvd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
rwa : Ideal.span {generator T} ≤ S
rwa₁ : {generator T} ⊆ (↑S : Set R)
rwa₂ rwa₃ rwa₄ rwa₅ : generator T ∈ (↑S : Set R)
⊢ T ≤ S

Tactic:
rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]

Premises used: Ideal.span_le, Set.singleton_subset_iff, Ideal.span_singleton_generator
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
⊢ T ≤ S

Tactic:
have hTS : T ≤ S := by
          rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
hTS : T ≤ S
⊢ 1 ∈ T

Tactic:
(hxS <| hTS hxT).elim

Premises used: False.elim
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
hTS : T ≤ S
⊢ 1 ∈ T

Tactic:
exact (hxS <| hTS hxT).elim

Premises used: False.elim
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
inr : ∀ (y : R) (hy : z = generator S * y), 1 ∈ T
⊢ 1 ∈ T

Tactic:
obtain ⟨y, hy⟩ := (mem_iff_generator_dvd _).1 h

Premises used: Iff.mp, Submodule.IsPrincipal.mem_iff_generator_dvd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
⊢ generator S ≠ 0

Tactic:
have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
this : generator S ≠ 0
inr : ∀ (h : z ∈ S) (y : R) (hz : 1 = generator T * y) (hy : z = generator S * y) (this : generator S ≠ 0), 1 ∈ T
⊢ 1 ∈ T

Tactic:
rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz

Premises used: mul_left_comm, Submodule.IsPrincipal.generator, mul_right_inj', mul_one
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
h : z ∈ S
y : R
hz : 1 = generator T * y
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T

Tactic:
hz.symm ▸ T.mul_mem_right _ (generator_mem T)

Premises used: Set.Mem, Eq.rec, Ideal.mul_mem_right, Submodule.IsPrincipal.generator_mem, Eq.symm
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
h : z ∈ S
y : R
hz : 1 = generator T * y
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T

Tactic:
exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
⊢ generator T ∈ S ∨ z ∈ S

Tactic:
cases hpi.mem_or_mem (show generator T * z ∈ S from hz ▸ generator_mem S) with
      | inl h =>
        have hTS : T ≤ S := by
          rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
        exact (hxS <| hTS hxT).elim
      | inr h =>
        obtain ⟨y, hy⟩ := (mem_iff_generator_dvd _).1 h
        have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS
        rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz
        exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)

Premises used: Eq.rec, mul_left_comm, Ideal.IsPrime.mem_or_mem, Submodule.IsPrincipal.generator, Submodule.IsPrincipal.generator_mem, mul_one
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : EuclideanDomain R
S : Ideal R
x y : R
hy : y ∈ S
⊢ x % y ∈ S ↔ x ∈ S

Tactic:
⟨fun hxy => div_add_mod x y ▸ S.add_mem (S.mul_mem_right _ hy) hxy, fun hx =>
    (mod_eq_sub_mul_div x y).symm ▸ S.sub_mem hx (S.mul_mem_right _ hy)⟩

Premises used: EuclideanDomain.div_add_mod, Eq.rec, Ideal.add_mem, HDiv.hDiv, EuclideanDomain.mod_eq_sub_mul_div, Ideal.mul_mem_right, Iff.intro, Ideal.sub_mem, 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}
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
⊢ x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h ∉ {x : R | x ∈ S ∧ x ≠ 0}

Tactic:
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)
-- 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 ∉ S ∨
    x % wf.min (r := EuclideanDomain.r) {x : R | x ∈ S ∧ x ≠ 0} h = 0

Tactic:
simp only [not_and_or, Set.mem_setOf_eq, not_ne_iff] at this

Premises used: not_ne_iff, Set.mem_setOf_eq, not_and_or
-- 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:
this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx

Premises used: Iff.mpr, mod_mem_iff, And.left, Or.neg_resolve_left