[GOAL]
R : Type u_1
inst✝ : AddMonoidWithOne R
n m : ℕ
⊢ IsNat n m → IsNat (↑n) m
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.refl
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ IsNat (↑↑m) m
[PROOFSTEP]
exact ⟨rfl⟩
[GOAL]
R : Type u_1
inst✝ : Ring R
n : ℤ
m : ℕ
⊢ IsNat n m → IsNat (↑n) m
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ IsNat (↑↑m) m
[PROOFSTEP]
exact ⟨by simp⟩
[GOAL]
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ ↑↑m = ↑m
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Ring R
n m : ℤ
⊢ IsInt n m → IsInt (↑n) m
[PROOFSTEP]
rintro ⟨⟨⟩⟩
[GOAL]
case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ IsInt (↑↑m) m
[PROOFSTEP]
exact ⟨rfl⟩
[GOAL]
R : Type u_1
inst✝ : DivisionRing R
n✝ : ℕ
⊢ ↑↑n✝ = ↑n✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : DivisionRing R
n✝ : ℤ
⊢ ↑↑n✝ = ↑n✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑qi * ↑denom✝ = 1
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑denom✝ * ↑qi = 1
[PROOFSTEP]
norm_cast
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * ⅟↑denom✝) = ↑num✝ * ⅟↑denom✝
[PROOFSTEP]
simp only []
[GOAL]
R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ : ℤ
denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑(↑num✝ * qi) = ↑num✝ * ↑qi
[PROOFSTEP]
norm_cast
[GOAL]
α : Type ?u.44519
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * (↑k * b) = 1
hc2 : ↑k * b * c = 1
⊢ Invertible b
[PROOFSTEP]
rw [← mul_assoc] at hc1 
[GOAL]
α : Type ?u.44519
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : ↑k * b * c = 1
⊢ Invertible b
[PROOFSTEP]
rw [Nat.cast_commute k, mul_assoc, Nat.cast_commute k] at hc2 
[GOAL]
α : Type ?u.44519
inst✝ : Semiring α
k : ℕ
b c : α
hc1 : c * ↑k * b = 1
hc2 : b * (c * ↑k) = 1
⊢ Invertible b
[PROOFSTEP]
exact ⟨_, hc1, hc2⟩
[GOAL]
α : Type ?u.46618
inst✝¹ : Semiring α
a k b : ℕ
inst✝ : Invertible ↑a
h : a = k * b
⊢ ↑a = ↑k * ↑b
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
⊢ f = HAdd.hAdd →
    IsRat a na da →
      IsRat b nb db →
        Int.add (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc → Nat.mul da db = Nat.mul k dc → IsRat (f a b) nc dc
[PROOFSTEP]
rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * db + nb * da = k * nc) (h₂ : da * db = k * dc)
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
[PROOFSTEP]
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da : α) db
[GOAL]
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)
[PROOFSTEP]
simpa using invertibleMul (da : α) db
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this : Invertible ↑(da * db)
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
[PROOFSTEP]
have := invertibleOfMul' (α := α) h₂
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ IsRat (↑na * ⅟↑da + ↑nb * ⅟↑db) nc dc
[PROOFSTEP]
use this
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
have h₁ := congr_arg (↑· * (⅟↑da * ⅟↑db : α)) h₁
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : (fun x => ↑x * (⅟↑da * ⅟↑db)) (na * ↑db + nb * ↑da) = (fun x => ↑x * (⅟↑da * ⅟↑db)) (↑k * nc)
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
simp only [Int.cast_add, Int.cast_mul, Int.cast_ofNat, ← mul_assoc, add_mul, mul_mul_invOf_self_cancel] at h₁ 
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑db * ⅟↑da * ⅟↑db + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑da * ⅟↑db
h₂ : (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (da * db) = (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (k * dc)
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
simp [← mul_assoc, H] at h₁ h₂ 
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
rw [h₁, h₂, Nat.cast_commute]
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * ↑db + nb * ↑da = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ⅟↑da + ↑nb * ⅟↑db = ↑k * ↑nc * ⅟↑db * ⅟↑da
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
⊢ ↑nc * ↑k * ⅟↑db * ⅟↑da = ↑nc * ↑k * ↑dc * ⅟↑db * ⅟↑da * ⅟↑dc
[PROOFSTEP]
simp only [mul_mul_invOf_self_cancel, (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
  (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]
[GOAL]
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ -(↑num✝ * ⅟↑denom✝) = ↑(Int.neg num✝) * ⅟↑denom✝
[PROOFSTEP]
rw [← neg_mul, ← Int.cast_neg]
[GOAL]
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ ↑(-num✝) * ⅟↑denom✝ = ↑(Int.neg num✝) * ⅟↑denom✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ IsRat (f a b) nc dc
[PROOFSTEP]
rw [hf, sub_eq_add_neg]
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ IsRat (a + -b) nc dc
[PROOFSTEP]
refine isRat_add rfl ra (isRat_neg (n' := -nb) rfl rb rfl) (k := k) (nc := nc) ?_ h₂
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ Int.add (Int.mul na ↑db) (Int.mul (-nb) ↑da) = Int.mul (↑k) nc
[PROOFSTEP]
rw [show Int.mul (-nb) _ = _ from neg_mul ..]
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : Int.sub (Int.mul na ↑db) (Int.mul nb ↑da) = Int.mul (↑k) nc
h₂ : Nat.mul da db = Nat.mul k dc
⊢ Int.add (Int.mul na ↑db) (-(nb * ↑da)) = Int.mul (↑k) nc
[PROOFSTEP]
exact h₁
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
⊢ f = HMul.hMul →
    IsRat a na da → IsRat b nb db → Int.mul na nb = Int.mul (↑k) nc → Nat.mul da db = Nat.mul k dc → IsRat (f a b) nc dc
[PROOFSTEP]
rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * nb = k * nc) (h₂ : da * db = k * dc)
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
[PROOFSTEP]
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da : α) db
[GOAL]
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
⊢ Invertible ↑(da * db)
[PROOFSTEP]
simpa using invertibleMul (da : α) db
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this : Invertible ↑(da * db)
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
[PROOFSTEP]
have := invertibleOfMul' (α := α) h₂
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
[PROOFSTEP]
refine ⟨this, ?_⟩
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
[PROOFSTEP]
have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
[PROOFSTEP]
have h₁ := congr_arg (Int.cast (R := α)) h₁
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑(na * nb) = ↑(↑k * nc)
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
[PROOFSTEP]
simp only [Int.cast_mul, Int.cast_ofNat] at h₁ 
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
[PROOFSTEP]
simp [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, h₁]
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (da * db) = (fun x => ↑nc * ↑x * (⅟↑da * ⅟↑db * ⅟↑dc)) (k * dc)
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
simp [← mul_assoc] at h₂ 
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ↑da * ↑db * ⅟↑da * ⅟↑db * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
rw [H] at h₂ 
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ↑da * ↑db * ⅟↑db * ⅟↑da * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
simp [mul_mul_invOf_self_cancel] at h₂ 
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
[PROOFSTEP]
rw [h₂, Nat.cast_commute]
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑nc * ↑k * ⅟↑da * ⅟↑db = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
[PROOFSTEP]
simp only [mul_mul_invOf_self_cancel, (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
  (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]
[GOAL]
«$α» : Type u
«$a» «$b» : «$α»
«$sα» : Semiring «$α»
«$f» : «$α» → «$α» → «$α» := HMul.hMul
«$e» : «$α» := «$a» * «$b»
«$mα'» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$mα» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
clear! «$mα» «$mα'»
[GOAL]
«$α» : Type u
«$a» «$b» : «$α»
«$sα» : Semiring «$α»
«$f» : «$α» → «$α» → «$α» := HMul.hMul
«$e» : «$α» := «$a» * «$b»
«$na» «$nb» : ℕ
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
apply AddCommMonoidWithOne.toAddMonoidWithOne
[GOAL]
a b : ℕ
c : ℕ
h1 : Nat.pow a b = c
⊢ Nat.pow a (2 * b) = Nat.mul c c
[PROOFSTEP]
simp [two_mul, pow_add, ← h1]
[GOAL]
a b : ℕ
c : ℕ
h1 : Nat.pow a b = c
⊢ Nat.pow a (2 * b + 1) = Nat.mul c (Nat.mul c a)
[PROOFSTEP]
simp [two_mul, pow_add, mul_assoc, ← h1]
[GOAL]
a✝ b✝ : Q(ℕ)
depth : ℕ
a b₀ c₀ b : Q(ℕ)
p : Q(Prop)
hp : «$p» =Q (Nat.pow «$a» «$b₀» = «$c₀»)
b' : ℕ := Expr.natLit! b
d : ℕ := depth >>> 1
hi : Q(ℕ)
⊢ «$p» =Q (Nat.pow «$a» «$b₀» = «$c₀»)
[PROOFSTEP]
exact hp
[GOAL]
a b : ℕ
c : ℕ
h1 : Nat.pow a b = c
⊢ Int.pow (Int.ofNat a) b = Int.ofNat c
[PROOFSTEP]
simp [← h1]
[GOAL]
a b' : ℕ
c' b c : ℕ
h1 : Nat.pow a b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.pow (Int.negOfNat a) b = Int.ofNat c
[PROOFSTEP]
rw [← hb, Int.negOfNat_eq, pow_eq, pow_mul, neg_pow_two, ← pow_mul, two_mul, pow_add, ← hc, ← h1]
[GOAL]
a b' : ℕ
c' b c : ℕ
h1 : Nat.pow a b' = c'
hb : 2 * b' = b
hc : c' * c' = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' = Int.ofNat (Nat.pow a b' * Nat.pow a b')
[PROOFSTEP]
simp
[GOAL]
a b' : ℕ
c' b c : ℕ
h1 : Nat.pow a b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.pow (Int.negOfNat a) b = Int.negOfNat c
[PROOFSTEP]
rw [← hb, Int.negOfNat_eq, Int.negOfNat_eq, pow_eq, pow_succ, pow_mul, neg_pow_two, ← pow_mul, two_mul, pow_add, ← hc, ←
  h1]
[GOAL]
a b' : ℕ
c' b c : ℕ
h1 : Nat.pow a b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ -Int.ofNat a * (Int.ofNat a ^ b' * Int.ofNat a ^ b') = -Int.ofNat (Nat.pow a b' * (Nat.pow a b' * a))
[PROOFSTEP]
simp [mul_assoc, mul_comm, mul_left_comm]
[GOAL]
α : Type u_1
inst✝ : Semiring α
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ ^ ↑n✝ = ↑(Nat.pow n✝¹ n✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
n✝¹ : ℤ
n✝ : ℕ
⊢ ↑n✝¹ ^ ↑n✝ = ↑(Int.pow n✝¹ n✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Ring α
f : α → ℕ → α
a : α
an cn : ℤ
ad b b' cd : ℕ
⊢ f = HPow.hPow → IsRat a an ad → IsNat b b' → Int.pow an b' = cn → Nat.pow ad b' = cd → IsRat (f a b) cn cd
[PROOFSTEP]
rintro rfl ⟨_, rfl⟩ ⟨rfl⟩ (rfl : an ^ b = _) (rfl : ad ^ b = _)
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
[PROOFSTEP]
have := invertiblePow (ad : α) b
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible (↑ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
[PROOFSTEP]
rw [← Nat.cast_pow] at this 
[GOAL]
case mk.mk
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ IsRat ((↑an * ⅟↑ad) ^ b) (an ^ b) (ad ^ b)
[PROOFSTEP]
use this
[GOAL]
case eq
α : Type u_1
inst✝ : Ring α
an : ℤ
ad b : ℕ
inv✝ : Invertible ↑ad
this : Invertible ↑(ad ^ b)
⊢ (↑an * ⅟↑ad) ^ b = ↑(an ^ b) * ⅟↑(ad ^ b)
[PROOFSTEP]
simp [invOf_pow, Commute.mul_pow]
[GOAL]
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.ofNat (Nat.succ n)) d → IsRat a⁻¹ (Int.ofNat d) (Nat.succ n)
[PROOFSTEP]
rintro ⟨_, rfl⟩
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (Int.ofNat d) (Nat.succ n)
[PROOFSTEP]
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑(Nat.succ n)
⊢ IsRat (↑(Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (Int.ofNat d) (Nat.succ n)
[PROOFSTEP]
refine ⟨this, by simp⟩
[GOAL]
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑(Nat.succ n)
⊢ (↑(Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ = ↑(Int.ofNat d) * ⅟↑(Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
⊢ (↑1)⁻¹ = ↑1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
⊢ (↑0)⁻¹ = ↑0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
⊢ (↑(Int.negOfNat 1))⁻¹ = ↑(Int.negOfNat 1)
[PROOFSTEP]
simp [inv_neg_one]
[GOAL]
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.negOfNat (Nat.succ n)) d → IsRat a⁻¹ (Int.negOfNat d) (Nat.succ n)
[PROOFSTEP]
rintro ⟨_, rfl⟩
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.negOfNat (Nat.succ n)) * ⅟↑d)⁻¹ (Int.negOfNat d) (Nat.succ n)
[PROOFSTEP]
simp only [Int.negOfNat_eq]
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(-Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (-Int.ofNat d) (Nat.succ n)
[PROOFSTEP]
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑(Nat.succ n)
⊢ IsRat (↑(-Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (-Int.ofNat d) (Nat.succ n)
[PROOFSTEP]
generalize Nat.succ n = n at *
[GOAL]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ IsRat (↑(-Int.ofNat n) * ⅟↑d)⁻¹ (-Int.ofNat d) n
[PROOFSTEP]
use this
[GOAL]
case eq
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ (↑(-Int.ofNat n) * ⅟↑d)⁻¹ = ↑(-Int.ofNat d) * ⅟↑n
[PROOFSTEP]
simp only [Int.ofNat_eq_coe, Int.cast_neg, Int.cast_ofNat, invOf_eq_inv, inv_neg, neg_mul, mul_inv_rev, inv_inv]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
x✝³ x✝² : α
x✝¹ : ℤ
x✝ : ℕ
h : IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsRat (x✝³ / x✝²) x✝¹ x✝
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
x✝³ x✝² : α
x✝¹ : ℤ
x✝ : ℕ
h : IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝
⊢ IsRat (x✝³ * x✝²⁻¹) x✝¹ x✝
[PROOFSTEP]
exact h
[GOAL]
n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (mkRat ↑n✝¹ ↑n✝) num✝ denom✝
[PROOFSTEP]
rw [Rat.mkRat_eq_div]
[GOAL]
n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (↑↑n✝¹ / ↑↑n✝) num✝ denom✝
[PROOFSTEP]
exact ⟨_, h⟩
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
x✝¹ x✝ : ℕ
num✝ : ℤ
denom✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
inv✝ : Invertible ↑denom✝
eq : ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ OfScientific.ofScientific x✝¹ true x✝ = ↑num✝ * ⅟↑denom✝
[PROOFSTEP]
simp only [σh, Rat.ofScientific_true_def]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
x✝¹ x✝ : ℕ
num✝ : ℤ
denom✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
inv✝ : Invertible ↑denom✝
eq : ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
[PROOFSTEP]
exact eq
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
n✝¹ n✝ x✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
h : x✝ = Nat.mul n✝¹ (10 ^ n✝)
⊢ OfScientific.ofScientific (↑n✝¹) false ↑n✝ = ↑x✝
[PROOFSTEP]
simp [σh, Rat.ofScientific_false_def, h]
[GOAL]
α : Type u_1
inst✝ : DivisionRing α
σα : OfScientific α
n✝¹ n✝ x✝ : ℕ
σh : OfScientific.ofScientific = fun m s e => ↑(Rat.ofScientific m s e)
h : x✝ = Nat.mul n✝¹ (10 ^ n✝)
⊢ ↑(↑n✝¹ * 10 ^ n✝) = ↑n✝¹ * 10 ^ n✝
[PROOFSTEP]
norm_cast
[GOAL]
x y : ℕ
⊢ Nat.ble x y = false ↔ y < x
[PROOFSTEP]
rw [← Nat.not_le, ← Bool.not_eq_true, Nat.ble_eq]
[GOAL]
α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : Nat.beq n✝¹ n✝ = false
⊢ ¬↑n✝¹ = ↑n✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
n✝¹ n✝ : ℕ
h : Nat.beq n✝¹ n✝ = false
⊢ ¬n✝¹ = n✝
[PROOFSTEP]
exact Nat.ne_of_beq_eq_false h
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
n✝¹ n✝ : ℤ
h : decide (n✝¹ = n✝) = false
⊢ ¬↑n✝¹ = ↑n✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
n✝¹ n✝ : ℤ
h : decide (n✝¹ = n✝) = false
⊢ ¬n✝¹ = n✝
[PROOFSTEP]
exact of_decide_eq_false h
[GOAL]
α : Type u_1
inst✝² : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁
[PROOFSTEP]
rw [mul_invOf_eq_iff_eq_mul_right, ← Int.commute_cast, mul_assoc, ← mul_left_eq_iff_eq_invOf_mul, Int.commute_cast]
[GOAL]
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ ↑num✝ * ⅟↑denom✝ = ↑num✝ * ⅟↑denom✝
[PROOFSTEP]
congr
[GOAL]
case e_a.h.e_5.h
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
have h := Int.cast_mono (α := α) <| of_decide_eq_true h
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
have ha : 0 ≤ ⅟(da : α) := invOf_nonneg.mpr <| Nat.cast_nonneg da
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
ha : 0 ≤ ⅟↑da
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
have hb : 0 ≤ ⅟(db : α) := invOf_nonneg.mpr <| Nat.cast_nonneg db
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
have h := (mul_le_mul_of_nonneg_left · hb) <| mul_le_mul_of_nonneg_right h ha
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h✝ : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h :
  ⅟↑db * ((fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) * ⅟↑da) ≤
    ⅟↑db * ((fun x => ↑x) (Int.mul num✝ (Int.ofNat da)) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
rw [← mul_assoc, Int.commute_cast] at h 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h✝ : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ↑(Int.mul num✝¹ (Int.ofNat db)) * ⅟↑db * ⅟↑da ≤ ⅟↑db * ((fun x => ↑x) (Int.mul num✝ (Int.ofNat da)) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
simp at h 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (Int.mul num✝¹ (Int.ofNat db) ≤ Int.mul num✝ (Int.ofNat da)) = true
h✝ : (fun x => ↑x) (Int.mul num✝¹ (Int.ofNat db)) ≤ (fun x => ↑x) (Int.mul num✝ (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ↑num✝¹ * ⅟↑da ≤ ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
[PROOFSTEP]
rwa [Int.commute_cast] at h 
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹ * ↑db < num✝ * ↑da) = true
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
have h := Int.cast_strictMono (α := α) <| of_decide_eq_true h
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
have ha : 0 < ⅟(da : α) := pos_invOf_of_invertible_cast da
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
have hb : 0 < ⅟(db : α) := pos_invOf_of_invertible_cast db
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
have h := (mul_lt_mul_of_pos_left · hb) <| mul_lt_mul_of_pos_right h ha
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ⅟↑db * ((fun x => ↑x) (num✝¹ * ↑db) * ⅟↑da) < ⅟↑db * ((fun x => ↑x) (num✝ * ↑da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
rw [← mul_assoc, Int.commute_cast] at h 
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑(num✝¹ * ↑db) * ⅟↑db * ⅟↑da < ⅟↑db * ((fun x => ↑x) (num✝ * ↑da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
simp at h 
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Nontrivial α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h✝ : (fun x => ↑x) (num✝¹ * ↑db) < (fun x => ↑x) (num✝ * ↑da)
ha : 0 < ⅟↑da
hb : 0 < ⅟↑db
h : ↑num✝¹ * ⅟↑da < ⅟↑db * ↑num✝
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
[PROOFSTEP]
rwa [Int.commute_cast] at h 
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (Int.mul num✝¹ (Int.ofNat denom✝) = Int.mul num✝ (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ⅟↑denom✝¹ = ↑num✝ * ⅟↑denom✝
[PROOFSTEP]
rw [Rat.invOf_denom_swap]
[GOAL]
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (Int.mul num✝¹ (Int.ofNat denom✝) = Int.mul num✝ (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹
[PROOFSTEP]
exact_mod_cast of_decide_eq_false h
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
clear! «$ra» «$rb»
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» «$nb» : ℕ
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
infer_instance
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
«$_i» : OrderedSemiring «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
clear! «$ra» «$rb»
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» «$nb» : ℕ
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
infer_instance
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$ra» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
clear! «$ra» «$rb»
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» «$nb» : ℕ
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
infer_instance
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» : ℕ
«$rb» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
«$_i» : OrderedSemiring «$α»
«$ra» : AddMonoidWithOne «$α» := inferInstance
«$pa» : IsNat «$a» «$na»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
clear! «$ra» «$rb»
[GOAL]
«$β» : Type := Prop
«$e» : «$β»
«$f» $a✝ $b✝ : Expr
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$na» «$nb» : ℕ
«$_i» : OrderedSemiring «$α»
⊢ AddMonoidWithOne «$α»
[PROOFSTEP]
infer_instance
[GOAL]
n✝ : ℕ
⊢ Nat.succ ↑n✝ = ↑(Nat.succ n✝)
[PROOFSTEP]
simp
[GOAL]
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ - ↑n✝ = ↑(Nat.sub n✝¹ n✝)
[PROOFSTEP]
simp
[GOAL]
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ % ↑n✝ = ↑(Nat.mod n✝¹ n✝)
[PROOFSTEP]
aesop
[GOAL]
n✝¹ n✝ : ℕ
⊢ ↑n✝¹ / ↑n✝ = ↑(Nat.div n✝¹ n✝)
[PROOFSTEP]
aesop
