awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1

Tactic:
exact Int.cast_one

Premises used: Int.cast_one
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : Nontrivial R
h : IsCoprime.{u} (R := R) (0 0) (0 1)
⊢ False

Tactic:
not_isCoprime_zero_zero h

Premises used: not_isCoprime_zero_zero
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : Nontrivial R
h : IsCoprime.{u} (R := R) (0 0) (0 1)
⊢ False

Tactic:
exact not_isCoprime_zero_zero h

Premises used: not_isCoprime_zero_zero
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y : R
inst_1 : Nontrivial R
h : IsCoprime x y
a : x = 0 → y ≠ 0
⊢ x ≠ 0 ∨ y ≠ 0

Tactic:
apply not_or_of_imp

Premises used: not_or_of_imp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : Nontrivial R
h : IsCoprime.{u} (R := R) 0 0
⊢ False

Tactic:
not_isCoprime_zero_zero h

Premises used: not_isCoprime_zero_zero
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : Nontrivial R
h : IsCoprime.{u} (R := R) 0 0
⊢ False

Tactic:
exact not_isCoprime_zero_zero h

Premises used: not_isCoprime_zero_zero
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : R
rw : 1 + 0 * x = 1
rw₁ : HAdd.hAdd (α := R) 1 0 = 1
rw₂ rw₃ : Eq.{u + 1} (α := R) 1 1
⊢ HMul.hMul (α := R) 1 1 + 0 * x = 1

Tactic:
rw [one_mul, zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, add_zero, one_mul
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : R
rw : 0 * x + 1 = 1
rw₁ : HAdd.hAdd (α := R) 0 1 = 1
rw₂ rw₃ : Eq.{u + 1} (α := R) 1 1
⊢ 0 * x + HMul.hMul (α := R) 1 1 = 1

Tactic:
rw [one_mul, zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, zero_add, one_mul
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
let : ∀ (a b : R) (H : a * x + b * z = 1), x ∣ y
⊢ x ∣ y

Tactic:
let ⟨a, b, H⟩ := H1
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
rw : x ∣ y * a * x + b * (y * z)
⊢ x ∣ y

Tactic:
rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]

Premises used: mul_assoc, mul_left_comm, mul_add, mul_one
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y * a * x + b * (y * z)

Tactic:
dvd_add (dvd_mul_left _ _) (H2.mul_left _)

Premises used: Dvd.dvd.mul_left, dvd_mul_left, dvd_add
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
a b : R
H : a * x + b * z = 1
⊢ x ∣ y * a * x + b * (y * z)

Tactic:
exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)

Premises used: Dvd.dvd.mul_left, dvd_mul_left, dvd_add
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
let : ∀ (a b : R) (H : a * x + b * y = 1), x ∣ z
⊢ x ∣ z

Tactic:
let ⟨a, b, H⟩ := H1
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
rw : x ∣ a * z * x + b * (y * z)
⊢ x ∣ z

Tactic:
rw [← one_mul z, ← H, add_mul, mul_right_comm, mul_assoc b]

Premises used: add_mul, mul_assoc, mul_right_comm, one_mul
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ a * z * x + b * (y * z)

Tactic:
dvd_add (dvd_mul_left _ _) (H2.mul_left _)

Premises used: Dvd.dvd.mul_left, dvd_mul_left, dvd_add
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
a b : R
H : a * x + b * y = 1
⊢ x ∣ a * z * x + b * (y * z)

Tactic:
exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)

Premises used: Dvd.dvd.mul_left, dvd_mul_left, dvd_add
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ a * c * (x * y) + (a * x * d + b * c * y + b * d * z) * z = (a * x + b * z) * (c * y + d * z)

Tactic:
ring
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
rw : 1 * (c * y + d * z) = 1
rw₁ : HMul.hMul (α := R) 1 1 = 1
rw₂ rw₃ : Eq.{u + 1} (α := R) 1 1
⊢ (a * x + b * z) * (c * y + d * z) = 1

Tactic:
rw [h1, h2, mul_one]

Premises used: mul_one
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : IsCoprime x z
rw : ∀ (H1 : IsCoprime y x) (H2 : IsCoprime z x), IsCoprime (y * z) x
⊢ IsCoprime x (y * z)

Tactic:
rw [isCoprime_comm] at H1 H2 ⊢

Premises used: isCoprime_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime y x
H2 : IsCoprime z x
⊢ IsCoprime (y * z) x

Tactic:
H1.mul_left H2

Premises used: IsCoprime.mul_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : IsCoprime y x
H2 : IsCoprime z x
⊢ IsCoprime (y * z) x

Tactic:
exact H1.mul_left H2

Premises used: IsCoprime.mul_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime x y
H1 : x ∣ z
H2 : y ∣ z
obtain : ∀ (a b : R) (h : a * x + b * y = 1), x * y ∣ z
⊢ x * y ∣ z

Tactic:
obtain ⟨a, b, h⟩ := H
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
rw : x * y ∣ z * (a * x) + z * (b * y)
⊢ x * y ∣ z

Tactic:
rw [← mul_one z, ← h, mul_add]

Premises used: mul_add, mul_one
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
h₁ : x * y ∣ z * (a * x)
h₂ : x * y ∣ z * (b * y)
⊢ x * y ∣ z * (a * x) + z * (b * y)

Tactic:
apply dvd_add

Premises used: dvd_add
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
h₁ : x * y ∣ a * (x * z)
⊢ x * y ∣ z * (a * x)

Tactic:
rw [mul_comm z, mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ a * (x * z)

Tactic:
(mul_dvd_mul_left _ H2).mul_left _

Premises used: Dvd.dvd.mul_left, mul_dvd_mul_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ a * (x * z)

Tactic:
exact (mul_dvd_mul_left _ H2).mul_left _

Premises used: Dvd.dvd.mul_left, mul_dvd_mul_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
h₂ : x * y ∣ z * y * b
⊢ x * y ∣ z * (b * y)

Tactic:
rw [mul_comm b, ← mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * y * b

Tactic:
(mul_dvd_mul_right H1 _).mul_right _

Premises used: Dvd.dvd.mul_right, mul_dvd_mul_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * y * b

Tactic:
exact (mul_dvd_mul_right H1 _).mul_right _

Premises used: Dvd.dvd.mul_right, mul_dvd_mul_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime (x * y) z
a b : R
h : a * (x * y) + b * z = 1
rwa : a * x * y + b * z = 1
rwa₁ rwa₂ rwa₃ rwa₄ : a * (x * y) + b * z = 1
⊢ a * y * x + b * z = 1

Tactic:
rwa [mul_right_comm, mul_assoc]

Premises used: mul_assoc, mul_right_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime (x * y) z
⊢ IsCoprime (y * x) z

Tactic:
rw [mul_comm] at H

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime (y * x) z
⊢ IsCoprime y z

Tactic:
H.of_mul_left_left

Premises used: IsCoprime.of_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime (y * x) z
⊢ IsCoprime y z

Tactic:
exact H.of_mul_left_left

Premises used: IsCoprime.of_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime x (y * z)
rw : ∀ (H : IsCoprime (y * z) x), IsCoprime y x
⊢ IsCoprime x y

Tactic:
rw [isCoprime_comm] at H ⊢

Premises used: isCoprime_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime (y * z) x
⊢ IsCoprime y x

Tactic:
H.of_mul_left_left

Premises used: IsCoprime.of_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime (y * z) x
⊢ IsCoprime y x

Tactic:
exact H.of_mul_left_left

Premises used: IsCoprime.of_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime x (y * z)
⊢ IsCoprime x (z * y)

Tactic:
rw [mul_comm] at H

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime x (z * y)
⊢ IsCoprime x z

Tactic:
H.of_mul_right_left

Premises used: IsCoprime.of_mul_right_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
H : IsCoprime x (z * y)
⊢ IsCoprime x z

Tactic:
exact H.of_mul_right_left

Premises used: IsCoprime.of_mul_right_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
⊢ IsCoprime (x * y) z ↔ IsCoprime x z ∧ IsCoprime y z

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

Premises used: IsCoprime.mul_left, HMul.hMul, And.intro, Iff.intro, _private.0.IsCoprime.mul_left_iff.match_1, IsCoprime.of_mul_left_right, IsCoprime, IsCoprime.of_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
rw : IsCoprime (y * z) x ↔ IsCoprime x y ∧ IsCoprime x z
rw₁ : IsCoprime y x ∧ IsCoprime z x ↔ IsCoprime x y ∧ IsCoprime x z
rw₂ : IsCoprime x y ∧ IsCoprime z x ↔ IsCoprime x y ∧ IsCoprime x z
rw₃ rw₄ : IsCoprime x y ∧ IsCoprime x z ↔ IsCoprime x y ∧ IsCoprime x z
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z

Tactic:
rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]

Premises used: isCoprime_comm, IsCoprime.mul_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime y z
hdvd : x ∣ y
obtain : ∀ (d : R) (h : IsCoprime (x * d) z), IsCoprime x z
⊢ IsCoprime x z

Tactic:
obtain ⟨d, rfl⟩ := hdvd

Premises used: rfl
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x z d : R
h : IsCoprime (x * d) z
⊢ IsCoprime x z

Tactic:
IsCoprime.of_mul_left_left h

Premises used: IsCoprime.of_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x z d : R
h : IsCoprime (x * d) z
⊢ IsCoprime x z

Tactic:
exact IsCoprime.of_mul_left_left h

Premises used: IsCoprime.of_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime z y
hdvd : x ∣ y
⊢ IsCoprime z x

Tactic:
(h.symm.of_isCoprime_of_dvd_left hdvd).symm

Premises used: IsCoprime.symm, IsCoprime.of_isCoprime_of_dvd_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z w : R
h₁ : x ∣ y
h₂ : z ∣ w
h : IsCoprime y w
⊢ IsCoprime x z

Tactic:
h.of_isCoprime_of_dvd_left h₁ |>.of_isCoprime_of_dvd_right h₂

Premises used: IsCoprime.of_isCoprime_of_dvd_left, IsCoprime.of_isCoprime_of_dvd_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y : R
H : IsCoprime x y
d : x ∣ y
⊢ IsUnit x

Tactic:
let ⟨k, hk⟩ := d
  isCoprime_self.1 <| IsCoprime.of_mul_right_left <| show IsCoprime x (x * k) from hk ▸ H

Premises used: _private.0.IsCoprime.isUnit_of_dvd.match_1, IsUnit, Eq.rec, IsCoprime.of_mul_right_left, isCoprime_self, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y : R
h₁ : IsCoprime x y
h₂ : Associated x y
⊢ IsUnit x ∧ IsUnit y

Tactic:
⟨h₁.isUnit_of_dvd (h₂.dvd), h₁.symm.isUnit_of_dvd (h₂.dvd')⟩

Premises used: Associated.dvd, IsCoprime.symm, IsCoprime.isUnit_of_dvd, And.intro, Associated.dvd'
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
a b x : R
h : IsCoprime a b
ha : x ∣ a
hb : x ∣ b
⊢ IsUnit x

Tactic:
(h.of_isCoprime_of_dvd_left ha).isUnit_of_dvd hb

Premises used: IsCoprime.isUnit_of_dvd, IsCoprime.of_isCoprime_of_dvd_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
a b : R
h : IsCoprime a b
⊢ IsRelPrime a b

Tactic:
fun _ ↦ h.isUnit_of_dvd'

Premises used: IsCoprime.isUnit_of_dvd', IsRelPrime
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y : R
H : IsCoprime x y
S : Type v
inst_1 : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
rw :
  HAdd.hAdd (α := S) ((f : (a : R) → S) (a * x) : S)
      (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S)) =
    1
rw₁ : HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) (a * x) : S) ((f : (a : R) → S) (b * y) : S) = 1
rw₂ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (a * x + b * y) : S) (1 : S)
rw₃ : Eq.{v + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)
rw₄ rw₅ : Eq.{v + 1} (α := S) 1 1
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) x : S) +
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) b : S) ((f : (a : R) → S) y : S) =
    1

Tactic:
rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]

Premises used: RingHom.map_one, RingHom.map_mul, RingHom.map_add
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
a b : R
H : a * (x + y * z) + b * y = 1
⊢ a * x + (a * z + b) * y = 1

Tactic:
simpa only [add_mul, mul_add, add_assoc, add_comm, add_left_comm, mul_assoc, mul_comm,
      mul_left_comm] using H

Premises used: add_mul, add_left_comm, add_assoc, mul_assoc, mul_left_comm, add_comm, mul_comm, mul_add
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime (x + y * z) y

Tactic:
rw [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y

Tactic:
h.of_add_mul_left_left

Premises used: IsCoprime.of_add_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_left_left

Premises used: IsCoprime.of_add_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
rw : ∀ (h : IsCoprime (y + x * z) x), IsCoprime y x
⊢ IsCoprime x y

Tactic:
rw [isCoprime_comm] at h ⊢

Premises used: isCoprime_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (y + x * z) x
⊢ IsCoprime y x

Tactic:
h.of_add_mul_left_left

Premises used: IsCoprime.of_add_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (y + x * z) x
⊢ IsCoprime y x

Tactic:
exact h.of_add_mul_left_left

Premises used: IsCoprime.of_add_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x (y + x * z)

Tactic:
rw [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y

Tactic:
h.of_add_mul_left_right

Premises used: IsCoprime.of_add_mul_left_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_left_right

Premises used: IsCoprime.of_add_mul_left_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (y * z + x) y
⊢ IsCoprime (x + y * z) y

Tactic:
rw [add_comm] at h

Premises used: add_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (z * y + x) y
⊢ IsCoprime (x + z * y) y

Tactic:
rw [add_comm] at h

Premises used: add_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y

Tactic:
h.of_add_mul_right_left

Premises used: IsCoprime.of_add_mul_right_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_right_left

Premises used: IsCoprime.of_add_mul_right_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (x * z + y)
⊢ IsCoprime x (y + x * z)

Tactic:
rw [add_comm] at h

Premises used: add_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (z * x + y)
⊢ IsCoprime x (y + z * x)

Tactic:
rw [add_comm] at h

Premises used: add_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y

Tactic:
h.of_add_mul_right_right

Premises used: IsCoprime.of_add_mul_right_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_right_right

Premises used: IsCoprime.of_add_mul_right_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsRelPrime (x + y * z) y
⊢ IsRelPrime x y

Tactic:
fun _ hx hy ↦ h (dvd_add hx <| dvd_mul_of_dvd_left hy z) hy

Premises used: dvd_mul_of_dvd_left, IsRelPrime, dvd_add
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsRelPrime x (y + x * z)
rw : ∀ (h : IsRelPrime (y + x * z) x), IsRelPrime y x
⊢ IsRelPrime x y

Tactic:
rw [isRelPrime_comm] at h ⊢

Premises used: isRelPrime_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsRelPrime (y + x * z) x
⊢ IsRelPrime y x

Tactic:
h.of_add_mul_left_left

Premises used: IsRelPrime.of_add_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y z : R
h : IsRelPrime (y + x * z) x
⊢ IsRelPrime y x

Tactic:
exact h.of_add_mul_left_left

Premises used: IsRelPrime.of_add_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
G : Type u_2
inst : CommSemiring R
inst_1 : Group G
inst_2 : MulAction G R
inst_3 : SMulCommClass G R R
inst_4 : IsScalarTower G R R
x : G
y z : R
h_1 : IsCoprime (x • y) z
a b : R
h : a * x • y + b * z = 1
rwa : x • (a * y) + b * z = 1
rwa₁ rwa₂ rwa₃ rwa₄ : a * x • y + b * z = 1
⊢ x • a * y + b * z = 1

Tactic:
rwa [smul_mul_assoc, ← mul_smul_comm]

Premises used: smul_mul_assoc, mul_smul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
G : Type u_2
inst : CommSemiring R
inst_1 : Group G
inst_2 : MulAction G R
inst_3 : SMulCommClass G R R
inst_4 : IsScalarTower G R R
x : G
y z : R
h_1 : IsCoprime y z
a b : R
h : a * y + b * z = 1
rwa : (x⁻¹ * x) • (a * y) + b * z = 1
rwa₁ : HSMul.hSMul.{u_2, u_1, u_1} (α := G) 1 (a * y) + b * z = 1
rwa₂ rwa₃ rwa₄ rwa₅ : a * y + b * z = 1
⊢ x⁻¹ • a * x • y + b * z = 1

Tactic:
rwa [smul_mul_smul_comm, inv_mul_cancel, one_smul]

Premises used: inv_mul_cancel, smul_mul_smul_comm, one_smul
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
G : Type u_2
inst : CommSemiring R
inst_1 : Group G
inst_2 : MulAction G R
inst_3 : SMulCommClass G R R
inst_4 : IsScalarTower G R R
x : G
y z : R
⊢ IsCoprime y (x • z) ↔ IsCoprime y z

Tactic:
isCoprime_comm.trans <| (isCoprime_group_smul_left x z y).trans isCoprime_comm

Premises used: isCoprime_comm, isCoprime_group_smul_left, Iff.trans
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
G : Type u_2
inst : CommSemiring R
inst_1 : Group G
inst_2 : MulAction G R
inst_3 : SMulCommClass G R R
inst_4 : IsScalarTower G R R
x : G
y z : R
⊢ IsCoprime (x • y) (x • z) ↔ IsCoprime y z

Tactic:
(isCoprime_group_smul_left x y (x • z)).trans (isCoprime_group_smul_right x y z)

Premises used: isCoprime_group_smul_right, isCoprime_group_smul_left, Iff.trans, HSMul.hSMul
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
hu : IsUnit x
y z : R
⊢ IsCoprime (x * y) z ↔ IsCoprime y z

Tactic:
let ⟨u, hu⟩ := hu
  hu ▸ isCoprime_group_smul_left u y z

Premises used: HMul.hMul, Eq.rec, isCoprime_group_smul_left, _private.0.isCoprime_mul_unit_left_left.match_1, Iff, IsCoprime
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
hu : IsUnit x
y z : R
⊢ IsCoprime y (x * z) ↔ IsCoprime y z

Tactic:
let ⟨u, hu⟩ := hu
  hu ▸ isCoprime_group_smul_right u y z

Premises used: HMul.hMul, isCoprime_group_smul_right, Eq.rec, _private.0.isCoprime_mul_unit_left_left.match_1, Iff, IsCoprime
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
hu : IsUnit x
y z : R
⊢ IsCoprime (y * x) z ↔ IsCoprime y z

Tactic:
mul_comm x y ▸ isCoprime_mul_unit_left_left hu y z

Premises used: isCoprime_mul_unit_left_left, Eq.rec, mul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
hu : IsUnit x
y z : R
⊢ IsCoprime y (z * x) ↔ IsCoprime y z

Tactic:
mul_comm x z ▸ isCoprime_mul_unit_left_right hu y z

Premises used: Eq.rec, isCoprime_mul_unit_left_right, mul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
hu : IsUnit u
hv : IsUnit v
y z : R
⊢ IsCoprime (u * y) (v * z) ↔ IsCoprime y z

Tactic:
Iff.trans
    (isCoprime_mul_unit_left_left hu _ _)
    (isCoprime_mul_unit_left_right hv _ _)

Premises used: isCoprime_mul_unit_left_left, isCoprime_mul_unit_left_right, Iff.trans
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
u v : R
hu : IsUnit u
hv : IsUnit v
y z : R
⊢ IsCoprime (y * u) (z * v) ↔ IsCoprime y z

Tactic:
Iff.trans
    (isCoprime_mul_unit_right_left hu _ _)
    (isCoprime_mul_unit_right_right hv _ _)

Premises used: isCoprime_mul_unit_right_right, isCoprime_mul_unit_right_left, Iff.trans
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
hu : IsUnit x
y z : R
⊢ IsCoprime (x * y) (x * z) ↔ IsCoprime y z

Tactic:
isCoprime_mul_units_left hu hu _ _

Premises used: isCoprime_mul_units_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
x : R
hu : IsUnit x
y z : R
⊢ IsCoprime (y * x) (z * x) ↔ IsCoprime y z

Tactic:
isCoprime_mul_units_right hu hu _ _

Premises used: isCoprime_mul_units_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z + y * -z) y

Tactic:
simpa only [mul_neg, add_neg_cancel_right] using h

Premises used: add_neg_cancel_right, mul_neg
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
z : R
rw : IsCoprime (x + y * z) y
⊢ IsCoprime (x + z * y) y

Tactic:
rw [mul_comm]

Premises used: mul_comm