[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H✝ : IsCoprime x y
a b : R
H : a * x + b * y = 1
⊢ b * y + a * x = 1
[PROOFSTEP]
rw [add_comm, H]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
x✝ : IsCoprime x x
a b : R
h : a * x + b * x = 1
⊢ x * (a + b) = 1
[PROOFSTEP]
rwa [mul_comm, add_mul]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsUnit x
b : R
hb : b * x = 1
⊢ b * x + 0 * x = 1
[PROOFSTEP]
rwa [zero_mul, add_zero]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
x✝ : IsCoprime 0 x
a b : R
H : a * 0 + b * x = 1
⊢ x * b = 1
[PROOFSTEP]
rwa [mul_zero, zero_add, mul_comm] at H 
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsUnit x
b : R
hb : b * x = 1
⊢ 1 * 0 + b * x = 1
[PROOFSTEP]
rwa [one_mul, zero_add]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
x y z : R
inst✝ : Nontrivial R
p : Fin 2 → R
h : IsCoprime (p 0) (p 1)
⊢ p ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
x y z : R
inst✝ : Nontrivial R
h : IsCoprime (OfNat.ofNat 0 0) (OfNat.ofNat 0 1)
⊢ False
[PROOFSTEP]
exact not_isCoprime_zero_zero h
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
x y z : R
inst✝ : Nontrivial R
h : IsCoprime x y
⊢ x ≠ 0 ∨ y ≠ 0
[PROOFSTEP]
apply not_or_of_imp
[GOAL]
case a
R : Type u
inst✝¹ : CommSemiring R
x y z : R
inst✝ : Nontrivial R
h : IsCoprime x y
⊢ x = 0 → y ≠ 0
[PROOFSTEP]
rintro rfl rfl
[GOAL]
case a
R : Type u
inst✝¹ : CommSemiring R
z : R
inst✝ : Nontrivial R
h : IsCoprime 0 0
⊢ False
[PROOFSTEP]
exact not_isCoprime_zero_zero h
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ 1 * 1 + 0 * x = 1
[PROOFSTEP]
rw [one_mul, zero_mul, add_zero]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ 0 * x + 1 * 1 = 1
[PROOFSTEP]
rw [one_mul, zero_mul, zero_add]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
⊢ x ∣ y
[PROOFSTEP]
let ⟨a, b, H⟩ := H1
[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
[PROOFSTEP]
rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]
[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)
[PROOFSTEP]
exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : x ∣ y * z
⊢ x ∣ z
[PROOFSTEP]
let ⟨a, b, H⟩ := H1
[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 ∣ z
[PROOFSTEP]
rw [← one_mul z, ← H, add_mul, mul_right_comm, mul_assoc b]
[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)
[PROOFSTEP]
exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)
[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)
[PROOFSTEP]
ring
[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 * x + b * z) * (c * y + d * z) = 1
[PROOFSTEP]
rw [h1, h2, mul_one]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x y
H2 : IsCoprime x z
⊢ IsCoprime x (y * z)
[PROOFSTEP]
rw [isCoprime_comm] at H1 H2 ⊢
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime y x
H2 : IsCoprime z x
⊢ IsCoprime (y * z) x
[PROOFSTEP]
exact H1.mul_left H2
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x y
H1 : x ∣ z
H2 : y ∣ z
⊢ x * y ∣ z
[PROOFSTEP]
obtain ⟨a, b, h⟩ := H
[GOAL]
case intro.intro
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
[PROOFSTEP]
rw [← mul_one z, ← h, mul_add]
[GOAL]
case intro.intro
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 * (a * x) + z * (b * y)
[PROOFSTEP]
apply dvd_add
[GOAL]
case intro.intro.h₁
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 * (a * x)
[PROOFSTEP]
rw [mul_comm z, mul_assoc]
[GOAL]
case intro.intro.h₁
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)
[PROOFSTEP]
exact (mul_dvd_mul_left _ H2).mul_left _
[GOAL]
case intro.intro.h₂
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 * (b * y)
[PROOFSTEP]
rw [mul_comm b, ← mul_assoc]
[GOAL]
case intro.intro.h₂
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
[PROOFSTEP]
exact (mul_dvd_mul_right H1 _).mul_right _
[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
⊢ a * y * x + b * z = 1
[PROOFSTEP]
rwa [mul_right_comm, mul_assoc]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (x * y) z
⊢ IsCoprime y z
[PROOFSTEP]
rw [mul_comm] at H 
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (y * x) z
⊢ IsCoprime y z
[PROOFSTEP]
exact H.of_mul_left_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x (y * z)
⊢ IsCoprime x y
[PROOFSTEP]
rw [isCoprime_comm] at H ⊢
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (y * z) x
⊢ IsCoprime y x
[PROOFSTEP]
exact H.of_mul_left_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x (y * z)
⊢ IsCoprime x z
[PROOFSTEP]
rw [mul_comm] at H 
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x (z * y)
⊢ IsCoprime x z
[PROOFSTEP]
exact H.of_mul_right_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
[PROOFSTEP]
rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime y z
hdvd : x ∣ y
⊢ IsCoprime x z
[PROOFSTEP]
obtain ⟨d, rfl⟩ := hdvd
[GOAL]
case intro
R : Type u
inst✝ : CommSemiring R
x z d : R
h : IsCoprime (x * d) z
⊢ IsCoprime x z
[PROOFSTEP]
exact IsCoprime.of_mul_left_left h
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
x y z : R
H : IsCoprime x y
S : Type v
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ ↑f a * ↑f x + ↑f b * ↑f y = 1
[PROOFSTEP]
rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]
[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
[PROOFSTEP]
simpa only [add_mul, mul_add, add_assoc, add_comm, add_left_comm, mul_assoc, mul_comm, mul_left_comm] using H
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y
[PROOFSTEP]
rw [mul_comm] at h 
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_left_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
[PROOFSTEP]
rw [isCoprime_comm] at h ⊢
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y + x * z) x
⊢ IsCoprime y x
[PROOFSTEP]
exact h.of_add_mul_left_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y
[PROOFSTEP]
rw [mul_comm] at h 
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_left_right
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y * z + x) y
⊢ IsCoprime x y
[PROOFSTEP]
rw [add_comm] at h 
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + y * z) y
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_left_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (z * y + x) y
⊢ IsCoprime x y
[PROOFSTEP]
rw [add_comm] at h 
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_right_left
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (x * z + y)
⊢ IsCoprime x y
[PROOFSTEP]
rw [add_comm] at h 
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + x * z)
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_left_right
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (z * x + y)
⊢ IsCoprime x y
[PROOFSTEP]
rw [add_comm] at h 
[GOAL]
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y
[PROOFSTEP]
exact h.of_add_mul_right_right
[GOAL]
R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime (x • y) z
a b : R
h : a * x • y + b * z = 1
⊢ x • a * y + b * z = 1
[PROOFSTEP]
rwa [smul_mul_assoc, ← mul_smul_comm]
[GOAL]
R : Type u_1
G : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Group G
inst✝² : MulAction G R
inst✝¹ : SMulCommClass G R R
inst✝ : IsScalarTower G R R
x : G
y z : R
x✝ : IsCoprime y z
a b : R
h : a * y + b * z = 1
⊢ x⁻¹ • a * x • y + b * z = 1
[PROOFSTEP]
rwa [smul_mul_smul, inv_mul_self, one_smul]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z + y * -z) y
[PROOFSTEP]
simpa only [mul_neg, add_neg_cancel_right] using h
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + z * y) y
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z) y
[PROOFSTEP]
exact h.add_mul_left_left z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + x * z)
[PROOFSTEP]
rw [isCoprime_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y + x * z) x
[PROOFSTEP]
exact h.symm.add_mul_left_left z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + z * x)
[PROOFSTEP]
rw [isCoprime_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y + z * x) x
[PROOFSTEP]
exact h.symm.add_mul_right_left z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y * z + x) y
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z) y
[PROOFSTEP]
exact h.add_mul_left_left z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (z * y + x) y
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + z * y) y
[PROOFSTEP]
exact h.add_mul_right_left z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (x * z + y)
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + x * z)
[PROOFSTEP]
exact h.add_mul_left_right z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (z * x + y)
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime x (y + z * x)
[PROOFSTEP]
exact h.add_mul_right_right z
[GOAL]
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
⊢ IsCoprime (-x) y
[PROOFSTEP]
obtain ⟨a, b, h⟩ := h
[GOAL]
case intro.intro
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ IsCoprime (-x) y
[PROOFSTEP]
use-a, b
[GOAL]
case h
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ -a * -x + b * y = 1
[PROOFSTEP]
rwa [neg_mul_neg]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
⊢ a ^ 2 + b ^ 2 ≠ 0
[PROOFSTEP]
intro h'
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ False
[PROOFSTEP]
obtain ⟨ha, hb⟩ :=
  (add_eq_zero_iff' (by rw [pow_two]; exact mul_self_nonneg _) (by rw [pow_two]; exact mul_self_nonneg _)).mp h'
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ a ^ 2
[PROOFSTEP]
rw [pow_two]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ a * a
[PROOFSTEP]
exact mul_self_nonneg _
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ b ^ 2
[PROOFSTEP]
rw [pow_two]
[GOAL]
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ b * b
[PROOFSTEP]
exact mul_self_nonneg _
[GOAL]
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
a b : R
h : IsCoprime a b
h' : a ^ 2 + b ^ 2 = 0
ha : a ^ 2 = 0
hb : b ^ 2 = 0
⊢ False
[PROOFSTEP]
obtain rfl := pow_eq_zero ha
[GOAL]
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
b : R
hb : b ^ 2 = 0
h : IsCoprime 0 b
h' : 0 ^ 2 + b ^ 2 = 0
ha : 0 ^ 2 = 0
⊢ False
[PROOFSTEP]
obtain rfl := pow_eq_zero hb
[GOAL]
case intro
R : Type u_1
inst✝ : LinearOrderedCommRing R
ha hb : 0 ^ 2 = 0
h : IsCoprime 0 0
h' : 0 ^ 2 + 0 ^ 2 = 0
⊢ False
[PROOFSTEP]
exact not_isCoprime_zero_zero h
