[GOAL]
⊢ DivisionRing ℚ
[PROOFSTEP]
infer_instance


[GOAL]
x : ℚ
⊢ 0 ≤ x ↔ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
[PROOFSTEP]
refine'
  ⟨fun hx => _, fun hx =>
    AddSubmonoid.closure_induction hx (by rintro - ⟨s, rfl⟩; exact mul_self_nonneg s) le_rfl fun _ _ => add_nonneg⟩
    /- If `x = p / q`, then, since `0 ≤ x`, we have `p q : ℕ`, and `p / q` is the sum of `p * q`
          copies of `(1 / q) ^ 2`, and so `x` lies in the `AddSubmonoid` generated by square elements.

          Note: it's possible to rephrase this argument as `x = (p * q) • (1 / q) ^ 2`, but this would
          be somewhat challenging without increasing import requirements. -/
        -- Porting note: rewrote proof to avoid removed constructor rat.mk_pnat
[GOAL]
x : ℚ
hx : x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
⊢ ∀ (x : ℚ), (x ∈ Set.range fun s => star s * s) → 0 ≤ x
[PROOFSTEP]
rintro - ⟨s, rfl⟩
[GOAL]
case intro
x : ℚ
hx : x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
s : ℚ
⊢ 0 ≤ (fun s => star s * s) s
[PROOFSTEP]
exact mul_self_nonneg s
[GOAL]
x : ℚ
hx : 0 ≤ x
⊢ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
[PROOFSTEP]
suffices (Finset.range (x.num.natAbs * x.den)).sum (Function.const ℕ ((1 : ℚ) / x.den * ((1 : ℚ) / x.den))) = x by
  exact this ▸ sum_mem fun n _ => AddSubmonoid.subset_closure ⟨_, rfl⟩
[GOAL]
x : ℚ
hx : 0 ≤ x
this : Finset.sum (Finset.range (Int.natAbs x.num * x.den)) (Function.const ℕ (1 / ↑x.den * (1 / ↑x.den))) = x
⊢ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
[PROOFSTEP]
exact this ▸ sum_mem fun n _ => AddSubmonoid.subset_closure ⟨_, rfl⟩
[GOAL]
x : ℚ
hx : 0 ≤ x
⊢ Finset.sum (Finset.range (Int.natAbs x.num * x.den)) (Function.const ℕ (1 / ↑x.den * (1 / ↑x.den))) = x
[PROOFSTEP]
simp only [Function.const_apply, Finset.sum_const, Finset.card_range, nsmul_eq_mul]
[GOAL]
x : ℚ
hx : 0 ≤ x
⊢ ↑(Int.natAbs x.num * x.den) * (1 / ↑x.den * (1 / ↑x.den)) = x
[PROOFSTEP]
rw [← Int.cast_ofNat, Int.ofNat_mul, Int.coe_natAbs, abs_of_nonneg (num_nonneg_iff_zero_le.mpr hx), Int.cast_mul,
  Int.cast_ofNat]
[GOAL]
x : ℚ
hx : 0 ≤ x
⊢ ↑x.num * ↑x.den * (1 / ↑x.den * (1 / ↑x.den)) = x
[PROOFSTEP]
rw [← mul_assoc, mul_assoc (x.num : ℚ), mul_one_div_cancel (Nat.cast_ne_zero.mpr x.pos.ne'), mul_one, mul_one_div,
  Rat.num_div_den]


[GOAL]
d : ℕ
h : d ≠ 0
w : Nat.coprime (Int.natAbs 0) d
⊢ mk' 0 d = 0
[PROOFSTEP]
congr
[GOAL]
q : ℚ
⊢ q.num = 0 ↔ q = 0
[PROOFSTEP]
induction q
[GOAL]
case mk'
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ (mk' num✝ den✝).num = 0 ↔ mk' num✝ den✝ = 0
[PROOFSTEP]
constructor
[GOAL]
case mk'.mp
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ (mk' num✝ den✝).num = 0 → mk' num✝ den✝ = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mk'.mp
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs 0) den✝
⊢ mk' 0 den✝ = 0
[PROOFSTEP]
exact zero_mk _ _ _
[GOAL]
case mk'.mpr
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
⊢ mk' num✝ den✝ = 0 → (mk' num✝ den✝).num = 0
[PROOFSTEP]
exact congr_arg num
[GOAL]
a b : ℤ
b0 : b ≠ 0
⊢ a /. b = 0 ↔ a = 0
[PROOFSTEP]
rw [← zero_divInt b, divInt_eq_iff b0 b0, zero_mul, mul_eq_zero, or_iff_left b0]
[GOAL]
C : ℚ → Sort u
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
H : (n : ℤ) → (d : ℕ) → 0 < d → Nat.coprime (Int.natAbs n) d → C (n /. ↑d)
⊢ C (mk' n d)
[PROOFSTEP]
rw [num_den']
[GOAL]
C : ℚ → Sort u
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
H : (n : ℤ) → (d : ℕ) → 0 < d → Nat.coprime (Int.natAbs n) d → C (n /. ↑d)
⊢ C (n /. ↑d)
[PROOFSTEP]
exact H n d (Nat.pos_of_ne_zero h) c
[GOAL]
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
⊢ f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
generalize ha : a /. b = x
[GOAL]
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
x : ℚ
ha : a /. b = x
⊢ f x (c /. d) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
cases' x with n₁ d₁ h₁ c₁
[GOAL]
case mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = mk' n₁ d₁
⊢ f (mk' n₁ d₁) (c /. d) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
rw [num_den'] at ha
[GOAL]
case mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
⊢ f (mk' n₁ d₁) (c /. d) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
generalize hc : c /. d = x
[GOAL]
case mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
x : ℚ
hc : c /. d = x
⊢ f (mk' n₁ d₁) x = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
cases' x with n₂ d₂ h₂ c₂
[GOAL]
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
hc : c /. d = mk' n₂ d₂
⊢ f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
rw [num_den'] at hc
[GOAL]
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
rw [fv]
[GOAL]
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
have d₁0 := ne_of_gt (Int.ofNat_lt.2 $ Nat.pos_of_ne_zero h₁)
[GOAL]
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
hc : c /. d = n₂ /. ↑d₂
d₁0 : ↑d₁ ≠ ↑0
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
have d₂0 := ne_of_gt (Int.ofNat_lt.2 $ Nat.pos_of_ne_zero h₂)
[GOAL]
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : Nat.coprime (Int.natAbs n₁) d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : Nat.coprime (Int.natAbs n₂) d₂}, f (mk' n₁ d₁) (mk' n₂ d₂) = f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
hc : c /. d = n₂ /. ↑d₂
d₁0 : ↑d₁ ≠ ↑0
d₂0 : ↑d₂ ≠ ↑0
⊢ f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂ = f₁ a b c d /. f₂ a b c d
[PROOFSTEP]
exact (divInt_eq_iff (f0 d₁0 d₂0) (f0 b0 d0)).2 (H ((divInt_eq_iff b0 d₁0).1 ha) ((divInt_eq_iff d0 d₂0).1 hc))
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ n /. ↑d + 0 = n /. ↑d
[PROOFSTEP]
rw [← zero_divInt d, add_def'', zero_mul, add_zero, divInt_mul_right]
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case b0
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case d0
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ 0 + n /. ↑d = n /. ↑d
[PROOFSTEP]
rw [← zero_divInt d, add_def'', zero_mul, zero_add, divInt_mul_right]
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case b0
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case d0
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ ↑d ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
⊢ n₁ /. ↑d₁ + n₂ /. ↑d₂ = n₂ /. ↑d₂ + n₁ /. ↑d₁
[PROOFSTEP]
simp [h₁, h₂, add_comm, mul_comm]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₁ /. ↑d₁ + n₂ /. ↑d₂ + n₃ /. ↑d₃ = n₁ /. ↑d₁ + (n₂ /. ↑d₂ + n₃ /. ↑d₃)
[PROOFSTEP]
simp [h₁, h₂, h₃]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ ((n₁ * ↑d₂ + n₂ * ↑d₁) * ↑d₃ + n₃ * (↑d₁ * ↑d₂)) /. (↑d₁ * ↑d₂ * ↑d₃) =
    (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₃ + n₃ * ↑d₂) * ↑d₁) /. (↑d₁ * (↑d₂ * ↑d₃))
[PROOFSTEP]
rw [mul_assoc, add_mul, add_mul, mul_assoc, add_assoc]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₁ * ↑d₃ + n₃ * (↑d₁ * ↑d₂))) /. (↑d₁ * (↑d₂ * ↑d₃)) =
    (n₁ * (↑d₂ * ↑d₃) + (n₂ * ↑d₃ * ↑d₁ + n₃ * ↑d₂ * ↑d₁)) /. (↑d₁ * (↑d₂ * ↑d₃))
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₂ * ↑d₁ * ↑d₃ + n₃ * (↑d₁ * ↑d₂) = n₂ * ↑d₃ * ↑d₁ + n₃ * ↑d₂ * ↑d₁
[PROOFSTEP]
ac_rfl
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
⊢ -(n /. ↑d) + n /. ↑d = 0
[PROOFSTEP]
simp [h, mkRat_add_mkRat]
[GOAL]
a b c : ℚ
⊢ 0 /. 1 = 0
[PROOFSTEP]
rw [divInt]
[GOAL]
a b c : ℚ
⊢ (match 0, 1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => normalize (-n) (Nat.succ d)) =
    0
[PROOFSTEP]
simp
[GOAL]
a b c : ℚ
⊢ 1 /. 1 = 1
[PROOFSTEP]
rw [divInt]
[GOAL]
a b c : ℚ
⊢ (match 1, 1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => normalize (-n) (Nat.succ d)) =
    1
[PROOFSTEP]
simp
[GOAL]
a b c : ℚ
⊢ -1 /. 1 = -1
[PROOFSTEP]
rw [divInt]
[GOAL]
a b c : ℚ
⊢ (match -1, 1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => normalize (-n) (Nat.succ d)) =
    -1
[PROOFSTEP]
simp
[GOAL]
a b c : ℚ
n : ℤ
⊢ n /. 1 = ↑n
[PROOFSTEP]
rw [divInt]
[GOAL]
a b c : ℚ
n : ℤ
⊢ (match n, 1 with
    | n, Int.ofNat d => inline (mkRat n d)
    | n, Int.negSucc d => normalize (-n) (Nat.succ d)) =
    ↑n
[PROOFSTEP]
simp [mkRat, normalize]
[GOAL]
a b c : ℚ
n : ℤ
⊢ mk' n 1 = ↑n
[PROOFSTEP]
rfl
[GOAL]
a b c : ℚ
n : ℤ
⊢ mkRat n 1 = ↑n
[PROOFSTEP]
simp [Rat.mkRat_eq, Rat.divInt_one]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₁ /. ↑d₁ * (n₂ /. ↑d₂) * (n₃ /. ↑d₃) = n₁ /. ↑d₁ * (n₂ /. ↑d₂ * (n₃ /. ↑d₃))
[PROOFSTEP]
simp [h₁, h₂, h₃, mul_ne_zero, mul_comm, mul_assoc, mul_left_comm]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ /. ↑d₁ + n₂ /. ↑d₂) * (n₃ /. ↑d₃) = n₁ /. ↑d₁ * (n₃ /. ↑d₃) + n₂ /. ↑d₂ * (n₃ /. ↑d₃)
[PROOFSTEP]
simp [h₁, h₂, h₃, mul_ne_zero]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * ↑d₂ + n₂ * ↑d₁) * n₃ /. (↑d₁ * ↑d₂ * ↑d₃) =
    (n₁ * n₃ * (↑d₂ * ↑d₃) + n₂ * n₃ * (↑d₁ * ↑d₃)) /. (↑d₁ * ↑d₃ * (↑d₂ * ↑d₃))
[PROOFSTEP]
rw [← divInt_mul_right (Int.coe_nat_ne_zero.2 h₃), add_mul, add_mul]
[GOAL]
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * ↑d₂ * n₃ * ↑d₃ + n₂ * ↑d₁ * n₃ * ↑d₃) /. (↑d₁ * ↑d₂ * ↑d₃ * ↑d₃) =
    (n₁ * n₃ * (↑d₂ * ↑d₃) + n₂ * n₃ * (↑d₁ * ↑d₃)) /. (↑d₁ * ↑d₃ * (↑d₂ * ↑d₃))
[PROOFSTEP]
ac_rfl
[GOAL]
a b c : ℚ
⊢ a * (b + c) = a * b + a * c
[PROOFSTEP]
rw [Rat.mul_comm, Rat.add_mul, Rat.mul_comm, Rat.mul_comm c a]
[GOAL]
a b c : ℚ
⊢ 0 ≠ 1
[PROOFSTEP]
rw [ne_comm, ← divInt_one_one, divInt_ne_zero one_ne_zero]
[GOAL]
a b c : ℚ
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
⊢ n /. ↑d * (n /. ↑d)⁻¹ = 1
[PROOFSTEP]
have n0 : n ≠ 0 := mt (by rintro rfl; simp) a0
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
⊢ n = 0 → n /. ↑d = 0
[PROOFSTEP]
rintro rfl
[GOAL]
a b c : ℚ
d : ℕ
h : d ≠ 0
a0 : 0 /. ↑d ≠ 0
⊢ 0 /. ↑d = 0
[PROOFSTEP]
simp
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
n0 : n ≠ 0
⊢ n /. ↑d * (n /. ↑d)⁻¹ = 1
[PROOFSTEP]
simpa [h, n0, mul_comm] using @divInt_mul_right 1 1 (n * d) (by simp [h, n0])
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : d ≠ 0
a0 : n /. ↑d ≠ 0
n0 : n ≠ 0
⊢ n * ↑d ≠ 0
[PROOFSTEP]
simp [h, n0]
[GOAL]
a b c : ℚ
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
simp only [coe_int_eq_divInt, add_def'' one_ne_zero one_ne_zero, ← divInt_one_one, Nat.cast_add, Nat.cast_one, mul_one]
[GOAL]
a b c : ℚ
⊢ 0⁻¹ = 0
[PROOFSTEP]
change Rat.inv 0 = 0
[GOAL]
a b c : ℚ
⊢ Rat.inv 0 = 0
[PROOFSTEP]
rw [Rat.inv_def]
[GOAL]
a b c : ℚ
⊢ ↑0.den /. 0.num = 0
[PROOFSTEP]
rfl
[GOAL]
a b c : ℚ
⊢ Nontrivial ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ CommSemiring ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ Semiring ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddCommGroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddGroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddCommMonoid ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddMonoid ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddLeftCancelSemigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddRightCancelSemigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddCommSemigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ AddSemigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ CommMonoid ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ Monoid ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ CommSemigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c : ℚ
⊢ Semigroup ℚ
[PROOFSTEP]
infer_instance
[GOAL]
a b c p q : ℚ
⊢ p = q ↔ p.num * ↑q.den = q.num * ↑p.den
[PROOFSTEP]
conv =>
  lhs
  rw [← @num_den p, ← @num_den q]
[GOAL]
a b c p q : ℚ
| p = q ↔ p.num * ↑q.den = q.num * ↑p.den
[PROOFSTEP]
  lhs
  rw [← @num_den p, ← @num_den q]
[GOAL]
a b c p q : ℚ
| p = q ↔ p.num * ↑q.den = q.num * ↑p.den
[PROOFSTEP]
  lhs
  rw [← @num_den p, ← @num_den q]
[GOAL]
a b c p q : ℚ
| p = q ↔ p.num * ↑q.den = q.num * ↑p.den
[PROOFSTEP]
lhs
[GOAL]
a b c p q : ℚ
| p = q
[PROOFSTEP]
rw [← @num_den p, ← @num_den q]
[GOAL]
a b c p q : ℚ
⊢ p.num /. ↑p.den = q.num /. ↑q.den ↔ p.num * ↑q.den = q.num * ↑p.den
[PROOFSTEP]
apply Rat.divInt_eq_iff
[GOAL]
case z₁
a b c p q : ℚ
⊢ ↑p.den ≠ 0
[PROOFSTEP]
rw [← Nat.cast_zero, Ne, Int.ofNat_inj]
[GOAL]
case z₁
a b c p q : ℚ
⊢ ¬p.den = 0
[PROOFSTEP]
apply den_nz
[GOAL]
case z₂
a b c p q : ℚ
⊢ ↑q.den ≠ 0
[PROOFSTEP]
rw [← Nat.cast_zero, Ne, Int.ofNat_inj]
[GOAL]
case z₂
a b c p q : ℚ
⊢ ¬q.den = 0
[PROOFSTEP]
apply den_nz
[GOAL]
a b c q : ℚ
hq : q.num = 0
⊢ q = 0
[PROOFSTEP]
have : q = q.num /. q.den := num_den.symm
[GOAL]
a b c q : ℚ
hq : q.num = 0
this : q = q.num /. ↑q.den
⊢ q = 0
[PROOFSTEP]
simpa [hq] using this
[GOAL]
a b c q : ℚ
x✝ : q = 0
⊢ q.num = 0
[PROOFSTEP]
simp [*]
[GOAL]
a b c q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : n = 0
⊢ q = 0
[PROOFSTEP]
simpa [this] using hqnd
[GOAL]
a b c q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : d = 0
⊢ q = 0
[PROOFSTEP]
simpa [this] using hqnd
[GOAL]
a b c q r : ℚ
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
[PROOFSTEP]
have hq' : (↑q.den : ℤ) ≠ 0 := by have := den_nz q; simpa
[GOAL]
a b c q r : ℚ
⊢ ↑q.den ≠ 0
[PROOFSTEP]
have := den_nz q
[GOAL]
a b c q r : ℚ
this : q.den ≠ 0
⊢ ↑q.den ≠ 0
[PROOFSTEP]
simpa
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
[PROOFSTEP]
have hr' : (↑r.den : ℤ) ≠ 0 := by have := den_nz r; simpa
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
⊢ ↑r.den ≠ 0
[PROOFSTEP]
have := den_nz r
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
this : r.den ≠ 0
⊢ ↑r.den ≠ 0
[PROOFSTEP]
simpa
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
[PROOFSTEP]
suffices q.num /. ↑q.den * (r.num /. ↑r.den) = q.num * r.num /. ↑(q.den * r.den) by simpa [num_den] using this
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
this : q.num /. ↑q.den * (r.num /. ↑r.den) = q.num * r.num /. ↑(q.den * r.den)
⊢ q * r = q.num * r.num /. ↑(q.den * r.den)
[PROOFSTEP]
simpa [num_den] using this
[GOAL]
a b c q r : ℚ
hq' : ↑q.den ≠ 0
hr' : ↑r.den ≠ 0
⊢ q.num /. ↑q.den * (r.num /. ↑r.den) = q.num * r.num /. ↑(q.den * r.den)
[PROOFSTEP]
simp [mul_def' hq' hr']
[GOAL]
a b c q r : ℚ
hr : r.num = 0
⊢ q / r = q.num * ↑r.den /. (↑q.den * r.num)
[PROOFSTEP]
have hr' : r = 0 := zero_of_num_zero hr
[GOAL]
a b c q r : ℚ
hr : r.num = 0
hr' : r = 0
⊢ q / r = q.num * ↑r.den /. (↑q.den * r.num)
[PROOFSTEP]
simp [*]
[GOAL]
a b c q r : ℚ
hr : ¬r.num = 0
⊢ q * r⁻¹ = q.num /. ↑q.den * (r.num /. ↑r.den)⁻¹
[PROOFSTEP]
simp [num_den]
[GOAL]
a b c q r : ℚ
hr : ¬r.num = 0
⊢ q.num /. ↑q.den * (r.num /. ↑r.den)⁻¹ = q.num /. ↑q.den * (↑r.den /. r.num)
[PROOFSTEP]
rw [inv_def']
[GOAL]
a b c q r : ℚ
hr : ¬r.num = 0
⊢ ↑q.den ≠ 0
[PROOFSTEP]
simpa using den_nz q
[GOAL]
a✝ b✝ c✝ : ℚ
a b c : ℤ
h : c = 0
⊢ (a + b) /. c = a /. c + b /. c
[PROOFSTEP]
simp [h]
[GOAL]
a✝ b✝ c✝ : ℚ
a b c : ℤ
h : ¬c = 0
⊢ (a + b) /. c = a /. c + b /. c
[PROOFSTEP]
rw [add_def'' h h, divInt_eq_iff h (mul_ne_zero h h)]
[GOAL]
a✝ b✝ c✝ : ℚ
a b c : ℤ
h : ¬c = 0
⊢ (a + b) * (c * c) = (a * c + b * c) * c
[PROOFSTEP]
simp [add_mul, mul_assoc]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ n /. d = ↑n / ↑d
[PROOFSTEP]
by_cases d0 : d = 0
[GOAL]
case pos
a b c : ℚ
n d : ℤ
d0 : d = 0
⊢ n /. d = ↑n / ↑d
[PROOFSTEP]
simp [d0, div_zero]
[GOAL]
case neg
a b c : ℚ
n d : ℤ
d0 : ¬d = 0
⊢ n /. d = ↑n / ↑d
[PROOFSTEP]
simp [division_def, coe_int_eq_divInt, mul_def' one_ne_zero d0]
[GOAL]
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (x /. d) = n /. d
[PROOFSTEP]
by_cases hd : d = 0
[GOAL]
case pos
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. d) = n /. d
[PROOFSTEP]
rw [hd]
[GOAL]
case pos
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. 0) = n /. 0
[PROOFSTEP]
simp
[GOAL]
case neg
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d
[PROOFSTEP]
rw [mul_def' hx hd, mul_comm x, divInt_mul_right hx]
[GOAL]
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x / (d /. x) = n /. d
[PROOFSTEP]
rw [div_eq_mul_inv, inv_def', divInt_mul_divInt_cancel hx]
[GOAL]
a b c : ℚ
x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ x /. n / (x /. d) = d /. n
[PROOFSTEP]
rw [div_eq_mul_inv, inv_def', mul_comm, divInt_mul_divInt_cancel hx]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ ↑n / ↑d = n /. d
[PROOFSTEP]
repeat' rw [coe_int_eq_divInt]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ ↑n / ↑d = n /. d
[PROOFSTEP]
rw [coe_int_eq_divInt]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ n /. 1 / ↑d = n /. d
[PROOFSTEP]
rw [coe_int_eq_divInt]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ n /. 1 / (d /. 1) = n /. d
[PROOFSTEP]
rw [coe_int_eq_divInt]
[GOAL]
a b c : ℚ
n d : ℤ
⊢ n /. 1 / (d /. 1) = n /. d
[PROOFSTEP]
exact divInt_div_divInt_cancel_left one_ne_zero n d
[GOAL]
a b c r : ℚ
⊢ ↑r.num / ↑r.den = r
[PROOFSTEP]
rw [← Int.cast_ofNat]
[GOAL]
a b c r : ℚ
⊢ ↑r.num / ↑↑r.den = r
[PROOFSTEP]
erw [← divInt_eq_div, num_den]
[GOAL]
a b c q : ℚ
hq : q.den = 1
⊢ ↑q.num = q
[PROOFSTEP]
conv_rhs => rw [← @num_den q, hq]
[GOAL]
a b c q : ℚ
hq : q.den = 1
| q
[PROOFSTEP]
rw [← @num_den q, hq]
[GOAL]
a b c q : ℚ
hq : q.den = 1
| q
[PROOFSTEP]
rw [← @num_den q, hq]
[GOAL]
a b c q : ℚ
hq : q.den = 1
| q
[PROOFSTEP]
rw [← @num_den q, hq]
[GOAL]
a b c q : ℚ
hq : q.den = 1
⊢ ↑q.num = q.num /. ↑1
[PROOFSTEP]
rw [coe_int_eq_divInt]
[GOAL]
a b c q : ℚ
hq : q.den = 1
⊢ q.num /. 1 = q.num /. ↑1
[PROOFSTEP]
rfl
[GOAL]
a b c : ℚ
n : ℕ
⊢ ↑n = ↑n /. 1
[PROOFSTEP]
rw [← Int.cast_ofNat, coe_int_eq_divInt]
[GOAL]
a b c : ℚ
n : ℕ
⊢ (↑n).num = ↑n
[PROOFSTEP]
rw [← Int.cast_ofNat, coe_int_num]
[GOAL]
a b c : ℚ
n : ℕ
⊢ (↑n).den = 1
[PROOFSTEP]
rw [← Int.cast_ofNat, coe_int_den]
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
⊢ mkRat n d = ↑n / ↑d
[PROOFSTEP]
simp [mkRat]
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
[PROOFSTEP]
by_cases d = 0
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
[PROOFSTEP]
by_cases d = 0
[GOAL]
case pos
a b c : ℚ
n : ℤ
d : ℕ
h : d = 0
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
[PROOFSTEP]
simp [h]
[GOAL]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ (if h : d = 0 then 0 else normalize n d) = ↑n / ↑d
[PROOFSTEP]
simp [h, HDiv.hDiv, Rat.div, Div.div]
[GOAL]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ normalize n d = ↑n * Rat.inv ↑d
[PROOFSTEP]
unfold Rat.inv
[GOAL]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
[PROOFSTEP]
have h₁ : 0 < d := Nat.pos_iff_ne_zero.2 h
[GOAL]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
[PROOFSTEP]
have h₂ : ¬(d : ℤ) < 0 := by simp
[GOAL]
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
⊢ ¬↑d < 0
[PROOFSTEP]
simp
[GOAL]
case neg
a b c : ℚ
n : ℤ
d : ℕ
h : ¬d = 0
h₁ : 0 < d
h₂ : ¬↑d < 0
⊢ normalize n d =
    ↑n *
      if h : (↑d).num < 0 then mk' (-↑(↑d).den) (Int.natAbs (↑d).num)
      else if h : (↑d).num > 0 then mk' (↑(↑d).den) (Int.natAbs (↑d).num) else ↑d
[PROOFSTEP]
simp [h, h₁, h₂, ← Rat.normalize_eq_mk', Rat.normalize_eq_mkRat, ← mkRat_one, Rat.mkRat_mul_mkRat]


[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
⊢ Rat.floor a = a.num / ↑a.den
[PROOFSTEP]
rw [Rat.floor]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
⊢ (if a.den = 1 then a.num else a.num / ↑a.den) = a.num / ↑a.den
[PROOFSTEP]
split
[GOAL]
case inl
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : a.den = 1
⊢ a.num = a.num / ↑a.den
[PROOFSTEP]
next h => simp [h]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h : a.den = 1
⊢ a.num = a.num / ↑a.den
[PROOFSTEP]
simp [h]
[GOAL]
case inr
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den
[PROOFSTEP]
next => rfl
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
⊢ z ≤ Rat.floor (mk' n d) ↔ ↑z ≤ mk' n d
[PROOFSTEP]
simp [Rat.floor_def']
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
⊢ z ≤ n / ↑d ↔ ↑z ≤ mk' n d
[PROOFSTEP]
rw [num_den']
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
[PROOFSTEP]
have h' := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h)
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
⊢ z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
[PROOFSTEP]
conv =>
  rhs
  rw [coe_int_eq_divInt, Rat.le_def zero_lt_one h', mul_one]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
| z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
[PROOFSTEP]
  rhs
  rw [coe_int_eq_divInt, Rat.le_def zero_lt_one h', mul_one]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
| z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
[PROOFSTEP]
  rhs
  rw [coe_int_eq_divInt, Rat.le_def zero_lt_one h', mul_one]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
| z ≤ n / ↑d ↔ ↑z ≤ n /. ↑d
[PROOFSTEP]
rhs
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
| ↑z ≤ n /. ↑d
[PROOFSTEP]
rw [coe_int_eq_divInt, Rat.le_def zero_lt_one h', mul_one]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
z n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (natAbs n) d
h' : ↑0 < ↑d
⊢ z ≤ n / ↑d ↔ z * ↑d ≤ n
[PROOFSTEP]
exact Int.le_ediv_iff_mul_le h'
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
⊢ ⌊↑n / ↑d⌋ = n / ↑d
[PROOFSTEP]
rw [Rat.floor_def]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
[PROOFSTEP]
obtain rfl | hd := @eq_zero_or_pos _ _ d
[GOAL]
case inl
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
⊢ (↑n / ↑0).num / ↑(↑n / ↑0).den = n / ↑0
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d
[PROOFSTEP]
set q := (n : ℚ) / d with q_eq
[GOAL]
case inr
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ q.num / ↑q.den = n / ↑d
[PROOFSTEP]
obtain ⟨c, n_eq_c_mul_num, d_eq_c_mul_denom⟩ : ∃ c, n = c * q.num ∧ (d : ℤ) = c * q.den :=
  by
  rw [q_eq]
  exact_mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (by exact_mod_cast hd.ne')
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * q.num ∧ ↑d = c * ↑q.den
[PROOFSTEP]
rw [q_eq]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ∃ c, n = c * (↑n / ↑d).num ∧ ↑d = c * ↑(↑n / ↑d).den
[PROOFSTEP]
exact_mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (by exact_mod_cast hd.ne')
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ ↑d ≠ 0
[PROOFSTEP]
exact_mod_cast hd.ne'
[GOAL]
case inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = n / ↑d
[PROOFSTEP]
rw [n_eq_c_mul_num, d_eq_c_mul_denom]
[GOAL]
case inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = c * q.num / (c * ↑q.den)
[PROOFSTEP]
refine' (Int.mul_ediv_mul_of_pos _ _ <| pos_of_mul_pos_left _ <| Int.coe_nat_nonneg q.den).symm
[GOAL]
case inr.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < c * ↑q.den
[PROOFSTEP]
rwa [← d_eq_c_mul_denom, Int.coe_nat_pos]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ ↑⌊x⌋ ≤ ↑x ∧ ↑x < ↑⌊x⌋ + 1
[PROOFSTEP]
exact_mod_cast floor_eq_iff.1 (Eq.refl ⌊x⌋)
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ ⌈↑x⌉ = ⌈x⌉
[PROOFSTEP]
rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ round ↑x = round x
[PROOFSTEP]
have H : ((2 : ℚ) : α) = (2 : α) := Rat.cast_coe_nat 2
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
⊢ round ↑x = round x
[PROOFSTEP]
have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp [H]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
⊢ ↑(x + 1 / 2) = ↑x + 1 / 2
[PROOFSTEP]
simp [H]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
H : ↑2 = 2
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ round ↑x = round x
[PROOFSTEP]
rw [round_eq, round_eq, ← this, floor_cast]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : ℚ
⊢ ↑(fract x) = fract ↑x
[PROOFSTEP]
simp only [fract, cast_sub, cast_coe_int, floor_cast]
[GOAL]
n : ℤ
d : ℕ
⊢ n % ↑d = n - ↑d * ⌊↑n / ↑d⌋
[PROOFSTEP]
rw [eq_sub_of_add_eq <| Int.emod_add_ediv n d, Rat.floor_int_div_nat_eq_div]
[GOAL]
n d : ℕ
n_coprime_d : coprime n d
⊢ coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
[PROOFSTEP]
have : (n : ℤ) % d = n - d * ⌊(n : ℚ) / d⌋ := Int.mod_nat_eq_sub_mul_floor_rat_div
[GOAL]
n d : ℕ
n_coprime_d : coprime n d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
[PROOFSTEP]
rw [← this]
[GOAL]
n d : ℕ
n_coprime_d : coprime n d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ coprime (natAbs (↑n % ↑d)) d
[PROOFSTEP]
have : d.coprime n := n_coprime_d.symm
[GOAL]
n d : ℕ
n_coprime_d : coprime n d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : coprime d n
⊢ coprime (natAbs (↑n % ↑d)) d
[PROOFSTEP]
rwa [Nat.coprime, Nat.gcd_rec] at this
[GOAL]
q : ℚ
⊢ q.num < (⌊q⌋ + 1) * ↑q.den
[PROOFSTEP]
suffices (q.num : ℚ) < (⌊q⌋ + 1) * q.den by exact_mod_cast this
[GOAL]
q : ℚ
this : ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
⊢ q.num < (⌊q⌋ + 1) * ↑q.den
[PROOFSTEP]
exact_mod_cast this
[GOAL]
q : ℚ
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
[PROOFSTEP]
suffices (q.num : ℚ) < (q - fract q + 1) * q.den
  by
  have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
  rwa [this]
[GOAL]
q : ℚ
this : ↑q.num < (q - fract q + 1) * ↑q.den
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
[PROOFSTEP]
have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
[GOAL]
q : ℚ
this✝ : ↑q.num < (q - fract q + 1) * ↑q.den
this : ↑⌊q⌋ = q - fract q
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den
[PROOFSTEP]
rwa [this]
[GOAL]
q : ℚ
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
[PROOFSTEP]
suffices (q.num : ℚ) < q.num + (1 - fract q) * q.den
  by
  have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den
  calc
    (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
    _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
    _ = q.num + (1 - fract q) * q.den := by simp
  rwa [this]
[GOAL]
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
[PROOFSTEP]
have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den
[GOAL]
case this
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
q : ℚ
this✝ : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
this : (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
[PROOFSTEP]
calc
  (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
  _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
  _ = q.num + (1 - fract q) * q.den := by simp
[GOAL]
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q - fract q + 1) * ↑q.den = (q + (1 - fract q)) * ↑q.den
[PROOFSTEP]
ring
[GOAL]
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ (q + (1 - fract q)) * ↑q.den = q * ↑q.den + (1 - fract q) * ↑q.den
[PROOFSTEP]
rw [add_mul]
[GOAL]
q : ℚ
this : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
⊢ q * ↑q.den + (1 - fract q) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
[PROOFSTEP]
simp
[GOAL]
q : ℚ
this✝ : ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
this : (q - fract q + 1) * ↑q.den = ↑q.num + (1 - fract q) * ↑q.den
⊢ ↑q.num < (q - fract q + 1) * ↑q.den
[PROOFSTEP]
rwa [this]
[GOAL]
q : ℚ
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
[PROOFSTEP]
suffices 0 < (1 - fract q) * q.den by
  rw [← sub_lt_iff_lt_add']
  simpa
[GOAL]
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num < ↑q.num + (1 - fract q) * ↑q.den
[PROOFSTEP]
rw [← sub_lt_iff_lt_add']
[GOAL]
q : ℚ
this : 0 < (1 - fract q) * ↑q.den
⊢ ↑q.num - ↑q.num < (1 - fract q) * ↑q.den
[PROOFSTEP]
simpa
[GOAL]
q : ℚ
⊢ 0 < (1 - fract q) * ↑q.den
[PROOFSTEP]
have : 0 < 1 - fract q := by
  have : fract q < 1 := fract_lt_one q
  have : 0 + fract q < 1 := by simp [this]
  rwa [lt_sub_iff_add_lt]
[GOAL]
q : ℚ
⊢ 0 < 1 - fract q
[PROOFSTEP]
have : fract q < 1 := fract_lt_one q
[GOAL]
q : ℚ
this : fract q < 1
⊢ 0 < 1 - fract q
[PROOFSTEP]
have : 0 + fract q < 1 := by simp [this]
[GOAL]
q : ℚ
this : fract q < 1
⊢ 0 + fract q < 1
[PROOFSTEP]
simp [this]
[GOAL]
q : ℚ
this✝ : fract q < 1
this : 0 + fract q < 1
⊢ 0 < 1 - fract q
[PROOFSTEP]
rwa [lt_sub_iff_add_lt]
[GOAL]
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < (1 - fract q) * ↑q.den
[PROOFSTEP]
exact mul_pos this (by exact_mod_cast q.pos)
[GOAL]
q : ℚ
this : 0 < 1 - fract q
⊢ 0 < ↑q.den
[PROOFSTEP]
exact_mod_cast q.pos
[GOAL]
q : ℚ
q_pos : 0 < q
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
have q_num_pos : 0 < q.num := Rat.num_pos_iff_pos.mpr q_pos
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
have q_num_abs_eq_q_num : (q.num.natAbs : ℤ) = q.num := Int.natAbs_of_nonneg q_num_pos.le
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
set q_inv := (q.den : ℚ) / q.num with q_inv_def
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
have q_inv_eq : q⁻¹ = q_inv := Rat.inv_def''
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
suffices (q_inv - ⌊q_inv⌋).num < q.num by rwa [q_inv_eq]
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : (q_inv - ↑⌊q_inv⌋).num < q.num
⊢ (fract q⁻¹).num < q.num
[PROOFSTEP]
rwa [q_inv_eq]
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ (q_inv - ↑⌊q_inv⌋).num < q.num
[PROOFSTEP]
suffices ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num < q.num by field_simp [this, ne_of_gt q_num_pos]
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
⊢ (q_inv - ↑⌊q_inv⌋).num < q.num
[PROOFSTEP]
field_simp [this, ne_of_gt q_num_pos]
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
[PROOFSTEP]
suffices (q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num by
  -- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
  have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ :=
    by
    suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.coprime q.num.natAbs by
      exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos this
    have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
    simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
  rwa [this]
    -- to show the claim, start with the following inequality
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ↑q.den - q.num * ⌊q_inv⌋ < q.num
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
[PROOFSTEP]
have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ :=
  by
  suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.coprime q.num.natAbs by
    exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos this
  have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
  simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ↑q.den - q.num * ⌊q_inv⌋ < q.num
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num = ↑q.den - q.num * ⌊q_inv⌋
[PROOFSTEP]
suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.coprime q.num.natAbs by
  exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos this
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this✝ : ↑q.den - q.num * ⌊q_inv⌋ < q.num
this : Nat.coprime (natAbs (↑q.den - q.num * ⌊q_inv⌋)) (natAbs q.num)
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num = ↑q.den - q.num * ⌊q_inv⌋
[PROOFSTEP]
exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos this
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ↑q.den - q.num * ⌊q_inv⌋ < q.num
⊢ Nat.coprime (natAbs (↑q.den - q.num * ⌊q_inv⌋)) (natAbs q.num)
[PROOFSTEP]
have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : ↑q.den - q.num * ⌊q_inv⌋ < q.num
tmp : Nat.coprime (natAbs (↑q.den - ↑(natAbs q.num) * ⌊↑q.den / ↑(natAbs q.num)⌋)) (natAbs q.num)
⊢ Nat.coprime (natAbs (↑q.den - q.num * ⌊q_inv⌋)) (natAbs q.num)
[PROOFSTEP]
simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this✝ : ↑q.den - q.num * ⌊q_inv⌋ < q.num
this : ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num = ↑q.den - q.num * ⌊q_inv⌋
⊢ ((↑q.den - ↑q.num * ↑⌊q_inv⌋) / ↑q.num).num < q.num
[PROOFSTEP]
rwa [this]
  -- to show the claim, start with the following inequality
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
[PROOFSTEP]
have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.den < q⁻¹.den :=
  by
  have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
  have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this
  rwa [← sub_lt_iff_lt_add'] at this
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
⊢ q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
[PROOFSTEP]
have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
⊢ q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
[PROOFSTEP]
have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
⊢ q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den
[PROOFSTEP]
rwa [right_distrib, one_mul] at this
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this✝ : q⁻¹.num < (⌊q⁻¹⌋ + 1) * ↑q⁻¹.den
this : q⁻¹.num < ⌊q⁻¹⌋ * ↑q⁻¹.den + ↑q⁻¹.den
⊢ q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
[PROOFSTEP]
rwa [← sub_lt_iff_lt_add'] at this
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
[PROOFSTEP]
have : q_inv.num = q.den ∧ q_inv.den = q.num.natAbs :=
  by
  have coprime_q_denom_q_num : q.den.coprime q.num.natAbs := q.reduced.symm
  have : Int.natAbs q.den = q.den := by simp
  rw [← this] at coprime_q_denom_q_num
  rw [q_inv_def]
  constructor
  · exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
  · suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact_mod_cast this
    rw [q_num_abs_eq_q_num]
    exact_mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = natAbs q.num
[PROOFSTEP]
have coprime_q_denom_q_num : q.den.coprime q.num.natAbs := q.reduced.symm
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime q.den (natAbs q.num)
⊢ q_inv.num = ↑q.den ∧ q_inv.den = natAbs q.num
[PROOFSTEP]
have : Int.natAbs q.den = q.den := by simp
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime q.den (natAbs q.num)
⊢ natAbs ↑q.den = q.den
[PROOFSTEP]
simp
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime q.den (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = natAbs q.num
[PROOFSTEP]
rw [← this] at coprime_q_denom_q_num
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ q_inv.num = ↑q.den ∧ q_inv.den = natAbs q.num
[PROOFSTEP]
rw [q_inv_def]
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ (↑q.den / ↑q.num).num = ↑q.den ∧ (↑q.den / ↑q.num).den = natAbs q.num
[PROOFSTEP]
constructor
[GOAL]
case left
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ (↑q.den / ↑q.num).num = ↑q.den
[PROOFSTEP]
exact_mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
[GOAL]
case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ (↑q.den / ↑q.num).den = natAbs q.num
[PROOFSTEP]
suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact_mod_cast this
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this✝ : natAbs ↑q.den = q.den
this : ↑(↑q.den / ↑q.num).den = ↑(natAbs q.num)
⊢ (↑q.den / ↑q.num).den = natAbs q.num
[PROOFSTEP]
exact_mod_cast this
[GOAL]
case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ ↑(↑q.den / ↑q.num).den = ↑(natAbs q.num)
[PROOFSTEP]
rw [q_num_abs_eq_q_num]
[GOAL]
case right
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : Nat.coprime (natAbs ↑q.den) (natAbs q.num)
this : natAbs ↑q.den = q.den
⊢ ↑(↑q.den / ↑q.num).den = q.num
[PROOFSTEP]
exact_mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
[GOAL]
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑(natAbs q.num) = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
this : q_inv.num = ↑q.den ∧ q_inv.den = natAbs q.num
⊢ ↑q.den - q.num * ⌊q_inv⌋ < q.num
[PROOFSTEP]
rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq


[GOAL]
α : Type u_1
p q : ℚ≥0
h : q ≤ p
⊢ ↑q ≤ ↑p - 0
[PROOFSTEP]
rwa [sub_zero]
[GOAL]
α : Type u_1
p q : ℚ≥0
⊢ ↑q = 0 ↔ q = 0
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
p q : ℚ≥0
n : ℕ
⊢ ↑(toNNRat ↑n) = ↑↑n
[PROOFSTEP]
simp only [Nat.cast_nonneg, Rat.coe_toNNRat]
[GOAL]
α : Type u_1
p q : ℚ≥0
n : ℕ
⊢ ↑n = ↑↑n
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ toNNRat (∑ a in s, f a) = ∑ a in s, toNNRat (f a)
[PROOFSTEP]
rw [← coe_inj, coe_sum, Rat.coe_toNNRat _ (Finset.sum_nonneg hf)]
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∑ i in s, f i = ∑ a in s, ↑(toNNRat (f a))
[PROOFSTEP]
exact Finset.sum_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(toNNRat (f x))
[PROOFSTEP]
rw [Rat.coe_toNNRat _ (hf x hxs)]
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ toNNRat (∏ a in s, f a) = ∏ a in s, toNNRat (f a)
[PROOFSTEP]
rw [← coe_inj, coe_prod, Rat.coe_toNNRat _ (Finset.prod_nonneg hf)]
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ ∏ i in s, f i = ∏ a in s, ↑(toNNRat (f a))
[PROOFSTEP]
exact Finset.prod_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]
[GOAL]
α : Type u_1
p q : ℚ≥0
s : Finset α
f : α → ℚ
hf : ∀ (a : α), a ∈ s → 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = ↑(toNNRat (f x))
[PROOFSTEP]
rw [Rat.coe_toNNRat _ (hf x hxs)]
[GOAL]
p q : ℚ
⊢ 0 < toNNRat q ↔ 0 < q
[PROOFSTEP]
simp [toNNRat, ← coe_lt_coe]
[GOAL]
p q : ℚ
⊢ toNNRat q = 0 ↔ q ≤ 0
[PROOFSTEP]
simpa [-toNNRat_pos] using (@toNNRat_pos q).not
[GOAL]
p q : ℚ
hp : 0 ≤ p
⊢ toNNRat q ≤ toNNRat p ↔ q ≤ p
[PROOFSTEP]
simp [← coe_le_coe, toNNRat, hp]
[GOAL]
p q : ℚ
⊢ toNNRat q < toNNRat p ↔ q < p ∧ 0 < p
[PROOFSTEP]
simp [← coe_lt_coe, toNNRat, lt_irrefl]
[GOAL]
p q : ℚ
hq : 0 ≤ q
hp : 0 ≤ p
⊢ ↑(toNNRat (q + p)) = ↑(toNNRat q + toNNRat p)
[PROOFSTEP]
simp [toNNRat, hq, hp, add_nonneg]
[GOAL]
p q✝ : ℚ
q : ℚ≥0
hp : 0 ≤ p
⊢ q ≤ toNNRat p ↔ ↑q ≤ p
[PROOFSTEP]
rw [← coe_le_coe, Rat.coe_toNNRat p hp]
[GOAL]
p q✝ : ℚ
q : ℚ≥0
hq : 0 < q
hp : p < 0
⊢ q ≤ toNNRat p ↔ ↑q ≤ p
[PROOFSTEP]
simp only [(hp.trans_le q.coe_nonneg).not_le, toNNRat_eq_zero.2 hp.le, hq.not_le]
[GOAL]
p✝ q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ toNNRat q < p ↔ q < ↑p
[PROOFSTEP]
rw [← coe_lt_coe, Rat.coe_toNNRat q hq]
[GOAL]
p q : ℚ
hp : 0 ≤ p
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
[PROOFSTEP]
cases' le_total 0 q with hq hq
[GOAL]
case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
[PROOFSTEP]
ext
[GOAL]
case inl.a.num
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (↑(toNNRat (p * q))).num = (↑(toNNRat p * toNNRat q)).num
[PROOFSTEP]
simp [toNNRat, hp, hq, max_eq_left, mul_nonneg]
[GOAL]
case inl.a.den
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (↑(toNNRat (p * q))).den = (↑(toNNRat p * toNNRat q)).den
[PROOFSTEP]
simp [toNNRat, hp, hq, max_eq_left, mul_nonneg]
[GOAL]
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
[PROOFSTEP]
have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq
[GOAL]
case inr
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ toNNRat (p * q) = toNNRat p * toNNRat q
[PROOFSTEP]
rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]
[GOAL]
p q✝ q : ℚ
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹
[PROOFSTEP]
obtain hq | hq := le_total q 0
[GOAL]
case inl
p q✝ q : ℚ
hq : q ≤ 0
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹
[PROOFSTEP]
rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]
[GOAL]
case inr
p q✝ q : ℚ
hq : 0 ≤ q
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹
[PROOFSTEP]
nth_rw 1 [← Rat.coe_toNNRat q hq]
[GOAL]
case inr
p q✝ q : ℚ
hq : 0 ≤ q
⊢ toNNRat (↑(toNNRat q))⁻¹ = (toNNRat q)⁻¹
[PROOFSTEP]
rw [← coe_inv, toNNRat_coe]
[GOAL]
p q : ℚ
hp : 0 ≤ p
⊢ toNNRat (p / q) = toNNRat p / toNNRat q
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]
[GOAL]
p q : ℚ
hq : 0 ≤ q
⊢ toNNRat (p / q) = toNNRat p / toNNRat q
[PROOFSTEP]
rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]
[GOAL]
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ p = q
[PROOFSTEP]
ext
[GOAL]
case a.num
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ (↑p).num = (↑q).num
[PROOFSTEP]
apply (Int.natAbs_inj_of_nonneg_of_nonneg _ _).1 hn
[GOAL]
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ 0 ≤ (↑p).num
p q : ℚ≥0 hn : num p = num q hd : den p = den q ⊢ 0 ≤ (↑q).num
[PROOFSTEP]
exact Rat.num_nonneg_iff_zero_le.2 p.2
[GOAL]
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ 0 ≤ (↑q).num
[PROOFSTEP]
exact Rat.num_nonneg_iff_zero_le.2 q.2
[GOAL]
case a.den
p q : ℚ≥0
hn : num p = num q
hd : den p = den q
⊢ (↑p).den = (↑q).den
[PROOFSTEP]
exact hd
[GOAL]
p q : ℚ≥0
⊢ p = q → num p = num q ∧ den p = den q
[PROOFSTEP]
rintro rfl
[GOAL]
p : ℚ≥0
⊢ num p = num p ∧ den p = den p
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
p q✝ q : ℚ≥0
⊢ ↑(num q) / ↑(den q) = q
[PROOFSTEP]
ext1
[GOAL]
case a
p q✝ q : ℚ≥0
⊢ ↑(↑(num q) / ↑(den q)) = ↑q
[PROOFSTEP]
rw [coe_div, coe_natCast, coe_natCast, num, ← Int.cast_ofNat,
  Int.natAbs_of_nonneg (Rat.num_nonneg_iff_zero_le.2 q.prop)]
[GOAL]
case a
p q✝ q : ℚ≥0
⊢ ↑(↑q).num / ↑(den q) = ↑q
[PROOFSTEP]
exact Rat.num_div_den q
[GOAL]
p q✝ : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (↑m / ↑n)
q : ℚ≥0
⊢ α q
[PROOFSTEP]
rw [← num_div_den q]
[GOAL]
p q✝ : ℚ≥0
α : ℚ≥0 → Sort u_1
h : (m n : ℕ) → α (↑m / ↑n)
q : ℚ≥0
⊢ α (↑(num q) / ↑(den q))
[PROOFSTEP]
apply h