awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Rat.Cast.Defs
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.den : ℤ) : ℚ) : M₀) ((g : (a : ℚ) → M₀) (↑(↑r.den : ℤ) : ℚ) : M₀)

Tactic:
apply h
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
M₀ : Type u_5
inst : MonoidWithZero M₀
f g : ℚ →*₀ M₀
h : Eq (α := ℤ →*₀ M₀) (f.comp (↑(Int.castRingHom ℚ) : ℤ →*₀ ℚ)) (g.comp (↑(Int.castRingHom ℚ) : ℤ →*₀ ℚ))
⊢ f = g

Tactic:
ext_rat' <| DFunLike.congr_fun h

Premises used: DFunLike.congr_fun, MonoidWithZeroHomClass.ext_rat'
-- Module: Mathlib.Data.Rat.Cast.Defs
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
same_on_neg_one : Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ) → M₀) (-1) : M₀) ((g : (a : ℚ) → M₀) (-1) : M₀)
same_on_pnat :
  ∀ (n : ℕ), 0 < n → Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ) → M₀) (↑n : ℚ) : M₀) ((g : (a : ℚ) → M₀) (↑n : ℚ) : M₀)
⊢ Eq (α := M₀) ((MonoidWithZeroHom.comp (↑f : ℚ →*₀ M₀) (↑(Int.castRingHom ℚ) : ℤ →*₀ ℚ) : (a : ℤ) → M₀) (-1) : M₀)
    ((MonoidWithZeroHom.comp (↑g : ℚ →*₀ M₀) (↑(Int.castRingHom ℚ) : ℤ →*₀ ℚ) : (a : ℤ) → M₀) (-1) : M₀)

Tactic:
simpa
-- Module: Mathlib.Data.Rat.Cast.Defs
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
same_on_neg_one : Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ) → M₀) (-1) : M₀) ((g : (a : ℚ) → M₀) (-1) : M₀)
same_on_pnat :
  ∀ (n : ℕ), 0 < n → Eq.{u_5 + 1} (α := M₀) ((f : (a : ℚ) → M₀) (↑n : ℚ) : M₀) ((g : (a : ℚ) → M₀) (↑n : ℚ) : M₀)
⊢ ∀ (n : ℕ),
    0 < n →
      Eq (α := M₀)
        ((MonoidWithZeroHom.comp (↑f : ℚ →*₀ M₀) (↑(Int.castRingHom ℚ) : ℤ →*₀ ℚ) : (a : ℤ) → M₀) (↑n : ℤ) : M₀)
        ((MonoidWithZeroHom.comp (↑g : ℚ →*₀ M₀) (↑(Int.castRingHom ℚ) : ℤ →*₀ ℚ) : (a : ℤ) → M₀) (↑n : ℤ) : M₀)

Tactic:
simpa
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
R : Type u_5
inst : Semiring R
inst_1 : FunLike F ℚ R
inst_2 : RingHomClass F ℚ R
f g : F
⊢ f = g

Tactic:
MonoidWithZeroHomClass.ext_rat' <|
    RingHom.congr_fun <|
      ((f : ℚ →+* R).comp (Int.castRingHom ℚ)).ext_int ((g : ℚ →+* R).comp (Int.castRingHom ℚ))

Premises used: RingHom.congr_fun, Rat, RingHom.ext_int, RingHom.comp, RingHomClass.toRingHom, Int.castRingHom, MonoidWithZeroHomClass.ext_rat'
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
R : Type u_5
inst_1 : Semiring R
f g : ℚ≥0 →+* R
⊢ ∀ (n : ℕ), Eq (α := R) ((f : (a : ℚ≥0) → R) (↑n : ℚ≥0) : R) ((g : (a : ℚ≥0) → R) (↑n : ℚ≥0) : R)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
inst : FunLike F α β
R : Type u_5
inst_1 : Semiring R
⊢ Subsingleton.{max (u_5 + 1) 1} (ℚ →+* R)

Tactic:
⟨RingHom.ext_rat⟩

Premises used: RingHom.ext_rat, Subsingleton.intro
-- Module: Mathlib.Data.Rat.Cast.Lemmas
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
rw₉ rw₁₀ : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n = HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) ^ n
⊢ (↑(p ^ n) : α) = 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]

Premises used: Rat.den_pow, Int.cast_pow, inv_pow, div_eq_mul_inv, Rat.cast_def, Commute.mul_pow, Rat.num_pow, Nat.cast_pow
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
zero : Eq.{u_1 + 1} (α := α) (↑(↑0 : ℚ)⁻¹ : α) (↑0 : α)⁻¹
succ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := α) (↑(↑(n + 1) : ℚ)⁻¹ : α) (↑(n + 1) : α)⁻¹
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℚ)⁻¹ : α) (↑n : α)⁻¹

Tactic:
rcases n with - | n
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
α : Type u_1
inst : DivisionRing α
⊢ Eq.{u_1 + 1} (α := α) (↑(↑0 : ℚ)⁻¹ : α) (↑0 : α)⁻¹

Tactic:
simp
-- Module: Mathlib.Data.Rat.Cast.Lemmas
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) : α)⁻¹
succ₆ succ₇ : Eq.{u_1 + 1} (α := α) (↑(n + 1) : α)⁻¹ (↑(n + 1) : α)⁻¹
⊢ 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]

Premises used: Rat.inv_natCast_num, Rat.inv_natCast_den, Rat.cast_def, Nat.succ_ne_zero, Int.ofNat_succ_pos, one_div, if_neg, Int.sign_eq_one_of_pos, Int.cast_one
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
α : Type u_1
inst : DivisionRing α
n : ℤ
ofNat : ∀ (n : ℕ), Eq.{u_1 + 1} (α := α) (↑(↑(Int.ofNat n) : ℚ)⁻¹ : α) (↑(Int.ofNat n) : α)⁻¹
negSucc : ∀ (n : ℕ), Eq.{u_1 + 1} (α := α) (↑(↑(Int.negSucc n) : ℚ)⁻¹ : α) (↑(Int.negSucc n) : α)⁻¹
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℚ)⁻¹ : α) (↑n : α)⁻¹

Tactic:
rcases n with n | n
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(Int.ofNat n) : ℚ)⁻¹ : α) (↑(Int.ofNat n) : α)⁻¹

Tactic:
simp [cast_inv_nat]

Premises used: Rat.cast_inv_nat
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
α : Type u_1
inst : DivisionRing α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(Int.negSucc n) : ℚ)⁻¹ : α) (↑(Int.negSucc n) : α)⁻¹

Tactic:
simp only [Int.cast_negSucc, cast_neg, inv_neg, cast_inv_nat]

Premises used: inv_neg, Int.cast_negSucc, Rat.cast_inv_nat, Rat.cast_neg
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
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)
⊢ Eq.{u_2 + 1} (α := K) (↑(↑q : ℚ) : K) (↑q : K)

Tactic:
rw [Rat.cast_def, NNRat.cast_def, NNRat.cast_def]

Premises used: NNRat.cast_def, Rat.cast_def
-- Module: Mathlib.Data.Rat.Cast.Lemmas
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)
have₁ : LT.lt (α := ℤ) 0 (↑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)

Tactic:
have hn := @num_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
hn : (HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).num = (↑q.num : ℤ)
⊢ 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
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
hn : (HDiv.hDiv (α := ℚ) (↑(↑q.num : ℤ) : ℚ) (↑(↑q.den : ℤ) : ℚ)).num = (↑q.num : ℤ)
⊢ 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
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
⊢ LT.lt (α := ℤ) 0 (↑q.den : ℤ)

Tactic:
simpa only [Int.natCast_pos] using q.den_pos

Premises used: NNRat.den_pos, Int.natCast_pos
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_2
inst : DivisionRing K
q : ℚ≥0
⊢ LT.lt (α := ℤ) 0 (↑q.den : ℤ)

Tactic:
case hdp => simpa only [Int.natCast_pos] using q.den_pos

Premises used: NNRat.den_pos, Int.natCast_pos
-- Module: Mathlib.Data.Rat.Cast.Lemmas
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 (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).num = (↑q.num : ℤ)

Tactic:
simp only [Int.cast_natCast, Nat.cast_inj] at hn hd

Premises used: Int.cast_natCast, Nat.cast_inj
-- Module: Mathlib.Data.Rat.Cast.Lemmas
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 (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)).den = q.den

Tactic:
simp only [Int.cast_natCast, Nat.cast_inj] at hn hd

Premises used: Int.cast_natCast, Nat.cast_inj
-- Module: Mathlib.Data.Rat.Cast.Lemmas
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)
rw₂ 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)

Tactic:
rw [hn, hd, Int.cast_natCast]

Premises used: Int.cast_natCast
-- Module: Mathlib.Data.Rat.Cast.Lemmas
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)
rw₂ 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)

Tactic:
rw [← NNRat.cast_ofScientific (K := K), ← NNRat.cast_ofScientific, cast_nnratCast]

Premises used: Rat.cast_nnratCast, NNRat.cast_ofScientific
-- Module: Mathlib.Data.Rat.Cast.Lemmas
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
rw₉ rw₁₀ : HDiv.hDiv (α := 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

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]

Premises used: NNRat.num_pow, NNRat.cast_def, inv_pow, div_eq_mul_inv, NNRat.den_pow, Commute.mul_pow, Nat.cast_pow
-- Module: Mathlib.Data.Rat.Cast.Lemmas
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 : ℤ)
inr : ∀ (n : ℕ), (↑(HPow.hPow (β := ℤ) q (-(↑n : ℤ))) : K) = HPow.hPow (α := K) (β := ℤ) (↑q : K) (-(↑n : ℤ))
⊢ (↑(q ^ z) : K) = HPow.hPow (α := K) (↑q : K) z

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Data.Rat.Cast.Lemmas
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 : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
hq : Ne.{u_1 + 1} (α := K) (↑q.num : K) 0
n : ℕ
inr : HPow.hPow (α := K) (↑q⁻¹ : K) n = HPow.hPow (α := K) (↑q : K)⁻¹ n
⊢ (↑(HPow.hPow (β := ℤ) q (-(↑n : ℤ))) : K) = HPow.hPow (α := K) (β := ℤ) (↑q : K) (-(↑n : ℤ))

Tactic:
simp_rw [zpow_neg, zpow_natCast, ← inv_pow, NNRat.cast_pow]

Premises used: zpow_natCast, inv_pow, NNRat.cast_pow, zpow_neg
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
hq : Ne.{u_1 + 1} (α := K) (↑q.num : K) 0
n : ℕ
inr : Eq.{u_1 + 1} (α := K) (↑q⁻¹ : K) (↑q : K)⁻¹
⊢ HPow.hPow (α := K) (↑q⁻¹ : K) n = HPow.hPow (α := K) (↑q : K)⁻¹ n

Tactic:
congr
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_1
inst : DivisionSemiring K
q : ℚ≥0
hq : Ne.{u_1 + 1} (α := K) (↑q.num : K) 0
n : ℕ
inr inr₁ : Eq.{u_1 + 1} (α := K) (↑q : K)⁻¹ (↑q : K)⁻¹
⊢ Eq.{u_1 + 1} (α := K) (↑q⁻¹ : K) (↑q : K)⁻¹

Tactic:
rw [cast_inv_of_ne_zero hq]

Premises used: NNRat.cast_inv_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
q : ℚ
h : 0 ≤ q
simp : HDiv.hDiv (α := K) (↑|q.num| : K) (↑q.den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
⊢ Eq.{u_1 + 1} (α := K) (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) q h) : K) (↑q : K)

Tactic:
simp only [NNRat.cast_def, NNRat.num_mk, Nat.cast_natAbs, NNRat.den_mk, Rat.cast_def]

Premises used: NNRat.cast_def, Nat.cast_natAbs, Rat.cast_def, NNRat.num_mk, NNRat.den_mk
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
q : ℚ
h : 0 ≤ q
⊢ 0 ≤ q.num

Tactic:
simpa
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_1
inst : DivisionRing K
q : ℚ
h : 0 ≤ q
rw rw₁ : HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K) = HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
⊢ 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)]

Premises used: abs_of_nonneg
-- Module: Mathlib.Data.Rat.Cast.Lemmas
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℕ
s : Bool
e : ℕ
⊢ Eq.{u_1 + 1} (α := K) (↑(ofScientific m s e) : K) (ofScientific m s e)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Cast.OfScientific
Goal:
K : Type u_1
inst : _root_.Field K
inst_1 : CharZero K
m : ℕ
s : Bool
e : ℕ
rw :
  (↑(↑(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
⊢ OfScientific.ofScientific m s e =
    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]

Premises used: NNRatCast.toOfScientific_def, NNRat.cast_ofScientific
-- Module: Mathlib.Data.Rat.Cast.OfScientific
Goal:
K : Type u_1
inst : _root_.Field K
inst_1 : CharZero K
m : ℕ
s : Bool
e : ℕ
simp :
  (↑(↑(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
⊢ (↑(↑(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

Tactic:
simp only [LawfulOfScientific.ofScientific_def]

Premises used: Lean.Grind.LawfulOfScientific.ofScientific_def
-- Module: Mathlib.Data.Rat.Cast.OfScientific
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
isFalse :
  ∀ (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

Tactic:
split
-- Module: Mathlib.Data.Rat.Cast.OfScientific
Goal:
K : Type u_1
inst : _root_.Field K
inst_1 : CharZero K
m : ℕ
s : Bool
e : ℕ
h : s = true
isTrue :
  (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑(HPow.hPow (α := ℕ) 10 e) : ℚ)) ⋯) : K) =
    HDiv.hDiv (α := K) (↑m : K) (↑(HPow.hPow (α := ℕ) 10 e) : K)
⊢ (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) ((↑m : ℚ) / HPow.hPow (α := ℚ) 10 e) ⋯) : ℚ≥0) : K) =
    (↑m : K) / HPow.hPow (α := K) 10 e

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.OfScientific
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) (HDiv.hDiv (α := ℚ) (↑m : ℚ) (↑(HPow.hPow (α := ℕ) 10 e) : ℚ)) ⋯) : K) =
    HDiv.hDiv (α := K) (↑m : K) (↑(HPow.hPow (α := ℕ) 10 e) : K)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Cast.OfScientific
Goal:
K : Type u_1
inst : _root_.Field K
inst_1 : CharZero K
m : ℕ
s : Bool
e : ℕ
h : ¬s = true
isFalse isFalse₁ isFalse₂ isFalse₃ :
  Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ) ⋯ = (↑(m * HPow.hPow (α := ℕ) 10 e) : ℚ≥0)
⊢ (↑(↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) ((↑m : ℚ) * HPow.hPow (α := ℚ) 10 e) ⋯) : ℚ≥0) : K) =
    (↑m : K) * HPow.hPow (α := K) 10 e

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
⊢ castHom ℚ = RingHom.id ℚ

Tactic:
RingHom.ext cast_id

Premises used: RingHom.ext, Rat.cast_id
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
hq : 0 < q
rw : 0 < HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)
⊢ LT.lt.{u_5} (α := K) 0 (↑q : K)

Tactic:
rw [Rat.cast_def]

Premises used: Rat.cast_def
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
hq : 0 < q
⊢ 0 < HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)

Tactic:
div_pos (Int.cast_pos.2 <| num_pos.2 hq) (Nat.cast_pos.2 q.pos)

Premises used: Iff.mpr, Nat.cast_pos, Rat.pos, Rat.num_pos, div_pos, Int.cast_pos
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
hq : 0 < q
⊢ 0 < HDiv.hDiv (α := K) (↑q.num : K) (↑q.den : K)

Tactic:
exact div_pos (Int.cast_pos.2 <| num_pos.2 hq) (Nat.cast_pos.2 q.pos)

Premises used: div_pos
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ
⊢ p < q → LT.lt.{u_5} (α := K) (↑p : K) (↑q : K)

Tactic:
simpa only [sub_pos, cast_sub] using cast_pos_of_pos (K := K) (q := q - p)

Premises used: sub_pos, Rat.cast_pos_of_pos, Rat.cast_sub
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ Monotone.{0, u_5} (β := K) Rat.cast

Tactic:
cast_strictMono.monotone

Premises used: StrictMono.monotone, Rat.cast_strictMono
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
p q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ LE.le.{u_5} (α := K) (↑p : K) (↑q : K) ↔ p ≤ q

Tactic:
castOrderEmbedding.le_iff_le

Premises used: Rat.castOrderEmbedding, OrderEmbedding.le_iff_le
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
p q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ LT.lt.{u_5} (α := K) (↑p : K) (↑q : K) ↔ p < q

Tactic:
cast_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Rat.cast_strictMono
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 ≤ q ↔ 0 ≤ q
⊢ LE.le.{u_5} (α := K) 0 (↑q : K) ↔ 0 ≤ q

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : q ≤ 0 ↔ q ≤ 0
⊢ LE.le.{u_5} (α := K) (↑q : K) 0 ↔ q ≤ 0

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < q ↔ 0 < q
⊢ LT.lt.{u_5} (α := K) 0 (↑q : K) ↔ 0 < q

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
q : ℚ
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : q < 0 ↔ q < 0
⊢ LT.lt.{u_5} (α := K) (↑q : K) 0 ↔ q < 0

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.Order
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)
rw₁ 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 : ℚ)

Tactic:
rw [← cast_le (K := K), cast_natCast]

Premises used: Rat.cast_natCast, Rat.cast_le
-- Module: Mathlib.Data.Rat.Cast.Order
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)
rw₁ 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

Tactic:
rw [← cast_le (K := K), cast_natCast]

Premises used: Rat.cast_natCast, Rat.cast_le