awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
q : ℚ
⊢ (↑q.num : ℚ) < (q - fract q + 1) * (↑q.den : ℚ)
have suffices : (↑q.num : ℚ) < (↑q.num : ℚ) + (1 - fract q) * (↑q.den : ℚ)
Tactic: suffices (q.num : ℚ) < q.num + (1 - fract q) * q.den by
    have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den := by
      calc
        (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
        _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
        _ = q.num + (1 - fract q) * q.den := by simp
    rwa [this]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
q : ℚ
this : 0 < (1 - fract q) * (↑q.den : ℚ)
⊢ (↑q.num : ℚ) < (↑q.num : ℚ) + (1 - fract q) * (↑q.den : ℚ)
have rw : HSub.hSub (α := ℚ) (↑q.num : ℚ) (↑q.num : ℚ) < (1 - fract q) * (↑q.den : ℚ)
Tactic: rw [← sub_lt_iff_lt_add']
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
Goal:
q : ℚ
⊢ (↑q.num : ℚ) < (↑q.num : ℚ) + (1 - fract q) * (↑q.den : ℚ)
have suffices : 0 < (1 - fract q) * (↑q.den : ℚ)
Tactic: suffices 0 < (1 - fract q) * q.den by
    rw [← sub_lt_iff_lt_add']
    simpa
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
q : ℚ
⊢ 0 < 1 - fract q
have this : fract q < 1
Tactic: have : fract q < 1 := fract_lt_one q
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
q : ℚ
this : fract q < 1
⊢ 0 < 1 - fract q
have this₁ : 0 + fract q < 1
Tactic: have : 0 + fract q < 1 := by simp [this]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
q : ℚ
⊢ 0 < (1 - fract q) * (↑q.den : ℚ)
have this : 0 < 1 - fract q
Tactic: have : 0 < 1 - fract q := by
    have : fract q < 1 := fract_lt_one q
    have : 0 + fract q < 1 := by simp [this]
    rwa [lt_sub_iff_add_lt]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
q : ℚ
q_pos : 0 < q
⊢ (fract q⁻¹).num < q.num
have q_num_pos : 0 < q.num
Tactic: have q_num_pos : 0 < q.num := Rat.num_pos.mpr q_pos
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
⊢ (fract q⁻¹).num < q.num
have q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
Tactic: have q_num_abs_eq_q_num : (q.num.natAbs : ℤ) = q.num := Int.natAbs_of_nonneg q_num_pos.le
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
Goal:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : (↑q.num.natAbs : ℤ) = q.num
⊢ (fract q⁻¹).num < q.num
have q_inv_def : let q_inv := HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ);
q_inv = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
Tactic: set q_inv : ℚ := q.den / q.num with q_inv_def
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℚ)
rw : q⁻¹ = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
⊢ q⁻¹ = q_inv
have rw₁ : (↑q.den : ℤ) /. q.num = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
Tactic: rw [q_inv_def, inv_def, divInt_eq_div, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℚ)
rw : q⁻¹ = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
rw₁ : (↑q.den : ℤ) /. q.num = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
⊢ q⁻¹ = q_inv
have rw₂ : HDiv.hDiv (α := ℚ) (↑(↑q.den : ℤ) : ℚ) (↑q.num : ℚ) = HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)
Tactic: rw [q_inv_def, inv_def, divInt_eq_div, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
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 : ℚ)
⊢ (fract q⁻¹).num < q.num
have q_inv_eq : q⁻¹ = q_inv
Tactic: have q_inv_eq : q⁻¹ = q_inv := by rw [q_inv_def, inv_def, divInt_eq_div, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
this : (q_inv - (↑⌊q_inv⌋ : ℚ)).num < q.num
⊢ (fract q⁻¹).num < q.num
have rwa : (fract q_inv).num < q.num
Tactic: rwa [q_inv_eq]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
⊢ (fract q⁻¹).num < q.num
have suffices : (q_inv - (↑⌊q_inv⌋ : ℚ)).num < q.num
Tactic: suffices (q_inv - ⌊q_inv⌋).num < q.num by rwa [q_inv_eq]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 - (↑⌊q_inv⌋ : ℚ)).num < q.num
have suffices : (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num < q.num
Tactic: suffices ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num < q.num by
    simp only [gt_iff_lt, q_inv]
    field_simp
    simp [q_inv, this]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
this : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
⊢ (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num = (↑q.den : ℤ) - q.num * ⌊q_inv⌋
have suffices : ((↑q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs
Tactic: suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
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
this : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
⊢ ((↑q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs
have tmp : ((↑q.den : ℤ) - (↑q.num.natAbs : ℤ) * ⌊HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num.natAbs : ℚ)⌋).natAbs.Coprime q.num.natAbs
Tactic: have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
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
this : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
⊢ (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num < q.num
have this₁ : (((↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num = (↑q.den : ℤ) - q.num * ⌊q_inv⌋
Tactic: have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ := by
      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
      have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
      simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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.den : ℚ) - HMul.hMul (α := ℚ) (↑q.num : ℚ) (↑⌊q_inv⌋ : ℚ)) / (↑q.num : ℚ)).num < q.num
have suffices : (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
Tactic: suffices (q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num by
    -- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
    have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ := by
      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
      have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
      simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
    rwa [this]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
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⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
have this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * (↑q⁻¹.den : ℤ)
Tactic: have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * (↑q⁻¹.den : ℤ)
⊢ q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)
have rwa : ∀ (this : q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + HMul.hMul (α := ℤ) 1 (↑q⁻¹.den : ℤ)),
  q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)
Tactic: rwa [right_distrib, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * (↑q⁻¹.den : ℤ)
rwa :
  ∀ (this : q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + HMul.hMul (α := ℤ) 1 (↑q⁻¹.den : ℤ)),
    q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)
⊢ q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)
have rwa₁ : ∀ (this : q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)), q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)
Tactic: rwa [right_distrib, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
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
this : q⁻¹.num < (⌊q⁻¹⌋ + 1) * (↑q⁻¹.den : ℤ)
⊢ q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
have this₁ : q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)
Tactic: have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
this_1 : q⁻¹.num < (⌊q⁻¹⌋ + 1) * (↑q⁻¹.den : ℤ)
this : q⁻¹.num < ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) + (↑q⁻¹.den : ℤ)
⊢ q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
have rwa : ∀ (this : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)), q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
Tactic: rwa [← sub_lt_iff_lt_add'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
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.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * (↑q⁻¹.den : ℤ) < (↑q⁻¹.den : ℤ)
Tactic: have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.den < q⁻¹.den := by
    have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
    have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this
    rwa [← sub_lt_iff_lt_add'] at this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
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
have coprime_q_denom_q_num : q.den.Coprime q.num.natAbs
Tactic: have coprime_q_denom_q_num : q.den.Coprime q.num.natAbs := q.reduced.symm
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
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
⊢ q_inv.num = (↑q.den : ℤ) ∧ q_inv.den = q.num.natAbs
have this : natAbs (↑q.den : ℤ) = q.den
Tactic: have : Int.natAbs q.den = q.den := by simp
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
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
⊢ q_inv.num = (↑q.den : ℤ) ∧ q_inv.den = q.num.natAbs
have coprime_q_denom_q_num₁ : (natAbs (↑q.den : ℤ)).Coprime q.num.natAbs
Tactic: rw [← this] at coprime_q_denom_q_num
Cleared hypotheses: coprime_q_denom_q_num, this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ) ∧
    (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den = q.num.natAbs
have left : (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).num = (↑q.den : ℤ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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 : ℤ)
⊢ (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).num = (↑q.den : ℤ) ∧
    (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den = q.num.natAbs
have right : (HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den = q.num.natAbs
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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.natAbs
have right : Eq (α := ℤ) (↑(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
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
⊢ Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den : ℤ) (↑q.num.natAbs : ℤ)
have right : (↑(HDiv.hDiv (α := ℚ) (↑q.den : ℚ) (↑q.num : ℚ)).den : ℤ) = q.num
Tactic: rw [q_num_abs_eq_q_num]
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (hypothesis)
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.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
have this : 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
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
⊢ (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
have 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
Tactic: rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq
Cleared hypotheses: q_inv_num_denom_ineq, this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
⊢ (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
have 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
Tactic: rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq
Cleared hypotheses: q_inv_num_denom_ineq, this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
⊢ (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
have 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
Tactic: rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq
Cleared hypotheses: q_inv_num_denom_ineq, this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
⊢ (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
have 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
Tactic: rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq
Cleared hypotheses: q_inv_num_denom_ineq, this
-- Lean 4 proof step from Mathlib.Data.Rat.Floor (goal)
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
⊢ (↑q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num
have 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
Tactic: rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq
Cleared hypotheses: q_inv_num_denom_ineq, this