Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
import Std.Data.Int.Lemmas
import Std.Data.Rat.Basic

/-! # Additional lemmas about the Rational Numbers -/

namespace Rat

@[simp] theorem 
maybeNormalize_eq: ∀ {num : Int} {den g : Nat} (den_nz : den / g ≠ 0) (reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)), maybeNormalize num den g den_nz reduced = mk' (Int.div num ↑g) (den / g)
maybeNormalize_eq
{
num: ?m.2
num
den: ?m.5
den
g: ?m.8
g
} (
den_nz: ?m.11
den_nz
reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
reduced
) :
maybeNormalize: (num : Int) → (den g : Nat) → den / g ≠ 0 → Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g) → Rat
maybeNormalize
num: ?m.2
num
den: ?m.5
den
g: ?m.8
g
den_nz: ?m.11
den_nz
reduced: ?m.14
reduced
= { num :=
num: ?m.2
num
.
div: Int → Int → Int
div
g: ?m.8
g
, den :=
den: ?m.5
den
/
g: ?m.8
g
,
den_nz: ?m.11
den_nz
, reduced } :=

Goals accomplished! 🐙
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)


maybeNormalize num den g den_nz reduced = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)


(if hg : g = 1 then mk' num den else mk' (Int.div num ↑g) (den / g)) = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)


(if hg : g = 1 then mk' num den else mk' (Int.div num ↑g) (den / g)) = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)


maybeNormalize num den g den_nz reduced = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: g = 1


inl
mk' num den = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: ¬g = 1


inr
mk' (Int.div num ↑g) (den / g) = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)


maybeNormalize num den g den_nz reduced = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: g = 1


inl
mk' num den = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: g = 1


inl
mk' num den = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: ¬g = 1


inr
mk' (Int.div num ↑g) (den / g) = mk' (Int.div num ↑g) (den / g)
num: Int

den: Nat

den_nz: den / 1 ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑1)) (den / 1)


inl
mk' num den = mk' (Int.div num ↑1) (den / 1)
num: Int

den: Nat

den_nz: den / 1 ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑1)) (den / 1)


inl
mk' num den = mk' (Int.div num ↑1) (den / 1)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: g = 1


inl
mk' num den = mk' (Int.div num ↑g) (den / g)

Goals accomplished! 🐙
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)


maybeNormalize num den g den_nz reduced = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: ¬g = 1


inr
mk' (Int.div num ↑g) (den / g) = mk' (Int.div num ↑g) (den / g)
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

h✝: ¬g = 1


inr
mk' (Int.div num ↑g) (den / g) = mk' (Int.div num ↑g) (den / g)

Goals accomplished! 🐙
theorem
normalize.reduced': ∀ {num : Int} {den g : Nat}, den ≠ 0 → g = Nat.gcd (Int.natAbs num) den → Nat.coprime (Int.natAbs (num / ↑g)) (den / g)
normalize.reduced'
{
num: Int
num
:
Int: Type
Int
} {
den: Nat
den
g: Nat
g
:
Nat: Type
Nat
} (
den_nz: den ≠ 0
den_nz
:
den: Nat
den
≠
0: ?m.684
0
) (
e: g = Nat.gcd (Int.natAbs num) den
e
:
g: Nat
g
=
num: Int
num
.
natAbs: Int → Nat
natAbs
.
gcd: Nat → Nat → Nat
gcd
den: Nat
den
) : (
num: Int
num
/
g: Nat
g
).
natAbs: Int → Nat
natAbs
.
coprime: Nat → Nat → Prop
coprime
(
den: Nat
den
/
g: Nat
g
) :=

Goals accomplished! 🐙
num: Int

den, g: Nat

den_nz: den ≠ 0

e: g = Nat.gcd (Int.natAbs num) den


Nat.coprime (Int.natAbs (num / ↑g)) (den / g)
num: Int

den, g: Nat

den_nz: den ≠ 0

e: g = Nat.gcd (Int.natAbs num) den


Nat.coprime (Int.natAbs (num / ↑g)) (den / g)
num: Int

den, g: Nat

den_nz: den ≠ 0

e: g = Nat.gcd (Int.natAbs num) den


Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
num: Int

den, g: Nat

den_nz: den ≠ 0

e: g = Nat.gcd (Int.natAbs num) den


Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
num: Int

den, g: Nat

den_nz: den ≠ 0

e: g = Nat.gcd (Int.natAbs num) den


Nat.coprime (Int.natAbs (num / ↑g)) (den / g)

Goals accomplished! 🐙
theorem
normalize_eq: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mk' (num / ↑(Nat.gcd (Int.natAbs num) den)) (den / Nat.gcd (Int.natAbs num) den)
normalize_eq
{
num: ?m.905
num
den: Nat
den
} (
den_nz: ?m.911
den_nz
) :
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
num: ?m.905
num
den: ?m.908
den
den_nz: ?m.911
den_nz
= { num :=
num: ?m.905
num
/
num: ?m.905
num
.
natAbs: Int → Nat
natAbs
.
gcd: Nat → Nat → Nat
gcd
den: ?m.908
den
den :=
den: ?m.908
den
/
num: ?m.905
num
.
natAbs: Int → Nat
natAbs
.
gcd: Nat → Nat → Nat
gcd
den: ?m.908
den
den_nz :=
normalize.den_nz: ∀ {num : Int} {den g : Nat}, den ≠ 0 → g = Nat.gcd (Int.natAbs num) den → den / g ≠ 0
normalize.den_nz
den_nz: ?m.911
den_nz
rfl: ∀ {α : Sort ?u.1057} {a : α}, a = a
rfl
reduced :=
normalize.reduced': ∀ {num : Int} {den g : Nat}, den ≠ 0 → g = Nat.gcd (Int.natAbs num) den → Nat.coprime (Int.natAbs (num / ↑g)) (den / g)
normalize.reduced'
den_nz: ?m.911
den_nz
rfl: ∀ {α : Sort ?u.1076} {a : α}, a = a
rfl
} :=

Goals accomplished! 🐙
num: Int

den: Nat

den_nz: den ≠ 0


normalize num den = mk' (num / ↑(Nat.gcd (Int.natAbs num) den)) (den / Nat.gcd (Int.natAbs num) den)

Goals accomplished! 🐙
@[simp] theorem
normalize_zero: ∀ {d : Nat} (nz : d ≠ 0), normalize 0 d = 0
normalize_zero
(
nz: d ≠ 0
nz
) :
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
0: ?m.1378
0
d: ?m.1370
d
nz: ?m.1373
nz
=
0: ?m.1381
0
:=

Goals accomplished! 🐙
d: Nat

nz: d ≠ 0


normalize 0 d = 0
d: Nat

nz: d ≠ 0


mk' 0 1 = 0
d: Nat

nz: d ≠ 0


mk' 0 1 = 0
d: Nat

nz: d ≠ 0


normalize 0 d = 0

Goals accomplished! 🐙
theorem
mk_eq_normalize: ∀ (num : Int) (den : Nat) (nz : den ≠ 0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = normalize num den
mk_eq_normalize
(
num: ?m.1668
num
den: Nat
den
nz: den ≠ 0
nz
c: Nat.coprime (Int.natAbs num) den
c
) : ⟨
num: ?m.1668
num
,
den: ?m.1671
den
,
nz: ?m.1674
nz
,
c: ?m.1677
c
⟩ =
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
num: ?m.1668
num
den: ?m.1671
den
nz: ?m.1674
nz
:=

Goals accomplished! 🐙
num: Int

den: Nat

nz: den ≠ 0

c: Nat.coprime (Int.natAbs num) den


mk' num den = normalize num den

Goals accomplished! 🐙
theorem
normalize_self: ∀ (r : Rat), normalize r.num r.den = r
normalize_self
(
r: Rat
r
:
Rat: Type
Rat
) :
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
r: Rat
r
.
num: Rat → Int
num
r: Rat
r
.
den: Rat → Nat
den
r: Rat
r
.
den_nz: ∀ (self : Rat), self.den ≠ 0
den_nz
=
r: Rat
r
:= (
mk_eq_normalize: ∀ (num : Int) (den : Nat) (nz : den ≠ 0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = normalize num den
mk_eq_normalize
..).
symm: ∀ {α : Sort ?u.2002} {a b : α}, a = b → b = a
symm
theorem
normalize_mul_left: ∀ {d : Nat} {n : Int} {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0), normalize (↑a * n) (a * d) = normalize n d
normalize_mul_left
{
a: Nat
a
:
Nat: Type
Nat
} (
d0: d ≠ 0
d0
:
d: ?m.2026
d
≠
0: ?m.2074
0
) (
a0: a ≠ 0
a0
:
a: Nat
a
≠
0: ?m.2088
0
) :
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
(↑
a: Nat
a
*
n: ?m.2066
n
) (
a: Nat
a
*
d: ?m.2026
d
) (
Nat.mul_ne_zero: ∀ {n m : Nat}, n ≠ 0 → m ≠ 0 → n * m ≠ 0
Nat.mul_ne_zero
a0: a ≠ 0
a0
d0: d ≠ 0
d0
) =
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
n: ?m.2066
n
d: ?m.2026
d
d0: d ≠ 0
d0
:=

Goals accomplished! 🐙
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


normalize (↑a * n) (a * d) = normalize n d

Goals accomplished! 🐙
theorem
normalize_mul_right: ∀ {d : Nat} {n : Int} {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0), normalize (n * ↑a) (d * a) = normalize n d
normalize_mul_right
{
a: Nat
a
:
Nat: Type
Nat
} (
d0: d ≠ 0
d0
:
d: ?m.2780
d
≠
0: ?m.2825
0
) (
a0: a ≠ 0
a0
:
a: Nat
a
≠
0: ?m.2839
0
) :
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
(
n: ?m.2817
n
*
a: Nat
a
) (
d: ?m.2780
d
*
a: Nat
a
) (
Nat.mul_ne_zero: ∀ {n m : Nat}, n ≠ 0 → m ≠ 0 → n * m ≠ 0
Nat.mul_ne_zero
d0: d ≠ 0
d0
a0: a ≠ 0
a0
) =
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
n: ?m.2817
n
d: ?m.2780
d
d0: d ≠ 0
d0
:=

Goals accomplished! 🐙
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


normalize (n * ↑a) (d * a) = normalize n d
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


normalize (n * ↑a) (d * a) = normalize n d
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d)
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d)
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d)
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


normalize (n * ↑a) (d * a) = normalize n d
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


e_num
n * ↑a = ↑a * n
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


e_den
d * a = a * d
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d)

Goals accomplished! 🐙
d: Nat

n: Int

a: Nat

d0: d ≠ 0

a0: a ≠ 0


normalize (n * ↑a) (d * a) = normalize (↑a * n) (a * d)

Goals accomplished! 🐙

Goals accomplished! 🐙
theorem
normalize_eq_iff: ∀ {d₁ d₂ : Nat} {n₁ n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0), normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
normalize_eq_iff
(
z₁: d₁ ≠ 0
z₁
:
d₁: ?m.3267
d₁
≠
0: unknown metavariable '?_uniq.3326'
0
) (
z₂: d₂ ≠ 0
z₂
:
d₂: ?m.3287
d₂
≠
0: ?m.3382
0
) :
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
n₁: ?m.3320
n₁
d₁: ?m.3267
d₁
z₁: d₁ ≠ 0
z₁
=
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
n₂: ?m.3362
n₂
d₂: ?m.3287
d₂
z₂: d₂ ≠ 0
z₂
↔
n₁: ?m.3320
n₁
*
d₂: ?m.3287
d₂
=
n₂: ?m.3362
n₂
*
d₁: ?m.3267
d₁
:=

Goals accomplished! 🐙
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


mp
normalize n₁ d₁ = normalize n₂ d₂ → n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


mpr
n₁ * ↑d₂ = n₂ * ↑d₁ → normalize n₁ d₁ = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


mp
normalize n₁ d₁ = normalize n₂ d₂ → n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


mpr
n₁ * ↑d₂ = n₂ * ↑d₁ → normalize n₁ d₁ = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize n₁ d₁ = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize n₁ d₁ = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: normalize n₁ d₁ = normalize n₂ d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * (↑d₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂)) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑(d₂ / Nat.gcd (Int.natAbs n₂) d₂) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑(d₁ / Nat.gcd (Int.natAbs n₁) d₁) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * (↑d₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁)) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) * ↑d₁ * ↑(Nat.gcd (Int.natAbs n₂) d₂) = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) * ↑(Nat.gcd (Int.natAbs n₂) d₂) * ↑d₁ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) * ↑(Nat.gcd (Int.natAbs n₂) d₂) * ↑d₁ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ / ↑(Nat.gcd (Int.natAbs n₁) d₁) = n₂ / ↑(Nat.gcd (Int.natAbs n₂) d₂) ∧ d₁ / Nat.gcd (Int.natAbs n₁) d₁ = d₂ / Nat.gcd (Int.natAbs n₂) d₂

hn₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ n₁

hn₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ n₂

hd₁: ↑(Nat.gcd (Int.natAbs n₁) d₁) ∣ ↑d₁

hd₂: ↑(Nat.gcd (Int.natAbs n₂) d₂) ∣ ↑d₂


mp
n₂ * ↑d₁ = n₂ * ↑d₁

Goals accomplished! 🐙
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize n₁ d₁ = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize n₁ d₁ = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize n₁ d₁ = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize (n₁ * ↑d₂) (d₁ * d₂) = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize n₁ d₁ = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize (n₁ * ↑d₂) (d₁ * d₂) = normalize (↑d₁ * n₂) (d₁ * d₂)
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize n₁ d₁ = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize (n₁ * ↑d₂) (d₁ * d₂) = normalize (n₂ * ↑d₁) (d₁ * d₂)
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize n₁ d₁ = normalize n₂ d₂
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0

h: n₁ * ↑d₂ = n₂ * ↑d₁


mpr
normalize (n₂ * ↑d₁) (d₁ * d₂) = normalize (n₂ * ↑d₁) (d₁ * d₂)

Goals accomplished! 🐙
theorem
maybeNormalize_eq_normalize: ∀ {num : Int} {den g : Nat} (den_nz : den / g ≠ 0) (reduced : Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)), ↑g ∣ num → g ∣ den → maybeNormalize num den g den_nz reduced = normalize num den
maybeNormalize_eq_normalize
{
num: Int
num
:
Int: Type
Int
} {
den: Nat
den
g: Nat
g
:
Nat: Type
Nat
} (
den_nz: den / g ≠ 0
den_nz
reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)
reduced
) (
hn: ?m.4055 ∣ num
hn
: ↑
g: Nat
g
∣
num: Int
num
) (
hd: g ∣ den
hd
:
g: Nat
g
∣
den: Nat
den
) :
maybeNormalize: (num : Int) → (den g : Nat) → den / g ≠ 0 → Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g) → Rat
maybeNormalize
num: Int
num
den: Nat
den
g: Nat
g
den_nz: ?m.4044
den_nz
reduced: ?m.4047
reduced
=
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
num: Int
num
den: Nat
den
(
mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt
(: den = 0 → den / g = 0
(

Goals accomplished! 🐙
simp [·]): den = 0 → den / g = 0
simp [·]): den = 0 → den / g = 0
simp
simp [·]): den = 0 → den / g = 0
[·])
den_nz: ?m.4044
den_nz
) :=

Goals accomplished! 🐙
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den


maybeNormalize num den g den_nz reduced = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den


normalize (num / ↑g) (den / g) = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den


maybeNormalize num den g den_nz reduced = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den


normalize (num / ↑g) (den / g) = normalize num den

Goals accomplished! 🐙
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0


normalize (num / ↑g) (den / g) = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den


maybeNormalize num den g den_nz reduced = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0


normalize (num / ↑g) (den / g) = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0


normalize (num / ↑g * ↑g) (den / g * g) = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0


normalize (num / ↑g) (den / g) = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0


normalize num (den / g * g) = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0


normalize num (den / g * g) = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den


maybeNormalize num den g den_nz reduced = normalize num den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0


e_den
den / g * g = den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den

this: g ≠ 0


e_den
den / g * g = den
num: Int

den, g: Nat

den_nz: den / g ≠ 0

reduced: Nat.coprime (Int.natAbs (Int.div num ↑g)) (den / g)

hn: ↑g ∣ num

hd: g ∣ den


maybeNormalize num den g den_nz reduced = normalize num den

Goals accomplished! 🐙
@[simp] theorem
normalize_eq_zero: ∀ {d : Nat} {n : Int} (d0 : d ≠ 0), normalize n d = 0 ↔ n = 0
normalize_eq_zero
(
d0: d ≠ 0
d0
:
d: ?m.4799
d
≠
0: unknown metavariable '?_uniq.4805'
0
) :
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
n: ?m.4818
n
d: ?m.4799
d
d0: d ≠ 0
d0
=
0: ?m.4846
0
↔
n: ?m.4818
n
=
0: ?m.4864
0
:=

Goals accomplished! 🐙
d: Nat

n: Int

d0: d ≠ 0


normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = normalize ?refine'_2 1 ↔ ?refine'_1 * ↑1 = ?refine'_2 * ↑d


refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0


refine'_2
d: Nat

n: Int

d0: d ≠ 0


normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = normalize ?refine'_2 1 ↔ ?refine'_1 * ↑1 = ?refine'_2 * ↑d


refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0


refine'_2
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d


refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d


refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d


refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d


refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0


normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

this: normalize ?refine'_1 d = 0 ↔ ?refine'_1 * ↑1 = 0 * ↑d


refine'_3
normalize n d = 0 ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0


refine'_1
d: Nat

n: Int

d0: d ≠ 0

this: normalize n d = 0 ↔ n * ↑1 = 0 * ↑d


refine'_3
n * ↑1 = 0 * ↑d ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

this: normalize n d = 0 ↔ n * ↑1 = 0 * ↑d


refine'_3
n * ↑1 = 0 * ↑d ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0

this: normalize n d = 0 ↔ n * ↑1 = 0 * ↑d


refine'_3
n * ↑1 = 0 * ↑d ↔ n = 0
d: Nat

n: Int

d0: d ≠ 0


normalize n d = 0 ↔ n = 0

Goals accomplished! 🐙
theorem
normalize_num_den': ∀ (num : Int) (den : Nat) (nz : den ≠ 0), ∃ d, d ≠ 0 ∧ num = (normalize num den).num * ↑d ∧ den = (normalize num den).den * d
normalize_num_den'
(
num: Int
num
den: ?m.5050
den
nz: ?m.5053
nz
) : ∃
d: Nat
d
:
Nat: Type
Nat
,
d: Nat
d
≠
0: ?m.5063
0
∧
num: ?m.5047
num
= (
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
num: ?m.5047
num
den: ?m.5050
den
nz: ?m.5053
nz
).
num: Rat → Int
num
*
d: Nat
d
∧
den: ?m.5050
den
= (
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
num: ?m.5047
num
den: ?m.5050
den
nz: ?m.5053
nz
).
den: Rat → Nat
den
*
d: Nat
d
:=

Goals accomplished! 🐙
num: Int

den: Nat

nz: den ≠ 0


∃ d, d ≠ 0 ∧ num = (normalize num den).num * ↑d ∧ den = (normalize num den).den * d
num: Int

den: Nat

nz: den ≠ 0


num = (normalize num den).num * ↑(Nat.gcd (Int.natAbs num) den) ∧ den = (normalize num den).den * Nat.gcd (Int.natAbs num) den
num: Int

den: Nat

nz: den ≠ 0


∃ d, d ≠ 0 ∧ num = (normalize num den).num * ↑d ∧ den = (normalize num den).den * d

Goals accomplished! 🐙
theorem
normalize_num_den: ∀ {n : Int} {d : Nat} {z : d ≠ 0} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : Nat.coprime (Int.natAbs n') d'}, normalize n d = mk' n' d' → ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
normalize_num_den
(
h: normalize n d = mk' n' d'
h
:
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
n: ?m.5692
n
d: ?m.5697
d
z: ?m.5702
z
= ⟨
n': ?m.5715
n'
,
d': ?m.5728
d'
,
z': ?m.5741
z'
,
c: ?m.5754
c
⟩) : ∃
m: Nat
m
:
Nat: Type
Nat
,
m: Nat
m
≠
0: ?m.5775
0
∧
n: ?m.5692
n
=
n': ?m.5715
n'
*
m: Nat
m
∧
d: ?m.5697
d
=
d': ?m.5728
d'
*
m: Nat
m
:=

Goals accomplished! 🐙
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: Nat.coprime (Int.natAbs n') d'

h: normalize n d = mk' n' d'


∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: Nat.coprime (Int.natAbs n') d'

h: normalize n d = mk' n' d'

this: ∃ d_1, d_1 ≠ 0 ∧ n = (normalize n d).num * ↑d_1 ∧ d = (normalize n d).den * d_1


∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: Nat.coprime (Int.natAbs n') d'

h: normalize n d = mk' n' d'

this: ∃ d_1, d_1 ≠ 0 ∧ n = (normalize n d).num * ↑d_1 ∧ d = (normalize n d).den * d_1


∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: Nat.coprime (Int.natAbs n') d'

h: normalize n d = mk' n' d'


∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: Nat.coprime (Int.natAbs n') d'

h: normalize n d = mk' n' d'

this: ∃ d_1, d_1 ≠ 0 ∧ n = (normalize n d).num * ↑d_1 ∧ d = (normalize n d).den * d_1


∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: Nat.coprime (Int.natAbs n') d'

h: normalize n d = mk' n' d'

this: ∃ d_1, d_1 ≠ 0 ∧ n = (mk' n' d').num * ↑d_1 ∧ d = (mk' n' d').den * d_1


∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
n: Int

d: Nat

z: d ≠ 0

n': Int

d': Nat

z': d' ≠ 0

c: Nat.coprime (Int.natAbs n') d'

h: normalize n d = mk' n' d'

this: ∃ d_1, d_1 ≠ 0 ∧ n = (mk' n' d').num * ↑d_1 ∧ d = (mk' n' d').den * d_1


∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m

Goals accomplished! 🐙
theorem
normalize_eq_mkRat: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mkRat num den
normalize_eq_mkRat
{
num: ?m.5975
num
den: Nat
den
} (
den_nz: den ≠ 0
den_nz
) :
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
num: ?m.5975
num
den: ?m.5978
den
den_nz: ?m.5981
den_nz
=
mkRat: Int → Nat → Rat
mkRat
num: ?m.5975
num
den: ?m.5978
den
:=

Goals accomplished! 🐙
num: Int

den: Nat

den_nz: den ≠ 0


normalize num den = mkRat num den

Goals accomplished! 🐙
theorem
mkRat_num_den: ∀ {d : Nat} {n n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : Nat.coprime (Int.natAbs n') d'}, d ≠ 0 → mkRat n d = mk' n' d' → ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
mkRat_num_den
(
z: d ≠ 0
z
:
d: ?m.6164
d
≠
0: ?m.6297
0
) (
h: mkRat n d = mk' n' d'
h
:
mkRat: Int → Nat → Rat
mkRat
n: ?m.6183
n
d: ?m.6164
d
= ⟨
n': ?m.6210
n'
,
d': ?m.6237
d'
,
z': ?m.6264
z'
,
c: ?m.6291
c
⟩) : ∃
m: Nat
m
:
Nat: Type
Nat
,
m: Nat
m
≠
0: ?m.6326
0
∧
n: ?m.6183
n
=
n': ?m.6210
n'
*
m: Nat
m
∧
d: ?m.6164
d
=
d': ?m.6237
d'
*
m: Nat
m
:=
normalize_num_den: ∀ {n : Int} {d : Nat} {z : d ≠ 0} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : Nat.coprime (Int.natAbs n') d'}, normalize n d = mk' n' d' → ∃ m, m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m
normalize_num_den
((
normalize_eq_mkRat: ∀ {num : Int} {den : Nat} (den_nz : den ≠ 0), normalize num den = mkRat num den
normalize_eq_mkRat
z: d ≠ 0
z
).
symm: ∀ {α : Sort ?u.6502} {a b : α}, a = b → b = a
symm
▸
h: mkRat n d = mk' n' d'
h
) theorem
mkRat_def: ∀ (n : Int) (d : Nat), mkRat n d = if d0 : d = 0 then 0 else normalize n d
mkRat_def
(
n: ?m.6570
n
d: ?m.6573
d
) :
mkRat: Int → Nat → Rat
mkRat
n: ?m.6570
n
d: ?m.6573
d
= if
d0: ?m.6618
d0
:
d: ?m.6573
d
=
0: ?m.6579
0
then
0: ?m.6605
0
else
normalize: Int → (den : optParam Nat 1) → autoParam (den ≠ 0) _auto✝ → Rat
normalize
n: ?m.6570
n
d: ?m.6573
d
d0: ?m.6618
d0
:=
rfl: ∀ {α : Sort ?u.6643} {a : α}, a = a
rfl
theorem
mkRat_self: ∀ (a : Rat), mkRat a.num a.den = a
mkRat_self
(
a: Rat
a
:
Rat: Type
Rat
) :
mkRat: Int → Nat → Rat
mkRat
a: Rat
a
.
num: Rat → Int
num
a: Rat
a
.
den: Rat → Nat
den
=
a: Rat
a
:=

Goals accomplished! 🐙
a: Rat


mkRat a.num a.den = a
a: Rat


mkRat a.num a.den = a
a: Rat


normalize a.num a.den = a
a: Rat


mkRat a.num a.den = a
a: Rat


a = a

Goals accomplished! 🐙
theorem
mk_eq_mkRat: ∀ (num : Int) (den : Nat) (nz : den ≠ 0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = mkRat num den
mk_eq_mkRat
(
num: ?m.6801
num
den: Nat
den
nz: ?m.6807
nz
c: ?m.6810
c
) : ⟨
num: ?m.6801
num
,
den: ?m.6804
den
,
nz: ?m.6807
nz
,
c: ?m.6810
c
⟩ =
mkRat: Int → Nat → Rat
mkRat
num: ?m.6801
num
den: ?m.6804
den
:=

Goals accomplished! 🐙
num: Int

den: Nat

nz: den ≠ 0

c: Nat.coprime (Int.natAbs num) den


mk' num den = mkRat num den

Goals accomplished! 🐙
@[simp] theorem
zero_mkRat: ∀ (n : Nat), mkRat 0 n = 0
zero_mkRat
(
n: Nat
n
) :
mkRat: Int → Nat → Rat
mkRat
0: ?m.6975
0
n: ?m.6970
n
=
0: ?m.6984
0
:=

Goals accomplished! 🐙
n: Nat


mkRat 0 n = 0
n: Nat


(if h : n = 0 then 0 else 0) = 0
n: Nat


(if h : n = 0 then 0 else 0) = 0
n: Nat


mkRat 0 n = 0

Goals accomplished! 🐙
@[simp] theorem
mkRat_zero: ∀ (n : Int), mkRat n 0 = 0
mkRat_zero
(
n: ?m.7382
n
) :
mkRat: Int → Nat → Rat
mkRat
n: ?m.7382
n
0: ?m.7387
0
=
0: ?m.7396
0
:=

Goals accomplished! 🐙
n: Int


mkRat n 0 = 0

Goals accomplished! 🐙
theorem
mkRat_eq_zero: ∀ {d : Nat} {n : Int}, d ≠ 0 → (mkRat n d = 0 ↔ n = 0)
mkRat_eq_zero
(
d0: d ≠ 0
d0
:
d: ?m.7564
d
≠
0: ?m.7589
0
) :
mkRat: Int → Nat → Rat
mkRat
n: ?m.7583
n
d: ?m.7564
d
=
0: ?m.7602
0
↔
n: ?m.7583
n
=
0: ?m.7622
0
:=

Goals accomplished! 🐙
d: Nat

n: Int

d0: d ≠ 0


mkRat n d = 0 ↔ n = 0

Goals accomplished! 🐙
theorem
mkRat_ne_zero: ∀ {d : Nat} {n : Int}, d ≠ 0 → (mkRat n d ≠ 0 ↔ n ≠ 0)
mkRat_ne_zero
(
d0: d ≠ 0
d0
:
d: ?m.7819
d
≠
0: ?m.7845
0
) :
mkRat: Int → Nat → Rat
mkRat
n: ?m.7839
n
d: ?m.7819
d
≠
0: ?m.7859
0
↔
n: ?m.7839
n
≠
0: ?m.7870
0
:=
not_congr: ∀ {a b : Prop}, (a ↔ b) → (¬a ↔ ¬b)
not_congr
(
mkRat_eq_zero: ∀ {d : Nat} {n : Int}, d ≠ 0 → (mkRat n d = 0 ↔ n = 0)
mkRat_eq_zero
d0: d ≠ 0
d0
) theorem
mkRat_mul_left: ∀ {n : Int} {d a : Nat}, a ≠ 0 → mkRat (↑a * n) (a * d) = mkRat n d
mkRat_mul_left
{
a: Nat
a
:
Nat: Type
Nat
} (
a0: a ≠ 0
a0
:
a: Nat
a
≠
0: ?m.7985
0
) :
mkRat: Int → Nat → Rat
mkRat
(↑
a: Nat
a
*
n: ?m.7923
n
) (
a: Nat
a
*
d: ?m.7977
d
) =
mkRat: Int → Nat → Rat
mkRat
n: ?m.7923
n
d: ?m.7977
d
:=

Goals accomplished! 🐙
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (↑a * n) (a * d) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (↑a * n) (a * d) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0

d0: d = 0


mkRat (↑a * n) (a * d) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (↑a * n) (a * d) = mkRat n d

Goals accomplished! 🐙
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (↑a * n) (a * d) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0


mkRat (↑a * n) (a * d) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (↑a * n) (a * d) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0


mkRat (↑a * n) (a * d) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0


mkRat (↑a * n) (a * d) = normalize n d
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0


mkRat (↑a * n) (a * d) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0


mkRat (↑a * n) (a * d) = normalize (↑a * n) (a * d)
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0


mkRat (↑a * n) (a * d) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0

d0: ¬d = 0


mkRat (↑a * n) (a * d) = mkRat (↑a * n) (a * d)

Goals accomplished! 🐙
theorem
mkRat_mul_right: ∀ {n : Int} {d a : Nat}, a ≠ 0 → mkRat (n * ↑a) (d * a) = mkRat n d
mkRat_mul_right
{
a: Nat
a
:
Nat: Type
Nat
} (
a0: a ≠ 0
a0
:
a: Nat
a
≠
0: ?m.8381
0
) :
mkRat: Int → Nat → Rat
mkRat
(
n: ?m.8262
n
*
a: Nat
a
) (
d: ?m.8373
d
*
a: Nat
a
) =
mkRat: Int → Nat → Rat
mkRat
n: ?m.8262
n
d: ?m.8373
d
:=

Goals accomplished! 🐙
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (n * ↑a) (d * a) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (n * ↑a) (d * a) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (n * ↑a) (d * a) = mkRat n d
n: Int

d, a: Nat

a0: a ≠ 0


e_num
n * ↑a = ↑a * n
n: Int

d, a: Nat

a0: a ≠ 0


e_den
d * a = a * d
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)

Goals accomplished! 🐙
n: Int

d, a: Nat

a0: a ≠ 0


mkRat (n * ↑a) (d * a) = mkRat (↑a * n) (a * d)

Goals accomplished! 🐙

Goals accomplished! 🐙
theorem
mkRat_eq_iff: ∀ {d₁ d₂ : Nat} {n₁ n₂ : Int}, d₁ ≠ 0 → d₂ ≠ 0 → (mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁)
mkRat_eq_iff
(
z₁: d₁ ≠ 0
z₁
:
d₁: ?m.8746
d₁
≠
0: unknown metavariable '?_uniq.8805'
0
) (
z₂: d₂ ≠ 0
z₂
:
d₂: ?m.8766
d₂
≠
0: ?m.8852
0
) :
mkRat: Int → Nat → Rat
mkRat
n₁: ?m.8799
n₁
d₁: ?m.8746
d₁
=
mkRat: Int → Nat → Rat
mkRat
n₂: ?m.8832
n₂
d₂: ?m.8766
d₂
↔
n₁: ?m.8799
n₁
*
d₂: ?m.8766
d₂
=
n₂: ?m.8832
n₂
*
d₁: ?m.8746
d₁
:=

Goals accomplished! 🐙
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


normalize n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


normalize n₁ d₁ = normalize n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁
d₁, d₂: Nat

n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


n₁ * ↑d₂ = n₂ * ↑d₁ ↔ n₁ * ↑d₂ = n₂ * ↑d₁

Goals accomplished! 🐙
@[simp] theorem
divInt_ofNat: ∀ (num : Int) (den : Nat), num /. ↑den = mkRat num den
divInt_ofNat
(
num: ?m.9108
num
den: ?m.9111
den
) :
num: ?m.9108
num
/. (
den: ?m.9111
den
:
Nat: Type
Nat
) =
mkRat: Int → Nat → Rat
mkRat
num: ?m.9108
num
den: ?m.9111
den
:=

Goals accomplished! 🐙
num: Int

den: Nat


num /. ↑den = mkRat num den

Goals accomplished! 🐙
theorem
mk_eq_divInt: ∀ (num : Int) (den : Nat) (nz : den ≠ 0) (c : Nat.coprime (Int.natAbs num) den), mk' num den = num /. ↑den
mk_eq_divInt
(
num: ?m.9212
num
den: ?m.9215
den
nz: ?m.9218
nz
c: ?m.9221
c
) : ⟨
num: ?m.9212
num
,
den: ?m.9215
den
,
nz: ?m.9218
nz
,
c: ?m.9221
c
⟩ =
num: ?m.9212
num
/. (
den: ?m.9215
den
:
Nat: Type
Nat
) :=

Goals accomplished! 🐙
num: Int

den: Nat

nz: den ≠ 0

c: Nat.coprime (Int.natAbs num) den


mk' num den = num /. ↑den

Goals accomplished! 🐙
theorem
divInt_self: ∀ (a : Rat), a.num /. ↑a.den = a
divInt_self
(
a: Rat
a
:
Rat: Type
Rat
) :
a: Rat
a
.
num: Rat → Int
num
/.
a: Rat
a
.
den: Rat → Nat
den
=
a: Rat
a
:=

Goals accomplished! 🐙
a: Rat


a.num /. ↑a.den = a
a: Rat


a.num /. ↑a.den = a
a: Rat


mkRat a.num a.den = a
a: Rat


a.num /. ↑a.den = a
a: Rat


a = a

Goals accomplished! 🐙
@[simp] theorem
zero_divInt: ∀ (n : Int), 0 /. n = 0
zero_divInt
(
n: ?m.9456
n
) :
0: ?m.9461
0
/.
n: ?m.9456
n
=
0: ?m.9470
0
:=

Goals accomplished! 🐙
n: Int


0 /. n = 0
a✝: Nat


ofNat
0 /. Int.ofNat a✝ = 0
a✝: Nat


negSucc
0 /. Int.negSucc a✝ = 0
n: Int


0 /. n = 0
a✝: Nat


ofNat
0 /. Int.ofNat a✝ = 0
a✝: Nat


negSucc
0 /. Int.negSucc a✝ = 0
n: Int


0 /. n = 0

Goals accomplished! 🐙
@[simp] theorem
divInt_zero: ∀ (n : Int), n /. 0 = 0
divInt_zero
(
n: Int
n
) :
n: ?m.9758
n
/.
0: ?m.9763
0
=
0: ?m.9772
0
:=
mkRat_zero: ∀ (n : Int), mkRat n 0 = 0
mkRat_zero
n: Int
n
theorem
neg_divInt_neg: ∀ (num den : Int), -num /. -den = num /. den
neg_divInt_neg
(
num: ?m.9818
num
den: ?m.9821
den
) : -
num: ?m.9818
num
/. -
den: ?m.9821
den
=
num: ?m.9818
num
/.
den: ?m.9821
den
:=

Goals accomplished! 🐙
num, den: Int


-num /. -den = num /. den
num, den: Int


-num /. -den = num /. den
num, den: Int

n: Nat


-num /. -↑(Nat.succ n) = num /. ↑(Nat.succ n)
num, den: Int


-num /. -den = num /. den

Goals accomplished! 🐙
num, den: Int


-num /. -den = num /. den
num, den: Int


-num /. -0 = num /. 0
num, den: Int


-num /. -den = num /. den

Goals accomplished! 🐙
num, den: Int


-num /. -den = num /. den
num, den: Int

n: Nat


num, den: Int


-num /. -den = num /. den

Goals accomplished! 🐙
theorem
divInt_neg': ∀ (num den : Int), num /. -den = -num /. den
divInt_neg'
(
num: ?m.11657
num
den: ?m.11660
den
) :
num: ?m.11657
num
/. -
den: ?m.11660
den
= -
num: ?m.11657
num
/.
den: ?m.11660
den
:=

Goals accomplished! 🐙
num, den: Int


num /. -den = -num /. den
num, den: Int


num /. -den = -num /. den
num, den: Int


-num /. - -den = -num /. den
num, den: Int


num /. -den = -num /. den
num, den: Int


-num /. den = -num /. den

Goals accomplished! 🐙
theorem
divInt_eq_iff: ∀ {d₁ d₂ n₁ n₂ : Int}, d₁ ≠ 0 → d₂ ≠ 0 → (n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁)
divInt_eq_iff
(
z₁: d₁ ≠ 0
z₁
:
d₁: ?m.11710
d₁
≠
0: unknown metavariable '?_uniq.11736'
0
) (
z₂: d₂ ≠ 0
z₂
:
d₂: ?m.11730
d₂
≠
0: unknown metavariable '?_uniq.11750'
0
) :
n₁: ?m.11763
n₁
/.
d₁: ?m.11710
d₁
=
n₂: ?m.11796
n₂
/.
d₂: ?m.11730
d₂
↔
n₁: ?m.11763
n₁
*
d₂: ?m.11730
d₂
=
n₂: ?m.11796
n₂
*
d₁: ?m.11710
d₁
:=

Goals accomplished! 🐙
d₁, d₂, n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁
d₂, n₁, n₂: Int

z₂: d₂ ≠ 0

w✝: Nat

z₁: ↑w✝ ≠ 0


intro.inl
n₁ /. ↑w✝ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * ↑w✝
d₂, n₁, n₂: Int

z₂: d₂ ≠ 0

w✝: Nat

z₁: -↑w✝ ≠ 0


intro.inr
n₁ /. -↑w✝ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * -↑w✝
d₁, d₂, n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁
d₂, n₁, n₂: Int

z₂: d₂ ≠ 0

w✝: Nat

z₁: ↑w✝ ≠ 0


intro.inl
n₁ /. ↑w✝ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * ↑w✝
d₂, n₁, n₂: Int

z₂: d₂ ≠ 0

w✝: Nat

z₁: -↑w✝ ≠ 0


intro.inr
n₁ /. -↑w✝ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * -↑w✝
d₁, d₂, n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁
n₁, n₂: Int

w✝¹: Nat

z₁: ↑w✝¹ ≠ 0

w✝: Nat

z₂: ↑w✝ ≠ 0


intro.inl.intro.inl
n₁ /. ↑w✝¹ = n₂ /. ↑w✝ ↔ n₁ * ↑w✝ = n₂ * ↑w✝¹
n₁, n₂: Int

w✝¹: Nat

z₁: ↑w✝¹ ≠ 0

w✝: Nat

z₂: -↑w✝ ≠ 0


intro.inl.intro.inr
n₁ /. ↑w✝¹ = n₂ /. -↑w✝ ↔ n₁ * -↑w✝ = n₂ * ↑w✝¹
d₁, d₂, n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁
n₁, n₂: Int

w✝¹: Nat

z₁: ↑w✝¹ ≠ 0

w✝: Nat

z₂: ↑w✝ ≠ 0


intro.inl.intro.inl
n₁ /. ↑w✝¹ = n₂ /. ↑w✝ ↔ n₁ * ↑w✝ = n₂ * ↑w✝¹
n₁, n₂: Int

w✝¹: Nat

z₁: ↑w✝¹ ≠ 0

w✝: Nat

z₂: -↑w✝ ≠ 0


intro.inl.intro.inr
n₁ /. ↑w✝¹ = n₂ /. -↑w✝ ↔ n₁ * -↑w✝ = n₂ * ↑w✝¹
n₁, n₂: Int

w✝¹: Nat

z₁: -↑w✝¹ ≠ 0

w✝: Nat

z₂: ↑w✝ ≠ 0


intro.inr.intro.inl
n₁ /. -↑w✝¹ = n₂ /. ↑w✝ ↔ n₁ * ↑w✝ = n₂ * -↑w✝¹
n₁, n₂: Int

w✝¹: Nat

z₁: -↑w✝¹ ≠ 0

w✝: Nat

z₂: -↑w✝ ≠ 0


intro.inr.intro.inr
n₁ /. -↑w✝¹ = n₂ /. -↑w✝ ↔ n₁ * -↑w✝ = n₂ * -↑w✝¹
d₁, d₂, n₁, n₂: Int

z₁: d₁ ≠ 0

z₂: d₂ ≠ 0


n₁ /. d₁ = n₂ /. d₂ ↔ n₁ * d₂ = n₂ * d₁

Goals accomplished! 🐙
theorem
divInt_mul_left: ∀ {n d a : Int}, a ≠ 0 → a * n /. (a * d) = n /. d
divInt_mul_left
{
a: Int
a
:
Int: Type
Int
} (
a0: a ≠ 0
a0
:
a: Int
a
≠
0: ?m.15110
0
) : (
a: Int
a
*
n: ?m.15051
n
) /. (
a: Int
a
*
d: ?m.15102
d
) =
n: ?m.15051
n
/.
d: ?m.15102
d
:=