[GOAL]
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + m / k * k = m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + k * (m / k) = m
[PROOFSTEP]
exact mod_add_div _ _
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m / k * k + m % k = m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ k * (m / k) + m % k = m
[PROOFSTEP]
exact div_add_mod _ _
[GOAL]
R✝ : Type u
inst✝¹ : EuclideanDomain R✝
R : Type u_1
inst✝ : EuclideanDomain R
a b : R
⊢ b * (a / b) + a % b - b * (a / b) = a - b * (a / b)
[PROOFSTEP]
rw [div_add_mod]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬a * b ≺ b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a ≠ 0
⊢ ¬b * a ≺ b
[PROOFSTEP]
exact mul_left_not_lt b h
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a : R
⊢ a % 0 = a
[PROOFSTEP]
simpa only [zero_mul, zero_add] using div_add_mod a 0
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a : R
this : (p : Prop) → Decidable p
h : ¬a = 0
⊢ ¬a ≺ 1
[PROOFSTEP]
simpa only [one_mul] using mul_left_not_lt 1 h
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
b d : R
ha : b * d ≠ 0
⊢ d = 0 → b * d = 0
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
b : R
ha : b * 0 ≠ 0
⊢ b * 0 = 0
[PROOFSTEP]
exact mul_zero _
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
P : R → R → Prop
a b : R
H0 : ∀ (x : R), P 0 x
H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b
a0 : a = 0
⊢ P a b
[PROOFSTEP]
change P a b
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
P : R → R → Prop
a b : R
H0 : ∀ (x : R), P 0 x
H1 : ∀ (a b : R), a ≠ 0 → P (b % a) a → P a b
a0 : a = 0
⊢ P a b
[PROOFSTEP]
exact a0.symm ▸ H0 b
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ gcd 0 a = a
[PROOFSTEP]
rw [gcd]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : 0 = 0 then a
    else
      let_fun x := (_ : a % 0 ≺ 0);
      gcd (a % 0) 0) =
    a
[PROOFSTEP]
exact if_pos rfl
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')
[PROOFSTEP]
unfold xgcdAux
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ (if _hr : 0 = 0 then (r', s', t')
    else
      let q := r' / 0;
      let_fun x := (_ : r' % 0 ≺ 0);
      xgcdAux (r' % 0) (s' - q * s) (t' - q * t) 0 s t) =
    (r', s', t')
[PROOFSTEP]
exact if_pos rfl
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
[PROOFSTEP]
conv =>
  lhs
  rw [xgcdAux]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
[PROOFSTEP]
  lhs
  rw [xgcdAux]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
[PROOFSTEP]
  lhs
  rw [xgcdAux]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
[PROOFSTEP]
lhs
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
| xgcdAux r s t r' s' t'
[PROOFSTEP]
rw [xgcdAux]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ (if _hr : r = 0 then (r', s', t')
    else
      let q := r' / r;
      let_fun x := (_ : r' % r ≺ r);
      xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t) =
    xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
[PROOFSTEP]
exact if_neg h
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdA 0 s = 0
[PROOFSTEP]
unfold gcdA
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).fst = 0
[PROOFSTEP]
rw [xgcd, xgcd_zero_left]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ gcdB 0 s = 1
[PROOFSTEP]
unfold gcdB
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s : R
⊢ (xgcd 0 s).snd = 1
[PROOFSTEP]
rw [xgcd, xgcd_zero_left]


[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
R : Type u_4
inst✝ : AddGroup R
a b : R
h : a - b = 0
⊢ a + -b = b + -b
[PROOFSTEP]
rw [← sub_eq_add_neg, h, add_neg_self]
  -- Porting note:
  -- This theorem was introduced during ad-hoc porting
  -- and hopefully can be removed again after `Mathlib.Algebra.Ring.Basic` is fully ported.
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
⊢ 1 ≠ 0
[PROOFSTEP]
intro h
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
⊢ False
[PROOFSTEP]
rcases exists_pair_ne M₀ with ⟨x, y, hx⟩
[GOAL]
case intro.intro
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ False
[PROOFSTEP]
apply hx
[GOAL]
case intro.intro
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ x = y
[PROOFSTEP]
calc
  x = 1 * x := by rw [one_mul]
  _ = 0 := by rw [h, zero_mul]
  _ = 1 * y := by rw [h, zero_mul]
  _ = y := by rw [one_mul]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ x = 1 * x
[PROOFSTEP]
rw [one_mul]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 1 * x = 0
[PROOFSTEP]
rw [h, zero_mul]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 0 = 1 * y
[PROOFSTEP]
rw [h, zero_mul]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
a b : M₀
h : 1 = 0
x y : M₀
hx : x ≠ y
⊢ 1 * y = y
[PROOFSTEP]
rw [one_mul]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
a b : M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬f 0 = f 1
[PROOFSTEP]
rw [zero, one]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
a b : M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬0 = 1
[PROOFSTEP]
exact zero_ne_one
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
⊢ 0 = a * b ↔ a = 0 ∨ b = 0
[PROOFSTEP]
rw [eq_comm, mul_eq_zero]
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
⊢ a * a = 0 ↔ a = 0
[PROOFSTEP]
simp
[GOAL]
G₀ : Type u
M₀ : Type u_1
M₀' : Type u_2
G₀' : Type u_3
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
⊢ 0 = a * a ↔ a = 0
[PROOFSTEP]
simp


[GOAL]
src✝¹ : CommRing ℤ := inferInstanceAs (CommRing ℤ)
src✝ : Nontrivial ℤ := inferInstanceAs (Nontrivial ℤ)
a b : ℤ
b0 : b ≠ 0
⊢ ↑(natAbs ((fun x x_1 => x % x_1) a b)) < ↑(natAbs b)
[PROOFSTEP]
rw [Int.natAbs_of_nonneg (Int.emod_nonneg _ b0), ← Int.abs_eq_natAbs]
[GOAL]
src✝¹ : CommRing ℤ := inferInstanceAs (CommRing ℤ)
src✝ : Nontrivial ℤ := inferInstanceAs (Nontrivial ℤ)
a b : ℤ
b0 : b ≠ 0
⊢ a % b < |b|
[PROOFSTEP]
exact Int.emod_lt _ b0
[GOAL]
src✝¹ : CommRing ℤ := inferInstanceAs (CommRing ℤ)
src✝ : Nontrivial ℤ := inferInstanceAs (Nontrivial ℤ)
a b : ℤ
b0 : b ≠ 0
⊢ natAbs (a * b) ≥ natAbs a
[PROOFSTEP]
rw [← mul_one a.natAbs, Int.natAbs_mul]
[GOAL]
src✝¹ : CommRing ℤ := inferInstanceAs (CommRing ℤ)
src✝ : Nontrivial ℤ := inferInstanceAs (Nontrivial ℤ)
a b : ℤ
b0 : b ≠ 0
⊢ natAbs a * natAbs b ≥ natAbs a * 1
[PROOFSTEP]
rw [← Int.natAbs_pos] at b0
[GOAL]
src✝¹ : CommRing ℤ := inferInstanceAs (CommRing ℤ)
src✝ : Nontrivial ℤ := inferInstanceAs (Nontrivial ℤ)
a b : ℤ
b0 : 0 < natAbs b
⊢ natAbs a * natAbs b ≥ natAbs a * 1
[PROOFSTEP]
exact Nat.mul_le_mul_of_nonneg_left b0
[GOAL]
K : Type u_1
inst✝ : Field K
a b : K
⊢ b * (fun x x_1 => x / x_1) a b + (fun a b => a - a * b / b) a b = a
[PROOFSTEP]
by_cases h : b = 0
[GOAL]
case pos
K : Type u_1
inst✝ : Field K
a b : K
h : b = 0
⊢ b * (fun x x_1 => x / x_1) a b + (fun a b => a - a * b / b) a b = a
[PROOFSTEP]
simp [h, mul_div_cancel']
[GOAL]
case neg
K : Type u_1
inst✝ : Field K
a b : K
h : ¬b = 0
⊢ b * (fun x x_1 => x / x_1) a b + (fun a b => a - a * b / b) a b = a
[PROOFSTEP]
simp [h, mul_div_cancel']
[GOAL]
K : Type u_1
inst✝ : Field K
a b : K
hnb : b ≠ 0
⊢ (fun a b => a = 0 ∧ b ≠ 0) ((fun a b => a - a * b / b) a b) b
[PROOFSTEP]
simp [hnb]


[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
hc : c ≠ 0
⊢ a / c / (b / c) = a / b
[PROOFSTEP]
rw [div_div_eq_mul_div, div_mul_cancel _ hc]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b c a : G₀
hc : c ≠ 0
⊢ a / c * (c / b) = a / b
[PROOFSTEP]
rw [← mul_div_assoc, div_mul_cancel _ hc]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b✝ c a b : G₀
h : b = 0 → a = 0
hb : b = 0
⊢ a / b * b = a
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a✝ b✝ c a b : G₀
h : b = 0 → a = 0
hb : b = 0
⊢ a * b / b = a
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a✝ b✝ c d a b : G₀
h : a = 0 → b = 0
⊢ a * b / a = b
[PROOFSTEP]
rw [mul_comm, mul_div_cancel_of_imp h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a✝ b✝ c d a b : G₀
h : b = 0 → a = 0
⊢ b * (a / b) = a
[PROOFSTEP]
rw [mul_comm, div_mul_cancel_of_imp h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a✝ b✝ c✝ d✝ a b c d : G₀
hb : b ≠ 0
hd : d ≠ 0
h : a / b = c / d
⊢ a * d = c * b
[PROOFSTEP]
rw [← mul_one a, ← div_self hb, ← mul_comm_div, h, div_mul_eq_mul_div, div_mul_cancel _ hd]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a b✝ c d b : G₀
h : a ≠ 0
⊢ 1 / (a * b) * a = 1 / b
[PROOFSTEP]
rw [div_mul_eq_mul_div, one_mul, div_mul_right _ h]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : CommGroupWithZero G₀
a✝ b✝ c d a b : G₀
hc : c ≠ 0
⊢ c / a / (c / b) = b / a
[PROOFSTEP]
rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : GroupWithZero G₀
inst✝³ : Nontrivial M₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : MonoidWithZeroHomClass F G₀ M₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f✝ : F
a : G₀
f g : F'
h : ↑f a = ↑g a
⊢ ↑f a⁻¹ = ↑g a⁻¹
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : GroupWithZero G₀
inst✝³ : Nontrivial M₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : MonoidWithZeroHomClass F G₀ M₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f✝ : F
f g : F'
h : ↑f 0 = ↑g 0
⊢ ↑f 0⁻¹ = ↑g 0⁻¹
[PROOFSTEP]
rw [inv_zero, map_zero, map_zero]
[GOAL]
case inr
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : GroupWithZero G₀
inst✝³ : Nontrivial M₀
inst✝² : MonoidWithZero M₀'
inst✝¹ : MonoidWithZeroHomClass F G₀ M₀
inst✝ : MonoidWithZeroHomClass F' G₀ M₀'
f✝ : F
a : G₀
f g : F'
h : ↑f a = ↑g a
ha : a ≠ 0
⊢ ↑f a⁻¹ = ↑g a⁻¹
[PROOFSTEP]
exact (IsUnit.mk0 a ha).eq_on_inv f g h
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a b : G₀
⊢ ↑f a⁻¹ = (↑f a)⁻¹
[PROOFSTEP]
by_cases h : a = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a b : G₀
h : a = 0
⊢ ↑f a⁻¹ = (↑f a)⁻¹
[PROOFSTEP]
simp [h, map_zero f]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a b : G₀
h : ¬a = 0
⊢ ↑f a⁻¹ = (↑f a)⁻¹
[PROOFSTEP]
apply eq_inv_of_mul_eq_one_left
[GOAL]
case neg.h
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero G₀'
inst✝ : MonoidWithZeroHomClass F G₀ G₀'
f : F
a b : G₀
h : ¬a = 0
⊢ ↑f a⁻¹ * ↑f a = 1
[PROOFSTEP]
rw [← map_mul, inv_mul_cancel h, map_one]


[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
have h1 : m - n + n = m := tsub_add_cancel_of_le h
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
have h2 : a ^ (m - n) * a ^ n = a ^ m := by rw [← pow_add, h1]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
⊢ a ^ (m - n) * a ^ n = a ^ m
[PROOFSTEP]
rw [← pow_add, h1]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
h1 : m - n + n = m
h2 : a ^ (m - n) * a ^ n = a ^ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
h : n < m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
obtain rfl | ha := eq_or_ne a 0
[GOAL]
case inl
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m✝ n✝ m n : ℕ
h : n < m
⊢ 0 ^ (m - n) = 0 ^ m * (0 ^ n)⁻¹
[PROOFSTEP]
rw [zero_pow (tsub_pos_of_lt h), zero_pow (n.zero_le.trans_lt h), zero_mul]
[GOAL]
case inr
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m✝ n✝ : ℕ
a : G₀
m n : ℕ
h : n < m
ha : a ≠ 0
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹
[PROOFSTEP]
exact pow_sub₀ _ ha h.le
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℕ
ha : a ≠ 0
h : n ≤ m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
[PROOFSTEP]
rw [pow_sub₀ _ (inv_ne_zero ha) h, inv_pow, inv_pow, inv_inv]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a✝ : G₀
m n : ℕ
a : G₀
h : n < m
⊢ a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
[PROOFSTEP]
rw [pow_sub_of_lt a⁻¹ h, inv_pow, inv_pow, inv_inv]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ 0 ^ ↑n = 0
[PROOFSTEP]
rw [zpow_ofNat, zero_pow']
[GOAL]
case a
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0
[PROOFSTEP]
simpa using h
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℕ
x✝ : -[n+1] ≠ 0
⊢ 0 ^ -[n+1] = 0
[PROOFSTEP]
simp
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
h : n = 0
⊢ 0 ^ n = 1
[PROOFSTEP]
rw [h, zpow_zero]
[GOAL]
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
h : ¬n = 0
⊢ 0 ^ n = 0
[PROOFSTEP]
rw [zero_zpow _ h]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (↑n + 1) = a ^ ↑n * a
[PROOFSTEP]
simp only [← Int.ofNat_succ, zpow_ofNat, pow_succ']
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a ^ (-[0+1] + 1) = a ^ -[0+1] * a
[PROOFSTEP]
erw [zpow_zero, zpow_negSucc, pow_one, inv_mul_cancel ha]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (-[n + 1+1] + 1) = a ^ -[n + 1+1] * a
[PROOFSTEP]
rw [Int.negSucc_eq, zpow_neg, neg_add, neg_add_cancel_right, zpow_neg, ← Int.ofNat_succ, zpow_ofNat, zpow_ofNat,
  pow_succ _ (n + 1), mul_inv_rev, mul_assoc, inv_mul_cancel ha, mul_one]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹
[PROOFSTEP]
rw [mul_assoc, mul_inv_cancel ha, mul_one]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℤ
⊢ a ^ (n - 1) * a * a⁻¹ = a ^ n * a⁻¹
[PROOFSTEP]
rw [← zpow_add_one₀ ha, sub_add_cancel]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
induction' n using Int.induction_on with n ihn n ihn
[GOAL]
case hz
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
⊢ a ^ (m + 0) = a ^ m * a ^ 0
[PROOFSTEP]
simp
[GOAL]
case hp
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + ↑n) = a ^ m * a ^ ↑n
⊢ a ^ (m + (↑n + 1)) = a ^ m * a ^ (↑n + 1)
[PROOFSTEP]
simp only [← add_assoc, zpow_add_one₀ ha, ihn, mul_assoc]
[GOAL]
case hn
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ m * a ^ (-↑n - 1)
[PROOFSTEP]
rw [zpow_sub_one₀ ha, ← mul_assoc, ← ihn, ← zpow_sub_one₀ ha, add_sub_assoc]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
by_cases hm : m = 0
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : m = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
simp [hm]
[GOAL]
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
subst a
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : 0 ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
⊢ 0 ^ (m + n) = 0 ^ m * 0 ^ n
[PROOFSTEP]
simp only [false_or_iff, eq_self_iff_true, not_true, Ne.def, hm, hn, false_and_iff, or_false_iff] at h
[GOAL]
case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
m n : ℤ
hm : ¬m = 0
hn : ¬n = 0
h : ¬m + n = 0
⊢ 0 ^ (m + n) = 0 ^ m * 0 ^ n
[PROOFSTEP]
rw [zero_zpow _ h, zero_zpow _ hm, zero_mul]
[GOAL]
case neg
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
m n : ℤ
h : a ≠ 0 ∨ m + n ≠ 0 ∨ m = 0 ∧ n = 0
hm : ¬m = 0
hn : ¬n = 0
ha : ¬a = 0
⊢ a ^ (m + n) = a ^ m * a ^ n
[PROOFSTEP]
exact zpow_add₀ ha m n
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
i : ℤ
⊢ a ^ (1 + i) = a * a ^ i
[PROOFSTEP]
rw [zpow_add₀ h, zpow_one]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)
[PROOFSTEP]
simp [h.pow_right n]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ -[n+1]) (y ^ -[n+1])
[PROOFSTEP]
simp only [zpow_negSucc, (h.pow_right (n + 1)).inv_right₀]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ a ^ bit1 n = a ^ n * a ^ n * a
[PROOFSTEP]
rw [← zpow_bit0, bit1, zpow_add', zpow_one]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ a ≠ 0 ∨ bit0 n + 1 ≠ 0 ∨ bit0 n = 0 ∧ 1 = 0
[PROOFSTEP]
right
[GOAL]
case h
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ bit0 n + 1 ≠ 0 ∨ bit0 n = 0 ∧ 1 = 0
[PROOFSTEP]
left
[GOAL]
case h.h
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ bit0 n + 1 ≠ 0
[PROOFSTEP]
apply bit1_ne_zero
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ a ^ ↑a✝ ≠ 0
[PROOFSTEP]
rw [zpow_ofNat]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ a ^ a✝ ≠ 0
[PROOFSTEP]
exact pow_ne_zero _ ha
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ a ^ -[a✝+1] ≠ 0
[PROOFSTEP]
rw [zpow_negSucc]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
a✝ : ℕ
⊢ (a ^ (a✝ + 1))⁻¹ ≠ 0
[PROOFSTEP]
exact inv_ne_zero (pow_ne_zero _ ha)
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
z1 z2 : ℤ
⊢ a ^ (z1 - z2) = a ^ z1 / a ^ z2
[PROOFSTEP]
rw [sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
⊢ a ^ bit1 n = (a * a) ^ n * a
[PROOFSTEP]
rw [zpow_bit1₀, (Commute.refl a).mul_zpow]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
x : G₀
h : x ≠ 0
⊢ x ^ (-n) * x ^ n = 1
[PROOFSTEP]
rw [zpow_neg]
[GOAL]
G₀ : Type u_1
inst✝ : GroupWithZero G₀
n : ℤ
x : G₀
h : x ≠ 0
⊢ (x ^ n)⁻¹ * x ^ n = 1
[PROOFSTEP]
exact inv_mul_cancel (zpow_ne_zero n h)
[GOAL]
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
⊢ a ^ 2 * b / a = a * b
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : a = 0
⊢ a ^ 2 * b / a = a * b
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
G₀ : Type u_1
inst✝ : CommGroupWithZero G₀
a b : G₀
ha : ¬a = 0
⊢ a ^ 2 * b / a = a * b
[PROOFSTEP]
rw [sq, mul_assoc, mul_div_cancel_left _ ha]


[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MulZeroClass G₀
a : G₀
⊢ SemiconjBy a 0 0
[PROOFSTEP]
simp only [SemiconjBy, mul_zero, zero_mul]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MulZeroClass G₀
x y : G₀
⊢ SemiconjBy 0 x y
[PROOFSTEP]
simp only [SemiconjBy, mul_zero, zero_mul]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
ha : a = 0
⊢ SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x
[PROOFSTEP]
simp only [ha, inv_zero, SemiconjBy.zero_left]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
⊢ SemiconjBy a x⁻¹ y⁻¹
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
[PROOFSTEP]
simp only [ha, zero_left]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
[PROOFSTEP]
subst x
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a y x' y' : G₀
ha : ¬a = 0
h : SemiconjBy a 0 y
⊢ SemiconjBy a 0⁻¹ y⁻¹
[PROOFSTEP]
simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a y x' y' : G₀
ha : ¬a = 0
h : y = 0 ∨ a = 0
⊢ SemiconjBy a 0⁻¹ y⁻¹
[PROOFSTEP]
simp [h.resolve_right ha]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹
[PROOFSTEP]
have := mul_ne_zero ha hx
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : a * x ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹
[PROOFSTEP]
rw [h.eq, mul_ne_zero_iff] at this
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : ¬x = 0
this : y ≠ 0 ∧ a ≠ 0
⊢ SemiconjBy a x⁻¹ y⁻¹
[PROOFSTEP]
exact @units_inv_right _ _ _ (Units.mk0 x hx) (Units.mk0 y this.1) h
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x / x') (y / y')
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : GroupWithZero G₀
a x y x' y' : G₀
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x * x'⁻¹) (y * y'⁻¹)
[PROOFSTEP]
exact h.mul_right h'.inv_right₀


[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
a0 : a ≠ 0
h : ¬b - a * b / a = 0
⊢ False
[PROOFSTEP]
have := mul_left_not_lt a h
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
a0 : a ≠ 0
h : ¬b - a * b / a = 0
this : ¬EuclideanDomain.r (a * (b - a * b / a)) a
⊢ False
[PROOFSTEP]
rw [mul_sub, sub_eq_iff_eq_add'.2 (div_add_mod (a * b) a).symm] at this
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
a0 : a ≠ 0
h : ¬b - a * b / a = 0
this : ¬EuclideanDomain.r (a * b % a) a
⊢ False
[PROOFSTEP]
exact this (mod_lt _ a0)
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
b0 : b ≠ 0
⊢ a * b / b = a
[PROOFSTEP]
rw [mul_comm]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
b0 : b ≠ 0
⊢ b * a / b = a
[PROOFSTEP]
exact mul_div_cancel_left a b0
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ a
[PROOFSTEP]
rw [← div_add_mod a b, h, add_zero]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ b * (a / b)
[PROOFSTEP]
exact dvd_mul_right _ _
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ a % b = 0
[PROOFSTEP]
rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ b * c = b * (b * c / b)
[PROOFSTEP]
haveI := Classical.dec
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
⊢ b * c = b * (b * c / b)
[PROOFSTEP]
by_cases b0 : b = 0
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)
[PROOFSTEP]
simp only [b0, zero_mul]
[GOAL]
case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)
[PROOFSTEP]
rw [mul_div_cancel_left _ b0]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : c ∣ b
⊢ c ∣ a % b ↔ c ∣ a
[PROOFSTEP]
rw [← dvd_add_right (h.mul_right _), div_add_mod]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : ¬a = 0
⊢ 0 / a = 0
[PROOFSTEP]
simpa only [zero_mul] using mul_div_cancel 0 a0
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a : R
a0 : a ≠ 0
⊢ a / a = 1
[PROOFSTEP]
simpa only [one_mul] using mul_div_cancel 1 a0
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
⊢ a = c / b
[PROOFSTEP]
rw [← h, mul_div_cancel _ hb]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
h : a * b = c
⊢ b = c / a
[PROOFSTEP]
rw [← h, mul_div_cancel_left _ ha]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
⊢ x * y / z = x * (y / z)
[PROOFSTEP]
by_cases hz : z = 0
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : z = 0
⊢ x * y / z = x * (y / z)
[PROOFSTEP]
subst hz
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
x y : R
h : 0 ∣ y
⊢ x * y / 0 = x * (y / 0)
[PROOFSTEP]
rw [div_zero, div_zero, mul_zero]
[GOAL]
case neg
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h : z ∣ y
hz : ¬z = 0
⊢ x * y / z = x * (y / z)
[PROOFSTEP]
rcases h with ⟨p, rfl⟩
[GOAL]
case neg.intro
R : Type u
inst✝ : EuclideanDomain R
x z : R
hz : ¬z = 0
p : R
⊢ x * (z * p) / z = x * (z * p / z)
[PROOFSTEP]
rw [mul_div_cancel_left _ hz, mul_left_comm, mul_div_cancel_left _ hz]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b : R
hb : b ≠ 0
hab : b ∣ a
⊢ b * (a / b) = a
[PROOFSTEP]
rw [← mul_div_assoc _ hab, mul_div_cancel_left _ hb]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
⊢ p / q ∣ p
[PROOFSTEP]
by_cases hq : q = 0
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : q = 0
⊢ p / q ∣ p
[PROOFSTEP]
rw [hq, zero_dvd_iff] at hpq
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ p / q ∣ p
[PROOFSTEP]
rw [hpq]
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : p = 0
hq : q = 0
⊢ 0 / q ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
case neg
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p / q ∣ p
[PROOFSTEP]
use q
[GOAL]
case h
R : Type u
inst✝ : EuclideanDomain R
p q : R
hpq : q ∣ p
hq : ¬q = 0
⊢ p = p / q * q
[PROOFSTEP]
rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, EuclideanDomain.mul_div_cancel _ hq]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
⊢ b ∣ c / a
[PROOFSTEP]
rcases eq_or_ne a 0 with (rfl | ha)
[GOAL]
case inl
R : Type u
inst✝ : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0
[PROOFSTEP]
simp only [div_zero, dvd_zero]
[GOAL]
case inr
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a
[PROOFSTEP]
rcases h with ⟨d, rfl⟩
[GOAL]
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ b ∣ a * b * d / a
[PROOFSTEP]
refine' ⟨d, _⟩
[GOAL]
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * b * d / a = b * d
[PROOFSTEP]
rw [mul_assoc, mul_div_cancel_left _ ha]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ gcd a 0 = a
[PROOFSTEP]
rw [gcd]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
⊢ (if a0 : a = 0 then 0
    else
      let_fun x := (_ : EuclideanDomain.r (0 % a) a);
      gcd (0 % a) a) =
    a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
h : a = 0
⊢ 0 = a
[PROOFSTEP]
simp only [h, zero_mod, gcd_zero_left]
[GOAL]
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a : R
h : ¬a = 0
⊢ (let_fun x := (_ : EuclideanDomain.r (0 % a) a);
    gcd (0 % a) a) =
    a
[PROOFSTEP]
simp only [h, zero_mod, gcd_zero_left]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = gcd (b % a) a
[PROOFSTEP]
rw [gcd]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ (if a0 : a = 0 then b
    else
      let_fun x := (_ : EuclideanDomain.r (b % a) a);
      gcd (b % a) a) =
    gcd (b % a) a
[PROOFSTEP]
split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ (if a0 : a = 0 then b
    else
      let_fun x := (_ : EuclideanDomain.r (b % a) a);
      gcd (b % a) a) =
    gcd (b % a) a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a = 0
⊢ b = gcd (b % a) a
[PROOFSTEP]
simp only [h, mod_zero, gcd_zero_right]
[GOAL]
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : ¬a = 0
⊢ (let_fun x := (_ : EuclideanDomain.r (b % a) a);
    gcd (b % a) a) =
    gcd (b % a) a
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ gcd 0 b ∣ 0 ∧ gcd 0 b ∣ b
[PROOFSTEP]
rw [gcd_zero_left]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b✝ b : R
⊢ b ∣ 0 ∧ b ∣ b
[PROOFSTEP]
exact ⟨dvd_zero _, dvd_rfl⟩
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ a b : R
x✝¹ : a ≠ 0
x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd a b ∣ a ∧ gcd a b ∣ b
[PROOFSTEP]
rw [gcd_val]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ a b : R
x✝¹ : a ≠ 0
x✝ : gcd (b % a) a ∣ b % a ∧ gcd (b % a) a ∣ a
IH₁ : gcd (b % a) a ∣ b % a
IH₂ : gcd (b % a) a ∣ a
⊢ gcd (b % a) a ∣ a ∧ gcd (b % a) a ∣ b
[PROOFSTEP]
exact ⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = 0
⊢ a = 0 ∧ b = 0
[PROOFSTEP]
simpa [h] using gcd_dvd a b
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = 0 ∧ b = 0 → gcd a b = 0
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
⊢ gcd 0 0 = 0
[PROOFSTEP]
exact gcd_zero_right _
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b c x✝¹ : R
x✝ : c ∣ 0
H : c ∣ x✝¹
⊢ c ∣ gcd 0 x✝¹
[PROOFSTEP]
simpa only [gcd_zero_left] using H
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ c a b : R
x✝ : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd a b
[PROOFSTEP]
rw [gcd_val]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ c a b : R
x✝ : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd (b % a) a
[PROOFSTEP]
exact IH ((dvd_mod_iff ca).2 cb) ca
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = a
⊢ a ∣ b
[PROOFSTEP]
rw [← h]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = a
⊢ gcd a b ∣ b
[PROOFSTEP]
apply gcd_dvd_right
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : a ∣ b
⊢ gcd a b = a
[PROOFSTEP]
rw [gcd_val, mod_eq_zero.2 h, gcd_zero_left]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ ∀ (x s t s' t' : R), (xgcdAux 0 s t x s' t').fst = gcd 0 x
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y x✝ s✝ t✝ s'✝ t'✝ : R
⊢ (xgcdAux 0 s✝ t✝ x✝ s'✝ t'✝).fst = gcd 0 x✝
[PROOFSTEP]
rw [xgcd_zero_left, gcd_zero_left]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : R
⊢ (xgcdAux x s t y s' t').fst = gcd x y
[PROOFSTEP]
simp only [xgcdAux_rec h, if_neg h, IH]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x✝ y✝ x y : R
h : x ≠ 0
IH : ∀ (s t s' t' : R), (xgcdAux (y % x) s t x s' t').fst = gcd (y % x) x
s t s' t' : R
⊢ gcd (y % x) x = gcd x y
[PROOFSTEP]
rw [← gcd_val]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
[PROOFSTEP]
rw [xgcd, ← xgcdAux_fst x y 1 0 0 1, Prod.mk.eta]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b r r' s t s' t' : R
p : EuclideanDomain.P a b (r, s, t)
p' : EuclideanDomain.P a b (r', s', t')
⊢ EuclideanDomain.P a b (xgcdAux r s t r' s' t')
[PROOFSTEP]
induction r, r' using GCD.induction generalizing s t s' t' with
| H0 n => simpa only [xgcd_zero_left]
| H1 _ _ h IH =>
  rw [xgcdAux_rec h]
  refine' IH _ p
  unfold P at p p' ⊢
  dsimp
  rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc, mul_comm _ t, ←
    mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b r r' s t s' t' : R
p : EuclideanDomain.P a b (r, s, t)
p' : EuclideanDomain.P a b (r', s', t')
⊢ EuclideanDomain.P a b (xgcdAux r s t r' s' t')
[PROOFSTEP]
induction r, r' using GCD.induction generalizing s t s' t' with
| H0 n => simpa only [xgcd_zero_left]
| H1 _ _ h IH =>
  rw [xgcdAux_rec h]
  refine' IH _ p
  unfold P at p p' ⊢
  dsimp
  rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc, mul_comm _ t, ←
    mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
[GOAL]
case H0
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b n s t s' t' : R
p : EuclideanDomain.P a b (0, s, t)
p' : EuclideanDomain.P a b (n, s', t')
⊢ EuclideanDomain.P a b (xgcdAux 0 s t n s' t')
[PROOFSTEP]

| H0 n => simpa only [xgcd_zero_left]
[GOAL]
case H0
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b n s t s' t' : R
p : EuclideanDomain.P a b (0, s, t)
p' : EuclideanDomain.P a b (n, s', t')
⊢ EuclideanDomain.P a b (xgcdAux 0 s t n s' t')
[PROOFSTEP]
simpa only [xgcd_zero_left]
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (xgcdAux a✝ s t b✝ s' t')
[PROOFSTEP]

| H1 _ _ h IH =>
  rw [xgcdAux_rec h]
  refine' IH _ p
  unfold P at p p' ⊢
  dsimp
  rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc, mul_comm _ t, ←
    mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (xgcdAux a✝ s t b✝ s' t')
[PROOFSTEP]
rw [xgcdAux_rec h]
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (xgcdAux (b✝ % a✝) (s' - b✝ / a✝ * s) (t' - b✝ / a✝ * t) a✝ s t)
[PROOFSTEP]
refine' IH _ p
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p : EuclideanDomain.P a b (a✝, s, t)
p' : EuclideanDomain.P a b (b✝, s', t')
⊢ EuclideanDomain.P a b (b✝ % a✝, s' - b✝ / a✝ * s, t' - b✝ / a✝ * t)
[PROOFSTEP]
unfold P at p p' ⊢
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ match (b✝ % a✝, s' - b✝ / a✝ * s, t' - b✝ / a✝ * t) with
  | (r, s, t) => r = a * s + b * t
[PROOFSTEP]
dsimp
[GOAL]
case H1
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b a✝ b✝ : R
h : a✝ ≠ 0
IH :
  ∀ {s t s' t' : R},
    EuclideanDomain.P a b (b✝ % a✝, s, t) →
      EuclideanDomain.P a b (a✝, s', t') → EuclideanDomain.P a b (xgcdAux (b✝ % a✝) s t a✝ s' t')
s t s' t' : R
p :
  match (a✝, s, t) with
  | (r, s, t) => r = a * s + b * t
p' :
  match (b✝, s', t') with
  | (r, s, t) => r = a * s + b * t
⊢ b✝ % a✝ = a * (s' - b✝ / a✝ * s) + b * (t' - b✝ / a✝ * t)
[PROOFSTEP]
rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc, mul_comm _ t, ← mul_assoc,
  ← add_mul, ← p, mod_eq_sub_mul_div]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ gcd a b = a * gcdA a b + b * gcdB a b
[PROOFSTEP]
have :=
  @xgcdAux_P _ _ _ a b a b 1 0 0 1 (by dsimp [P]; rw [mul_one, mul_zero, add_zero])
    (by dsimp [P]; rw [mul_one, mul_zero, zero_add])
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ EuclideanDomain.P a b (a, 1, 0)
[PROOFSTEP]
dsimp [P]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = a * 1 + b * 0
[PROOFSTEP]
rw [mul_one, mul_zero, add_zero]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ EuclideanDomain.P a b (b, 0, 1)
[PROOFSTEP]
dsimp [P]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ b = a * 0 + b * 1
[PROOFSTEP]
rw [mul_one, mul_zero, zero_add]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
this : EuclideanDomain.P a b (xgcdAux a 1 0 b 0 1)
⊢ gcd a b = a * gcdA a b + b * gcdB a b
[PROOFSTEP]
rwa [xgcdAux_val, xgcd_val] at this
[GOAL]
R✝ : Type u
inst✝¹ : EuclideanDomain R✝
inst✝ : DecidableEq R✝
R : Type u_1
e : EuclideanDomain R
this : DecidableEq R
a b : R
h : a * b = 0
h0 : ¬a = 0 ∧ ¬b = 0
⊢ a = 0
[PROOFSTEP]
rw [← mul_div_cancel a h0.2, h, zero_div]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ lcm x y
[PROOFSTEP]
rw [lcm, hxy, div_zero]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ x ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : ¬gcd x y = 0
z : R
hz : y = gcd x y * z
⊢ x * z * gcd x y = x * y
[PROOFSTEP]
rw [mul_right_comm, mul_assoc, ← hz]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ lcm x y
[PROOFSTEP]
rw [lcm, hxy, div_zero]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : gcd x y = 0
⊢ y ∣ 0
[PROOFSTEP]
exact dvd_zero _
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : ¬gcd x y = 0
z : R
hz : x = gcd x y * z
⊢ gcd x y * (y * z) = x * y
[PROOFSTEP]
rw [← mul_assoc, mul_right_comm, ← hz]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
⊢ lcm x y ∣ z
[PROOFSTEP]
rw [lcm]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
by_cases hxy : gcd x y = 0
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
rw [hxy, div_zero]
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : gcd x y = 0
⊢ 0 ∣ z
[PROOFSTEP]
rw [EuclideanDomain.gcd_eq_zero_iff] at hxy
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : x = 0 ∧ y = 0
⊢ 0 ∣ z
[PROOFSTEP]
rwa [hxy.1] at hxz
[GOAL]
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
suffices x * y ∣ z * gcd x y by
  cases' this with p hp
  use p
  generalize gcd x y = g at hxy hs hp ⊢
  subst hs
  rw [mul_left_comm, mul_div_cancel_left _ hxy, ← mul_left_inj' hxy, hp]
  rw [← mul_assoc]
  simp only [mul_right_comm]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
this : x * y ∣ z * gcd x y
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
cases' this with p hp
[GOAL]
case intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
p : R
hp : z * gcd x y = x * y * p
⊢ x * y / gcd x y ∣ z
[PROOFSTEP]
use p
[GOAL]
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
p : R
hp : z * gcd x y = x * y * p
⊢ z = x * y / gcd x y * p
[PROOFSTEP]
generalize gcd x y = g at hxy hs hp ⊢
[GOAL]
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
r : R
hr : x = gcd x y * r
s p g : R
hxy : ¬g = 0
hs : y = g * s
hp : z * g = x * y * p
⊢ z = x * y / g * p
[PROOFSTEP]
subst hs
[GOAL]
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ z = x * (g * s) / g * p
[PROOFSTEP]
rw [mul_left_comm, mul_div_cancel_left _ hxy, ← mul_left_inj' hxy, hp]
[GOAL]
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ x * (g * s) * p = x * s * p * g
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
case h
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x z : R
hxz : x ∣ z
r s p g : R
hxy : ¬g = 0
hyz : g * s ∣ z
hr : x = gcd x (g * s) * r
hp : z * g = x * (g * s) * p
⊢ x * g * s * p = x * s * p * g
[PROOFSTEP]
simp only [mul_right_comm]
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * gcd x y
[PROOFSTEP]
rw [gcd_eq_gcd_ab, mul_add]
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (x * gcdA x y) + z * (y * gcdB x y)
[PROOFSTEP]
apply dvd_add
[GOAL]
case neg.intro.intro.intro.h₁
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (x * gcdA x y)
[PROOFSTEP]
rw [mul_left_comm]
[GOAL]
case neg.intro.intro.intro.h₁
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ x * (z * gcdA x y)
[PROOFSTEP]
exact mul_dvd_mul_left _ (hyz.mul_right _)
[GOAL]
case neg.intro.intro.intro.h₂
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (y * gcdB x y)
[PROOFSTEP]
rw [mul_left_comm, mul_comm]
[GOAL]
case neg.intro.intro.intro.h₂
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ y * x ∣ y * (z * gcdB x y)
[PROOFSTEP]
exact mul_dvd_mul_left _ (hxz.mul_right _)
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ lcm 0 x = 0
[PROOFSTEP]
rw [lcm, zero_mul, zero_div]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ lcm x 0 = 0
[PROOFSTEP]
rw [lcm, mul_zero, zero_div]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ lcm x y = 0 ↔ x = 0 ∨ y = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ lcm x y = 0 → x = 0 ∨ y = 0
[PROOFSTEP]
intro hxy
[GOAL]
case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : lcm x y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
rw [lcm, mul_div_assoc _ (gcd_dvd_right _ _), mul_eq_zero] at hxy
[GOAL]
case mp
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
apply Or.imp_right _ hxy
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
⊢ y / gcd x y = 0 → y = 0
[PROOFSTEP]
intro hy
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
⊢ y = 0
[PROOFSTEP]
by_cases hgxy : gcd x y = 0
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : gcd x y = 0
⊢ y = 0
[PROOFSTEP]
rw [EuclideanDomain.gcd_eq_zero_iff] at hgxy
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : x = 0 ∧ y = 0
⊢ y = 0
[PROOFSTEP]
exact hgxy.2
[GOAL]
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
⊢ y = 0
[PROOFSTEP]
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
hy : y / gcd x y = 0
hgxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ y = 0
[PROOFSTEP]
generalize gcd x y = g at hr hs hy hgxy ⊢
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hxy : x = 0 ∨ y / gcd x y = 0
r s g : R
hr : x = g * r
hs : y = g * s
hy : y / g = 0
hgxy : ¬g = 0
⊢ y = 0
[PROOFSTEP]
subst hs
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : g * s / g = 0
⊢ g * s = 0
[PROOFSTEP]
rw [mul_div_cancel_left _ hgxy] at hy
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x r s g : R
hr : x = g * r
hgxy : ¬g = 0
hxy : x = 0 ∨ g * s / gcd x (g * s) = 0
hy : s = 0
⊢ g * s = 0
[PROOFSTEP]
rw [hy, mul_zero]
[GOAL]
case mpr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ x = 0 ∨ y = 0 → lcm x y = 0
[PROOFSTEP]
rintro (hx | hy)
[GOAL]
case mpr.inl
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hx : x = 0
⊢ lcm x y = 0
[PROOFSTEP]
rw [hx, lcm_zero_left]
[GOAL]
case mpr.inr
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
hy : y = 0
⊢ lcm x y = 0
[PROOFSTEP]
rw [hy, lcm_zero_right]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * lcm x y = x * y
[PROOFSTEP]
rw [lcm]
[GOAL]
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * (x * y / gcd x y) = x * y
[PROOFSTEP]
by_cases h : gcd x y = 0
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y
[PROOFSTEP]
rw [h, zero_mul]
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ 0 = x * y
[PROOFSTEP]
rw [EuclideanDomain.gcd_eq_zero_iff] at h
[GOAL]
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : x = 0 ∧ y = 0
⊢ 0 = x * y
[PROOFSTEP]
rw [h.1, zero_mul]
[GOAL]
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y
[PROOFSTEP]
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ gcd x y * (x * y / gcd x y) = x * y
[PROOFSTEP]
generalize gcd x y = g at h hr ⊢
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y r s : R
hs : y = gcd x y * s
g : R
h : ¬g = 0
hr : x = g * r
⊢ g * (x * y / g) = x * y
[PROOFSTEP]
subst hr
[GOAL]
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
y r s g : R
h : ¬g = 0
hs : y = gcd (g * r) y * s
⊢ g * (g * r * y / g) = g * r * y
[PROOFSTEP]
rw [mul_assoc, mul_div_cancel_left _ h]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
⊢ a * b / (a * c) = b / c
[PROOFSTEP]
by_cases hc : c = 0
[GOAL]
case pos
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : c = 0
⊢ a * b / (a * c) = b / c
[PROOFSTEP]
simp [hc]
[GOAL]
case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c
[PROOFSTEP]
refine' eq_div_of_mul_eq_right hc (mul_left_cancel₀ ha _)
[GOAL]
case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * (c * (a * b / (a * c))) = a * b
[PROOFSTEP]
rw [← mul_assoc, ← mul_div_assoc _ (mul_dvd_mul_left a hcb), mul_div_cancel_left _ (mul_ne_zero ha hc)]
[GOAL]
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
⊢ a * b / (c * d) = a / c * (b / d)
[PROOFSTEP]
rcases eq_or_ne c 0 with (rfl | hc0)
[GOAL]
case inl
R : Type u
inst✝ : EuclideanDomain R
a b d : R
hbd : d ∣ b
hac : 0 ∣ a
⊢ a * b / (0 * d) = a / 0 * (b / d)
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
[PROOFSTEP]
rcases eq_or_ne d 0 with (rfl | hd0)
[GOAL]
case inr.inl
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hac : c ∣ a
hc0 : c ≠ 0
hbd : 0 ∣ b
⊢ a * b / (c * 0) = a / c * (b / 0)
[PROOFSTEP]
simp
[GOAL]
case inr.inr
R : Type u
inst✝ : EuclideanDomain R
a b c d : R
hac : c ∣ a
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
⊢ a * b / (c * d) = a / c * (b / d)
[PROOFSTEP]
obtain ⟨k1, rfl⟩ := hac
[GOAL]
case inr.inr.intro
R : Type u
inst✝ : EuclideanDomain R
b c d : R
hbd : d ∣ b
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 : R
⊢ c * k1 * b / (c * d) = c * k1 / c * (b / d)
[PROOFSTEP]
obtain ⟨k2, rfl⟩ := hbd
[GOAL]
case inr.inr.intro.intro
R : Type u
inst✝ : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)
[PROOFSTEP]
rw [mul_div_cancel_left _ hc0, mul_div_cancel_left _ hd0, mul_mul_mul_comm, mul_div_cancel_left _ (mul_ne_zero hc0 hd0)]