awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Defs (goal)
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 : ℚ
⊢ Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ) → M₀) r : M₀) ((g : (a : ℚ) → M₀) r : M₀)
have rw : Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ) → M₀) (↑(↑r.den : ℤ) : ℚ) : M₀) ((g : (a : ℚ) → M₀) (↑(↑r.den : ℤ) : ℚ) : M₀)
Tactic: rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, ← Int.cast_natCast,
      eq_on_inv₀ f g]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
p : ℚ
n : ℕ
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n
have rw : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HPow.hPow (α := α) (↑p : α) n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
p : ℚ
n : ℕ
rw : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HPow.hPow (α := α) (↑p : α) n
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n
have rw₁ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
p : ℚ
n : ℕ
rw : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HPow.hPow (α := α) (↑p : α) n
rw₁ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n
have rw₂ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
p : ℚ
n : ℕ
rw : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HPow.hPow (α := α) (↑p : α) n
rw₁ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₂ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n
have rw₃ : HDiv.hDiv (α := α) (↑(p.num ^ n) : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
p : ℚ
n : ℕ
rw : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HPow.hPow (α := α) (↑p : α) n
rw₁ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₂ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₃ : HDiv.hDiv (α := α) (↑(p.num ^ n) : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n
have rw₄ : (↑(p.num ^ n) : α) / HPow.hPow (α := α) (↑p.den : α) n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
p : ℚ
n : ℕ
rw : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HPow.hPow (α := α) (↑p : α) n
rw₁ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₂ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₃ : HDiv.hDiv (α := α) (↑(p.num ^ n) : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₄ : (↑(p.num ^ n) : α) / HPow.hPow (α := α) (↑p.den : α) n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n
have rw₅ : HPow.hPow (α := α) (↑p.num : α) n / HPow.hPow (α := α) (↑p.den : α) n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
p : ℚ
n : ℕ
rw : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HPow.hPow (α := α) (↑p : α) n
rw₁ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₂ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₃ : HDiv.hDiv (α := α) (↑(p.num ^ n) : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₄ : (↑(p.num ^ n) : α) / HPow.hPow (α := α) (↑p.den : α) n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₅ :
  HPow.hPow (α := α) (↑p.num : α) n / HPow.hPow (α := α) (↑p.den : α) n =
    HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n
have rw₆ : HPow.hPow (α := α) (↑p.num : α) n * (HPow.hPow (α := α) (↑p.den : α) n)⁻¹ =
  HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
p : ℚ
n : ℕ
rw : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HPow.hPow (α := α) (↑p : α) n
rw₁ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₂ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₃ : HDiv.hDiv (α := α) (↑(p.num ^ n) : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₄ : (↑(p.num ^ n) : α) / HPow.hPow (α := α) (↑p.den : α) n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₅ :
  HPow.hPow (α := α) (↑p.num : α) n / HPow.hPow (α := α) (↑p.den : α) n =
    HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₆ :
  HPow.hPow (α := α) (↑p.num : α) n * (HPow.hPow (α := α) (↑p.den : α) n)⁻¹ =
    HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n
have rw₇ : HPow.hPow (α := α) (↑p.num : α) n * HPow.hPow (α := α) (↑p.den : α)⁻¹ n =
  HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
p : ℚ
n : ℕ
rw : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HPow.hPow (α := α) (↑p : α) n
rw₁ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₂ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₃ : HDiv.hDiv (α := α) (↑(p.num ^ n) : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₄ : (↑(p.num ^ n) : α) / HPow.hPow (α := α) (↑p.den : α) n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₅ :
  HPow.hPow (α := α) (↑p.num : α) n / HPow.hPow (α := α) (↑p.den : α) n =
    HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₆ :
  HPow.hPow (α := α) (↑p.num : α) n * (HPow.hPow (α := α) (↑p.den : α) n)⁻¹ =
    HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₇ :
  HPow.hPow (α := α) (↑p.num : α) n * HPow.hPow (α := α) (↑p.den : α)⁻¹ n =
    HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n
have rw₈ : HMul.hMul (α := α) (↑p.num : α) (↑p.den : α)⁻¹ ^ n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
p : ℚ
n : ℕ
rw : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HPow.hPow (α := α) (↑p : α) n
rw₁ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p ^ n).den : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₂ : HDiv.hDiv (α := α) (↑(p ^ n).num : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₃ : HDiv.hDiv (α := α) (↑(p.num ^ n) : α) (↑(p.den ^ n) : α) = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₄ : (↑(p.num ^ n) : α) / HPow.hPow (α := α) (↑p.den : α) n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₅ :
  HPow.hPow (α := α) (↑p.num : α) n / HPow.hPow (α := α) (↑p.den : α) n =
    HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₆ :
  HPow.hPow (α := α) (↑p.num : α) n * (HPow.hPow (α := α) (↑p.den : α) n)⁻¹ =
    HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₇ :
  HPow.hPow (α := α) (↑p.num : α) n * HPow.hPow (α := α) (↑p.den : α)⁻¹ n =
    HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
rw₈ : HMul.hMul (α := α) (↑p.num : α) (↑p.den : α)⁻¹ ^ n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n
have rw₉ : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Int.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Int.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℚ)⁻¹ : α) (↑n : α)⁻¹
have zero : Eq.{u_1 + 1} (α := α) (↑(↑0 : ℚ)⁻¹ : α) (↑0 : α)⁻¹
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
zero : Eq.{u_1 + 1} (α := α) (↑(↑0 : ℚ)⁻¹ : α) (↑0 : α)⁻¹
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℚ)⁻¹ : α) (↑n : α)⁻¹
have succ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := α) (↑(↑(n + 1) : ℚ)⁻¹ : α) (↑(n + 1) : α)⁻¹
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(n + 1) : ℚ)⁻¹ : α) (↑(n + 1) : α)⁻¹
have succ : HDiv.hDiv (α := α) (↑(num (↑(n + 1) : ℚ)⁻¹) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
Tactic: rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
    Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
succ : HDiv.hDiv (α := α) (↑(num (↑(n + 1) : ℚ)⁻¹) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(n + 1) : ℚ)⁻¹ : α) (↑(n + 1) : α)⁻¹
have succ₁ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
Tactic: rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
    Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
succ : HDiv.hDiv (α := α) (↑(num (↑(n + 1) : ℚ)⁻¹) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
succ₁ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(n + 1) : ℚ)⁻¹ : α) (↑(n + 1) : α)⁻¹
have succ₂ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(if n + 1 = 0 then 1 else n + 1) : α) = (↑(n + 1) : α)⁻¹
Tactic: rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
    Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
succ : HDiv.hDiv (α := α) (↑(num (↑(n + 1) : ℚ)⁻¹) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
succ₁ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
succ₂ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(if n + 1 = 0 then 1 else n + 1) : α) = (↑(n + 1) : α)⁻¹
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(n + 1) : ℚ)⁻¹ : α) (↑(n + 1) : α)⁻¹
have succ₃ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(n + 1) : α) = (↑(n + 1) : α)⁻¹
Tactic: rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
    Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
succ : HDiv.hDiv (α := α) (↑(num (↑(n + 1) : ℚ)⁻¹) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
succ₁ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
succ₂ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(if n + 1 = 0 then 1 else n + 1) : α) = (↑(n + 1) : α)⁻¹
succ₃ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(n + 1) : α) = (↑(n + 1) : α)⁻¹
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(n + 1) : ℚ)⁻¹ : α) (↑(n + 1) : α)⁻¹
have succ₄ : HDiv.hDiv (α := α) (↑1 : α) (↑(n + 1) : α) = (↑(n + 1) : α)⁻¹
Tactic: rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
    Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
succ : HDiv.hDiv (α := α) (↑(num (↑(n + 1) : ℚ)⁻¹) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
succ₁ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
succ₂ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(if n + 1 = 0 then 1 else n + 1) : α) = (↑(n + 1) : α)⁻¹
succ₃ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(n + 1) : α) = (↑(n + 1) : α)⁻¹
succ₄ : HDiv.hDiv (α := α) (↑1 : α) (↑(n + 1) : α) = (↑(n + 1) : α)⁻¹
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(n + 1) : ℚ)⁻¹ : α) (↑(n + 1) : α)⁻¹
have succ₅ : HDiv.hDiv (α := α) 1 (↑(n + 1) : α) = (↑(n + 1) : α)⁻¹
Tactic: rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
    Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
succ : HDiv.hDiv (α := α) (↑(num (↑(n + 1) : ℚ)⁻¹) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
succ₁ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(den (↑(n + 1) : ℚ)⁻¹) : α) = (↑(n + 1) : α)⁻¹
succ₂ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(if n + 1 = 0 then 1 else n + 1) : α) = (↑(n + 1) : α)⁻¹
succ₃ : HDiv.hDiv (α := α) (↑(Int.sign (↑(n + 1) : ℤ)) : α) (↑(n + 1) : α) = (↑(n + 1) : α)⁻¹
succ₄ : HDiv.hDiv (α := α) (↑1 : α) (↑(n + 1) : α) = (↑(n + 1) : α)⁻¹
succ₅ : HDiv.hDiv (α := α) 1 (↑(n + 1) : α) = (↑(n + 1) : α)⁻¹
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(n + 1) : ℚ)⁻¹ : α) (↑(n + 1) : α)⁻¹
have succ₆ : Eq.{u_1 + 1} (α := α) (↑(n + 1) : α)⁻¹ (↑(n + 1) : α)⁻¹
Tactic: rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero,
    Int.sign_eq_one_of_pos (Int.ofNat_succ_pos n), Int.cast_one, one_div]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℚ)⁻¹ : α) (↑n : α)⁻¹
have ofNat : ∀ (n : ℕ), Eq.{u_1 + 1} (α := α) (↑(↑(Int.ofNat n) : ℚ)⁻¹ : α) (↑(Int.ofNat n) : α)⁻¹
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
ofNat : ∀ (n : ℕ), Eq.{u_1 + 1} (α := α) (↑(↑(Int.ofNat n) : ℚ)⁻¹ : α) (↑(Int.ofNat n) : α)⁻¹
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℚ)⁻¹ : α) (↑n : α)⁻¹
have negSucc : ∀ (n : ℕ), Eq.{u_1 + 1} (α := α) (↑(↑(Int.negSucc n) : ℚ)⁻¹ : α) (↑(Int.negSucc n) : α)⁻¹
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
⊢ Eq.{u_2 + 1} (α := K) (↑(↑q : ℚ) : K) (↑q : K)
have rw : HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
    (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
  HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
Tactic: rw [Rat.cast_def, NNRat.cast_def, NNRat.cast_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
⊢ HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
      (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
have have : ∀ (hn : (HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).num = (↑q.num : ℤ)),
  HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
      (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
Tactic: have hn := @num_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
have :
  ∀ (hn : (HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).num = (↑q.num : ℤ)),
    HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
        (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
      HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
⊢ HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
      (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
have have₁ : LT.lt (α := ℤ) 0 (↑q.den : ℤ)
Tactic: have hn := @num_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
hn : (HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).num = (↑q.num : ℤ)
⊢ HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
      (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
have hd : Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).den : ℤ) (↑q.den : ℤ)
Tactic: have hd := @den_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
hn : (HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).num = (↑q.num : ℤ)
⊢ HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
      (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
have hd : Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).den : ℤ) (↑q.den : ℤ)
Tactic: on_goal 1 => have hd := @den_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
hn : (HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).num = (↑q.num : ℤ)
hd : Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).den : ℤ) (↑q.den : ℤ)
⊢ HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
      (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
have hn₁ : (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num = (↑q.num : ℤ)
Tactic: simp only [Int.cast_natCast, Nat.cast_inj] at hn hd
Cleared hypotheses: hn, hd
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (hypothesis)
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
hn : (HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).num = (↑q.num : ℤ)
hd : Eq (α := ℤ) (↑(HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).den : ℤ) (↑q.den : ℤ)
hn₁ : (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num = (↑q.num : ℤ)
⊢ HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
      (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
have hd₁ : (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den = q.den
Tactic: simp only [Int.cast_natCast, Nat.cast_inj] at hn hd
Cleared hypotheses: hn, hd
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
hn : (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num = (↑q.num : ℤ)
hd : (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den = q.den
⊢ HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
      (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
have rw : HDiv.hDiv (α := K) (↑(↑q.num : ℤ) : K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
  HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
Tactic: rw [hn, hd, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
hn : (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num = (↑q.num : ℤ)
hd : (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den = q.den
rw :
  HDiv.hDiv (α := K) (↑(↑q.num : ℤ) : K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
⊢ HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
      (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
have rw₁ : HDiv.hDiv (α := K) (↑(↑q.num : ℤ) : K) (↑q.den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
Tactic: rw [hn, hd, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
hn : (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num = (↑q.num : ℤ)
hd : (HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den = q.den
rw :
  HDiv.hDiv (α := K) (↑(↑q.num : ℤ) : K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
rw₁ : HDiv.hDiv (α := K) (↑(↑q.num : ℤ) : K) (↑q.den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
⊢ HDiv.hDiv (α := K) (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num : K)
      (↑(HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den : K) =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
have rw₂ : HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
Tactic: rw [hn, hd, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_2
inst : DivisionRing K
m : ℕ
s : Bool
e : ℕ
⊢ Eq.{u_2 + 1} (α := K) (↑(OfScientific.ofScientific m s e) : K) (OfScientific.ofScientific m s e)
have rw : Eq.{u_2 + 1} (α := K) (↑(OfScientific.ofScientific m s e) : K) (↑(OfScientific.ofScientific m s e) : K)
Tactic: rw [← NNRat.cast_ofScientific (K := K), ← NNRat.cast_ofScientific, cast_nnratCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_2
inst : DivisionRing K
m : ℕ
s : Bool
e : ℕ
rw : Eq.{u_2 + 1} (α := K) (↑(OfScientific.ofScientific m s e) : K) (↑(OfScientific.ofScientific m s e) : K)
⊢ Eq.{u_2 + 1} (α := K) (↑(OfScientific.ofScientific m s e) : K) (OfScientific.ofScientific m s e)
have rw₁ : Eq.{u_2 + 1} (α := K) (↑(↑(OfScientific.ofScientific m s e) : ℚ) : K) (↑(OfScientific.ofScientific m s e) : K)
Tactic: rw [← NNRat.cast_ofScientific (K := K), ← NNRat.cast_ofScientific, cast_nnratCast]