α : 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
α : 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
have h := Int.cast_mono (α := α) <| of_decide_eq_true h
α : 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
α : 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
have ha : 0 ≤ ⅟(da : α) := invOf_nonneg.mpr <| Nat.cast_nonneg da
α : 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
α : 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
have hb : 0 ≤ ⅟(db : α) := invOf_nonneg.mpr <| Nat.cast_nonneg db
α : 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
α : 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
rw [← mul_assoc, Int.commute_cast] at h
α : 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
α : 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
simp at h
no goals
α : 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
rwa [Int.commute_cast] at h