awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : DecompositionMonoid G₁
inst_4 : DecompositionMonoid G₂
a b c : G₁ × G₂
h : a.1 ∣ (b * c).1 ∧ a.2 ∣ (b * c).2
a₁ a₁' : G₁
h₁ : a₁ ∣ b.1
h₁' : a₁' ∣ c.1
eq₁ : a.1 = a₁ * a₁'
a₂ a₂' : G₂
h₂ : a₂ ∣ b.2
h₂' : a₂' ∣ c.2
eq₂ : a.2 = a₂ * a₂'
⊢ ∃ (a₁ : G₁ × G₂), ∃ (a₂ : G₁ × G₂), (a₁.1 ∣ b.1 ∧ a₁.2 ∣ b.2) ∧ (a₂.1 ∣ c.1 ∧ a₂.2 ∣ c.2) ∧ a = a₁ * a₂

Tactic:
⟨(a₁, a₂), (a₁', a₂'), ⟨h₁, h₂⟩, ⟨h₁', h₂'⟩, Prod.ext eq₁ eq₂⟩

Premises used: Prod.mk, Prod.ext, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : DecompositionMonoid G₁
inst_4 : DecompositionMonoid G₂
a b c : G₁ × G₂
h : a.1 ∣ (b * c).1 ∧ a.2 ∣ (b * c).2
a₁ a₁' : G₁
h₁ : a₁ ∣ b.1
h₁' : a₁' ∣ c.1
eq₁ : a.1 = a₁ * a₁'
a₂ a₂' : G₂
h₂ : a₂ ∣ b.2
h₂' : a₂' ∣ c.2
eq₂ : a.2 = a₂ * a₂'
⊢ ∃ (a₁ : G₁ × G₂), ∃ (a₂ : G₁ × G₂), (a₁.1 ∣ b.1 ∧ a₁.2 ∣ b.2) ∧ (a₂.1 ∣ c.1 ∧ a₂.2 ∣ c.2) ∧ a = a₁ * a₂

Tactic:
exact ⟨(a₁, a₂), (a₁', a₂'), ⟨h₁, h₂⟩, ⟨h₁', h₂'⟩, Prod.ext eq₁ eq₂⟩
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
simp_rw :
  (∃ (c : (i : ι) → G i), ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∃ (f : (x : ι) → G x), ∀ (x_1 : ι), y x_1 = x x_1 * f x_1
⊢ x ∣ y ↔ ∀ (i : ι), x i ∣ y i

Tactic:
simp_rw [dvd_def, funext_iff, Classical.skolem]

Premises used: Classical.skolem, dvd_def, funext_iff
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
ι : Type u_1
G : ι → Type u_4
inst : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ (∃ (c : (i : ι) → G i), ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∃ (f : (x : ι) → G x), ∀ (x_1 : ι), y x_1 = x x_1 * f x_1

Tactic:
rfl
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : ∀ (i : ι), DecompositionMonoid.{u_4} (G i)
a b c : (i : ι) → G i
h : a ∣ b * c
simp_rw :
  ∀ (h : ∀ (i : ι), a i ∣ (b * c) i),
    ∃ (a₁ : (i : ι) → G i), ∃ (a₂ : (i : ι) → G i), (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂
⊢ ∃ (a₁ : (i : ι) → G i), ∃ (a₂ : (i : ι) → G i), a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
simp_rw [pi_dvd_iff] at h ⊢

Premises used: pi_dvd_iff
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : ∀ (i : ι), DecompositionMonoid.{u_4} (G i)
a b c : (i : ι) → G i
h : ∀ (i : ι), a i ∣ (b * c) i
choose :
  ∀ (a₁ a₂ : (i : ι) → G i) (h₁ : ∀ (i : ι), a₁ i ∣ b i) (h₂ : ∀ (i : ι), a₂ i ∣ c i)
    (eq : ∀ (i : ι), a i = a₁ i * a₂ i),
    ∃ (a₁ : (i : ι) → G i), ∃ (a₂ : (i : ι) → G i), (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂
⊢ ∃ (a₁ : (i : ι) → G i), ∃ (a₂ : (i : ι) → G i), (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂

Tactic:
choose a₁ a₂ h₁ h₂ eq using fun i ↦ DecompositionMonoid.primal _ (h i)

Premises used: DecompositionMonoid.primal
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : ∀ (i : ι), DecompositionMonoid.{u_4} (G i)
a b c : (i : ι) → G i
h : ∀ (i : ι), a i ∣ (b * c) i
a₁ a₂ : (i : ι) → G i
h₁ : ∀ (i : ι), a₁ i ∣ b i
h₂ : ∀ (i : ι), a₂ i ∣ c i
eq : ∀ (i : ι), a i = a₁ i * a₂ i
⊢ ∃ (a₁ : (i : ι) → G i), ∃ (a₂ : (i : ι) → G i), (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂

Tactic:
⟨a₁, a₂, h₁, h₂, funext eq⟩

Premises used: funext, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Divisibility.Prod
Goal:
ι : Type u_1
G₁ : Type u_2
G₂ : Type u_3
G : ι → Type u_4
inst : Semigroup G₁
inst_1 : Semigroup G₂
inst_2 : (i : ι) → Semigroup (G i)
inst_3 : ∀ (i : ι), DecompositionMonoid.{u_4} (G i)
a b c : (i : ι) → G i
h : ∀ (i : ι), a i ∣ (b * c) i
a₁ a₂ : (i : ι) → G i
h₁ : ∀ (i : ι), a₁ i ∣ b i
h₂ : ∀ (i : ι), a₂ i ∣ c i
eq : ∀ (i : ι), a i = a₁ i * a₂ i
⊢ ∃ (a₁ : (i : ι) → G i), ∃ (a₂ : (i : ι) → G i), (∀ (i : ι), a₁ i ∣ b i) ∧ (∀ (i : ι), a₂ i ∣ c i) ∧ a = a₁ * a₂

Tactic:
exact ⟨a₁, a₂, h₁, h₂, funext eq⟩
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : Monoid α
a : α
u : αˣ
⊢ a = (↑u : α) * ((↑u⁻¹ : α) * a)

Tactic:
simp
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : Monoid α
a b : α
u : αˣ
h : a ∣ b * (↑u : α)
c : α
eq : b * (↑u : α) = a * c
rw : b = a * c * (↑u⁻¹ : α)
rw₁ : b = b * (↑u : α) * (↑u⁻¹ : α)
rw₂ rw₃ : b = b
⊢ b = a * (c * (↑u⁻¹ : α))

Tactic:
rw [← mul_assoc, ← eq, Units.mul_inv_cancel_right]

Premises used: mul_assoc, Units.mul_inv_cancel_right
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : Monoid α
a b : α
u : αˣ
h : a ∣ b
rw : a * ((↑u : α) * (↑u⁻¹ : α)) = a
rw₁ : a * 1 = a
rw₂ rw₃ : a = a
⊢ a * (↑u : α) * (↑u⁻¹ : α) = a

Tactic:
rw [mul_assoc, u.mul_inv, mul_one]

Premises used: mul_assoc, Units.mul_inv, mul_one
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
u : αˣ
rw : a ∣ b * (↑u : α) ↔ a ∣ b
⊢ a ∣ (↑u : α) * b ↔ a ∣ b

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ b * (↑u : α) ↔ a ∣ b

Tactic:
apply dvd_mul_right

Premises used: Units.dvd_mul_right
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
u : αˣ
rw : a * (↑u : α) ∣ b ↔ a ∣ b
⊢ (↑u : α) * a ∣ b ↔ a ∣ b

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
u : αˣ
⊢ a * (↑u : α) ∣ b ↔ a ∣ b

Tactic:
apply mul_right_dvd

Premises used: Units.mul_right_dvd
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : Monoid α
a u : α
hu : IsUnit u
rcases : ∀ (u : αˣ), (↑u : α) ∣ a
⊢ u ∣ a

Tactic:
rcases hu with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : Monoid α
a : α
u : αˣ
⊢ (↑u : α) ∣ a

Tactic:
apply Units.coe_dvd

Premises used: Units.coe_dvd
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : Monoid α
a b u : α
hu : IsUnit u
rcases : ∀ (u : αˣ), a ∣ b * (↑u : α) ↔ a ∣ b
⊢ a ∣ b * u ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : Monoid α
a b : α
u : αˣ
⊢ a ∣ b * (↑u : α) ↔ a ∣ b

Tactic:
apply Units.dvd_mul_right

Premises used: Units.dvd_mul_right
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : Monoid α
a b u : α
hu : IsUnit u
rcases : ∀ (u : αˣ), a * (↑u : α) ∣ b ↔ a ∣ b
⊢ a * u ∣ b ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : Monoid α
a b : α
u : αˣ
⊢ a * (↑u : α) ∣ b ↔ a ∣ b

Tactic:
apply Units.mul_right_dvd

Premises used: Units.mul_right_dvd
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : Monoid α
u : α
hu : IsUnit u
⊢ IsPrimal u

Tactic:
fun _ _ _ ↦ ⟨u, 1, hu.dvd, one_dvd _, (mul_one u).symm⟩

Premises used: IsPrimal, IsUnit.dvd, one_dvd, And.intro, Exists.intro, mul_one, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
a b u : α
hu : IsUnit u
rcases : ∀ (u : αˣ), a ∣ (↑u : α) * b ↔ a ∣ b
⊢ a ∣ u * b ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ (↑u : α) * b ↔ a ∣ b

Tactic:
apply Units.dvd_mul_left

Premises used: Units.dvd_mul_left
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
a b u : α
hu : IsUnit u
rcases : ∀ (u : αˣ), (↑u : α) * a ∣ b ↔ a ∣ b
⊢ u * a ∣ b ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
u : αˣ
⊢ (↑u : α) * a ∣ b ↔ a ∣ b

Tactic:
apply Units.mul_left_dvd

Premises used: Units.mul_left_dvd
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x : α
h_1 : x ∣ 1
y : α
h : 1 = x * y
rw : y * x = x * y
rw₁ rw₂ : x * y = x * y
⊢ y * x = 1

Tactic:
rw [h, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x : α
⊢ IsUnit x ↔ ∀ (y : α), x ∣ y

Tactic:
isUnit_iff_dvd_one.trans ⟨fun h _ => h.trans (one_dvd _), fun h => h _⟩

Premises used: one_dvd, Iff.intro, Iff.trans, OfNat.ofNat, isUnit_iff_dvd_one, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y : α
xy : x ∣ y
hu : IsUnit y
⊢ IsUnit x

Tactic:
isUnit_iff_dvd_one.2 <| xy.trans <| isUnit_iff_dvd_one.1 hu

Premises used: Iff.mpr, Iff.mp, isUnit_iff_dvd_one, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
a : α
h : a ∣ 1
⊢ IsUnit a

Tactic:
isUnit_iff_dvd_one.mpr h

Premises used: Iff.mpr, isUnit_iff_dvd_one
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
a b : α
ha : ¬IsUnit a
hb : a ∣ b
⊢ ¬IsUnit b

Tactic:
mt (isUnit_of_dvd_unit hb) ha

Premises used: isUnit_of_dvd_unit, mt
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x : α
n : ℕ
inl : x ∣ HPow.hPow (β := ℕ) x 0 ↔ Ne (α := ℕ) 0 0 ∨ IsUnit x
inr : ∀ (hn : n ≠ 0), x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x : α
⊢ x ∣ HPow.hPow (β := ℕ) x 0 ↔ Ne (α := ℕ) 0 0 ∨ IsUnit x

Tactic:
simp [isUnit_iff_dvd_one]

Premises used: isUnit_iff_dvd_one
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x : α
n : ℕ
hn : n ≠ 0
⊢ x ∣ x ^ n ↔ n ≠ 0 ∨ IsUnit x

Tactic:
simp [hn, dvd_pow_self]

Premises used: dvd_pow_self
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y : α
H : IsRelPrime x y
⊢ IsRelPrime y x

Tactic:
fun _ hx hy ↦ H hy hx

Premises used: IsRelPrime
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
⊢ Symmetric.{u_1 + 1} (α := α) IsRelPrime

Tactic:
fun _ _ ↦ .symm

Premises used: Symmetric, IsRelPrime.symm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y : α
⊢ IsRelPrime x y ↔ IsRelPrime y x

Tactic:
⟨IsRelPrime.symm, IsRelPrime.symm⟩

Premises used: IsRelPrime.symm, Iff.intro
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x : α
⊢ IsRelPrime x x ↔ IsUnit x

Tactic:
⟨(· dvd_rfl dvd_rfl), fun hu _ _ dvd ↦ isUnit_of_dvd_unit dvd hu⟩

Premises used: isUnit_of_dvd_unit, Iff.intro, dvd_rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y : α
h : IsUnit x
⊢ IsRelPrime x y

Tactic:
fun _ hx _ ↦ isUnit_of_dvd_unit hx h

Premises used: isUnit_of_dvd_unit, IsRelPrime
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y : α
h : IsUnit y
⊢ IsRelPrime x y

Tactic:
h.isRelPrime_left.symm

Premises used: IsRelPrime.symm, IsUnit.isRelPrime_left
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x : α
⊢ IsRelPrime 1 x

Tactic:
isUnit_one.isRelPrime_left

Premises used: IsUnit.isRelPrime_left, isUnit_one
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x : α
⊢ IsRelPrime x 1

Tactic:
isUnit_one.isRelPrime_right

Premises used: IsUnit.isRelPrime_right, isUnit_one
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime (x * y) z
⊢ IsRelPrime x z

Tactic:
fun _ hx ↦ H (dvd_mul_of_dvd_left hx _)

Premises used: dvd_mul_of_dvd_left, IsRelPrime
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime x (y * z)
rw : ∀ (H : IsRelPrime (y * z) x), IsRelPrime y x
⊢ IsRelPrime x y

Tactic:
rw [isRelPrime_comm] at H ⊢

Premises used: isRelPrime_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime (y * z) x
⊢ IsRelPrime y x

Tactic:
H.of_mul_left_left

Premises used: IsRelPrime.of_mul_left_left
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime (y * z) x
⊢ IsRelPrime y x

Tactic:
exact H.of_mul_left_left

Premises used: IsRelPrime.of_mul_left_left
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
h : IsRelPrime y z
dvd : x ∣ y
obtain : ∀ (d : α) (h : IsRelPrime (x * d) z), IsRelPrime x z
⊢ IsRelPrime x z

Tactic:
obtain ⟨d, rfl⟩ := dvd

Premises used: rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x z d : α
h : IsRelPrime (x * d) z
⊢ IsRelPrime x z

Tactic:
IsRelPrime.of_mul_left_left h

Premises used: IsRelPrime.of_mul_left_left
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x z d : α
h : IsRelPrime (x * d) z
⊢ IsRelPrime x z

Tactic:
exact IsRelPrime.of_mul_left_left h

Premises used: IsRelPrime.of_mul_left_left
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
h : IsRelPrime z y
dvd : x ∣ y
⊢ IsRelPrime z x

Tactic:
(h.symm.of_dvd_left dvd).symm

Premises used: IsRelPrime.symm, IsRelPrime.of_dvd_left
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y : α
H : IsRelPrime x y
d : x ∣ y
⊢ IsUnit x

Tactic:
H dvd_rfl d

Premises used: dvd_rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (x * y) z ↔ IsRelPrime y z

Tactic:
⟨IsRelPrime.of_mul_left_right, fun H _ h ↦ H (hu.dvd_mul_left.mp h)⟩

Premises used: IsUnit.dvd_mul_left, Iff.intro, Iff.mp, IsRelPrime.of_mul_left_right
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime (x * z) y ↔ IsRelPrime y z
rw₁ : IsRelPrime z y ↔ IsRelPrime y z
rw₂ rw₃ : IsRelPrime y z ↔ IsRelPrime y z
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z

Tactic:
rw [isRelPrime_comm, isRelPrime_mul_unit_left_left hu, isRelPrime_comm]

Premises used: isRelPrime_mul_unit_left_left, isRelPrime_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime y (x * z) ↔ IsRelPrime y z
rw₁ rw₂ : IsRelPrime y z ↔ IsRelPrime y z
⊢ IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z

Tactic:
rw [isRelPrime_mul_unit_left_left hu, isRelPrime_mul_unit_left_right hu]

Premises used: isRelPrime_mul_unit_left_left, isRelPrime_mul_unit_left_right
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime (x * y) z ↔ IsRelPrime y z
rw₁ rw₂ : IsRelPrime y z ↔ IsRelPrime y z
⊢ IsRelPrime (y * x) z ↔ IsRelPrime y z

Tactic:
rw [mul_comm, isRelPrime_mul_unit_left_left hu]

Premises used: isRelPrime_mul_unit_left_left, mul_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime y (x * z) ↔ IsRelPrime y z
rw₁ rw₂ : IsRelPrime y z ↔ IsRelPrime y z
⊢ IsRelPrime y (z * x) ↔ IsRelPrime y z

Tactic:
rw [mul_comm, isRelPrime_mul_unit_left_right hu]

Premises used: isRelPrime_mul_unit_left_right, mul_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
hu : IsUnit x
rw : IsRelPrime y (z * x) ↔ IsRelPrime y z
rw₁ rw₂ : IsRelPrime y z ↔ IsRelPrime y z
⊢ IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z

Tactic:
rw [isRelPrime_mul_unit_right_left hu, isRelPrime_mul_unit_right_right hu]

Premises used: isRelPrime_mul_unit_right_left, isRelPrime_mul_unit_right_right
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H1 : IsRelPrime x z
H2 : x ∣ y * z
h : IsPrimal x
obtain :
  ∀ (a b : α) (ha : a ∣ y) (hb : b ∣ z) (H1 : IsRelPrime (a * b) z) (H2 : a * b ∣ y * z) (h : IsPrimal (a * b)),
    a * b ∣ y
⊢ x ∣ y

Tactic:
obtain ⟨a, b, ha, hb, rfl⟩ := h H2

Premises used: rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
y z a b : α
ha : a ∣ y
hb : b ∣ z
H1 : IsRelPrime (a * b) z
H2 : a * b ∣ y * z
h : IsPrimal (a * b)
⊢ a * b ∣ y

Tactic:
(H1.of_mul_left_right.isUnit_of_dvd hb).mul_right_dvd.mpr ha

Premises used: Iff.mpr, IsRelPrime.isUnit_of_dvd, IsUnit.mul_right_dvd, IsRelPrime.of_mul_left_right
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
y z a b : α
ha : a ∣ y
hb : b ∣ z
H1 : IsRelPrime (a * b) z
H2 : a * b ∣ y * z
h : IsPrimal (a * b)
⊢ a * b ∣ y

Tactic:
exact (H1.of_mul_left_right.isUnit_of_dvd hb).mul_right_dvd.mpr ha

Premises used: Iff.mpr, IsRelPrime.isUnit_of_dvd, IsUnit.mul_right_dvd, IsRelPrime.of_mul_left_right
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H1 : IsRelPrime x y
H2 : x ∣ y * z
h : IsPrimal x
⊢ x ∣ z

Tactic:
H1.dvd_of_dvd_mul_right_of_isPrimal (mul_comm y z ▸ H2) h

Premises used: Eq.rec, IsRelPrime.dvd_of_dvd_mul_right_of_isPrimal, mul_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hy : IsPrimal y
obtain : ∀ (w : α) (H2 : y ∣ x * w), x * y ∣ x * w
⊢ x * y ∣ z

Tactic:
obtain ⟨w, rfl⟩ := H1

Premises used: rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y : α
H : IsRelPrime x y
hy : IsPrimal y
w : α
H2 : y ∣ x * w
⊢ x * y ∣ x * w

Tactic:
mul_dvd_mul_left x (H.symm.dvd_of_dvd_mul_left_of_isPrimal H2 hy)

Premises used: mul_dvd_mul_left, IsRelPrime.symm, IsRelPrime.dvd_of_dvd_mul_left_of_isPrimal
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y : α
H : IsRelPrime x y
hy : IsPrimal y
w : α
H2 : y ∣ x * w
⊢ x * y ∣ x * w

Tactic:
exact mul_dvd_mul_left x (H.symm.dvd_of_dvd_mul_left_of_isPrimal H2 hy)

Premises used: mul_dvd_mul_left, IsRelPrime.symm, IsRelPrime.dvd_of_dvd_mul_left_of_isPrimal
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
rw : y * x ∣ z
⊢ x * y ∣ z

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ y * x ∣ z

Tactic:
H.symm.mul_dvd_of_right_isPrimal H2 H1 hx

Premises used: IsRelPrime.mul_dvd_of_right_isPrimal, IsRelPrime.symm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ y * x ∣ z

Tactic:
exact H.symm.mul_dvd_of_right_isPrimal H2 H1 hx

Premises used: IsRelPrime.mul_dvd_of_right_isPrimal, IsRelPrime.symm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : x ∣ y * z
⊢ x ∣ y

Tactic:
H1.dvd_of_dvd_mul_right_of_isPrimal H2 (DecompositionMonoid.primal x)

Premises used: DecompositionMonoid.primal, IsRelPrime.dvd_of_dvd_mul_right_of_isPrimal
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H1 : IsRelPrime x y
H2 : x ∣ y * z
⊢ x ∣ z

Tactic:
H1.dvd_of_dvd_mul_right (mul_comm y z ▸ H2)

Premises used: IsRelPrime.dvd_of_dvd_mul_right, Eq.rec, mul_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
x_1 : α
h : x_1 ∣ x * y
hz : x_1 ∣ z
obtain : ∀ (a b : α) (ha : a ∣ x) (hb : b ∣ y) (h : a * b ∣ x * y) (hz : a * b ∣ z), IsUnit (a * b)
⊢ IsUnit x_1

Tactic:
obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul h

Premises used: exists_dvd_and_dvd_of_dvd_mul, rfl
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
a b : α
ha : a ∣ x
hb : b ∣ y
h : a * b ∣ x * y
hz : a * b ∣ z
⊢ IsUnit (a * b)

Tactic:
(H1 ha <| (dvd_mul_right a b).trans hz).mul (H2 hb <| (dvd_mul_left b a).trans hz)

Premises used: IsUnit.mul, dvd_mul_left, dvd_mul_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
a b : α
ha : a ∣ x
hb : b ∣ y
h : a * b ∣ x * y
hz : a * b ∣ z
⊢ IsUnit (a * b)

Tactic:
exact (H1 ha <| (dvd_mul_right a b).trans hz).mul (H2 hb <| (dvd_mul_left b a).trans hz)

Premises used: IsUnit.mul, dvd_mul_left, dvd_mul_right, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H1 : IsRelPrime x y
H2 : IsRelPrime x z
rw : ∀ (H1 : IsRelPrime y x) (H2 : IsRelPrime z x), IsRelPrime (y * z) x
⊢ IsRelPrime x (y * z)

Tactic:
rw [isRelPrime_comm] at H1 H2 ⊢

Premises used: isRelPrime_comm
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H1 : IsRelPrime y x
H2 : IsRelPrime z x
⊢ IsRelPrime (y * z) x

Tactic:
H1.mul_left H2

Premises used: IsRelPrime.mul_left
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H1 : IsRelPrime y x
H2 : IsRelPrime z x
⊢ IsRelPrime (y * z) x

Tactic:
exact H1.mul_left H2

Premises used: IsRelPrime.mul_left
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
⊢ IsRelPrime (x * y) z ↔ IsRelPrime x z ∧ IsRelPrime y z

Tactic:
⟨fun H ↦ ⟨H.of_mul_left_left, H.of_mul_left_right⟩, fun ⟨H1, H2⟩ ↦ H1.mul_left H2⟩

Premises used: HMul.hMul, IsRelPrime, IsRelPrime.mul_left, IsRelPrime.of_mul_left_left, And.intro, Iff.intro, _private.0.IsRelPrime.mul_left_iff.match_1, IsRelPrime.of_mul_left_right
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
⊢ IsRelPrime x (y * z) ↔ IsRelPrime x y ∧ IsRelPrime x z

Tactic:
⟨fun H ↦ ⟨H.of_mul_right_left, H.of_mul_right_right⟩, fun ⟨H1, H2⟩ ↦ H1.mul_right H2⟩

Premises used: HMul.hMul, IsRelPrime.of_mul_right_right, IsRelPrime, IsRelPrime.of_mul_right_left, And.intro, Iff.intro, _private.0.IsRelPrime.mul_right_iff.match_1, IsRelPrime.mul_right
-- Module: Mathlib.Algebra.Divisibility.Units
Goal:
α : Type u_1
inst : CommMonoid α
x y z : α
inst_1 : DecompositionMonoid α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
⊢ x * y ∣ z

Tactic:
H.mul_dvd_of_left_isPrimal H1 H2 (DecompositionMonoid.primal x)

Premises used: DecompositionMonoid.primal, IsRelPrime.mul_dvd_of_left_isPrimal
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
⊢ Eq.{u_1 + 1} (α := R) (fst ε) 0

Tactic:
rfl

Premises used: TrivSqZeroExt.fst, rfl
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : Zero R
inst_1 : One R
⊢ Eq.{u_1 + 1} (α := R) (snd ε) 1

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, rfl
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : Semiring R
x y : R[ε]
⊢ snd (x * y) = fst x * snd y + snd x * fst y

Tactic:
rfl

Premises used: TrivSqZeroExt.snd, TrivSqZeroExt.fst, MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : Semiring R
⊢ HMul.hMul (α := R[ε]) ε ε = 0

Tactic:
inr_mul_inr _ _ _

Premises used: TrivSqZeroExt.inr_mul_inr
-- Module: Mathlib.Algebra.DualNumber
Goal:
R : Type u_1
inst : Semiring R
⊢ HPow.hPow (α := R[ε]) (β := ℕ) ε 2 = 0

Tactic:
simp [pow_two]

Premises used: pow_two