awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ (↑(q ^ n) : K) = HPow.hPow (α := K) (↑q : K) n
have rw : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HPow.hPow (α := K) (↑q : K) n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
n : ℕ
rw : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HPow.hPow (α := K) (↑q : K) n
⊢ (↑(q ^ n) : K) = HPow.hPow (α := K) (↑q : K) n
have rw₁ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
n : ℕ
rw : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HPow.hPow (α := K) (↑q : K) n
rw₁ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
⊢ (↑(q ^ n) : K) = HPow.hPow (α := K) (↑q : K) n
have rw₂ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
n : ℕ
rw : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HPow.hPow (α := K) (↑q : K) n
rw₁ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₂ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
⊢ (↑(q ^ n) : K) = HPow.hPow (α := K) (↑q : K) n
have rw₃ : HDiv.hDiv (α := K) (↑(q.num ^ n) : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
n : ℕ
rw : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HPow.hPow (α := K) (↑q : K) n
rw₁ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₂ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₃ : HDiv.hDiv (α := K) (↑(q.num ^ n) : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
⊢ (↑(q ^ n) : K) = HPow.hPow (α := K) (↑q : K) n
have rw₄ : HPow.hPow (α := K) (↑q.num : K) n / (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
n : ℕ
rw : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HPow.hPow (α := K) (↑q : K) n
rw₁ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₂ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₃ : HDiv.hDiv (α := K) (↑(q.num ^ n) : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₄ : HPow.hPow (α := K) (↑q.num : K) n / (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
⊢ (↑(q ^ n) : K) = HPow.hPow (α := K) (↑q : K) n
have rw₅ : HPow.hPow (α := K) (↑q.num : K) n / HPow.hPow (α := K) (↑q.den : K) n = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
n : ℕ
rw : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HPow.hPow (α := K) (↑q : K) n
rw₁ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₂ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₃ : HDiv.hDiv (α := K) (↑(q.num ^ n) : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₄ : HPow.hPow (α := K) (↑q.num : K) n / (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₅ :
  HPow.hPow (α := K) (↑q.num : K) n / HPow.hPow (α := K) (↑q.den : K) n =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
⊢ (↑(q ^ n) : K) = HPow.hPow (α := K) (↑q : K) n
have rw₆ : HPow.hPow (α := K) (↑q.num : K) n * (HPow.hPow (α := K) (↑q.den : K) n)⁻¹ =
  HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
n : ℕ
rw : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HPow.hPow (α := K) (↑q : K) n
rw₁ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₂ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₃ : HDiv.hDiv (α := K) (↑(q.num ^ n) : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₄ : HPow.hPow (α := K) (↑q.num : K) n / (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₅ :
  HPow.hPow (α := K) (↑q.num : K) n / HPow.hPow (α := K) (↑q.den : K) n =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₆ :
  HPow.hPow (α := K) (↑q.num : K) n * (HPow.hPow (α := K) (↑q.den : K) n)⁻¹ =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
⊢ (↑(q ^ n) : K) = HPow.hPow (α := K) (↑q : K) n
have rw₇ : HPow.hPow (α := K) (↑q.num : K) n * HPow.hPow (α := K) (↑q.den : K)⁻¹ n =
  HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
n : ℕ
rw : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HPow.hPow (α := K) (↑q : K) n
rw₁ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₂ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₃ : HDiv.hDiv (α := K) (↑(q.num ^ n) : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₄ : HPow.hPow (α := K) (↑q.num : K) n / (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₅ :
  HPow.hPow (α := K) (↑q.num : K) n / HPow.hPow (α := K) (↑q.den : K) n =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₆ :
  HPow.hPow (α := K) (↑q.num : K) n * (HPow.hPow (α := K) (↑q.den : K) n)⁻¹ =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₇ :
  HPow.hPow (α := K) (↑q.num : K) n * HPow.hPow (α := K) (↑q.den : K)⁻¹ n =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
⊢ (↑(q ^ n) : K) = HPow.hPow (α := K) (↑q : K) n
have rw₈ : HMul.hMul (α := K) (↑q.num : K) (↑q.den : K)⁻¹ ^ n = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
n : ℕ
rw : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HPow.hPow (α := K) (↑q : K) n
rw₁ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q ^ n).den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₂ : HDiv.hDiv (α := K) (↑(q ^ n).num : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₃ : HDiv.hDiv (α := K) (↑(q.num ^ n) : K) (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₄ : HPow.hPow (α := K) (↑q.num : K) n / (↑(q.den ^ n) : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₅ :
  HPow.hPow (α := K) (↑q.num : K) n / HPow.hPow (α := K) (↑q.den : K) n =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₆ :
  HPow.hPow (α := K) (↑q.num : K) n * (HPow.hPow (α := K) (↑q.den : K) n)⁻¹ =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₇ :
  HPow.hPow (α := K) (↑q.num : K) n * HPow.hPow (α := K) (↑q.den : K)⁻¹ n =
    HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
rw₈ : HMul.hMul (α := K) (↑q.num : K) (↑q.den : K)⁻¹ ^ n = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
⊢ (↑(q ^ n) : K) = HPow.hPow (α := K) (↑q : K) n
have rw₉ : HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) ^ n
Tactic: rw [cast_def, cast_def, den_pow, num_pow, Nat.cast_pow, Nat.cast_pow, div_eq_mul_inv, ← inv_pow,
    ← (Nat.cast_commute _ _).mul_pow, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
z : ℤ
hq : Ne.{u_1 + 1} (α := K) (↑q.num : K) 0
⊢ (↑(q ^ z) : K) = HPow.hPow (α := K) (↑q : K) z
have inl : ∀ (n : ℕ), (↑(HPow.hPow (β := ℤ) q (↑n : ℤ)) : K) = HPow.hPow (α := K) (β := ℤ) (↑q : K) (↑n : ℤ)
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
z : ℤ
hq : Ne.{u_1 + 1} (α := K) (↑q.num : K) 0
inl : ∀ (n : ℕ), (↑(HPow.hPow (β := ℤ) q (↑n : ℤ)) : K) = HPow.hPow (α := K) (β := ℤ) (↑q : K) (↑n : ℤ)
⊢ (↑(q ^ z) : K) = HPow.hPow (α := K) (↑q : K) z
have inr : ∀ (n : ℕ), (↑(HPow.hPow (β := ℤ) q (-(↑n : ℤ))) : K) = HPow.hPow (α := K) (β := ℤ) (↑q : K) (-(↑n : ℤ))
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
hq : Ne.{u_1 + 1} (α := K) (↑q.num : K) 0
n : ℕ
⊢ (↑(HPow.hPow (β := ℤ) q (-(↑n : ℤ))) : K) = HPow.hPow (α := K) (β := ℤ) (↑q : K) (-(↑n : ℤ))
have inr : HPow.hPow (α := K) (↑q⁻¹ : K) n = HPow.hPow (α := K) (↑q : K)⁻¹ n
Tactic: simp_rw [zpow_neg, zpow_natCast, ← inv_pow, NNRat.cast_pow]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
hq : Ne.{u_1 + 1} (α := K) (↑q.num : K) 0
n : ℕ
⊢ HPow.hPow (α := K) (↑q⁻¹ : K) n = HPow.hPow (α := K) (↑q : K)⁻¹ n
have inr : Eq.{u_1 + 1} (α := K) (↑q⁻¹ : K) (↑q : K)⁻¹
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
hq : Ne.{u_1 + 1} (α := K) (↑q.num : K) 0
n : ℕ
⊢ Eq.{u_1 + 1} (α := K) (↑q⁻¹ : K) (↑q : K)⁻¹
have inr : Eq.{u_1 + 1} (α := K) (↑q : K)⁻¹ (↑q : K)⁻¹
Tactic: rw [cast_inv_of_ne_zero hq]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ Eq.{u_1 + 1} (α := K) (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) q h) : K) (↑q : K)
have simp : HDiv.hDiv (α := K) (↑|q.num| : K) (↑q.den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
Tactic: simp only [NNRat.cast_def, NNRat.num_mk, Nat.cast_natAbs, NNRat.den_mk, Rat.cast_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Lemmas (goal)
Goal:
K : Type u_1
inst : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ HDiv.hDiv (α := K) (↑|q.num| : K) (↑q.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 [abs_of_nonneg (by simpa)]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.OfScientific (goal)
Goal:
K : Type u_1
inst : _root_.Field K
inst_1 : CharZero K
m : ℕ
s : Bool
e : ℕ
⊢ OfScientific.ofScientific m s e =
    if s = true then (↑m : K) / HPow.hPow (α := K) 10 e else (↑m : K) * HPow.hPow (α := K) 10 e
have rw : (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (OfScientific.ofScientific m s e) sorry) : ℚ≥0) : K) =
  if s = true then (↑m : K) / HPow.hPow (α := K) 10 e else (↑m : K) * HPow.hPow (α := K) 10 e
Tactic: rw [← NNRat.cast_ofScientific, NNRatCast.toOfScientific_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.OfScientific (goal)
Goal:
K : Type u_1
inst : _root_.Field K
inst_1 : CharZero K
m : ℕ
s : Bool
e : ℕ
⊢ (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (OfScientific.ofScientific m s e) ⋯) : ℚ≥0) : K) =
    if s = true then (↑m : K) / HPow.hPow (α := K) 10 e else (↑m : K) * HPow.hPow (α := K) 10 e
have simp : (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q)
            (if s = true then (↑m : ℚ) / HPow.hPow (α := ℚ) 10 e else (↑m : ℚ) * HPow.hPow (α := ℚ) 10 e) sorry) :
        ℚ≥0) :
    K) =
  if s = true then (↑m : K) / HPow.hPow (α := K) 10 e else (↑m : K) * HPow.hPow (α := K) 10 e
Tactic: simp only [LawfulOfScientific.ofScientific_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.OfScientific (goal)
Goal:
K : Type u_1
inst : _root_.Field K
inst_1 : CharZero K
m : ℕ
s : Bool
e : ℕ
⊢ (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q)
              (if s = true then (↑m : ℚ) / HPow.hPow (α := ℚ) 10 e else (↑m : ℚ) * HPow.hPow (α := ℚ) 10 e) ⋯) :
          ℚ≥0) :
      K) =
    if s = true then (↑m : K) / HPow.hPow (α := K) 10 e else (↑m : K) * HPow.hPow (α := K) 10 e
have isTrue : ∀ (h : s = true),
  (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) ((↑m : ℚ) / HPow.hPow (α := ℚ) 10 e) sorry) : ℚ≥0) : K) =
    (↑m : K) / HPow.hPow (α := K) 10 e
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.OfScientific (goal)
Goal:
K : Type u_1
inst : _root_.Field K
inst_1 : CharZero K
m : ℕ
s : Bool
e : ℕ
isTrue :
  ∀ (h : s = true),
    (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) ((↑m : ℚ) / HPow.hPow (α := ℚ) 10 e) ⋯) : ℚ≥0) : K) =
      (↑m : K) / HPow.hPow (α := K) 10 e
⊢ (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q)
              (if s = true then (↑m : ℚ) / HPow.hPow (α := ℚ) 10 e else (↑m : ℚ) * HPow.hPow (α := ℚ) 10 e) ⋯) :
          ℚ≥0) :
      K) =
    if s = true then (↑m : K) / HPow.hPow (α := K) 10 e else (↑m : K) * HPow.hPow (α := K) 10 e
have isFalse : ∀ (h : ¬s = true),
  (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) ((↑m : ℚ) * HPow.hPow (α := ℚ) 10 e) sorry) : ℚ≥0) : K) =
    (↑m : K) * HPow.hPow (α := K) 10 e
Tactic: split
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.OfScientific (goal)
Goal:
K : Type u_1
inst : _root_.Field K
inst_1 : CharZero K
m : ℕ
s : Bool
e : ℕ
h : s = true
⊢ (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) ((↑m : ℚ) / HPow.hPow (α := ℚ) 10 e) ⋯) : ℚ≥0) : K) =
    (↑m : K) / HPow.hPow (α := K) 10 e
have isTrue : (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑(HPow.hPow (α := ℕ) 10 e) : ℚ)) sorry) : K) =
  HDiv.hDiv (α := K) (↑m : K) (↑(HPow.hPow (α := ℕ) 10 e) : K)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.OfScientific (goal)
Goal:
K : Type u_1
inst : _root_.Field K
inst_1 : CharZero K
m : ℕ
s : Bool
e : ℕ
h : ¬s = true
⊢ (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) ((↑m : ℚ) * HPow.hPow (α := ℚ) 10 e) ⋯) : ℚ≥0) : K) =
    (↑m : K) * HPow.hPow (α := K) 10 e
have isFalse : Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ) sorry = (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
hq : 0 < q
⊢ LT.lt.{u_5} (α := K) 0 (↑q : K)
have rw : 0 < HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
Tactic: rw [Rat.cast_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ LE.le.{u_5} (α := K) 0 (↑q : K) ↔ 0 ≤ q
have norm_cast : 0 ≤ q ↔ 0 ≤ q
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ LE.le.{u_5} (α := K) (↑q : K) 0 ↔ q ≤ 0
have norm_cast : q ≤ 0 ↔ q ≤ 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ LT.lt.{u_5} (α := K) 0 (↑q : K) ↔ 0 < q
have norm_cast : 0 < q ↔ 0 < q
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ LT.lt.{u_5} (α := K) (↑q : K) 0 ↔ q < 0
have norm_cast : q < 0 ↔ q < 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ
n : ℕ
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m ≤ (↑n : ℚ)
have rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ) : K)
Tactic: rw [← cast_le (K := K), cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ
n : ℕ
rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ) : K)
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m ≤ (↑n : ℚ)
have rw₁ : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑m : K) (↑n : K)
Tactic: rw [← cast_le (K := K), cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℕ
n : ℚ
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ) ≤ n
have rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑(↑m : ℚ) : K) (↑n : K)
Tactic: rw [← cast_le (K := K), cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℕ
n : ℚ
rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑(↑m : ℚ) : K) (↑n : K)
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ) ≤ n
have rw₁ : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑m : K) (↑n : K)
Tactic: rw [← cast_le (K := K), cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m ≤ (↑n : ℚ)
have rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ) : K)
Tactic: rw [← cast_le (K := K), cast_intCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ
n : ℤ
rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ) : K)
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m ≤ (↑n : ℚ)
have rw₁ : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑m : K) (↑n : K)
Tactic: rw [← cast_le (K := K), cast_intCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ) ≤ n
have rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑(↑m : ℚ) : K) (↑n : K)
Tactic: rw [← cast_le (K := K), cast_intCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℤ
n : ℚ
rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑(↑m : ℚ) : K) (↑n : K)
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ) ≤ n
have rw₁ : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑m : K) (↑n : K)
Tactic: rw [← cast_le (K := K), cast_intCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ
n : ℕ
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m < (↑n : ℚ)
have rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ) : K)
Tactic: rw [← cast_lt (K := K), cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ
n : ℕ
rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ) : K)
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m < (↑n : ℚ)
have rw₁ : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K)
Tactic: rw [← cast_lt (K := K), cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℕ
n : ℚ
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ) < n
have rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑(↑m : ℚ) : K) (↑n : K)
Tactic: rw [← cast_lt (K := K), cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℕ
n : ℚ
rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑(↑m : ℚ) : K) (↑n : K)
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ) < n
have rw₁ : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K)
Tactic: rw [← cast_lt (K := K), cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ
n : ℤ
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m < (↑n : ℚ)
have rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ) : K)
Tactic: rw [← cast_lt (K := K), cast_intCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ
n : ℤ
rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ) : K)
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m < (↑n : ℚ)
have rw₁ : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K)
Tactic: rw [← cast_lt (K := K), cast_intCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℤ
n : ℚ
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ) < n
have rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑(↑m : ℚ) : K) (↑n : K)
Tactic: rw [← cast_lt (K := K), cast_intCast]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℤ
n : ℚ
rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑(↑m : ℚ) : K) (↑n : K)
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ) < n
have rw₁ : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K)
Tactic: rw [← cast_lt (K := K), cast_intCast]