awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : q.den.Coprime q.num.natAbs
⊢ natAbs (↑q.den : ℤ) = q.den

Tactic:
simp
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : q.den.Coprime q.num.natAbs
⊢ natAbs (↑q.den : ℤ) = q.den

Tactic:
have : Int.natAbs q.den = q.den := by simp
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : q.den.Coprime q.num.natAbs
this : natAbs (↑q.den : ℤ) = q.den
⊢ (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs

Tactic:
rw [← this] at coprime_q_denom_q_num
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : q.den.Coprime q.num.natAbs
this : natAbs (↑q.den : ℤ) = q.den
coprime_q_denom_q_num₁ : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
⊢ natAbs (↑q.den : ℤ) = q.den

Tactic:
rw [← this] at coprime_q_denom_q_num
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
this : natAbs (↑q.den : ℤ) = q.den
rw :
  (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).num = (↑q.den : ℤ) ∧
    (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den = q.num.natAbs
⊢ q_inv.num = (↑q.den : ℤ) ∧ q_inv.den = q.num.natAbs

Tactic:
rw [q_inv_def]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
this : natAbs (↑q.den : ℤ) = q.den
left : (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).num = (↑q.den : ℤ)
right : (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den = q.num.natAbs
⊢ (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).num = (↑q.den : ℤ) ∧
    (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den = q.num.natAbs

Tactic:
constructor
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
this : natAbs (↑q.den : ℤ) = q.den
⊢ (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).num = (↑q.den : ℤ)

Tactic:
mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num

Premises used: Int.cast, Int.cast_natCast, Rat.num, congrArg, cast, Rat.cast_divInt._simp_1, Rat.den, HDiv.hDiv, Nat.cast, congrFun', Eq.symm, Rat.num_div_eq_of_coprime, Eq, Eq.trans
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
this : natAbs (↑q.den : ℤ) = q.den
⊢ (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).num = (↑q.den : ℤ)

Tactic:
exact mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num

Premises used: Rat.num_div_eq_of_coprime
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
this_1 : natAbs (↑q.den : ℤ) = q.den
this : Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den : ℤ) (↑q.num.natAbs : ℤ)
⊢ (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den = q.num.natAbs

Tactic:
mod_cast this

Premises used: Int.cast, Int.cast_natCast, Rat.num, congrArg, cast, Rat.cast_divInt._simp_1, Rat.den, HDiv.hDiv, Nat.cast, Int.natAbs, Nat.cast_inj._simp_1, congrFun', Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
this_1 : natAbs (↑q.den : ℤ) = q.den
this : Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den : ℤ) (↑q.num.natAbs : ℤ)
⊢ (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den = q.num.natAbs

Tactic:
exact mod_cast this
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
this : natAbs (↑q.den : ℤ) = q.den
right : Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den : ℤ) (↑q.num.natAbs : ℤ)
⊢ (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den = q.num.natAbs

Tactic:
suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact mod_cast this
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
this : natAbs (↑q.den : ℤ) = q.den
right : (↑(HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den : ℤ) = q.num
⊢ Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den : ℤ) (↑q.num.natAbs : ℤ)

Tactic:
rw [q_num_abs_eq_q_num]
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
this : natAbs (↑q.den : ℤ) = q.den
⊢ (↑(HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den : ℤ) = q.num

Tactic:
mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num

Premises used: Int.cast, Int.cast_natCast, Rat.num, congrArg, cast, Rat.cast_divInt._simp_1, Rat.den, HDiv.hDiv, Nat.cast, Rat.den_div_eq_of_coprime, congrFun', Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
coprime_q_denom_q_num : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
this : natAbs (↑q.den : ℤ) = q.den
⊢ (↑(HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den : ℤ) = q.num

Tactic:
exact mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num

Premises used: Rat.den_div_eq_of_coprime
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
⊢ q_inv.num = (↑q.den : ℤ) ∧ q_inv.den = q.num.natAbs

Tactic:
have : q_inv.num = q.den ∧ q_inv.den = q.num.natAbs := by
    have coprime_q_denom_q_num : q.den.Coprime q.num.natAbs := q.reduced.symm
    have : Int.natAbs q.den = q.den := by simp
    rw [← this] at coprime_q_denom_q_num
    rw [q_inv_def]
    constructor
    · exact mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
    · suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact mod_cast this
      rw [q_num_abs_eq_q_num]
      exact mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
-- Module: Mathlib.Data.Rat.Floor
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
q_inv : ℚ := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_def : q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
this : q_inv.num = (↑q.den : ℤ) ∧ q_inv.den = q.num.natAbs
rwa :
  ∀ (q_inv_num_denom_ineq : q_inv.num - ⌊q_inv⌋ * (↑q_inv.den : ℤ) < (↑q_inv.den : ℤ))
    (this : q_inv.num = (↑q.den : ℤ) ∧ q_inv.den = q.num.natAbs), (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
rwa₁ :
  ∀ (q_inv_num_denom_ineq : (↑q.den : ℤ) - ⌊q_inv⌋ * (↑q_inv.den : ℤ) < (↑q_inv.den : ℤ))
    (this : q_inv.num = (↑q.den : ℤ) ∧ q_inv.den = q.num.natAbs), (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
rwa₂ :
  ∀ (q_inv_num_denom_ineq : (↑q.den : ℤ) - ⌊q_inv⌋ * (↑q.num.natAbs : ℤ) < (↑q.num.natAbs : ℤ))
    (this : q_inv.num = (↑q.den : ℤ) ∧ q_inv.den = q.num.natAbs), (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
rwa₃ :
  ∀ (q_inv_num_denom_ineq : (↑q.den : ℤ) - ⌊q_inv⌋ * q.num < q.num)
    (this : q_inv.num = (↑q.den : ℤ) ∧ q_inv.den = q.num.natAbs), (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
rwa₄ rwa₅ rwa₆ rwa₇ :
  ∀ (q_inv_num_denom_ineq : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num)
    (this : q_inv.num = (↑q.den : ℤ) ∧ q_inv.den = q.num.natAbs), (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
⊢ (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num

Tactic:
rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq

Premises used: And.right, And.left, mul_comm
-- Module: Mathlib.Data.Rat.Init
Goal:
q : ℚ
hq : 0 ≤ q
⊢ num (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) q hq) = q.num.natAbs

Tactic:
rfl

Premises used: NNRat.num, rfl
-- Module: Mathlib.Data.Rat.Init
Goal:
q : ℚ
hq : 0 ≤ q
⊢ den (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) q hq) = q.den

Tactic:
rfl

Premises used: NNRat.den, rfl
-- Module: Mathlib.Data.Rat.Init
Goal:
n : ℚ≥0
⊢ (↑n : ℚ≥0) = n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Init
Goal:
⊢ NNRat.cast = id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Init
Goal:
n : ℚ
⊢ (↑n : ℚ) = n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Init
Goal:
⊢ Rat.cast = id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
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 : ℚ }.num ∣ a
⊢ (a /. b).num ∣ a

Tactic:
rcases e : a /. b with ⟨n, d, h, c⟩
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
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 }
⊢ a * (↑d : ℤ) = n * b

Tactic:
rw [Rat.mk_eq_divInt, divInt_eq_divInt_iff b0 (mod_cast h)] at e

Premises used: Rat.mk_eq_divInt, Rat.divInt_eq_divInt_iff
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
⊢ { num := n, den := d, den_nz := h, reduced := c : ℚ }.num ∣ a

Tactic:
Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <|
    c.dvd_of_dvd_mul_right ?_

Premises used: Iff.mpr, Int.dvd_natAbs, Iff.mp, Int.natAbs_dvd, Nat.Coprime.dvd_of_dvd_mul_right, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
refine : n.natAbs ∣ a.natAbs * d
⊢ { num := n, den := d, den_nz := h, reduced := c : ℚ }.num ∣ a

Tactic:
refine Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <|
    c.dvd_of_dvd_mul_right ?_

Premises used: Iff.mpr, Int.dvd_natAbs, Iff.mp, Int.natAbs_dvd, Nat.Coprime.dvd_of_dvd_mul_right, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
⊢ (a * (↑d : ℤ)).natAbs = (n * b).natAbs

Tactic:
have := congr_arg Int.natAbs e
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
this : (a * (↑d : ℤ)).natAbs = (n * b).natAbs
⊢ a.natAbs * d = n.natAbs * b.natAbs

Tactic:
simp only [Int.natAbs_mul, Int.natAbs_natCast] at this

Premises used: Int.natAbs_mul, Int.natAbs_natCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
this : a.natAbs * d = n.natAbs * b.natAbs
⊢ n.natAbs ∣ a.natAbs * d

Tactic:
simp [this]
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
pos : ∀ (b0 : b = 0), (↑(a /. b).den : ℤ) ∣ b
neg : ∀ (b0 : ¬b = 0), (↑(a /. b).den : ℤ) ∣ b
⊢ (↑(a /. b).den : ℤ) ∣ b

Tactic:
by_cases b0 : b = 0
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : b = 0
⊢ (↑(a /. b).den : ℤ) ∣ b

Tactic:
simp [b0]
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : ¬b = 0
neg :
  ∀ (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 }.den : ℤ) ∣ b
⊢ (↑(a /. b).den : ℤ) ∣ b

Tactic:
rcases e : a /. b with ⟨n, d, h, c⟩
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
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 }
⊢ a * (↑d : ℤ) = n * b

Tactic:
rw [mk_eq_divInt,
    divInt_eq_divInt_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e

Premises used: Iff.mpr, Rat.mk_eq_divInt, ne_of_gt, Rat.divInt_eq_divInt_iff, Nat.pos_of_ne_zero, Int.natCast_pos
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c }.den : ℤ) ∣ b

Tactic:
Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.symm.dvd_of_dvd_mul_left ?_

Premises used: Iff.mpr, Nat.Coprime.symm, Int.dvd_natAbs, Iff.mp, Nat.Coprime.dvd_of_dvd_mul_left, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
neg : d ∣ n.natAbs * b.natAbs
⊢ (↑{ num := n, den := d, den_nz := h, reduced := c }.den : ℤ) ∣ b

Tactic:
refine Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.symm.dvd_of_dvd_mul_left ?_

Premises used: Iff.mpr, Nat.Coprime.symm, Int.dvd_natAbs, Iff.mp, Nat.Coprime.dvd_of_dvd_mul_left, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
neg : (↑d : ℤ) ∣ a * (↑d : ℤ)
⊢ d ∣ n.natAbs * b.natAbs

Tactic:
rw [← Int.natAbs_mul, ← Int.natCast_dvd_natCast, Int.dvd_natAbs, ← e]

Premises used: Int.dvd_natAbs, Int.natAbs_mul, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * (↑d : ℤ) = n * b
⊢ (↑d : ℤ) ∣ a * (↑d : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
inl : ∀ (qdf : q = 0 /. d), ∃ (c : ℤ), 0 = c * q.num ∧ d = c * (↑q.den : ℤ)
inr : ∀ (hn : n ≠ 0), ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)
⊢ ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)

Tactic:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
d : ℤ
hd : d ≠ 0
qdf : q = 0 /. d
⊢ ∃ (c : ℤ), 0 = c * q.num ∧ d = c * (↑q.den : ℤ)

Tactic:
simp [qdf]
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num * d = n * (↑q.den : ℤ)

Tactic:
(divInt_eq_divInt_iff ?_ hd).mp ?_

Premises used: Rat.divInt_eq_divInt_iff, Iff.mp
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
refine_1 : Ne (α := ℤ) (↑q.den : ℤ) 0
refine_2 : q.num /. (↑q.den : ℤ) = n /. d
⊢ q.num * d = n * (↑q.den : ℤ)

Tactic:
refine (divInt_eq_divInt_iff ?_ hd).mp ?_

Premises used: Rat.divInt_eq_divInt_iff, Iff.mp
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ Ne (α := ℤ) (↑q.den : ℤ) 0

Tactic:
Int.natCast_ne_zero.mpr (Rat.den_nz _)

Premises used: Iff.mpr, Int.natCast_ne_zero, Rat.den_nz
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ Ne (α := ℤ) (↑q.den : ℤ) 0

Tactic:
exact Int.natCast_ne_zero.mpr (Rat.den_nz _)

Premises used: Iff.mpr, Int.natCast_ne_zero, Rat.den_nz
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
refine_2 refine_2₁ refine_2₂ refine_2₃ : q = n /. d
⊢ q.num /. (↑q.den : ℤ) = n /. d

Tactic:
rwa [num_divInt_den]

Premises used: Rat.num_divInt_den
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
⊢ q.num * d = n * (↑q.den : ℤ)

Tactic:
have : q.num * d = n * ↑q.den := by
    refine (divInt_eq_divInt_iff ?_ hd).mp ?_
    · exact Int.natCast_ne_zero.mpr (Rat.den_nz _)
    · rwa [num_divInt_den]
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
rw : (n /. d).num ∣ n
⊢ q.num ∣ n

Tactic:
rw [qdf]
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
⊢ (n /. d).num ∣ n

Tactic:
Rat.num_dvd _ hd

Premises used: Rat.num_dvd
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
⊢ (n /. d).num ∣ n

Tactic:
exact Rat.num_dvd _ hd

Premises used: Rat.num_dvd
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
⊢ q.num ∣ n

Tactic:
have hqdn : q.num ∣ n := by
    rw [qdf]
    exact Rat.num_dvd _ hd
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
⊢ ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)

Tactic:
⟨n / q.num, ?_, ?_⟩

Premises used: Rat.num, HDiv.hDiv, And.intro, Exists.intro
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
inr : n = n / q.num * q.num
inr₁ : d = n / q.num * (↑q.den : ℤ)
⊢ ∃ (c : ℤ), n = c * q.num ∧ d = c * (↑q.den : ℤ)

Tactic:
refine ⟨n / q.num, ?_, ?_⟩
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
inr inr₁ : n = n
⊢ n = n / q.num * q.num

Tactic:
rw [Int.ediv_mul_cancel hqdn]

Premises used: Int.ediv_mul_cancel
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
⊢ d = n / q.num * (↑q.den : ℤ)

Tactic:
Int.eq_mul_div_of_mul_eq_mul_of_dvd_left ?_ hqdn this

Premises used: Int.eq_mul_div_of_mul_eq_mul_of_dvd_left
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
inr : q.num ≠ 0
⊢ d = n / q.num * (↑q.den : ℤ)

Tactic:
refine Int.eq_mul_div_of_mul_eq_mul_of_dvd_left ?_ hqdn this

Premises used: Int.eq_mul_div_of_mul_eq_mul_of_dvd_left
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
inr : (n /. d).num ≠ 0
⊢ q.num ≠ 0

Tactic:
rw [qdf]
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
⊢ (n /. d).num ≠ 0

Tactic:
Rat.num_ne_zero.2 ((divInt_ne_zero hd).mpr hn)

Premises used: Iff.mpr, Rat.num_ne_zero, Rat.divInt_ne_zero
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q : ℚ
n d : ℤ
hd : d ≠ 0
qdf : q = n /. d
hn : n ≠ 0
this : q.num * d = n * (↑q.den : ℤ)
hqdn : q.num ∣ n
⊢ (n /. d).num ≠ 0

Tactic:
exact Rat.num_ne_zero.2 ((divInt_ne_zero hd).mpr hn)

Premises used: Iff.mpr, Rat.num_ne_zero, Rat.divInt_ne_zero
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n d : ℤ
⊢ (n /. d).num = d.sign * n / (↑(n.gcd d) : ℤ)

Tactic:
Int.gcd_comm .. ▸ Rat.num_divInt ..

Premises used: Rat.num_divInt, Eq.rec, Int.gcd_comm
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
n d : ℤ
⊢ (n /. d).den = if d = 0 then 1 else d.natAbs / n.gcd d

Tactic:
Int.gcd_comm .. ▸ Rat.den_divInt ..

Premises used: Rat.den_divInt, Eq.rec, Int.gcd_comm
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ 0 < q₁.den * q₂.den

Tactic:
simp [Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ q₁.den ≠ 0

Tactic:
simp
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ q₂.den ≠ 0

Tactic:
simp
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
rw :
  q₁.den.gcd q₂.den ∣ (q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)).natAbs ∧
    q₁.den.gcd q₂.den ∣ q₁.den.gcd q₂.den * q₁.den.lcm q₂.den
⊢ (q₁ + q₂).den ∣ q₁.den.lcm q₂.den

Tactic:
rw [add_def, normalize_eq, Nat.div_dvd_iff_dvd_mul (Nat.gcd_dvd_right _ _)
    (Nat.gcd_pos_of_pos_right _ (by simp [Nat.pos_iff_ne_zero])), ← Nat.gcd_mul_lcm,
    mul_dvd_mul_iff_right (Nat.lcm_ne_zero (by simp) (by simp)), Nat.dvd_gcd_iff]

Premises used: Nat.dvd_gcd_iff, Nat.gcd_mul_lcm, mul_dvd_mul_iff_right, Rat.add_def, Nat.div_dvd_iff_dvd_mul, Nat.lcm_ne_zero, Nat.gcd_pos_of_pos_right, Nat.gcd_dvd_right, Rat.normalize_eq
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)).natAbs ∧
    q₁.den.gcd q₂.den ∣ q₁.den.gcd q₂.den * q₁.den.lcm q₂.den

Tactic:
⟨?_, dvd_mul_right _ _⟩

Premises used: And.intro, dvd_mul_right
-- Module: Mathlib.Data.Rat.Lemmas
Goal:
q₁ q₂ : ℚ
refine : q₁.den.gcd q₂.den ∣ (q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)).natAbs
⊢ q₁.den.gcd q₂.den ∣ (q₁.num * (↑q₂.den : ℤ) + q₂.num * (↑q₁.den : ℤ)).natAbs ∧
    q₁.den.gcd q₂.den ∣ q₁.den.gcd q₂.den * q₁.den.lcm q₂.den

Tactic:
refine ⟨?_, dvd_mul_right _ _⟩