awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      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₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. (↑d₁ : ℤ)
x : ℚ
hc : c /. d = x
obtain :
  ∀ (n₂ : ℤ) (d₂ : ℕ) (h₂ : d₂ ≠ 0) (c₂ : n₂.natAbs.Coprime d₂)
    (hc : c /. d = { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ }),
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      f₁ a b c d /. f₂ a b c d
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ } x = f₁ a b c d /. f₂ a b c d

Tactic:
obtain ⟨n₂, d₂, h₂, c₂⟩ := x
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      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₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. (↑d₁ : ℤ)
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ }
⊢ c /. d = n₂ /. (↑d₂ : ℤ)

Tactic:
rw [mk_eq_divInt] at hc

Premises used: Rat.mk_eq_divInt
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      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₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. (↑d₁ : ℤ)
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. (↑d₂ : ℤ)
rw : f₁ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) /. f₂ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) = f₁ a b c d /. f₂ a b c d
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
      { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
    f₁ a b c d /. f₂ a b c d

Tactic:
rw [fv]
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      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₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. (↑d₁ : ℤ)
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. (↑d₂ : ℤ)
⊢ Ne (α := ℤ) (↑d₁ : ℤ) 0

Tactic:
have d₁0 := Int.ofNat_ne_zero.2 h₁
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      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₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. (↑d₁ : ℤ)
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. (↑d₂ : ℤ)
d₁0 : Ne (α := ℤ) (↑d₁ : ℤ) 0
⊢ Ne (α := ℤ) (↑d₂ : ℤ) 0

Tactic:
have d₂0 := Int.ofNat_ne_zero.2 h₂
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      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₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. (↑d₁ : ℤ)
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. (↑d₂ : ℤ)
d₁0 : Ne (α := ℤ) (↑d₁ : ℤ) 0
d₂0 : Ne (α := ℤ) (↑d₂ : ℤ) 0
⊢ f₁ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) /. f₂ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) = f₁ a b c d /. f₂ a b c d

Tactic:
(divInt_eq_divInt_iff (f0 d₁0 d₂0) (f0 b0 d0)).2
    (H ((divInt_eq_divInt_iff b0 d₁0).1 ha) ((divInt_eq_divInt_iff d0 d₂0).1 hc))

Premises used: Iff.mpr, Rat.divInt_eq_divInt_iff, Iff.mp
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      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₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. (↑d₁ : ℤ)
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. (↑d₂ : ℤ)
d₁0 : Ne (α := ℤ) (↑d₁ : ℤ) 0
d₂0 : Ne (α := ℤ) (↑d₂ : ℤ) 0
⊢ f₁ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) /. f₂ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) = f₁ a b c d /. f₂ a b c d

Tactic:
exact (divInt_eq_divInt_iff (f0 d₁0 d₂0) (f0 b0 d0)).2
    (H ((divInt_eq_divInt_iff b0 d₁0).1 ha) ((divInt_eq_divInt_iff d0 d₂0).1 hc))

Premises used: Iff.mpr, Rat.divInt_eq_divInt_iff, Iff.mp
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
rw : -q = -(q.num /. (↑q.den : ℤ))
rw₁ rw₂ : -q = -q
⊢ -q = -q.num /. (↑q.den : ℤ)

Tactic:
rw [← neg_divInt, num_divInt_den]

Premises used: Rat.num_divInt_den, Rat.neg_divInt
-- Module: Mathlib.Data.Rat.Defs
Goal:
n d : ℤ
⊢ n /. -d = -n /. d

Tactic:
divInt_neg' ..

Premises used: Rat.divInt_neg'
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
rw : (n₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)
⊢ (n₁ * n₂).natAbs.Coprime (d₁ * d₂)

Tactic:
rw [Int.natAbs_mul]

Premises used: Int.natAbs_mul
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)

Tactic:
(hnd₁.mul_left h₂₁).mul_right (h₁₂.mul_left hnd₂)

Premises used: Nat.Coprime.mul_right, Nat.Coprime.mul_left
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)

Tactic:
exact (hnd₁.mul_left h₂₁).mul_right (h₁₂.mul_left hnd₂)

Premises used: Nat.Coprime.mul_right, Nat.Coprime.mul_left
-- Module: Mathlib.Data.Rat.Defs
Goal:
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
rw :
  normalize
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ : ℚ }.num *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ : ℚ }.num)
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ : ℚ }.den *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ : ℚ }.den)
      ⋯ =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }
⊢ { num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ : ℚ } *
      { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ : ℚ } =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Tactic:
rw [mul_def]

Premises used: Rat.mul_def
-- Module: Mathlib.Data.Rat.Defs
Goal:
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ normalize
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ : ℚ }.num *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ : ℚ }.num)
      ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ : ℚ }.den *
        { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ : ℚ }.den)
      ⋯ =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }

Tactic:
simp [mk_eq_normalize]

Premises used: Rat.mk_eq_normalize
-- Module: Mathlib.Data.Rat.Defs
Goal:
q r : ℚ
rw : normalize (q.num * r.num) (q.den * r.den) ⋯ = mkRat (q.num * r.num) (q.den * r.den)
rw₁ rw₂ : mkRat (q.num * r.num) (q.den * r.den) = mkRat (q.num * r.num) (q.den * r.den)
⊢ q * r = mkRat (q.num * r.num) (q.den * r.den)

Tactic:
rw [mul_def, normalize_eq_mkRat]

Premises used: Rat.normalize_eq_mkRat, Rat.mul_def
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
n : ℕ
rw : { num := q.num ^ n, den := q.den ^ n, den_nz := ⋯, reduced := ⋯ : ℚ } = mkRat (q.num ^ n) (q.den ^ n)
rw₁ rw₂ : mkRat (q.num ^ n) (q.den ^ n) = mkRat (q.num ^ n) (q.den ^ n)
⊢ q ^ n = mkRat (q.num ^ n) (q.den ^ n)

Tactic:
rw [pow_def, mk_eq_mkRat]

Premises used: Rat.pow_def, Rat.mk_eq_mkRat
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
n : ℕ
rw :
  { num := q.num ^ n, den := q.den ^ n, den_nz := ⋯, reduced := ⋯ : ℚ } = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
rw₁ : q.num ^ n /. (↑(q.den ^ n) : ℤ) = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
rw₂ rw₃ : q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
⊢ q ^ n = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n

Tactic:
rw [pow_def, mk_eq_divInt, Int.natCast_pow]

Premises used: Rat.mk_eq_divInt, Int.natCast_pow, Rat.pow_def
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ den ^ n ≠ 0

Tactic:
simp [Nat.pow_eq_zero, hd]

Premises used: Nat.pow_eq_zero
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
rw : (num.natAbs ^ n).Coprime (den ^ n)
⊢ (num ^ n).natAbs.Coprime (den ^ n)

Tactic:
rw [Int.natAbs_pow]

Premises used: Int.natAbs_pow
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num.natAbs ^ n).Coprime (den ^ n)

Tactic:
hdn.pow _ _

Premises used: Nat.Coprime.pow
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num.natAbs ^ n).Coprime (den ^ n)

Tactic:
exact hdn.pow _ _

Premises used: Nat.Coprime.pow
-- Module: Mathlib.Data.Rat.Defs
Goal:
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ { num := num, den := den, den_nz := hd, reduced := hdn : ℚ } ^ n =
    { num := num ^ n, den := den ^ n, den_nz := ⋯, reduced := ⋯ }

Tactic:
rfl

Premises used: Rat.pow, rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
a : ℤ
b : ℕ
rw : (a /. (↑b : ℤ))⁻¹ = (↑b : ℤ) /. a
rw₁ rw₂ : (↑b : ℤ) /. a = (↑b : ℤ) /. a
⊢ (mkRat a b)⁻¹ = (↑b : ℤ) /. a

Tactic:
rw [mkRat_eq_divInt, inv_divInt]

Premises used: Rat.inv_divInt, Rat.mkRat_eq_divInt
-- Module: Mathlib.Data.Rat.Defs
Goal:
n₁ d₁ n₂ d₂ : ℤ
rw : n₁ /. d₁ * (n₂ /. d₂)⁻¹ = n₁ * d₂ /. (d₁ * n₂)
rw₁ : n₁ /. d₁ * (d₂ /. n₂) = n₁ * d₂ /. (d₁ * n₂)
rw₂ rw₃ : n₁ * d₂ /. (d₁ * n₂) = n₁ * d₂ /. (d₁ * n₂)
⊢ n₁ /. d₁ / (n₂ /. d₂) = n₁ * d₂ /. (d₁ * n₂)

Tactic:
rw [div_def, inv_divInt, divInt_mul_divInt]

Premises used: Rat.div_def, Rat.inv_divInt, Rat.divInt_mul_divInt
-- Module: Mathlib.Data.Rat.Defs
Goal:
q r : ℚ
rw : q / r = q.num /. (↑q.den : ℤ) / (r.num /. (↑r.den : ℤ))
rw₁ : q / r = q / (r.num /. (↑r.den : ℤ))
rw₂ rw₃ : q / r = q / r
⊢ q / r = q.num * (↑r.den : ℤ) /. ((↑q.den : ℤ) * r.num)

Tactic:
rw [← divInt_div_divInt, num_divInt_den, num_divInt_den]

Premises used: Rat.num_divInt_den, Rat.divInt_div_divInt
-- Module: Mathlib.Data.Rat.Defs
Goal:
n : ℤ
⊢ n /. 1 = (↑n : ℚ)

Tactic:
simp [divInt, mkRat, normalize]

Premises used: Rat.divInt, Rat.normalize, mkRat, OfNat.ofNat
-- Module: Mathlib.Data.Rat.Defs
Goal:
rw : Eq (α := ℚ) (↑1 : ℚ) 1
rw₁ rw₂ : Eq (α := ℚ) 1 1
⊢ 1 /. 1 = 1

Tactic:
rw [divInt_one, Rat.intCast_one]

Premises used: Rat.divInt_one, Rat.intCast_one
-- Module: Mathlib.Data.Rat.Defs
Goal:
rw rw₁ : Ne (α := ℤ) 1 0
⊢ Ne (α := ℚ) 0 1

Tactic:
rw [ne_comm, ← divInt_one_one, divInt_ne_zero]

Premises used: Rat.divInt_one_one, Rat.divInt_ne_zero, ne_comm
-- Module: Mathlib.Data.Rat.Defs
Goal:
⊢ Ne (α := ℤ) 1 0

Tactic:
lia
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ Ne (α := ℚ) 1 0

Tactic:
decide
-- Module: Mathlib.Data.Rat.Defs
Goal:
q_1 a b c : ℚ
n : ℕ
q : ℚ
rw : (↑(↑n : ℤ) : ℚ) * q + q = (↑n : ℚ) * q + q
⊢ (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℚ) * q = (↑n : ℚ) * q + q

Tactic:
rw [Rat.intCast_add, Rat.add_mul, Rat.intCast_one, Rat.one_mul]

Premises used: Rat.add_mul, Rat.intCast_add, Rat.intCast_one, Rat.one_mul
-- Module: Mathlib.Data.Rat.Defs
Goal:
q_1 a b c : ℚ
n : ℕ
q : ℚ
⊢ (↑(↑n : ℤ) : ℚ) * q + q = (↑n : ℚ) * q + q

Tactic:
rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
x : ℕ
x_1 : ℚ
⊢ (↑(↑x.succ : ℤ) : ℚ) * x_1 = (↑(↑x : ℤ) : ℚ) * x_1 + x_1

Tactic:
simp [Rat.add_mul]

Premises used: Rat.add_mul
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
x : ℕ
x_1 : ℚ
rw : -((↑(HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : ℚ) * x_1) = -((↑(↑x.succ : ℤ) : ℚ) * x_1)
⊢ (↑(Int.negSucc x) : ℚ) * x_1 = -((↑(↑x.succ : ℤ) : ℚ) * x_1)

Tactic:
rw [Int.negSucc_eq, Rat.intCast_neg, Rat.neg_mul]

Premises used: Rat.intCast_neg, Rat.neg_mul, Int.negSucc_eq
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
x : ℕ
x_1 : ℚ
⊢ -((↑(HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : ℚ) * x_1) = -((↑(↑x.succ : ℤ) : ℚ) * x_1)

Tactic:
rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ AddGroup ℚ

Tactic:
infer_instance
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ AddCommMonoid ℚ

Tactic:
infer_instance
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ AddMonoid ℚ

Tactic:
infer_instance
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ AddLeftCancelSemigroup ℚ

Tactic:
infer_instance
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ AddRightCancelSemigroup ℚ

Tactic:
infer_instance
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ AddCommSemigroup ℚ

Tactic:
infer_instance
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ AddSemigroup ℚ

Tactic:
infer_instance
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ Monoid ℚ

Tactic:
infer_instance
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ CommSemigroup ℚ

Tactic:
infer_instance
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ Semigroup ℚ

Tactic:
infer_instance
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
⊢ (-q).den = q.den

Tactic:
rfl

Premises used: Int.neg, rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
⊢ (-q).num = -q.num

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
⊢ num 0 = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
⊢ den 0 = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
hq : q.num = 0
⊢ q = 0

Tactic:
simpa [hq] using q.num_divInt_den.symm

Premises used: Rat.num_divInt_den, Eq.symm
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
h : q = 0
⊢ q.num = 0

Tactic:
simp [*]
-- Module: Mathlib.Data.Rat.Defs
Goal:
⊢ num 1 = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
⊢ den 1 = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : n = 0
⊢ q = 0

Tactic:
simpa [this] using hqnd
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
n d : ℤ
hq : q ≠ 0
hqnd : q = n /. d
this : d = 0
⊢ q = 0

Tactic:
simpa [this] using hqnd
-- Module: Mathlib.Data.Rat.Defs
Goal:
n d : ℤ
h : n ≠ 0
hd : d ≠ 0
⊢ n /. d ≠ 0

Tactic:
(divInt_ne_zero hd).mpr h

Premises used: Iff.mpr, Rat.divInt_ne_zero
-- Module: Mathlib.Data.Rat.Defs
Goal:
a b c : ℤ
h : c = 0
⊢ (a + b) /. c = a /. c + b /. c

Tactic:
simp [h]
-- Module: Mathlib.Data.Rat.Defs
Goal:
a b c : ℤ
h : ¬c = 0
rw : (a + b) * (c * c) = (a * c + b * c) * c
⊢ (a + b) /. c = a /. c + b /. c

Tactic:
rw [divInt_add_divInt _ _ h h, divInt_eq_divInt_iff h (Int.mul_ne_zero h h)]

Premises used: Int.mul_ne_zero, Rat.divInt_eq_divInt_iff, Rat.divInt_add_divInt
-- Module: Mathlib.Data.Rat.Defs
Goal:
a b c : ℤ
h : ¬c = 0
⊢ (a + b) * (c * c) = (a * c + b * c) * c

Tactic:
simp [Int.add_mul, Int.mul_assoc]

Premises used: Int.mul_assoc, Int.add_mul
-- Module: Mathlib.Data.Rat.Defs
Goal:
n d : ℤ
rw rw₁ : HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
⊢ HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = n /. d

Tactic:
rw [divInt_eq_div]

Premises used: Rat.divInt_eq_div
-- Module: Mathlib.Data.Rat.Defs
Goal:
n d : ℕ
⊢ HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ) = (↑n : ℤ) /. (↑d : ℤ)

Tactic:
Rat.intCast_div_eq_divInt n d

Premises used: Nat.cast, Rat.intCast_div_eq_divInt
-- Module: Mathlib.Data.Rat.Defs
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
pos : ∀ (hd : d = 0), n /. x * (x /. d) = n /. d
neg : ∀ (hd : ¬d = 0), n /. x * (x /. d) = n /. d
⊢ n /. x * (x /. d) = n /. d

Tactic:
by_cases hd : d = 0
-- Module: Mathlib.Data.Rat.Defs
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
pos : n /. x * (x /. 0) = n /. 0
⊢ n /. x * (x /. d) = n /. d

Tactic:
rw [hd]
-- Module: Mathlib.Data.Rat.Defs
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : d = 0
⊢ n /. x * (x /. 0) = n /. 0

Tactic:
simp
-- Module: Mathlib.Data.Rat.Defs
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
neg : n * x /. (x * d) = n /. d
neg₁ : n * x /. (d * x) = n /. d
neg₂ neg₃ : n /. d = n /. d
⊢ n /. x * (x /. d) = n /. d

Tactic:
rw [divInt_mul_divInt, x.mul_comm, divInt_mul_right hx]

Premises used: Rat.divInt_mul_divInt, Int.mul_comm, Rat.divInt_mul_right
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
hq : q.den = 1
rw : q.num /. (↑1 : ℤ)
| q

Tactic:
rw [← num_divInt_den q, hq]

Premises used: Rat.num_divInt_den
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
hq : q.den = 1
conv_rhs : (↑q.num : ℚ) = q.num /. (↑1 : ℤ)
⊢ (↑q.num : ℚ) = q

Tactic:
conv_rhs => rw [← num_divInt_den q, hq]

Premises used: Rat.num_divInt_den
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
hq : q.den = 1
rw : q.num /. 1 = q.num /. (↑1 : ℤ)
⊢ (↑q.num : ℚ) = q.num /. (↑1 : ℤ)

Tactic:
rw [intCast_eq_divInt]

Premises used: Rat.intCast_eq_divInt
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
hq : q.den = 1
⊢ q.num /. 1 = q.num /. (↑1 : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
h : q.isInt = true
⊢ q.den = 1

Tactic:
rw [Rat.isInt, Nat.beq_eq_true_eq] at h

Premises used: Rat.isInt, Nat.beq_eq_true_eq
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
h : q.den = 1
⊢ q = (↑q.num : ℚ)

Tactic:
(Rat.coe_int_num_of_den_eq_one h).symm

Premises used: Rat.coe_int_num_of_den_eq_one, Eq.symm
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
h : q.den = 1
⊢ q = (↑q.num : ℚ)

Tactic:
exact (Rat.coe_int_num_of_den_eq_one h).symm

Premises used: Rat.coe_int_num_of_den_eq_one, Eq.symm
-- Module: Mathlib.Data.Rat.Defs
Goal:
r : ℚ
⊢ r.den = 1 ↔ (↑r.num : ℚ) = r

Tactic:
⟨Rat.coe_int_num_of_den_eq_one, fun h => h ▸ Rat.den_intCast r.num⟩

Premises used: Rat.num, Eq.rec, Rat.den_intCast, Rat.coe_int_num_of_den_eq_one, Iff.intro
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a b c : ℚ
⊢ CanLift ℚ ℤ Int.cast fun (q : ℚ) ↦ q.den = 1

Tactic:
⟨fun q hq => ⟨q.num, coe_int_num_of_den_eq_one hq⟩⟩

Premises used: Rat.num, Rat.coe_int_num_of_den_eq_one, Exists.intro, CanLift.mk
-- Module: Mathlib.Data.Rat.Defs
Goal:
m n : ℤ
⊢ Eq (α := ℚ) (↑m : ℚ) (↑n : ℚ) ↔ m = n

Tactic:
⟨congr_arg num, congr_arg _⟩

Premises used: Rat.num, congr_arg, Iff.intro
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a_1 b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
rw : C (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑(↑d : ℤ) : ℚ))
⊢ C { num := n, den := d, den_nz := nz, reduced := red }

Tactic:
rw [Rat.mk_eq_divInt, Rat.divInt_eq_div]

Premises used: Rat.mk_eq_divInt, Rat.divInt_eq_div
-- Module: Mathlib.Data.Rat.Defs
Goal:
q a_1 b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ))
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑(↑d : ℤ) : ℚ))

Tactic:
exact div n d nz red
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
⊢ ⌊q⌋ = q.num / (↑q.den : ℤ)

Tactic:
Rat.floor_def q

Premises used: Int.floor, Rat.floor_def, Rat.floor, ite
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
change : -⌊-q⌋ = -(-q.num / (↑q.den : ℤ))
⊢ ⌈q⌉ = -(-q.num / (↑q.den : ℤ))

Tactic:
change -⌊-q⌋ = _
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
rw : -((-q).num / (↑(-q).den : ℤ)) = -(-q.num / (↑q.den : ℤ))
rw₁ : -(-q.num / (↑(-q).den : ℤ)) = -(-q.num / (↑q.den : ℤ))
rw₂ rw₃ : -(-q.num / (↑q.den : ℤ)) = -(-q.num / (↑q.den : ℤ))
⊢ -⌊-q⌋ = -(-q.num / (↑q.den : ℤ))

Tactic:
rw [Rat.floor_def', num_neg_eq_neg_num, den_neg_eq_den]

Premises used: Rat.den_neg_eq_den, Rat.num_neg_eq_neg_num, Rat.floor_def'
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
rw : (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ) = n / (↑d : ℤ)
⊢ ⌊HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)⌋ = n / (↑d : ℤ)

Tactic:
rw [Rat.floor_def']

Premises used: Rat.floor_def'
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
inl : (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑0 : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑0 : ℚ)).den : ℤ) = n / (↑0 : ℤ)
inr :
  ∀ (hd : 0 < d),
    (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ) = n / (↑d : ℤ)
⊢ (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ) = n / (↑d : ℤ)

Tactic:
obtain rfl | hd := eq_zero_or_pos (a := d)

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
⊢ (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑0 : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑0 : ℚ)).den : ℤ) = n / (↑0 : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
hd : 0 < d
inr :
  let q := HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ);
  ∀ (q_eq : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)), q.num / (↑q.den : ℤ) = n / (↑d : ℤ)
⊢ (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num / (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ) = n / (↑d : ℤ)

Tactic:
set q := (n : ℚ) / d with q_eq

Premises used: Int.cast
-- Module: Mathlib.Data.Rat.Floor
Goal:
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
q_eq : q = HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)
rw :
  ∃ (c : ℤ),
    n = c * (HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).num ∧
      (↑d : ℤ) = c * (↑(HDiv.hDiv (α := ℚ) (↑n : ℚ) (↑d : ℚ)).den : ℤ)
⊢ ∃ (c : ℤ), n = c * q.num ∧ (↑d : ℤ) = c * (↑q.den : ℤ)

Tactic:
rw [q_eq]