awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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

Tactic:
h.add_mul_left_left z

Premises used: IsCoprime.add_mul_left_left
-- 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

Tactic:
exact h.add_mul_left_left z

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

Tactic:
rw [isCoprime_comm]

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

Tactic:
h.symm.add_mul_left_left z

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

Tactic:
exact h.symm.add_mul_left_left z

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

Tactic:
rw [isCoprime_comm]

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

Tactic:
h.symm.add_mul_right_left z

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

Tactic:
exact h.symm.add_mul_right_left z

Premises used: IsCoprime.symm, IsCoprime.add_mul_right_left
-- 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 (y * z + x) y

Tactic:
rw [add_comm]

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

Tactic:
rw [add_comm]

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

Tactic:
h.add_mul_right_left z

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

Tactic:
exact h.add_mul_right_left z

Premises used: IsCoprime.add_mul_right_left
-- 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 + x * z)
⊢ IsCoprime x (x * z + y)

Tactic:
rw [add_comm]

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

Tactic:
h.add_mul_left_right z

Premises used: IsCoprime.add_mul_left_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 + x * z)

Tactic:
exact h.add_mul_left_right z

Premises used: IsCoprime.add_mul_left_right
-- 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 * x)
⊢ IsCoprime x (z * x + y)

Tactic:
rw [add_comm]

Premises used: add_comm
-- 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 * x)

Tactic:
h.add_mul_right_right z

Premises used: IsCoprime.add_mul_right_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 * x)

Tactic:
exact h.add_mul_right_right z

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

Tactic:
⟨of_add_mul_left_left, fun h => h.add_mul_left_left z⟩

Premises used: IsCoprime.of_add_mul_left_left, Iff.intro, IsCoprime.add_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime (x + z * y) y ↔ IsCoprime x y

Tactic:
⟨of_add_mul_right_left, fun h => h.add_mul_right_left z⟩

Premises used: IsCoprime.of_add_mul_right_left, IsCoprime.add_mul_right_left, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime x (y + x * z) ↔ IsCoprime x y

Tactic:
⟨of_add_mul_left_right, fun h => h.add_mul_left_right z⟩

Premises used: Iff.intro, IsCoprime.add_mul_left_right, IsCoprime.of_add_mul_left_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime x (y + z * x) ↔ IsCoprime x y

Tactic:
⟨of_add_mul_right_right, fun h => h.add_mul_right_right z⟩

Premises used: IsCoprime.add_mul_right_right, Iff.intro, IsCoprime.of_add_mul_right_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime (y * z + x) y ↔ IsCoprime x y

Tactic:
⟨of_mul_add_left_left, fun h => h.mul_add_left_left z⟩

Premises used: Iff.intro, IsCoprime.mul_add_left_left, IsCoprime.of_mul_add_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime (z * y + x) y ↔ IsCoprime x y

Tactic:
⟨of_mul_add_right_left, fun h => h.mul_add_right_left z⟩

Premises used: IsCoprime.mul_add_right_left, IsCoprime.of_mul_add_right_left, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime x (x * z + y) ↔ IsCoprime x y

Tactic:
⟨of_mul_add_left_right, fun h => h.mul_add_left_right z⟩

Premises used: IsCoprime.of_mul_add_left_right, IsCoprime.mul_add_left_right, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
⊢ IsCoprime x (z * x + y) ↔ IsCoprime x y

Tactic:
⟨of_mul_add_right_right, fun h => h.mul_add_right_right z⟩

Premises used: Iff.intro, IsCoprime.mul_add_right_right, IsCoprime.of_mul_add_right_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
obtain : ∀ (a b : R) (h : a * x + b * y = 1), IsCoprime (-x) y
⊢ IsCoprime (-x) y

Tactic:
obtain ⟨a, b, h⟩ := h
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y a b : R
h : a * x + b * y = 1
h₁ : -a * -x + b * y = 1
⊢ IsCoprime (-x) y

Tactic:
use -a, b
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y a b : R
h : a * x + b * y = 1
h₁ h₂ h₃ h₄ : a * x + b * y = 1
⊢ -a * -x + b * y = 1

Tactic:
rwa [neg_mul_neg]

Premises used: neg_mul_neg
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
⊢ IsCoprime (-x) y ↔ IsCoprime x y

Tactic:
⟨fun h => neg_neg x ▸ h.neg_left, neg_left⟩

Premises used: Eq.rec, neg_neg, IsCoprime.neg_left, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
⊢ IsCoprime x (-y)

Tactic:
h.symm.neg_left.symm

Premises used: IsCoprime.symm, IsCoprime.neg_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
⊢ IsCoprime x (-y) ↔ IsCoprime x y

Tactic:
⟨fun h => neg_neg y ▸ h.neg_right, neg_right⟩

Premises used: IsCoprime.neg_right, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
h : IsCoprime x y
⊢ IsCoprime (-x) (-y)

Tactic:
h.neg_left.neg_right

Premises used: IsCoprime.neg_right, IsCoprime.neg_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
⊢ IsCoprime (-x) (-y) ↔ IsCoprime x y

Tactic:
(neg_left_iff _ _).trans (neg_right_iff _ _)

Premises used: IsCoprime.neg_right_iff, Iff.trans, IsCoprime.neg_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime (x + -(y * z)) y ↔ IsCoprime x y
rw₁ : IsCoprime (x + y * -z) y ↔ IsCoprime x y
rw₂ rw₃ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime (x - y * z) y ↔ IsCoprime x y

Tactic:
rw [sub_eq_add_neg, ← mul_neg, add_mul_left_left_iff]

Premises used: sub_eq_add_neg, IsCoprime.add_mul_left_left_iff, mul_neg
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime (x + -(z * y)) y ↔ IsCoprime x y
rw₁ : IsCoprime (x + -z * y) y ↔ IsCoprime x y
rw₂ rw₃ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime (x - z * y) y ↔ IsCoprime x y

Tactic:
rw [sub_eq_add_neg, ← neg_mul, add_mul_right_left_iff]

Premises used: IsCoprime.add_mul_right_left_iff, sub_eq_add_neg, neg_mul
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (y + -(x * z)) ↔ IsCoprime x y
rw₁ : IsCoprime x (y + x * -z) ↔ IsCoprime x y
rw₂ rw₃ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime x (y - x * z) ↔ IsCoprime x y

Tactic:
rw [sub_eq_add_neg, ← mul_neg, add_mul_left_right_iff]

Premises used: sub_eq_add_neg, IsCoprime.add_mul_left_right_iff, mul_neg
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (y + -(z * x)) ↔ IsCoprime x y
rw₁ : IsCoprime x (y + -z * x) ↔ IsCoprime x y
rw₂ rw₃ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime x (y - z * x) ↔ IsCoprime x y

Tactic:
rw [sub_eq_add_neg, ← neg_mul, add_mul_right_right_iff]

Premises used: sub_eq_add_neg, IsCoprime.add_mul_right_right_iff, neg_mul
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime (-x + y * z) y ↔ IsCoprime x y
rw₁ : IsCoprime (-x) y ↔ IsCoprime x y
rw₂ rw₃ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime (y * z - x) y ↔ IsCoprime x y

Tactic:
rw [sub_eq_neg_add, add_mul_left_left_iff, neg_left_iff]

Premises used: sub_eq_neg_add, IsCoprime.neg_left_iff, IsCoprime.add_mul_left_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime (-x + z * y) y ↔ IsCoprime x y
rw₁ : IsCoprime (-x) y ↔ IsCoprime x y
rw₂ rw₃ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime (z * y - x) y ↔ IsCoprime x y

Tactic:
rw [sub_eq_neg_add, add_mul_right_left_iff, neg_left_iff]

Premises used: IsCoprime.add_mul_right_left_iff, sub_eq_neg_add, IsCoprime.neg_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (x * z + -y) ↔ IsCoprime x y
rw₁ : IsCoprime x (-y) ↔ IsCoprime x y
rw₂ rw₃ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime x (x * z - y) ↔ IsCoprime x y

Tactic:
rw [sub_eq_add_neg, mul_add_left_right_iff, neg_right_iff]

Premises used: IsCoprime.mul_add_left_right_iff, sub_eq_add_neg, IsCoprime.neg_right_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y z : R
rw : IsCoprime x (z * x + -y) ↔ IsCoprime x y
rw₁ : IsCoprime x (-y) ↔ IsCoprime x y
rw₂ rw₃ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime x (z * x - y) ↔ IsCoprime x y

Tactic:
rw [sub_eq_add_neg, mul_add_right_right_iff, neg_right_iff]

Premises used: sub_eq_add_neg, IsCoprime.neg_right_iff, IsCoprime.mul_add_right_right_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
h : y ∣ x
obtain : ∀ (z : R), IsCoprime (y * z + 1) y
⊢ IsCoprime (x + 1) y

Tactic:
obtain ⟨z, rfl⟩ := h

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

Tactic:
rw [mul_add_left_left_iff]

Premises used: IsCoprime.mul_add_left_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
y z : R
⊢ IsCoprime 1 y

Tactic:
isCoprime_one_left

Premises used: isCoprime_one_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
y z : R
⊢ IsCoprime 1 y

Tactic:
exact isCoprime_one_left

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

Tactic:
isCoprime_comm.mp (add_one_left_of_dvd h)

Premises used: isCoprime_comm, IsCoprime.add_one_left_of_dvd, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
h : y ∣ x
rw : IsCoprime (-x + 1) y
⊢ IsCoprime (x - 1) y

Tactic:
rw [← neg_sub, neg_left_iff, sub_eq_neg_add]

Premises used: neg_sub, sub_eq_neg_add, IsCoprime.neg_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
h : y ∣ x
⊢ IsCoprime (-x + 1) y

Tactic:
add_one_left_of_dvd h.neg_right

Premises used: Dvd.dvd.neg_right, IsCoprime.add_one_left_of_dvd
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
h : y ∣ x
⊢ IsCoprime (-x + 1) y

Tactic:
exact add_one_left_of_dvd h.neg_right

Premises used: Dvd.dvd.neg_right, IsCoprime.add_one_left_of_dvd
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x y : R
h : x ∣ y
⊢ IsCoprime x (y - 1)

Tactic:
isCoprime_comm.mp (sub_one_left_of_dvd h)

Premises used: isCoprime_comm, IsCoprime.sub_one_left_of_dvd, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x : R
h : 2 ∣ x
⊢ 2 + (x - 1) = x + 1

Tactic:
ring
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
x : R
h : 2 ∣ x
⊢ IsCoprime (x + 1) (x - 1)

Tactic:
simpa [show 2 + (x - 1) = x + 1 by ring] using add_mul_left_left (sub_one_right_of_dvd h) 1

Premises used: IsCoprime.sub_one_right_of_dvd, OfNat.ofNat, IsCoprime.add_mul_left_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
h : 0 ≤ x
inl inl₁ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime |x| y ↔ IsCoprime x y

Tactic:
rw [abs_of_nonneg h]

Premises used: abs_of_nonneg
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
h : x < 0
inr : IsCoprime (-x) y ↔ IsCoprime x y
inr₁ inr₂ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime |x| y ↔ IsCoprime x y

Tactic:
rw [abs_of_neg h, IsCoprime.neg_left_iff]

Premises used: abs_of_neg, IsCoprime.neg_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
⊢ 0 ≤ x ∨ x < 0

Tactic:
cases le_or_gt 0 x with
  | inl h => rw [abs_of_nonneg h]
  | inr h => rw [abs_of_neg h, IsCoprime.neg_left_iff]

Premises used: le_or_gt, IsCoprime.neg_left_iff, OfNat.ofNat
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
h : IsCoprime x y
⊢ IsCoprime |x| y

Tactic:
abs_left_iff _ _ |>.2 h

Premises used: Iff.mpr, IsCoprime.abs_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
rw : IsCoprime |y| x ↔ IsCoprime x y
rw₁ : IsCoprime y x ↔ IsCoprime x y
rw₂ rw₃ : IsCoprime x y ↔ IsCoprime x y
⊢ IsCoprime x |y| ↔ IsCoprime x y

Tactic:
rw [isCoprime_comm, IsCoprime.abs_left_iff, isCoprime_comm]

Premises used: isCoprime_comm, IsCoprime.abs_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
h : IsCoprime x y
⊢ IsCoprime x |y|

Tactic:
abs_right_iff _ _ |>.2 h

Premises used: Iff.mpr, IsCoprime.abs_right_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
⊢ IsCoprime |x| |y| ↔ IsCoprime x y

Tactic:
(abs_left_iff _ _).trans (abs_right_iff _ _)

Premises used: IsCoprime.abs_right_iff, IsCoprime.abs_left_iff, Iff.trans
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : AddLeftMono R
x y : R
h : IsCoprime x y
⊢ IsCoprime |x| |y|

Tactic:
h.abs_left.abs_right

Premises used: IsCoprime.abs_right, IsCoprime.abs_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 0
⊢ HPow.hPow (β := ℕ) a 2 = 0

Tactic:
obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp h'

Premises used: add_eq_zero_iff_of_nonneg, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 0
ha : HPow.hPow (β := ℕ) a 2 = 0
⊢ HPow.hPow (β := ℕ) b 2 = 0

Tactic:
obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp h'

Premises used: add_eq_zero_iff_of_nonneg, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 0
ha : HPow.hPow (β := ℕ) a 2 = 0
hb : HPow.hPow (β := ℕ) b 2 = 0
⊢ IsCoprime 0 b

Tactic:
obtain rfl := eq_zero_of_pow_eq_zero ha

Premises used: eq_zero_of_pow_eq_zero, rfl
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 0
ha : HPow.hPow (β := ℕ) a 2 = 0
hb : HPow.hPow (β := ℕ) b 2 = 0
h₁ : IsCoprime 0 b
⊢ HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = 0

Tactic:
obtain rfl := eq_zero_of_pow_eq_zero ha

Premises used: eq_zero_of_pow_eq_zero, rfl
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
a b : R
h : IsCoprime a b
h' : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 0
ha : HPow.hPow (β := ℕ) a 2 = 0
hb : HPow.hPow (β := ℕ) b 2 = 0
h₁ : IsCoprime 0 b
h'₁ : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = 0
⊢ HPow.hPow (α := R) (β := ℕ) 0 2 = 0

Tactic:
obtain rfl := eq_zero_of_pow_eq_zero ha

Premises used: eq_zero_of_pow_eq_zero, rfl
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
b : R
hb : HPow.hPow (β := ℕ) b 2 = 0
h : IsCoprime 0 b
h' : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = 0
ha : HPow.hPow (α := R) (β := ℕ) 0 2 = 0
⊢ HPow.hPow (α := R) (β := ℕ) 0 2 = 0

Tactic:
obtain rfl := eq_zero_of_pow_eq_zero hb

Premises used: eq_zero_of_pow_eq_zero, rfl
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
b : R
hb : HPow.hPow (β := ℕ) b 2 = 0
h : IsCoprime 0 b
h' : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = 0
ha hb₁ : HPow.hPow (α := R) (β := ℕ) 0 2 = 0
⊢ IsCoprime.{u_1} (R := R) 0 0

Tactic:
obtain rfl := eq_zero_of_pow_eq_zero hb

Premises used: eq_zero_of_pow_eq_zero, rfl
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
b : R
hb : HPow.hPow (β := ℕ) b 2 = 0
h : IsCoprime 0 b
h' : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) b 2 = 0
ha hb₁ : HPow.hPow (α := R) (β := ℕ) 0 2 = 0
h₁ : IsCoprime.{u_1} (R := R) 0 0
⊢ HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (α := R) (β := ℕ) 0 2 = 0

Tactic:
obtain rfl := eq_zero_of_pow_eq_zero hb

Premises used: eq_zero_of_pow_eq_zero, rfl
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha hb : HPow.hPow (α := R) (β := ℕ) 0 2 = 0
h : IsCoprime.{u_1} (R := R) 0 0
h' : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (α := R) (β := ℕ) 0 2 = 0
⊢ False

Tactic:
not_isCoprime_zero_zero h

Premises used: not_isCoprime_zero_zero
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
ha hb : HPow.hPow (α := R) (β := ℕ) 0 2 = 0
h : IsCoprime.{u_1} (R := R) 0 0
h' : HPow.hPow (α := R) (β := ℕ) 0 2 + HPow.hPow (α := R) (β := ℕ) 0 2 = 0
⊢ False

Tactic:
exact not_isCoprime_zero_zero h

Premises used: not_isCoprime_zero_zero
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
m n : ℕ
⊢ IsCoprime m n ↔ m = 1 ∨ n = 1

Tactic:
⟨fun ⟨a, b, H⟩ => ?_, fun h => ?_⟩

Premises used: Iff.intro, Or, OfNat.ofNat, Eq, _private.0.Nat.isCoprime_iff.match_1
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
m n : ℕ
refine_1 : IsCoprime m n → ∀ (a b : ℕ) (H : a * m + b * n = 1), m = 1 ∨ n = 1
refine_2 : ∀ (h : m = 1 ∨ n = 1), IsCoprime m n
⊢ IsCoprime m n ↔ m = 1 ∨ n = 1

Tactic:
refine ⟨fun ⟨a, b, H⟩ => ?_, fun h => ?_⟩
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
m n : ℕ
h : IsCoprime m n
a b : ℕ
H : a * m + b * n = 1
⊢ (a = 0 ∨ m = 0) ∧ b = 1 ∧ n = 1 ∨ (a = 1 ∧ m = 1) ∧ (b = 0 ∨ n = 0)

Tactic:
simp_rw [Nat.add_eq_one_iff, mul_eq_one, mul_eq_zero] at H

Premises used: mul_eq_one, Nat.add_eq_one_iff, Nat.mul_eq_zero
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
m n : ℕ
h : IsCoprime m n
a b : ℕ
H : (a = 0 ∨ m = 0) ∧ b = 1 ∧ n = 1 ∨ (a = 1 ∧ m = 1) ∧ (b = 0 ∨ n = 0)
⊢ m = 1 ∨ n = 1

Tactic:
H.symm.imp (·.1.2) (·.2.2)

Premises used: Or.symm, Or.imp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
m n : ℕ
h : IsCoprime m n
a b : ℕ
H : (a = 0 ∨ m = 0) ∧ b = 1 ∧ n = 1 ∨ (a = 1 ∧ m = 1) ∧ (b = 0 ∨ n = 0)
⊢ m = 1 ∨ n = 1

Tactic:
exact H.symm.imp (·.1.2) (·.2.2)

Premises used: Or.symm, Or.imp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
m n : ℕ
h : m = 1 ∨ n = 1
refine_2 : IsCoprime 1 n
refine_2₁ : IsCoprime m 1
⊢ IsCoprime m n

Tactic:
obtain rfl | rfl := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
n : ℕ
⊢ IsCoprime 1 n

Tactic:
isCoprime_one_left

Premises used: isCoprime_one_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
n : ℕ
⊢ IsCoprime 1 n

Tactic:
exact isCoprime_one_left

Premises used: isCoprime_one_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
m : ℕ
⊢ IsCoprime m 1

Tactic:
isCoprime_one_right

Premises used: isCoprime_one_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
m : ℕ
⊢ IsCoprime m 1

Tactic:
exact isCoprime_one_right

Premises used: isCoprime_one_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
m n : ℕ+
⊢ IsCoprime (↑m : ℕ) (↑n : ℕ) ↔ m = 1 ∨ n = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : Semifield R
m n : R
inl : IsCoprime m 0 ↔ m ≠ 0 ∨ Ne.{u_1 + 1} (α := R) 0 0
inr : ∀ (hn : n ≠ 0), IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : Semifield R
m : R
⊢ IsCoprime m 0 ↔ m ≠ 0 ∨ Ne.{u_1 + 1} (α := R) 0 0

Tactic:
simp [isCoprime_zero_right]

Premises used: isCoprime_zero_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : Semifield R
m n : R
hn : n ≠ 0
this : IsCoprime m n
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
simpa [hn]
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : Semifield R
m n : R
hn : n ≠ 0
inr : IsCoprime m n
⊢ IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

Tactic:
suffices IsCoprime m n by simpa [hn]
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : Semifield R
m n : R
hn : n ≠ 0
⊢ IsCoprime m n

Tactic:
⟨0, n⁻¹, ?_⟩

Premises used: Inv.inv, Exists.intro, OfNat.ofNat, IsCoprime
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : Semifield R
m n : R
hn : n ≠ 0
inr : 0 * m + n⁻¹ * n = 1
⊢ IsCoprime m n

Tactic:
refine ⟨0, n⁻¹, ?_⟩
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : Semifield R
m n : R
hn : n ≠ 0
⊢ 0 * m + n⁻¹ * n = 1

Tactic:
simp [inv_mul_cancel₀ hn]

Premises used: inv_mul_cancel₀
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime (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