awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ (t_1 : Finset α) (u_1 : Finset α) (b : R) (c_1 : R),
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b * c_1 ∧ p i * d * ∏ i ∈ t, p i = b * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i

Tactic:
exact ⟨insert i t, u, d, c, by rw [insert_union, htus], disjoint_insert_left.2 ⟨hiu, htu⟩, by
          simp [hbc, prod_insert hit, mul_comm, mul_left_comm]⟩
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = b * (p i * d)
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ a = b * d

Tactic:
rw [← mul_assoc, mul_right_comm b, mul_left_inj' hpi.ne_zero] at hbc

Premises used: mul_assoc, mul_right_comm, Prime.ne_zero, mul_left_inj'
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = b * (p i * d)
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hbc₁ : a = b * d
⊢ (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x

Tactic:
rw [← mul_assoc, mul_right_comm b, mul_left_inj' hpi.ne_zero] at hbc

Premises used: mul_assoc, mul_right_comm, Prime.ne_zero, mul_left_inj'
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = b * d
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
rw : insert i (t ∪ u) = insert i s
rw₁ rw₂ : insert i s = insert i s
⊢ t ∪ insert i u = insert i s

Tactic:
rw [union_insert, htus]

Premises used: Finset.union_insert
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = b * d
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ a = b * d ∧ b * ∏ i ∈ t, p i = b * ∏ i ∈ t, p i ∧ p i * d * ∏ i ∈ u, p i = d * ∏ i ∈ insert i u, p i

Tactic:
simp [← hbc, prod_insert hiu, mul_comm, mul_left_comm]

Premises used: Finset.prod_insert, mul_left_comm, mul_comm
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = b * d
hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c : R),
    t_1 ∪ u_1 = insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ p i * d * ∏ i ∈ u, p i = c * ∏ i ∈ u_1, p i

Tactic:
exact ⟨t, insert i u, b, d, by rw [union_insert, htus], disjoint_insert_right.2 ⟨hit, htu⟩, by
          simp [← hbc, prod_insert hiu, mul_comm, mul_left_comm]⟩
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
x y a : R
s : Finset α
p : α → R
hp : ∀ i ∈ s, Prime (p i)
hx : x * y = a * ∏ i ∈ s, p i
empty :
  ∀ {x y a : R} (hp : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Prime (p i)) (hx : x * y = a * ∏ i ∈ ∅, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = ∅ ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
insert :
  ∀ (i : α) (s : Finset α) (his : i ∉ s)
    (ih :
      ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
        ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
          t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i)
    {x y a : R} (hp : ∀ i_1 ∈ Insert.insert i s, Prime (p i_1)) (hx : x * y = a * ∏ i ∈ Insert.insert i s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = Insert.insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
⊢ ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
    t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i

Tactic:
induction s using Finset.induction generalizing x y a with
  | empty => exact ⟨∅, ∅, x, y, by simp [hx]⟩
  | insert i s his ih =>
    rw [prod_insert his, ← mul_assoc] at hx
    have hpi : Prime (p i) := hp i (mem_insert_self _ _)
    rcases ih (fun i hi ↦ hp i (mem_insert_of_mem hi)) hx with
      ⟨t, u, b, c, htus, htu, hbc, rfl, rfl⟩
    have hit : i ∉ t := fun hit ↦ his (htus ▸ mem_union_left _ hit)
    have hiu : i ∉ u := fun hiu ↦ his (htus ▸ mem_union_right _ hiu)
    obtain ⟨d, rfl⟩ | ⟨d, rfl⟩ : p i ∣ b ∨ p i ∣ c := hpi.dvd_or_dvd ⟨a, by rw [← hbc, mul_comm]⟩
    · rw [mul_assoc, mul_comm a, mul_right_inj' hpi.ne_zero] at hbc
      exact ⟨insert i t, u, d, c, by rw [insert_union, htus], disjoint_insert_left.2 ⟨hiu, htu⟩, by
          simp [hbc, prod_insert hit, mul_comm, mul_left_comm]⟩
    · rw [← mul_assoc, mul_right_comm b, mul_left_inj' hpi.ne_zero] at hbc
      exact ⟨t, insert i u, b, d, by rw [union_insert, htus], disjoint_insert_right.2 ⟨hit, htu⟩, by
          simp [← hbc, prod_insert hiu, mul_comm, mul_left_comm]⟩

Premises used: mul_assoc, Insert.insert, mul_comm, rfl
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y a p : R
n : ℕ
hp : Prime p
hx : x * y = a * p ^ n
⊢ x * y = a * ∏ x ∈ range n, p

Tactic:
simpa
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x y a p : R
n : ℕ
hp : Prime p
hx : x * y = a * p ^ n
rcases :
  ∀ (t u : Finset ℕ) (b c : R) (htus : t ∪ u = range n) (htu : Disjoint t u)
    (hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n),
    ∃ (i : ℕ) (j : ℕ) (b_1 : R) (c_1 : R),
      i + j = n ∧ b * c = b_1 * c_1 ∧ b * ∏ i ∈ t, p = b_1 * p ^ i ∧ c * ∏ i ∈ u, p = c_1 * p ^ j
⊢ ∃ (i : ℕ) (j : ℕ) (b : R) (c : R), i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j

Tactic:
rcases mul_eq_mul_prime_prod (fun _ _ ↦ hp)
    (show x * y = a * (range n).prod fun _ ↦ p by simpa) with
      ⟨t, u, b, c, htus, htu, rfl, rfl, rfl⟩

Premises used: rfl, mul_eq_mul_prime_prod
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
rw : #(t ∪ u) = n
rw₁ : #(range n) = n
rw₂ rw₃ : n = n
⊢ #t + #u = n

Tactic:
rw [← card_union_of_disjoint htu, htus, card_range]

Premises used: Finset.card_range, Finset.card_union_of_disjoint
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
⊢ b * c = b * c ∧ b * ∏ i ∈ t, p = b * p ^ #t ∧ c * ∏ i ∈ u, p = c * p ^ #u

Tactic:
simp
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
p : R
n : ℕ
hp : Prime p
t u : Finset ℕ
b c : R
htus : t ∪ u = range n
htu : Disjoint t u
hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n
⊢ ∃ (i : ℕ) (j : ℕ) (b_1 : R) (c_1 : R),
    i + j = n ∧ b * c = b_1 * c_1 ∧ b * ∏ i ∈ t, p = b_1 * p ^ i ∧ c * ∏ i ∈ u, p = c_1 * p ^ j

Tactic:
exact ⟨#t, #u, b, c, by rw [← card_union_of_disjoint htu, htus, card_range], by simp⟩
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
p : α
hp : Prime p
⊢ p ≠ 0

Tactic:
obtain ⟨h1, h2, h3⟩ := hp
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
p : α
hp : Prime p
h1 : p ≠ 0
⊢ ¬IsUnit p

Tactic:
obtain ⟨h1, h2, h3⟩ := hp
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
p : α
hp : Prime p
h1 : p ≠ 0
h2 : ¬IsUnit p
⊢ ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
obtain ⟨h1, h2, h3⟩ := hp
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
rwa rwa₁ rwa₂ rwa₃ : ¬IsUnit p
⊢ ¬IsUnit (-p)

Tactic:
rwa [IsUnit.neg_iff]

Premises used: IsUnit.neg_iff
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ ∀ (a b : α), -p ∣ a * b → -p ∣ a ∨ -p ∣ b

Tactic:
simpa [neg_dvd] using h3

Premises used: neg_dvd
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
p : α
h1 : p ≠ 0
h2 : ¬IsUnit p
h3 : ∀ (a b : α), p ∣ a * b → p ∣ a ∨ p ∣ b
⊢ Prime (-p)

Tactic:
exact ⟨neg_ne_zero.mpr h1, by rwa [IsUnit.neg_iff], by simpa [neg_dvd] using h3⟩
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
p : α
hp : Prime p
inl : ∀ (h : |p| = p), Prime |p|
inr : ∀ (h : |p| = -p), Prime |p|
⊢ Prime |p|

Tactic:
obtain h | h := abs_choice p

Premises used: abs_choice
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
p : α
hp : Prime p
h : |p| = p
inl : Prime p
⊢ Prime |p|

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
inr : Prime (-p)
⊢ Prime |p|

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
p : α
hp : Prime p
h : |p| = p
⊢ Prime p

Tactic:
hp
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
p : α
hp : Prime p
h : |p| = p
⊢ Prime p

Tactic:
exact hp
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime (-p)

Tactic:
hp.neg

Premises used: Prime.neg
-- Module: Mathlib.RingTheory.Prime
Goal:
α : Type u_1
inst : CommRing α
inst_1 : LinearOrder α
p : α
hp : Prime p
h : |p| = -p
⊢ Prime (-p)

Tactic:
exact hp.neg

Premises used: Prime.neg
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := Submodule R M) ⊥ (R ∙ 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsPrincipal.{u, u} (R := R) (M := R) ⊤

Tactic:
⟨⟨1, Ideal.span_singleton_one.symm⟩⟩

Premises used: Ideal.span_singleton_one, Submodule.IsPrincipal.mk, Exists.intro, OfNat.ofNat, Eq.symm
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
⊢ IsBezout R

Tactic:
⟨fun I _ => IsPrincipalIdealRing.principal I⟩

Premises used: IsBezout.mk, IsPrincipalIdealRing.principal
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
K : Type u
inst_3 : DivisionSemiring K
S : Ideal K
inl : IsPrincipal.{u, u} (R := K) (M := K) ⊥
inr : IsPrincipal.{u, u} (R := K) (M := K) ⊤
⊢ IsPrincipal S

Tactic:
rcases Ideal.eq_bot_or_top S with (rfl | rfl)

Premises used: Ideal.eq_bot_or_top, rfl
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
K : Type u
inst_3 : DivisionSemiring K
⊢ IsPrincipal.{u, u} (R := K) (M := K) ⊥

Tactic:
apply bot_isPrincipal

Premises used: bot_isPrincipal
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
K : Type u
inst_3 : DivisionSemiring K
⊢ IsPrincipal.{u, u} (R := K) (M := K) ⊤

Tactic:
apply top_isPrincipal

Premises used: top_isPrincipal
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Semiring R
I : Ideal R
inst_1 : IsPrincipal I
⊢ Ideal.span {generator I} = I

Tactic:
Eq.symm (Classical.choose_spec (principal I))

Premises used: Classical.choose_spec, Eq.symm, Submodule.IsPrincipal.principal
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
⊢ Membership.mem (γ := Submodule R M) (R ∙ generator S) (generator S)

Tactic:
have : generator S ∈ span R {generator S} := subset_span (mem_singleton _)
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
this : Membership.mem (γ := Submodule R M) (R ∙ generator S) (generator S)
⊢ Membership.mem (γ := Submodule R M) (R ∙ generator S) (generator S)

Tactic:
this
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
this : Membership.mem (γ := Submodule R M) (R ∙ generator S) (generator S)
h : S = R ∙ generator S
⊢ generator S ∈ S

Tactic:
convert! this
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
this : Membership.mem (γ := Submodule R M) (R ∙ generator S) (generator S)
⊢ S = R ∙ generator S

Tactic:
span_singleton_generator S |>.symm

Premises used: Submodule.IsPrincipal.span_singleton_generator, Eq.symm
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
this : Membership.mem (γ := Submodule R M) (R ∙ generator S) (generator S)
⊢ S = R ∙ generator S

Tactic:
exact span_singleton_generator S |>.symm

Premises used: Submodule.IsPrincipal.span_singleton_generator, Eq.symm
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
x : M
simp_rw : x ∈ S ↔ ∃ (s : R), s • generator S = x
simp_rw₁ : x ∈ S ↔ Membership.mem (γ := Submodule R M) (R ∙ generator S) x
⊢ x ∈ S ↔ ∃ (s : R), x = s • generator S

Tactic:
simp_rw [@eq_comm _ x, ← mem_span_singleton, span_singleton_generator]

Premises used: Submodule.mem_span_singleton, eq_comm, Submodule.IsPrincipal.span_singleton_generator
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
inst_3 : S.IsPrincipal
rw : S = ⊥ ↔ Eq (α := Submodule R M) (R ∙ generator S) ⊥
rw₁ rw₂ : S = ⊥ ↔ S = ⊥
⊢ S = ⊥ ↔ generator S = 0

Tactic:
rw [← @span_singleton_eq_bot R M, span_singleton_generator]

Premises used: Submodule.span_singleton_eq_bot, Submodule.IsPrincipal.span_singleton_generator
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
⊢ Eq.{v + 1} (α := M) (generator.{u, v} (R := R) ⊥) 0

Tactic:
(eq_bot_iff_generator_eq_zero ⊥).mp rfl

Premises used: Bot.bot, Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero, Iff.mp, rfl
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
S : Submodule R M
h : S.IsPrincipal
⊢ span R (↑{generator S} : Set M) = S

Tactic:
simp only [Finset.coe_singleton, span_singleton_generator]

Premises used: Finset.coe_singleton, Submodule.IsPrincipal.span_singleton_generator
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
r : R
rw : Eq (α := Ideal R) (Ideal.span {generator (Ideal.span {r})}) (Ideal.span {r})
⊢ Associated (generator (Ideal.span {r})) r

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 : CommSemiring R
inst_1 : IsDomain R
r : R
⊢ Eq (α := Ideal R) (Ideal.span {generator (Ideal.span {r})}) (Ideal.span {r})

Tactic:
Ideal.span_singleton_generator _

Premises used: Ideal.span_singleton_generator
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsDomain R
r : R
⊢ Eq (α := Ideal R) (Ideal.span {generator (Ideal.span {r})}) (Ideal.span {r})

Tactic:
exact Ideal.span_singleton_generator _

Premises used: Ideal.span_singleton_generator
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommSemiring R
S : Ideal R
inst_1 : IsPrincipal S
x a : R
⊢ x = a • generator S ↔ x = generator S * a

Tactic:
simp only [mul_comm, smul_eq_mul]

Premises used: mul_comm, smul_eq_mul
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : CommSemiring R
S : Ideal R
inst_1 : IsPrincipal S
is_prime : S.IsPrime
ne_bot : S ≠ ⊥
x x_1 : R
⊢ generator S ∣ x * x_1 → generator S ∣ x ∨ generator S ∣ x_1

Tactic:
simpa only [← mem_iff_generator_dvd S] using is_prime.2

Premises used: Ideal.IsPrime.mem_or_mem', Submodule.IsPrincipal.mem_iff_generator_dvd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst_3 : (map ϕ N).IsPrincipal
x : M
hx : x ∈ N
rw : ∃ y ∈ N, Eq.{u + 1} (α := R) ((ϕ : (a : M) → R) y : R) ((ϕ : (a : M) → R) x : R)
⊢ generator (map ϕ N) ∣ (ϕ : (a : M) → R) x

Tactic:
rw [← mem_iff_generator_dvd, Submodule.mem_map]

Premises used: Submodule.mem_map, Submodule.IsPrincipal.mem_iff_generator_dvd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst_3 : (map ϕ N).IsPrincipal
x : M
hx : x ∈ N
⊢ ∃ y ∈ N, Eq.{u + 1} (α := R) ((ϕ : (a : M) → R) y : R) ((ϕ : (a : M) → R) x : R)

Tactic:
⟨x, hx, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst_3 : (map ϕ N).IsPrincipal
x : M
hx : x ∈ N
⊢ ∃ y ∈ N, Eq.{u + 1} (α := R) ((ϕ : (a : M) → R) y : R) ((ϕ : (a : M) → R) x : R)

Tactic:
exact ⟨x, hx, rfl⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
inst_3 : (ϕ.submoduleImage N).IsPrincipal
x : M
hx : x ∈ N
rw :
  ∃ (y : M) (yN : y ∈ N),
    Eq.{u + 1} (α := R) ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
      ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : R)
⊢ generator (ϕ.submoduleImage N) ∣ (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯)

Tactic:
rw [← mem_iff_generator_dvd, LinearMap.mem_submoduleImage_of_le hNO]

Premises used: LinearMap.mem_submoduleImage_of_le, Submodule.IsPrincipal.mem_iff_generator_dvd
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
inst_3 : (ϕ.submoduleImage N).IsPrincipal
x : M
hx : x ∈ N
⊢ ∃ (y : M) (yN : y ∈ N),
    Eq.{u + 1} (α := R) ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
      ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : R)

Tactic:
⟨x, hx, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : AddCommMonoid M
inst_1 : CommSemiring R
inst_2 : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u, u, v, u} (RingHom.id R) (↥O) R
inst_3 : (ϕ.submoduleImage N).IsPrincipal
x : M
hx : x ∈ N
⊢ ∃ (y : M) (yN : y ∈ N),
    Eq.{u + 1} (α := R) ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
      ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) x ⋯) : R)

Tactic:
exact ⟨x, hx, rfl⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : IsBezout R
x y : R
⊢ Eq (α := Ideal R) (Ideal.span (↑{x, y} : Set R)) (Ideal.span {x, y})

Tactic:
simp
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : IsBezout R
x y : R
⊢ IsPrincipal (R := R) (Ideal.span {x, y})

Tactic:
exact isPrincipal_of_FG (Ideal.span {x, y}) ⟨{x, y}, by simp⟩

Premises used: Insert.insert, IsBezout.isPrincipal_of_FG, Exists.intro, Ideal.span, Singleton.singleton
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
M : Type v
inst : Ring R
inst_1 : IsBezout R
x y : R
⊢ IsPrincipal (R := R) (Ideal.span {x, y})

Tactic:
classical exact isPrincipal_of_FG (Ideal.span {x, y}) ⟨{x, y}, by simp⟩
-- Module: Mathlib.RingTheory.PrincipalIdealDomain
Goal:
R : Type u
inst : Ring R
x y : R
inst_1 : IsPrincipal (R := R) (Ideal.span {x, y})
⊢ Eq (α := Ideal R) (Ideal.span {gcd x y}) (Ideal.span {x, y})

Tactic:
Ideal.span_singleton_generator _

Premises used: IsBezout.gcd, Ideal.span_singleton_generator
-- 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) {x, y} x

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})
⊢ Membership.mem (γ := Set R) {x, y} y

Tactic:
simp