awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_intCast]

Premises used: Rat.cast_intCast, 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_intCast]

Premises used: Rat.cast_intCast, 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 : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ) : K)
rw₁ 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 : ℚ)

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

Premises used: Rat.cast_lt, Rat.cast_natCast
-- 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 : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑(↑m : ℚ) : K) (↑n : K)
rw₁ 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

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

Premises used: Rat.cast_lt, Rat.cast_natCast
-- 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 : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ) : K)
rw₁ 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 : ℚ)

Tactic:
rw [← cast_lt (K := K), cast_intCast]

Premises used: Rat.cast_intCast, Rat.cast_lt
-- 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 : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑(↑m : ℚ) : K) (↑n : K)
rw₁ 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

Tactic:
rw [← cast_lt (K := K), cast_intCast]

Premises used: Rat.cast_intCast, Rat.cast_lt
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ
⊢ Eq.{u_5 + 1} (α := K) (↑(min p q) : K) (min (↑p : K) (↑q : K))

Tactic:
(@cast_mono K _).map_min

Premises used: Rat.cast_mono, Monotone.map_min
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ
⊢ Eq.{u_5 + 1} (α := K) (↑(max p q) : K) (max (↑p : K) (↑q : K))

Tactic:
(@cast_mono K _).map_max

Premises used: Monotone.map_max, Rat.cast_mono
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ
⊢ Eq.{u_5 + 1} (α := K) (↑|q| : K) |(↑q : K)|

Tactic:
simp [abs_eq_max_neg]

Premises used: abs_eq_max_neg
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ
⊢ preimage.{0, u_5} (β := K) Rat.cast (Icc (↑p : K) (↑q : K)) = Icc p q

Tactic:
castOrderEmbedding.preimage_Icc ..

Premises used: OrderEmbedding.preimage_Icc, Rat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ
⊢ preimage.{0, u_5} (β := K) Rat.cast (Ico (↑p : K) (↑q : K)) = Ico p q

Tactic:
castOrderEmbedding.preimage_Ico ..

Premises used: Rat.castOrderEmbedding, OrderEmbedding.preimage_Ico
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ
⊢ preimage.{0, u_5} (β := K) Rat.cast (Ioc (↑p : K) (↑q : K)) = Ioc p q

Tactic:
castOrderEmbedding.preimage_Ioc p q

Premises used: OrderEmbedding.preimage_Ioc, Rat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ
⊢ preimage.{0, u_5} (β := K) Rat.cast (Ioo (↑p : K) (↑q : K)) = Ioo p q

Tactic:
castOrderEmbedding.preimage_Ioo p q

Premises used: Rat.castOrderEmbedding, OrderEmbedding.preimage_Ioo
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ
⊢ preimage.{0, u_5} (β := K) Rat.cast (Ici (↑q : K)) = Ici q

Tactic:
castOrderEmbedding.preimage_Ici q

Premises used: OrderEmbedding.preimage_Ici, Rat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ
⊢ preimage.{0, u_5} (β := K) Rat.cast (Iic (↑q : K)) = Iic q

Tactic:
castOrderEmbedding.preimage_Iic q

Premises used: OrderEmbedding.preimage_Iic, Rat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ
⊢ preimage.{0, u_5} (β := K) Rat.cast (Ioi (↑q : K)) = Ioi q

Tactic:
castOrderEmbedding.preimage_Ioi q

Premises used: Rat.castOrderEmbedding, OrderEmbedding.preimage_Ioi
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ
⊢ preimage.{0, u_5} (β := K) Rat.cast (Iio (↑q : K)) = Iio q

Tactic:
castOrderEmbedding.preimage_Iio q

Premises used: Rat.castOrderEmbedding, OrderEmbedding.preimage_Iio
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ
⊢ preimage.{0, u_5} (β := K) Rat.cast (uIcc (↑p : K) (↑q : K)) = uIcc p q

Tactic:
(castOrderEmbedding (K := K)).preimage_uIcc p q

Premises used: Rat.castOrderEmbedding, OrderEmbedding.preimage_uIcc
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ
⊢ preimage.{0, u_5} (β := K) Rat.cast (uIoc (↑p : K) (↑q : K)) = uIoc p q

Tactic:
(castOrderEmbedding (K := K)).preimage_uIoc p q

Premises used: OrderEmbedding.preimage_uIoc, Rat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
hb : LT.lt.{u_5} (α := K) 0 (↑p.den : K)
hd : LT.lt.{u_5} (α := K) 0 (↑q.den : K)
⊢ LT.lt.{u_5} (α := K) (↑p : K) (↑q : K)

Tactic:
rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff₀, ← Nat.cast_mul, ← Nat.cast_mul,
    Nat.cast_lt (α := K), ← NNRat.lt_def]

Premises used: NNRat.cast_def, NNRat.lt_def, Nat.cast_mul, div_lt_div_iff₀, Nat.cast_lt
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ LT.lt.{u_5} (α := K) 0 (↑p.den : K)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ LT.lt.{u_5} (α := K) 0 (↑q.den : K)

Tactic:
simp
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ Monotone.{0, u_5} (β := K) NNRat.cast

Tactic:
cast_strictMono.monotone

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

Tactic:
castOrderEmbedding.le_iff_le

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

Tactic:
cast_strictMono.lt_iff_lt

Premises used: NNRat.cast_strictMono, StrictMono.lt_iff_lt
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ≥0
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:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ≥0
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:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ≥0
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 : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ≥0
⊢ ¬LT.lt.{u_5} (α := K) (↑q : K) 0

Tactic:
mod_cast not_lt_zero

Premises used: congrArg, cast, LT.lt, NNRat.cast_lt._simp_1, not_lt_zero, NNRat.cast_zero, Nat.cast_zero, Eq.symm, NNRat.cast, Not, Eq.trans
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : p ≤ 1 ↔ p ≤ 1
⊢ LE.le.{u_5} (α := K) (↑p : K) 1 ↔ p ≤ 1

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

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

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

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst_3 : n.AtLeastTwo
⊢ LE.le.{u_5} (α := K) (↑p : K) (OfNat.ofNat n) ↔ p ≤ OfNat.ofNat n

Tactic:
simp [← cast_le (K := K)]

Premises used: NNRat.cast_le
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst_3 : n.AtLeastTwo
⊢ LE.le.{u_5} (α := K) (OfNat.ofNat n) (↑p : K) ↔ OfNat.ofNat n ≤ p

Tactic:
simp [← cast_le (K := K)]

Premises used: NNRat.cast_le
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst_3 : n.AtLeastTwo
⊢ LT.lt.{u_5} (α := K) (↑p : K) (OfNat.ofNat n) ↔ p < OfNat.ofNat n

Tactic:
simp [← cast_lt (K := K)]

Premises used: NNRat.cast_lt
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
n : ℕ
inst_3 : n.AtLeastTwo
⊢ LT.lt.{u_5} (α := K) (OfNat.ofNat n) (↑p : K) ↔ OfNat.ofNat n < p

Tactic:
simp [← cast_lt (K := K)]

Premises used: NNRat.cast_lt
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ≥0
n : ℕ
rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ≥0) : 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 : ℚ≥0)

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

Premises used: NNRat.cast_le, NNRat.cast_natCast
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℕ
n : ℚ≥0
rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑(↑m : ℚ≥0) : 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 : ℚ≥0) ≤ n

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

Premises used: NNRat.cast_le, NNRat.cast_natCast
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ≥0
n : ℕ
rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ≥0) : K)
rw₁ 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 : ℚ≥0)

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

Premises used: NNRat.cast_lt, NNRat.cast_natCast
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℕ
n : ℚ≥0
rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑(↑m : ℚ≥0) : K) (↑n : K)
rw₁ 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 : ℚ≥0) < n

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

Premises used: NNRat.cast_lt, NNRat.cast_natCast
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
⊢ Eq.{u_5 + 1} (α := K) (↑(min p q) : K) (min (↑p : K) (↑q : K))

Tactic:
(@cast_mono K _).map_min

Premises used: NNRat.cast_mono, Monotone.map_min
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
⊢ Eq.{u_5 + 1} (α := K) (↑(max p q) : K) (max (↑p : K) (↑q : K))

Tactic:
(@cast_mono K _).map_max

Premises used: NNRat.cast_mono, Monotone.map_max
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
⊢ preimage.{0, u_5} (β := K) NNRat.cast (Icc (↑p : K) (↑q : K)) = Icc p q

Tactic:
castOrderEmbedding.preimage_Icc ..

Premises used: OrderEmbedding.preimage_Icc, NNRat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
⊢ preimage.{0, u_5} (β := K) NNRat.cast (Ico (↑p : K) (↑q : K)) = Ico p q

Tactic:
castOrderEmbedding.preimage_Ico ..

Premises used: OrderEmbedding.preimage_Ico, NNRat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
⊢ preimage.{0, u_5} (β := K) NNRat.cast (Ioc (↑p : K) (↑q : K)) = Ioc p q

Tactic:
castOrderEmbedding.preimage_Ioc p q

Premises used: OrderEmbedding.preimage_Ioc, NNRat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
⊢ preimage.{0, u_5} (β := K) NNRat.cast (Ioo (↑p : K) (↑q : K)) = Ioo p q

Tactic:
castOrderEmbedding.preimage_Ioo p q

Premises used: NNRat.castOrderEmbedding, OrderEmbedding.preimage_Ioo
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
⊢ preimage.{0, u_5} (β := K) NNRat.cast (Ici (↑p : K)) = Ici p

Tactic:
castOrderEmbedding.preimage_Ici p

Premises used: OrderEmbedding.preimage_Ici, NNRat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
⊢ preimage.{0, u_5} (β := K) NNRat.cast (Iic (↑p : K)) = Iic p

Tactic:
castOrderEmbedding.preimage_Iic p

Premises used: OrderEmbedding.preimage_Iic, NNRat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
⊢ preimage.{0, u_5} (β := K) NNRat.cast (Ioi (↑p : K)) = Ioi p

Tactic:
castOrderEmbedding.preimage_Ioi p

Premises used: NNRat.castOrderEmbedding, OrderEmbedding.preimage_Ioi
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
⊢ preimage.{0, u_5} (β := K) NNRat.cast (Iio (↑p : K)) = Iio p

Tactic:
castOrderEmbedding.preimage_Iio p

Premises used: OrderEmbedding.preimage_Iio, NNRat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
⊢ preimage.{0, u_5} (β := K) NNRat.cast (uIcc (↑p : K) (↑q : K)) = uIcc p q

Tactic:
(castOrderEmbedding (K := K)).preimage_uIcc p q

Premises used: OrderEmbedding.preimage_uIcc, NNRat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Cast.Order
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p q : ℚ≥0
⊢ preimage.{0, u_5} (β := K) NNRat.cast (uIoc (↑p : K) (↑q : K)) = uIoc p q

Tactic:
(castOrderEmbedding (K := K)).preimage_uIoc p q

Premises used: OrderEmbedding.preimage_uIoc, NNRat.castOrderEmbedding
-- Module: Mathlib.Data.Rat.Defs
Goal:
a : ℚ
⊢ 0 < a.den

Tactic:
Nat.pos_of_ne_zero a.den_nz

Premises used: Rat.den_nz, Nat.pos_of_ne_zero
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
⊢ { num := q.num, den := q.den, den_nz := ⋯, reduced := ⋯ : ℚ } = q

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
⊢ Injective (β := ℚ) Int.cast

Tactic:
fun _ _ ↦ congr_arg num

Premises used: Rat.num, congr_arg, Function.Injective
-- Module: Mathlib.Data.Rat.Defs
Goal:
⊢ Injective (β := ℚ) Nat.cast

Tactic:
intCast_injective.comp fun _ _ ↦ Int.natCast_inj.1

Premises used: Function.Injective.comp, Iff.mp, Rat.intCast_injective, Int.natCast_inj
-- Module: Mathlib.Data.Rat.Defs
Goal:
n : ℤ
⊢ Eq (α := ℚ) (↑n : ℚ) 1 ↔ n = 1

Tactic:
intCast_inj

Premises used: Rat.intCast_inj
-- Module: Mathlib.Data.Rat.Defs
Goal:
n : ℕ
⊢ Eq (α := ℚ) (↑n : ℚ) 1 ↔ n = 1

Tactic:
natCast_inj

Premises used: Rat.natCast_inj
-- Module: Mathlib.Data.Rat.Defs
Goal:
n : ℤ
d : ℕ
⊢ mkRat n d = n /. (↑d : ℤ)

Tactic:
rfl

Premises used: Rat.divInt, inline, dite, mkRat, rfl
-- Module: Mathlib.Data.Rat.Defs
Goal:
d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
e_den : d = 1
⊢ { num := 0, den := d, den_nz := h, reduced := w : ℚ } = 0

Tactic:
congr
-- Module: Mathlib.Data.Rat.Defs
Goal:
d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ d = 1

Tactic:
simp_all
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
⊢ q.num ≠ 0 ↔ q ≠ 0

Tactic:
num_eq_zero.not

Premises used: Iff.not, Rat.num_eq_zero
-- Module: Mathlib.Data.Rat.Defs
Goal:
q : ℚ
⊢ q.den ≠ 0

Tactic:
q.den_pos.ne'

Premises used: LT.lt.ne', Rat.den_pos
-- Module: Mathlib.Data.Rat.Defs
Goal:
a b : ℤ
b0 : b ≠ 0
rw : a /. b = 0 /. b ↔ a = 0
rw₁ : a * b = 0 * b ↔ a = 0
rw₂ : a * b = 0 ↔ a = 0
rw₃ : a = 0 ∨ b = 0 ↔ a = 0
rw₄ rw₅ : a = 0 ↔ a = 0
⊢ a /. b = 0 ↔ a = 0

Tactic:
rw [← zero_divInt b, divInt_eq_divInt_iff b0 b0, Int.zero_mul, Int.mul_eq_zero, or_iff_left b0]

Premises used: Rat.divInt_eq_divInt_iff, Rat.zero_divInt, Int.mul_eq_zero, or_iff_left, Int.zero_mul
-- Module: Mathlib.Data.Rat.Defs
Goal:
a b : ℤ
b0 : b ≠ 0
⊢ a /. b ≠ 0 ↔ a ≠ 0

Tactic:
(divInt_eq_zero b0).not

Premises used: Iff.not, Rat.divInt_eq_zero
-- Module: Mathlib.Data.Rat.Defs
Goal:
z : ℤ
⊢ (↑z : ℚ) = z /. 1

Tactic:
mk_eq_divInt

Premises used: Rat.mk_eq_divInt, Rat.ofInt
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      f₁ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) /. f₂ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ)
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
generalize : ∀ (x : ℚ) (ha : a /. b = x), f x (c /. d) = f₁ a b c d /. f₂ a b c d
⊢ f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d

Tactic:
generalize ha : a /. b = x
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      f₁ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) /. f₂ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ)
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
x : ℚ
ha : a /. b = x
obtain :
  ∀ (n₁ : ℤ) (d₁ : ℕ) (h₁ : d₁ ≠ 0) (c₁ : n₁.natAbs.Coprime d₁)
    (ha : a /. b = { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ }),
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ } (c /. d) = f₁ a b c d /. f₂ a b c d
⊢ f x (c /. d) = f₁ a b c d /. f₂ a b c d

Tactic:
obtain ⟨n₁, d₁, h₁, c₁⟩ := x
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      f₁ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) /. f₂ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ)
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ }
⊢ a /. b = n₁ /. (↑d₁ : ℤ)

Tactic:
rw [mk_eq_divInt] at ha

Premises used: Rat.mk_eq_divInt
-- Module: Mathlib.Data.Rat.Defs
Goal:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
        { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
      f₁ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) /. f₂ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ)
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. (↑d₁ : ℤ)
generalize :
  ∀ (x : ℚ) (hc : c /. d = x), f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ } x = f₁ a b c d /. f₂ a b c d
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ } (c /. d) = f₁ a b c d /. f₂ a b c d

Tactic:
generalize hc : c /. d = x