awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
refine : b = 0 → Eq.{u_3 + 1} (α := α) (↑b : α) 0
⊢ b ≠ 0

Tactic:
refine mt ?_ b0

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

Tactic:
simp +contextual
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
⊢ b ≠ 0

Tactic:
have b0' : b ≠ 0 := by
    refine mt ?_ b0
    simp +contextual
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
rcases :
  ∀ (n : ℤ) (d : ℕ) (h : d ≠ 0) (c : n.natAbs.Coprime d)
    (e : a /. b = { num := n, den := d, den_nz := h, reduced := c }),
    (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)
⊢ (↑(a /. b) : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)

Tactic:
rcases e : a /. b with ⟨n, d, h, c⟩
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
⊢ (↑(a /. b).den : ℤ) ∣ b

Tactic:
have dd := den_dvd a b
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
rwa rwa₁ rwa₂ rwa₃ : ∀ (dd : (↑{ num := n, den := d, den_nz := h, reduced := c }.den : ℤ) ∣ b), (↑d : ℤ) ∣ b
⊢ (↑d : ℤ) ∣ b

Tactic:
rwa [e] at dd
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
rcases : ∀ (k : ℤ) (ke : b = (↑d : ℤ) * k), False
⊢ False

Tactic:
rcases show (d : ℤ) ∣ b by rwa [e] at dd with ⟨k, ke⟩
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
k : ℤ
ke : b = (↑d : ℤ) * k
rw : (↑((↑d : ℤ) * k) : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
rw₁ : HMul.hMul (α := α) (↑(↑d : ℤ) : α) (↑k : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
rw₂ rw₃ : HMul.hMul (α := α) (↑d : α) (↑k : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
⊢ (↑b : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)

Tactic:
rw [ke, Int.cast_mul, Int.cast_natCast]

Premises used: Int.cast_natCast, Int.cast_mul
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
k : ℤ
ke : b = (↑d : ℤ) * k
⊢ (↑b : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)

Tactic:
have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_natCast]
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
k : ℤ
ke : b = (↑d : ℤ) * k
this : (↑b : α) = HMul.hMul (α := α) (↑d : α) (↑k : α)
⊢ Eq.{u_3 + 1} (α := α) (↑b : α) 0

Tactic:
rw [d0, zero_mul] at this

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : Eq.{u_3 + 1} (α := α) (↑d : α) 0
dd : (↑(a /. b).den : ℤ) ∣ b
k : ℤ
ke : b = (↑d : ℤ) * k
this : Eq.{u_3 + 1} (α := α) (↑b : α) 0
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ Ne.{u_3 + 1} (α := α) (↑d : α) 0

Tactic:
have d0 : (d : α) ≠ 0 := by
    intro d0
    have dd := den_dvd a b
    rcases show (d : ℤ) ∣ b by rwa [e] at dd with ⟨k, ke⟩
    have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_natCast]
    rw [d0, zero_mul] at this
    contradiction
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
⊢ a /. b = n /. (↑d : ℤ)

Tactic:
rw [mk_eq_divInt] at e

Premises used: Rat.mk_eq_divInt
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
e₁ : a /. b = n /. (↑d : ℤ)
⊢ Ne.{u_3 + 1} (α := α) (↑d : α) 0

Tactic:
rw [mk_eq_divInt] at e

Premises used: Rat.mk_eq_divInt
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
⊢ Eq.{u_3 + 1} (α := α) (↑(a * (↑d : ℤ)) : α) (↑(n * b) : α)

Tactic:
have := congr_arg ((↑) : ℤ → α)
    ((divInt_eq_divInt_iff b0' <| ne_of_gt <| Int.natCast_pos.2 h.bot_lt).1 e)
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
this : Eq.{u_3 + 1} (α := α) (↑(a * (↑d : ℤ)) : α) (↑(n * b) : α)
⊢ HMul.hMul (α := α) (↑a : α) (↑d : α) = HMul.hMul (α := α) (↑n : α) (↑b : α)

Tactic:
rw [Int.cast_mul, Int.cast_mul, Int.cast_natCast] at this

Premises used: Int.cast_natCast, Int.cast_mul
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a b : ℤ
b0 : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. (↑d : ℤ)
d0 : Ne.{u_3 + 1} (α := α) (↑d : α) 0
this : HMul.hMul (α := α) (↑a : α) (↑d : α) = HMul.hMul (α := α) (↑n : α) (↑b : α)
rw : HDiv.hDiv (α := α) (↑a : α) (↑b : α) = (↑{ num := n, den := d, den_nz := h, reduced := c } : α)
rw₁ :
  HDiv.hDiv (α := α) (↑a : α) (↑b : α) =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
rw₂ :
  HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ =
    HDiv.hDiv (α := α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
      (↑{ num := n, den := d, den_nz := h, reduced := c }.den : α)
rw₃ : HMul.hMul (α := α) (↑a : α) (↑b : α)⁻¹ * (↑d : α) = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₄ : (↑a : α) * HMul.hMul (α := α) (↑b : α)⁻¹ (↑d : α) = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₅ : (↑a : α) * HMul.hMul (α := α) (↑d : α) (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₆ : HMul.hMul (α := α) (↑a : α) (↑d : α) * (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₇ : HMul.hMul (α := α) (↑n : α) (↑b : α) * (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₈ : (↑n : α) * HMul.hMul (α := α) (↑b : α) (↑b : α)⁻¹ = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₉ : HMul.hMul (α := α) (↑n : α) 1 = (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
rw₁₀ rw₁₁ : Eq.{u_3 + 1} (α := α) (↑n : α) (↑{ num := n, den := d, den_nz := h, reduced := c }.num : α)
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c } : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)

Tactic:
rw [eq_comm, cast_def, div_eq_mul_inv, eq_div_iff_mul_eq d0, mul_assoc, (d.commute_cast _).eq,
    ← mul_assoc, this, mul_assoc, mul_inv_cancel₀ b0, mul_one]

Premises used: Nat.commute_cast, mul_inv_cancel₀, mul_assoc, eq_comm, div_eq_mul_inv, Rat.cast_def, eq_div_iff_mul_eq, mul_one, Commute.eq
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a : ℤ
b : ℕ
hb : Ne.{u_3 + 1} (α := α) (↑b : α) 0
b0 : Ne.{u_3 + 1} (α := α) (↑(↑b : ℤ) : α) 0
⊢ (↑(mkRat a b) : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)

Tactic:
rw [Rat.mkRat_eq_divInt, cast_divInt_of_ne_zero, Int.cast_natCast]

Premises used: Int.cast_natCast, Rat.mkRat_eq_divInt, Rat.cast_divInt_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
a : ℤ
b : ℕ
hb b0 b0₁ b0₂ b0₃ : Ne.{u_3 + 1} (α := α) (↑b : α) 0
⊢ Ne.{u_3 + 1} (α := α) (↑(↑b : ℤ) : α) 0

Tactic:
rwa [Int.cast_natCast]

Premises used: Int.cast_natCast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
q r : ℚ
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_mkRat_of_ne_zero, cast_def, cast_def, mul_comm r.num,
    (Nat.cast_commute _ _).div_add_div (Nat.commute_cast _ _) hq hr]

Premises used: Nat.commute_cast, Rat.add_def', Rat.num, Rat.cast_mkRat_of_ne_zero, Commute.div_add_div, Rat.cast_def, mul_comm, Nat.cast_commute
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
q r : ℚ
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 : DivisionRing α
q r : ℚ
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 : DivisionRing α
q r : ℚ
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 : DivisionRing α
q r : ℚ
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 : DivisionRing α
q r : ℚ
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 : DivisionRing α
q : ℚ
⊢ Eq.{u_3 + 1} (α := α) (↑(-q) : α) (-(↑q : α))

Tactic:
simp [cast_def, neg_div]

Premises used: neg_div, Rat.cast_def
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
⊢ (↑(p - q) : α) = HSub.hSub (α := α) (↑p : α) (↑q : α)

Tactic:
simp [sub_eq_add_neg, cast_add_of_ne_zero, hp, hq]

Premises used: sub_eq_add_neg, Rat.cast_add_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
rw :
  HDiv.hDiv (α := α) (↑(p.num * q.num) : α) (↑(p.den * q.den) : α) =
    HMul.hMul (α := α) (↑p.num : α) (↑q.num : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.den : α)
hb : Ne.{u_3 + 1} (α := α) (↑(p.den * q.den) : α) 0
⊢ (↑(p * q) : α) = HMul.hMul (α := α) (↑p : α) (↑q : α)

Tactic:
rw [mul_eq_mkRat, cast_mkRat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Int.commute_cast _ _)]

Premises used: Rat.mul_eq_mkRat, Commute.div_mul_div_comm, Rat.cast_mkRat_of_ne_zero, Rat.cast_def
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
push_cast :
  HMul.hMul (α := α) (↑p.num : α) (↑q.num : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.den : α) =
    HMul.hMul (α := α) (↑p.num : α) (↑q.num : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.den : α)
⊢ HDiv.hDiv (α := α) (↑(p.num * q.num) : α) (↑(p.den * q.den) : α) =
    HMul.hMul (α := α) (↑p.num : α) (↑q.num : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.den : α)

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

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

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

Tactic:
mul_ne_zero hp hq

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

Tactic:
exact mul_ne_zero hp hq

Premises used: mul_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
q : ℚ
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw : Eq.{u_3 + 1} (α := α) (↑((↑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₃ : HDiv.hDiv (α := α) (↑(↑q.den : ℤ) : α) (↑q.num : α) = HDiv.hDiv (α := α) (↑q.den : α) (↑q.num : α)
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_divInt_of_ne_zero _ hq, cast_def, inv_div, Int.cast_natCast]

Premises used: Int.cast_natCast, Rat.cast_def, Rat.inv_def, inv_div, Rat.cast_divInt_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
rw :
  HDiv.hDiv (α := α) (↑(p.num * (↑q.den : ℤ)) : α) (↑((↑p.den : ℤ) * q.num) : α) =
    HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.num : α)
b0 : Ne.{u_3 + 1} (α := α) (↑((↑p.den : ℤ) * q.num) : α) 0
⊢ (↑(p / q) : α) = HDiv.hDiv (α := α) (↑p : α) (↑q : α)

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

Premises used: Rat.div_def', Commute.div_mul_div_comm, HDiv.hDiv, div_eq_mul_inv, Rat.cast_def, inv_div, Rat.cast_divInt_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
push_cast :
  HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.num : α) =
    HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.num : α)
⊢ HDiv.hDiv (α := α) (↑(p.num * (↑q.den : ℤ)) : α) (↑((↑p.den : ℤ) * q.num) : α) =
    HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) / HMul.hMul (α := α) (↑p.den : α) (↑q.num : α)

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

Tactic:
rfl
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionRing α
p q : ℚ
hp : Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hq : Ne.{u_3 + 1} (α := α) (↑q.num : α) 0
b0 : HMul.hMul (α := α) (↑p.den : α) (↑q.num : α) ≠ 0
⊢ Ne.{u_3 + 1} (α := α) (↑((↑p.den : ℤ) * q.num) : α) 0

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

Tactic:
mul_ne_zero hp hq

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

Tactic:
exact mul_ne_zero hp hq

Premises used: mul_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : DivisionSemiring α
inst_2 : DivisionSemiring β
inst_3 : RingHomClass F α β
f : F
q : ℚ≥0
simp_rw :
  (f : (a : α) → β) (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)) = HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)
simp_rw₁ :
  HDiv.hDiv (α := β) (β := β) ((f : (a : α) → β) (↑q.num : α) : β) ((f : (a : α) → β) (↑q.den : α) : β) =
    HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)

Tactic:
simp_rw [NNRat.cast_def, map_div₀, map_natCast]

Premises used: NNRat.cast_def, map_div₀, map_natCast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
α : Type u_3
inst : DivisionSemiring α
inst_1 : FunLike F ℚ≥0 α
inst_2 : RingHomClass F ℚ≥0 α
f : F
q : ℚ≥0
rw : Eq.{u_3 + 1} (α := α) ((f : (a : ℚ≥0) → α) q : α) ((f : (a : ℚ≥0) → α) (↑q : ℚ≥0) : α)
rw₁ rw₂ : Eq.{u_3 + 1} (α := α) ((f : (a : ℚ≥0) → α) q : α) ((f : (a : ℚ≥0) → α) q : α)
⊢ Eq.{u_3 + 1} (α := α) ((f : (a : ℚ≥0) → α) q : α) ((↑q : α) : α)

Tactic:
rw [← map_nnratCast f, NNRat.cast_id]

Premises used: map_nnratCast, NNRat.cast_id
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : FunLike F α β
inst_1 : DivisionRing α
inst_2 : DivisionRing β
inst_3 : RingHomClass F α β
f : F
q : ℚ
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)) : β) ((↑q : β) : β)
rw₁ : HDiv.hDiv (α := β) (β := β) ((f : (a : α) → β) (↑q.num : α) : β) ((f : (a : α) → β) (↑q.den : α) : β) = (↑q : β)
rw₂ : HDiv.hDiv (α := β) (β := β) ((↑q.num : β) : β) ((f : (a : α) → β) (↑q.den : α) : β) = (↑q : β)
rw₃ : HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β) = (↑q : β)
rw₄ rw₅ : HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β) = HDiv.hDiv (α := β) (↑q.num : β) (↑q.den : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (↑q : α) : β) ((↑q : β) : β)

Tactic:
rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]

Premises used: map_intCast, Rat.cast_def, map_div₀, map_natCast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
α : Type u_3
inst : DivisionRing α
inst_1 : FunLike F ℚ α
inst_2 : RingHomClass F ℚ α
f : F
q : ℚ
rw : Eq.{u_3 + 1} (α := α) ((f : (a : ℚ) → α) q : α) ((f : (a : ℚ) → α) (↑q : ℚ) : α)
rw₁ rw₂ : Eq.{u_3 + 1} (α := α) ((f : (a : ℚ) → α) q : α) ((f : (a : ℚ) → α) q : α)
⊢ Eq.{u_3 + 1} (α := α) ((f : (a : ℚ) → α) q : α) ((↑q : α) : α)

Tactic:
rw [← map_ratCast f, Rat.cast_id]

Premises used: map_ratCast, Rat.cast_id
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
M₀ : Type u_5
inst : MonoidWithZero M₀
inst_1 : FunLike F ℚ≥0 M₀
inst_2 : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ≥0) → M₀) (↑n : ℚ≥0) : M₀) ((g : (a : ℚ≥0) → M₀) (↑n : ℚ≥0) : M₀)
r : ℚ≥0
rw : Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ≥0) → M₀) (↑r.den : ℚ≥0) : M₀) ((g : (a : ℚ≥0) → M₀) (↑r.den : ℚ≥0) : M₀)
⊢ Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ≥0) → M₀) r : M₀) ((g : (a : ℚ≥0) → M₀) r : M₀)

Tactic:
rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, eq_on_inv₀ f g]

Premises used: div_eq_mul_inv, map_mul, eq_on_inv₀, NNRat.num_div_den
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
M₀ : Type u_5
inst : MonoidWithZero M₀
inst_1 : FunLike F ℚ≥0 M₀
inst_2 : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ≥0) → M₀) (↑n : ℚ≥0) : M₀) ((g : (a : ℚ≥0) → M₀) (↑n : ℚ≥0) : M₀)
r : ℚ≥0
⊢ Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ≥0) → M₀) (↑r.den : ℚ≥0) : M₀) ((g : (a : ℚ≥0) → M₀) (↑r.den : ℚ≥0) : M₀)

Tactic:
apply h
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
M₀ : Type u_5
inst : MonoidWithZero M₀
f g : ℚ≥0 →*₀ M₀
h : Eq (α := ℕ →*₀ M₀) (f.comp (↑(Nat.castRingHom ℚ≥0) : ℕ →*₀ ℚ≥0)) (g.comp (↑(Nat.castRingHom ℚ≥0) : ℕ →*₀ ℚ≥0))
⊢ f = g

Tactic:
ext_nnrat' <| DFunLike.congr_fun h

Premises used: DFunLike.congr_fun, MonoidWithZeroHomClass.ext_nnrat'
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
M₀ : Type u_5
inst : MonoidWithZero M₀
inst_1 : FunLike F ℚ≥0 M₀
inst_2 : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
same_on_pnat :
  ∀ (n : ℕ),
    0 < n → Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ≥0) → M₀) (↑n : ℚ≥0) : M₀) ((g : (a : ℚ≥0) → M₀) (↑n : ℚ≥0) : M₀)
⊢ ∀ {n : ℕ},
    0 < n →
      Eq (α := M₀)
        ((MonoidWithZeroHom.comp (↑f : ℚ≥0 →*₀ M₀) (↑(Nat.castRingHom ℚ≥0) : ℕ →*₀ ℚ≥0) : (a : ℕ) → M₀) n : M₀)
        ((MonoidWithZeroHom.comp (↑g : ℚ≥0 →*₀ M₀) (↑(Nat.castRingHom ℚ≥0) : ℕ →*₀ ℚ≥0) : (a : ℕ) → M₀) n : M₀)

Tactic:
simpa
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
M₀ : Type u_5
inst : MonoidWithZero M₀
inst_1 : FunLike F ℚ M₀
inst_2 : MonoidWithZeroHomClass F ℚ M₀
f g : F
h : ∀ (m : ℤ), Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ) → M₀) (↑m : ℚ) : M₀) ((g : (a : ℚ) → M₀) (↑m : ℚ) : M₀)
r : ℚ
rw : Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ) → M₀) (↑(↑r.den : ℤ) : ℚ) : M₀) ((g : (a : ℚ) → M₀) (↑(↑r.den : ℤ) : ℚ) : M₀)
⊢ Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ) → M₀) r : M₀) ((g : (a : ℚ) → M₀) r : M₀)

Tactic:
rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, ← Int.cast_natCast,
      eq_on_inv₀ f g]

Premises used: Rat.num_div_den, Int.cast_natCast, div_eq_mul_inv, map_mul, eq_on_inv₀