awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a : α
q : ℚ≥0
⊢ Commute a (↑q : α)

Tactic:
(cast_commute ..).symm

Premises used: NNRat.cast_commute, Commute.symm
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q : ℚ≥0
a : α
⊢ (↑q : α) * a = a * (↑q : α)

Tactic:
cast_commute _ _

Premises used: NNRat.cast_commute, SemiconjBy, Commute
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
rcases :
  ∀ (n : ℤ) (d : ℕ) (h : d ≠ 0) (c : n.natAbs.Coprime d)
    (hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ })
    (e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn),
    (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn) : α) =
      HDiv.hDiv (α := α) (↑a : α) (↑b : α)
⊢ (↑(divNat a b) : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)

Tactic:
rcases e : divNat a b with ⟨⟨n, d, h, c⟩, hn⟩

Premises used: NNRat.divNat
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn
⊢ 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }.num

Tactic:
rw [← Rat.num_nonneg] at hn

Premises used: Rat.num_nonneg
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn
hn₁ : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }.num
⊢ divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn

Tactic:
rw [← Rat.num_nonneg] at hn

Premises used: Rat.num_nonneg
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn_1 : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }.num
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn_1
⊢ 0 ≤ n

Tactic:
hn
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
hn_1 : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }
hn : 0 ≤ { num := n, den := d, den_nz := h, reduced := c : ℚ }.num
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn_1
lift :
  ∀ (n : ℕ) (c : (Int.natAbs (↑n : ℤ)).Coprime d)
    (hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ })
    (e :
      divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn),
    (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : α) =
      HDiv.hDiv (α := α) (↑a : α) (↑b : α)
⊢ (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := n, den := d, den_nz := h, reduced := c } hn_1) : α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)

Tactic:
lift n to ℕ using hn
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
⊢ Ne.{u_3 + 1} (α := α) (↑d : α) 0

Tactic:
fun hd ↦ hb ?_

Premises used: Not
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
refine : ∀ (hd : Eq.{u_3 + 1} (α := α) (↑d : α) 0), Eq.{u_3 + 1} (α := α) (↑b : α) 0
⊢ Ne.{u_3 + 1} (α := α) (↑d : α) 0

Tactic:
refine fun hd ↦ hb ?_
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
hd : Eq.{u_3 + 1} (α := α) (↑d : α) 0
⊢ Rat.divInt (↑a : ℤ) (↑b : ℤ) =
    (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : ℚ)

Tactic:
have : Rat.divInt a b = _ := congr_arg NNRat.cast e
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
hd : Eq.{u_3 + 1} (α := α) (↑d : α) 0
this :
  Rat.divInt (↑a : ℤ) (↑b : ℤ) =
    (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : ℚ)
⊢ d ∣ b

Tactic:
simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b

Premises used: Nat.cast, Rat.den_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
hd : Eq.{u_3 + 1} (α := α) (↑d : α) 0
this :
  Rat.divInt (↑a : ℤ) (↑b : ℤ) =
    (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : ℚ)
obtain :
  ∀ (k : ℕ) (hb : Ne.{u_3 + 1} (α := α) (↑(d * k) : α) 0)
    (e :
      divNat a (d * k) =
        Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn)
    (this :
      Rat.divInt (↑a : ℤ) (↑(d * k) : ℤ) =
        (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : ℚ)),
    Eq.{u_3 + 1} (α := α) (↑(d * k) : α) 0
⊢ Eq.{u_3 + 1} (α := α) (↑b : α) 0

Tactic:
obtain ⟨k, rfl⟩ : d ∣ b := by simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b

Premises used: rfl
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Eq.{u_3 + 1} (α := α) (↑d : α) 0
k : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑(d * k) : α) 0
e : divNat a (d * k) = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
this :
  Rat.divInt (↑a : ℤ) (↑(d * k) : ℤ) =
    (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : ℚ)
⊢ Eq.{u_3 + 1} (α := α) (↑(d * k) : α) 0

Tactic:
simp [*]
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
⊢ Ne.{u_3 + 1} (α := α) (↑d : α) 0

Tactic:
have hd : (d : α) ≠ 0 := by
    refine fun hd ↦ hb ?_
    have : Rat.divInt a b = _ := congr_arg NNRat.cast e
    obtain ⟨k, rfl⟩ : d ∣ b := by simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b
    simp [*]
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb : Ne.{u_3 + 1} (α := α) (↑0 : α) 0
e : divNat a 0 = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
⊢ False

Tactic:
hb Nat.cast_zero

Premises used: Nat.cast_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb : Ne.{u_3 + 1} (α := α) (↑0 : α) 0
e : divNat a 0 = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
⊢ False

Tactic:
exact hb Nat.cast_zero

Premises used: Nat.cast_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
⊢ b ≠ 0

Tactic:
have hb' : b ≠ 0 := by rintro rfl; exact hb Nat.cast_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
e : divNat a b = Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
⊢ a * d = n * b

Tactic:
simp_rw [Rat.mk_eq_divInt, mk_divInt, divNat_inj hb' h] at e

Premises used: NNRat.mk_divInt, NNRat.divNat_inj, Rat.mk_eq_divInt
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
rw :
  HDiv.hDiv (α := α)
      (↑(num (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ } hn)) :
        α)
      (↑(den (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ } hn)) :
        α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)
⊢ (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c } hn) : α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)

Tactic:
rw [cast_def]

Premises used: NNRat.cast_def
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
dsimp : HDiv.hDiv (α := α) (↑n : α) (↑d : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
⊢ HDiv.hDiv (α := α)
      (↑(num (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ } hn)) :
        α)
      (↑(den (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ } hn)) :
        α) =
    HDiv.hDiv (α := α) (↑a : α) (↑b : α)

Tactic:
dsimp
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
rw : HMul.hMul (α := α) (↑n : α) (↑b : α) = HMul.hMul (α := α) (↑a : α) (↑d : α)
rw₁ : Commute.{u_3} (S := α) (↑d : α) (↑b : α)
⊢ HDiv.hDiv (α := α) (↑n : α) (↑d : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)

Tactic:
rw [Commute.div_eq_div_iff _ hd hb]

Premises used: Commute.div_eq_div_iff
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
norm_cast : Eq.{u_3 + 1} (α := α) (↑(n * b) : α) (↑(a * d) : α)
⊢ HMul.hMul (α := α) (↑n : α) (↑b : α) = HMul.hMul (α := α) (↑a : α) (↑d : α)

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
rw rw₁ : Eq.{u_3 + 1} (α := α) (↑(n * b) : α) (↑(n * b) : α)
⊢ Eq.{u_3 + 1} (α := α) (↑(n * b) : α) (↑(a * d) : α)

Tactic:
rw [e]
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
⊢ Commute.{u_3} (S := α) (↑d : α) (↑b : α)

Tactic:
b.commute_cast _

Premises used: Nat.commute_cast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
a b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (Int.natAbs (↑n : ℤ)).Coprime d
hn : 0 ≤ { num := (↑n : ℤ), den := d, den_nz := h, reduced := c : ℚ }
hd : Ne.{u_3 + 1} (α := α) (↑d : α) 0
hb' : b ≠ 0
e : a * d = n * b
⊢ Commute.{u_3} (S := α) (↑d : α) (↑b : α)

Tactic:
exact b.commute_cast _

Premises used: Nat.commute_cast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
rw :
  HDiv.hDiv (α := α) (↑(q.num * r.den + q.den * r.num) : α) (↑(q.den * r.den) : α) =
    (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)) /
      HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
hb : Ne.{u_3 + 1} (α := α) (↑(q.den * r.den) : α) 0
⊢ (↑(q + r) : α) = HAdd.hAdd (α := α) (↑q : α) (↑r : α)

Tactic:
rw [add_def, cast_divNat_of_ne_zero, cast_def, cast_def, mul_comm _ q.den,
    (Nat.commute_cast _ _).div_add_div (Nat.commute_cast _ _) hq hr]

Premises used: Nat.commute_cast, NNRat.cast_def, NNRat.add_def, Commute.div_add_div, NNRat.den, mul_comm, NNRat.cast_divNat_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
push_cast :
  (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)) /
      HMul.hMul (α := α) (↑q.den : α) (↑r.den : α) =
    (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)) /
      HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
⊢ HDiv.hDiv (α := α) (↑(q.num * r.den + q.den * r.num) : α) (↑(q.den * r.den) : α) =
    (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)) /
      HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)

Tactic:
push_cast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
⊢ (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)) /
      HMul.hMul (α := α) (↑q.den : α) (↑r.den : α) =
    (HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) + HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)) /
      HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)

Tactic:
rfl
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
hb : HMul.hMul (α := α) (↑q.den : α) (↑r.den : α) ≠ 0
⊢ Ne.{u_3 + 1} (α := α) (↑(q.den * r.den) : α) 0

Tactic:
push_cast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
⊢ HMul.hMul (α := α) (↑q.den : α) (↑r.den : α) ≠ 0

Tactic:
mul_ne_zero hq hr

Premises used: mul_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
⊢ HMul.hMul (α := α) (↑q.den : α) (↑r.den : α) ≠ 0

Tactic:
exact mul_ne_zero hq hr

Premises used: mul_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
rw :
  HDiv.hDiv (α := α) (↑(q.num * r.num) : α) (↑(q.den * r.den) : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
hb : Ne.{u_3 + 1} (α := α) (↑(q.den * r.den) : α) 0
⊢ (↑(q * r) : α) = HMul.hMul (α := α) (↑q : α) (↑r : α)

Tactic:
rw [mul_def, cast_divNat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]

Premises used: NNRat.mul_def, NNRat.cast_def, Commute.div_mul_div_comm, NNRat.cast_divNat_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
push_cast :
  HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)
⊢ HDiv.hDiv (α := α) (↑(q.num * r.num) : α) (↑(q.den * r.den) : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)

Tactic:
push_cast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.den : α) 0
⊢ HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.num : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.den : α)

Tactic:
rfl
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw : Eq.{u_3 + 1} (α := α) (↑(divNat q.den q.num) : α) (↑q : α)⁻¹
rw₁ : HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α) = (↑q : α)⁻¹
rw₂ : HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α) = (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α))⁻¹
rw₃ rw₄ : HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α) = HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α)
⊢ Eq.{u_3 + 1} (α := α) (↑q⁻¹ : α) (↑q : α)⁻¹

Tactic:
rw [inv_def, cast_divNat_of_ne_zero _ hq, cast_def, inv_div]

Premises used: NNRat.cast_def, NNRat.inv_def, NNRat.cast_divNat_of_ne_zero, inv_div
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.num : α) 0
rw :
  HDiv.hDiv (α := α) (↑(q.num * r.den) : α) (↑(q.den * r.num) : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)
hb : Ne.{u_3 + 1} (α := α) (↑(q.den * r.num) : α) 0
⊢ (↑(q / r) : α) = HDiv.hDiv (α := α) (↑q : α) (↑r : α)

Tactic:
rw [div_def, cast_divNat_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _),
    inv_div, (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]

Premises used: NNRat.cast_def, Commute.div_mul_div_comm, HDiv.hDiv, NNRat.div_def, div_eq_mul_inv, NNRat.cast_divNat_of_ne_zero, inv_div
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.num : α) 0
push_cast :
  HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)
⊢ HDiv.hDiv (α := α) (↑(q.num * r.den) : α) (↑(q.den * r.num) : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)

Tactic:
push_cast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.num : α) 0
⊢ HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α) =
    HMul.hMul (α := α) (↑q.num : α) (↑r.den : α) / HMul.hMul (α := α) (↑q.den : α) (↑r.num : α)

Tactic:
rfl
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.num : α) 0
hb : HMul.hMul (α := α) (↑q.den : α) (↑r.num : α) ≠ 0
⊢ Ne.{u_3 + 1} (α := α) (↑(q.den * r.num) : α) 0

Tactic:
push_cast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.num : α) 0
⊢ HMul.hMul (α := α) (↑q.den : α) (↑r.num : α) ≠ 0

Tactic:
mul_ne_zero hq hr

Premises used: mul_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q r : ℚ≥0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
hr : Ne.{u_3 + 1} (α := α) (↑r.num : α) 0
⊢ HMul.hMul (α := α) (↑q.den : α) (↑r.num : α) ≠ 0

Tactic:
exact mul_ne_zero hq hr

Premises used: mul_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
n : ℤ
rw : HDiv.hDiv (α := α) (↑n : α) 1 = (↑n : α)
rw₁ rw₂ : Eq.{u_3 + 1} (α := α) (↑n : α) (↑n : α)
⊢ HDiv.hDiv (α := α) (↑n : α) (↑1 : α) = (↑n : α)

Tactic:
rw [Nat.cast_one, div_one]

Premises used: div_one, Nat.cast_one
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
n : ℕ
rw : Eq.{u_3 + 1} (α := α) (↑(↑(↑n : ℤ) : ℚ) : α) (↑n : α)
rw₁ : Eq.{u_3 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)
rw₂ rw₃ : Eq.{u_3 + 1} (α := α) (↑n : α) (↑n : α)
⊢ Eq.{u_3 + 1} (α := α) (↑(↑n : ℚ) : α) (↑n : α)

Tactic:
rw [← Int.cast_natCast, cast_intCast, Int.cast_natCast]

Premises used: Int.cast_natCast, Rat.cast_intCast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_3 + 1} (α := α) (↑(OfNat.ofNat n) : α) (OfNat.ofNat n)

Tactic:
simp [cast_def]

Premises used: Rat.cast_def
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
⊢ Eq.{u_3 + 1} (α := α) (↑0 : α) 0

Tactic:
(cast_intCast _).trans Int.cast_zero

Premises used: Rat.cast_intCast, Int.cast_zero, Eq.trans
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
⊢ Eq.{u_3 + 1} (α := α) (↑1 : α) 1

Tactic:
(cast_intCast _).trans Int.cast_one

Premises used: Rat.cast_intCast, Int.cast_one, Eq.trans
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
r : ℚ
a : α
⊢ Commute (↑r : α) a

Tactic:
simpa only [cast_def] using (r.1.cast_commute a).div_left (r.2.cast_commute a)

Premises used: Rat.num, Commute.div_left, Rat.den, Rat.cast_def, Int.cast_commute, Nat.cast_commute
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
r : ℚ
a : α
⊢ (↑r : α) * a = a * (↑r : α)

Tactic:
(cast_commute r a).eq

Premises used: Rat.cast_commute, Commute.eq
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a : α
r : ℚ
⊢ Commute a (↑r : α)

Tactic:
(r.cast_commute a).symm

Premises used: Commute.symm, Rat.cast_commute
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
⊢ b ≠ 0

Tactic:
mt ?_ b0

Premises used: mt