/-
Copyright (c) 2018 Louis Carlin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Louis Carlin, Mario Carneiro

! This file was ported from Lean 3 source module algebra.euclidean_domain.instances
! leanprover-community/mathlib commit e1bccd6e40ae78370f01659715d3c948716e3b7e
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.EuclideanDomain.Defs
import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.GroupWithZero.Units.Lemmas
import Mathlib.Algebra.Order.Ring.Lemmas
import Mathlib.Init.Data.Int.Order
import Mathlib.Data.Int.Basic
import Mathlib.Data.Nat.Order.Basic
import Mathlib.Data.Int.Order.Basic

/-!
# Instances for Euclidean domains
* `Int.euclideanDomain`: shows that `ℤ` is a Euclidean domain.
* `Field.toEuclideanDomain`: shows that any field is a Euclidean domain.
-/

instance 
Int.euclideanDomain: EuclideanDomain ℤ
Int.euclideanDomain : 
EuclideanDomain: Type ?u.2 → Type ?u.2
EuclideanDomain 
ℤ: Type
ℤ :=
  { 
inferInstanceAs: (α : Sort ?u.6) → [i : α] → α
inferInstanceAs (
CommRing: Type ?u.7 → Type ?u.7
CommRing 
Int: Type
Int), 
inferInstanceAs: ∀ (α : Sort ?u.18) [i : α], α
inferInstanceAs (
Nontrivial: Type ?u.19 → Prop
Nontrivial 
Int: Type
Int) with
    add := 
(· + ·): ℤ → ℤ → ℤ
(· + ·), mul := 
(· * ·): ℤ → ℤ → ℤ
(· * ·), one := 
1: ?m.413
1, zero := 
0: ?m.147
0,
    neg := 
Neg.neg: {α : Type ?u.495} → [self : Neg α] → α → α
Neg.neg,
    quotient := 
(· / ·): ℤ → ℤ → ℤ
(· / ·), quotient_zero := 
Int.ediv_zero: ∀ (a : ℤ), a / 0 = 0
Int.ediv_zero, remainder := 
(· % ·): ℤ → ℤ → ℤ
(· % ·),
    quotient_mul_add_remainder_eq := 
Int.ediv_add_emod: ∀ (a b : ℤ), b * (a / b) + a % b = a
Int.ediv_add_emod,
    r := fun 
a: ?m.748
a 
b: ?m.751
b => 
a: ?m.748
a.
natAbs: ℤ → ℕ
natAbs < 
b: ?m.751
b.
natAbs: ℤ → ℕ
natAbs,
    r_wellFounded := (
measure: {α : Sort ?u.765} → (α → ℕ) → WellFoundedRelation α
measure 
natAbs: ℤ → ℕ
natAbs).
wf: ∀ {α : Sort ?u.770} [self : WellFoundedRelation α], WellFounded WellFoundedRelation.rel
wf
    remainder_lt := fun 
a: ?m.782
a 
b: ?m.785
b 
b0: ?m.788
b0 => 
Int.ofNat_lt: ∀ {n m : ℕ}, ↑n < ↑m ↔ n < m
Int.ofNat_lt.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 <| by
Goals accomplished! 🐙
      
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

↑(natAbs ((fun x x_1 => x % x_1) a b)) < ↑(natAbs b)rw [
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

↑(natAbs ((fun x x_1 => x % x_1) a b)) < ↑(natAbs b)
Int.natAbs_of_nonneg: ∀ {a : ℤ}, 0 ≤ a → ↑(natAbs a) = a
Int.natAbs_of_nonneg (
Int.emod_nonneg: ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → 0 ≤ a % b
Int.emod_nonneg 
_: ℤ
_ 
b0: b ≠ 0
b0),
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

a % b < ↑(natAbs b) 
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

↑(natAbs ((fun x x_1 => x % x_1) a b)) < ↑(natAbs b)← 
Int.abs_eq_natAbs: ∀ (a : ℤ), abs a = ↑(natAbs a)
Int.abs_eq_natAbs
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

a % b < abs b]
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

a % b < abs b
      
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

↑(natAbs ((fun x x_1 => x % x_1) a b)) < ↑(natAbs b)exact 
Int.emod_lt: ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → a % b < abs b
Int.emod_lt 
_: ℤ
_ 
b0: b ≠ 0
b0
Goals accomplished! 🐙
    mul_left_not_lt := fun 
a: ?m.812
a 
b: ?m.815
b 
b0: ?m.818
b0 =>
      
not_lt_of_ge: ∀ {α : Type ?u.820} [inst : Preorder α] {a b : α}, a ≥ b → ¬a < b
not_lt_of_ge <| by
Goals accomplished! 🐙
        
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

natAbs (a * b) ≥ natAbs arw [
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

natAbs (a * b) ≥ natAbs a← 
mul_one: ∀ {M : Type ?u.949} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one 
a: ℤ
a.
natAbs: ℤ → ℕ
natAbs,
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

natAbs (a * b) ≥ natAbs a * 1 
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

natAbs (a * b) ≥ natAbs a
Int.natAbs_mul: ∀ (a b : ℤ), natAbs (a * b) = natAbs a * natAbs b
Int.natAbs_mul
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

natAbs a * natAbs b ≥ natAbs a * 1]
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

natAbs a * natAbs b ≥ natAbs a * 1
        
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

natAbs (a * b) ≥ natAbs arw [
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

natAbs a * natAbs b ≥ natAbs a * 1←
Int.natAbs_pos: ∀ {a : ℤ}, 0 < natAbs a ↔ a ≠ 0
Int.natAbs_pos
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: 0 < natAbs b

natAbs a * natAbs b ≥ natAbs a * 1]
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: 0 < natAbs b

natAbs a * natAbs b ≥ natAbs a * 1 at 
b0: b ≠ 0
b0
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: 0 < natAbs b

natAbs a * natAbs b ≥ natAbs a * 1
        
src✝¹:= inferInstanceAs (CommRing ℤ): CommRing ℤ

src✝:= inferInstanceAs (Nontrivial ℤ): Nontrivial ℤ

a, b: ℤ

b0: b ≠ 0

natAbs (a * b) ≥ natAbs aexact 
Nat.mul_le_mul_of_nonneg_left: ∀ {a b c : ℕ}, a ≤ b → c * a ≤ c * b
Nat.mul_le_mul_of_nonneg_left 
b0: 0 < natAbs b
b0
Goals accomplished! 🐙  }

-- Porting note: this seems very slow.
-- see Note [lower instance priority]
instance (priority := 100) 
Field.toEuclideanDomain: {K : Type ?u.2448} → [inst : Field K] → EuclideanDomain K
Field.toEuclideanDomain {
K: Type ?u.2448
K : 
Type _: Type (?u.2448+1)
Type _} [
Field: Type ?u.2451 → Type ?u.2451
Field 
K: Type ?u.2448
K] : 
EuclideanDomain: Type ?u.2454 → Type ?u.2454
EuclideanDomain 
K: Type ?u.2448
K :=
  { ‹Field K› with
    add := 
(· + ·): K → K → K
(· + ·), mul := 
(· * ·): K → K → K
(· * ·), one := 
1: ?m.3123
1, zero := 
0: ?m.2705
0, neg := 
Neg.neg: {α : Type ?u.3336} → [self : Neg α] → α → α
Neg.neg,
    quotient := 
(· / ·): K → K → K
(· / ·), remainder := fun 
a: ?m.3635
a 
b: ?m.3638
b => 
a: ?m.3635
a - 
a: ?m.3635
a * 
b: ?m.3638
b / 
b: ?m.3638
b, quotient_zero := 
div_zero: ∀ {G₀ : Type ?u.3589} [inst : GroupWithZero G₀] (a : G₀), a / 0 = 0
div_zero,
    quotient_mul_add_remainder_eq := fun 
a: ?m.3866
a 
b: ?m.3869
b => by
Goals accomplished! 🐙
      -- Porting note: was `by_cases h : b = 0 <;> simp [h, mul_div_cancel']`
      
K: Type ?u.2448

inst✝: Field K

src✝:= 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 = aby_cases 
h: ?m.4972
h : 
b: K
b = 
0: ?m.4799
0
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (fun x x_1 => x / x_1) a b + (fun a b => a - a * b / b) a b = a
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
b * (fun x x_1 => x / x_1) a b + (fun a b => a - a * b / b) a b = a 
K: Type ?u.2448

inst✝: Field K

src✝:= 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<;>
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (fun x x_1 => x / x_1) a b + (fun a b => a - a * b / b) a b = a
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
b * (fun x x_1 => x / x_1) a b + (fun a b => a - a * b / b) a b = a 
K: Type ?u.2448

inst✝: Field K

src✝:= 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 = adsimp only
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = a
      
K: Type ?u.2448

inst✝: Field K

src✝:= 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·
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = a 
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = a
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
b * (a / b) + (a - a * b / b) = adsimp only
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = a
        
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = arw [
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = a
h: ?m.4965
h,
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
0 * (a / 0) + (a - a * 0 / 0) = a 
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = a
zero_mul: ∀ {M₀ : Type ?u.5043} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0
zero_mul,
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
0 + (a - a * 0 / 0) = a 
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = a
mul_zero: ∀ {M₀ : Type ?u.5171} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
mul_zero,
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
0 + (a - 0 / 0) = a 
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = a
zero_div: ∀ {G₀ : Type ?u.5202} [inst : GroupWithZero G₀] (a : G₀), 0 / a = 0
zero_div,
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
0 + (a - 0) = a 
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = a
zero_add: ∀ {M : Type ?u.5256} [inst : AddZeroClass M] (a : M), 0 + a = a
zero_add,
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
a - 0 = a 
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
b * (a / b) + (a - a * b / b) = a
sub_zero: ∀ {G : Type ?u.5360} [inst : SubNegZeroMonoid G] (a : G), a - 0 = a
sub_zero
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: b = 0

pos
a = a]
Goals accomplished! 🐙
      
K: Type ?u.2448

inst✝: Field K

src✝:= 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·
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
b * (a / b) + (a - a * b / b) = a 
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
b * (a / b) + (a - a * b / b) = adsimp only
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
b * (a / b) + (a - a * b / b) = a
        
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
b * (a / b) + (a - a * b / b) = arw [
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
b * (a / b) + (a - a * b / b) = a
mul_div_cancel': ∀ {G₀ : Type ?u.5492} [inst : CommGroupWithZero G₀] {b : G₀} (a : G₀), b ≠ 0 → b * (a / b) = a
mul_div_cancel' 
_: ?m.5493
_ 
h: ?m.4972
h
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
a + (a - a * b / b) = a]
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
a + (a - a * b / b) = a
        
K: Type ?u.2448

inst✝: Field K

src✝:= inst✝: Field K

a, b: K

h: ¬b = 0

neg
b * (a / b) + (a - a * b / b) = asimp only [
ne_eq: ∀ {α : Sort ?u.5547} (a b : α), (a ≠ b) = ¬a = b
ne_eq, 
h: ?m.4972
h, 
not_false_iff: ¬False ↔ True
not_false_iff, 
mul_div_cancel: ∀ {G₀ : Type ?u.5565} [inst : GroupWithZero G₀] {b : G₀} (a : G₀), b ≠ 0 → a * b / b = a
mul_div_cancel, 
sub_self: ∀ {G : Type ?u.5589} [inst : AddGroup G] (a : G), a - a = 0
sub_self, 
add_zero: ∀ {M : Type ?u.5603} [inst : AddZeroClass M] (a : M), a + 0 = a
add_zero]
Goals accomplished! 🐙
    r := fun 
a: ?m.3878
a 
b: ?m.3881
b => 
a: ?m.3878
a = 
0: ?m.3885
0 ∧ 
b: ?m.3881
b ≠ 
0: ?m.3904
0,
    r_wellFounded :=
      
WellFounded.intro: ∀ {α : Sort ?u.3910} {r : α → α → Prop}, (∀ (a : α), Acc r a) → WellFounded r
WellFounded.intro fun 
a: ?m.3922
a =>
        (
Acc.intro: ∀ {α : Sort ?u.3924} {r : α → α → Prop} (x : α), (∀ (y : α), r y x → Acc r y) → Acc r x
Acc.intro 
_: ?m.3925
_) fun 
b: ?m.3939
b ⟨
hb: b = 0
hb, _⟩ => (
Acc.intro: ∀ {α : Sort ?u.3972} {r : α → α → Prop} (x : α), (∀ (y : α), r y x → Acc r y) → Acc r x
Acc.intro 
_: ?m.3973
_) fun 
c: ?m.3982
c ⟨_, 
hnb: b ≠ 0
hnb⟩ => 
False.elim: ∀ {C : Sort ?u.4012}, False → C
False.elim <| 
hnb: b ≠ 0
hnb 
hb: b = 0
hb,
    remainder_lt := fun 
a: ?m.4148
a 
b: ?m.4151
b 
hnb: ?m.4154
hnb => by
Goals accomplished! 🐙 
K: Type ?u.2448

inst✝: Field K

src✝:= 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) bsimp [
hnb: b ≠ 0
hnb]
Goals accomplished! 🐙,
    mul_left_not_lt := fun 
a: ?m.4168
a 
b: ?m.4171
b 
hnb: ?m.4174
hnb ⟨
hab: a * b = 0
hab, 
hna: a ≠ 0
hna⟩ => 
Or.casesOn: ∀ {a b : Prop} {motive : a ∨ b → Prop} (t : a ∨ b),
  (∀ (h : a), motive (_ : a ∨ b)) → (∀ (h : b), motive (_ : a ∨ b)) → motive t
Or.casesOn (
mul_eq_zero: ∀ {M₀ : Type ?u.4299} [inst : MulZeroClass M₀] [inst_1 : NoZeroDivisors M₀] {a b : M₀}, a * b = 0 ↔ a = 0 ∨ b = 0
mul_eq_zero.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 
hab: a * b = 0
hab) 
hna: a ≠ 0
hna 
hnb: ?m.4174
hnb }
#align field.to_euclidean_domain 
Field.toEuclideanDomain: {K : Type u_1} → [inst : Field K] → EuclideanDomain K
Field.toEuclideanDomain