awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
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) (↑p : K) (↑q : K)
have hb : LT.lt.{u_5} (α := K) 0 (↑p.den : 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]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
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)
⊢ LT.lt.{u_5} (α := K) (↑p : K) (↑q : K)
have hd : LT.lt.{u_5} (α := K) 0 (↑q.den : 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]
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ≥0
⊢ 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:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ≥0
⊢ 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:
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 ↔ 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 : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
⊢ LE.le.{u_5} (α := K) (↑p : K) 1 ↔ p ≤ 1
have norm_cast : p ≤ 1 ↔ p ≤ 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
⊢ LE.le.{u_5} (α := K) 1 (↑p : K) ↔ 1 ≤ p
have norm_cast : 1 ≤ p ↔ 1 ≤ p
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
⊢ LT.lt.{u_5} (α := K) (↑p : K) 1 ↔ p < 1
have norm_cast : p < 1 ↔ p < 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
p : ℚ≥0
⊢ LT.lt.{u_5} (α := K) 1 (↑p : K) ↔ 1 < p
have norm_cast : 1 < p ↔ 1 < p
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Rat.Cast.Order (goal)
Goal:
K : Type u_5
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ≥0
n : ℕ
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m ≤ (↑n : ℚ≥0)
have rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ≥0) : 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 : 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)
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m ≤ (↑n : ℚ≥0)
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 : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℕ
n : ℚ≥0
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ≥0) ≤ n
have rw : LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LE.le.{u_5} (α := K) (↑(↑m : ℚ≥0) : 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 : 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)
⊢ LE.le.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ≥0) ≤ 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 : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℚ≥0
n : ℕ
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m < (↑n : ℚ≥0)
have rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑m : K) (↑(↑n : ℚ≥0) : 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 : 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)
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ m < (↑n : ℚ≥0)
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 : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
m : ℕ
n : ℚ≥0
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ≥0) < n
have rw : LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ LT.lt.{u_5} (α := K) (↑(↑m : ℚ≥0) : 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 : 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)
⊢ LT.lt.{u_5} (α := K) (↑m : K) (↑n : K) ↔ (↑m : ℚ≥0) < 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.Defs (goal)
Goal:
d : ℕ
h : d ≠ 0
w : (Int.natAbs 0).Coprime d
⊢ { num := 0, den := d, den_nz := h, reduced := w : ℚ } = 0
have e_den : d = 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
a b : ℤ
b0 : b ≠ 0
⊢ a /. b = 0 ↔ a = 0
have rw : a /. b = 0 /. b ↔ a = 0
Tactic: rw [← zero_divInt b, divInt_eq_divInt_iff b0 b0, Int.zero_mul, Int.mul_eq_zero, or_iff_left b0]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
a b : ℤ
b0 : b ≠ 0
rw : a /. b = 0 /. b ↔ a = 0
⊢ a /. b = 0 ↔ a = 0
have rw₁ : a * b = 0 * b ↔ a = 0
Tactic: rw [← zero_divInt b, divInt_eq_divInt_iff b0 b0, Int.zero_mul, Int.mul_eq_zero, or_iff_left b0]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
a b : ℤ
b0 : b ≠ 0
rw : a /. b = 0 /. b ↔ a = 0
rw₁ : a * b = 0 * b ↔ a = 0
⊢ a /. b = 0 ↔ a = 0
have rw₂ : 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]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
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
⊢ a /. b = 0 ↔ a = 0
have rw₃ : a = 0 ∨ 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]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
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
⊢ a /. b = 0 ↔ a = 0
have rw₄ : a = 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]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
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₂
⊢ f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d
have generalize : ∀ (x : ℚ) (ha : a /. b = x), f x (c /. d) = f₁ a b c d /. f₂ a b c d
Tactic: generalize ha : a /. b = x
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
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
⊢ f x (c /. d) = f₁ a b c d /. f₂ a b c d
have 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
Tactic: obtain ⟨n₁, d₁, h₁, c₁⟩ := x
Cleared hypotheses: x, ha
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (hypothesis)
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₁ }
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ } (c /. d) = f₁ a b c d /. f₂ a b c d
have ha₁ : a /. b = n₁ /. (↑d₁ : ℤ)
Tactic: rw [mk_eq_divInt] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
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₁ : ℤ)
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ } (c /. d) = f₁ a b c d /. f₂ a b c d
have 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
Tactic: generalize hc : c /. d = x
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
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₁ : ℤ)
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
have obtain : ∀ (n₂ : ℤ) (d₂ : ℕ) (h₂ : d₂ ≠ 0) (c₂ : n₂.natAbs.Coprime d₂)
  (hc : c /. d = { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ }),
  f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
      { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
    f₁ a b c d /. f₂ a b c d
Tactic: obtain ⟨n₂, d₂, h₂, c₂⟩ := x
Cleared hypotheses: x, hc
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (hypothesis)
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₁ : ℤ)
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ }
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
      { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
    f₁ a b c d /. f₂ a b c d
have hc₁ : c /. d = n₂ /. (↑d₂ : ℤ)
Tactic: rw [mk_eq_divInt] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
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₁ : ℤ)
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. (↑d₂ : ℤ)
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ : ℚ }
      { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ : ℚ } =
    f₁ a b c d /. f₂ a b c d
have rw : f₁ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) /. f₂ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) = f₁ a b c d /. f₂ a b c d
Tactic: rw [fv]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (hypothesis)
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₁ : ℤ)
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. (↑d₂ : ℤ)
⊢ f₁ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) /. f₂ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) = f₁ a b c d /. f₂ a b c d
have d₁0 : Ne (α := ℤ) (↑d₁ : ℤ) 0
Tactic: have d₁0 := Int.ofNat_ne_zero.2 h₁
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (hypothesis)
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₁ : ℤ)
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. (↑d₂ : ℤ)
d₁0 : Ne (α := ℤ) (↑d₁ : ℤ) 0
⊢ f₁ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) /. f₂ n₁ (↑d₁ : ℤ) n₂ (↑d₂ : ℤ) = f₁ a b c d /. f₂ a b c d
have d₂0 : Ne (α := ℤ) (↑d₂ : ℤ) 0
Tactic: have d₂0 := Int.ofNat_ne_zero.2 h₂
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
⊢ -q = -q.num /. (↑q.den : ℤ)
have rw : -q = -(q.num /. (↑q.den : ℤ))
Tactic: rw [← neg_divInt, num_divInt_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
rw : -q = -(q.num /. (↑q.den : ℤ))
⊢ -q = -q.num /. (↑q.den : ℤ)
have rw₁ : -q = -q
Tactic: rw [← neg_divInt, num_divInt_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ (n₁ * n₂).natAbs.Coprime (d₁ * d₂)
have rw : (n₁.natAbs * n₂.natAbs).Coprime (d₁ * d₂)
Tactic: rw [Int.natAbs_mul]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
n₁ n₂ : ℤ
d₁ d₂ : ℕ
hd₁ : d₁ ≠ 0
hd₂ : d₂ ≠ 0
hnd₁ : n₁.natAbs.Coprime d₁
hnd₂ : n₂.natAbs.Coprime d₂
h₁₂ : n₁.natAbs.Coprime d₂
h₂₁ : n₂.natAbs.Coprime d₁
⊢ { num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ : ℚ } *
      { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ : ℚ } =
    { num := n₁ * n₂, den := d₁ * d₂, den_nz := ⋯, reduced := ⋯ }
have rw : normalize
    ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ : ℚ }.num *
      { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ : ℚ }.num)
    ({ num := n₁, den := d₁, den_nz := hd₁, reduced := hnd₁ : ℚ }.den *
      { num := n₂, den := d₂, den_nz := hd₂, reduced := hnd₂ : ℚ }.den)
    sorry =
  { num := n₁ * n₂, den := d₁ * d₂, den_nz := sorry, reduced := sorry }
Tactic: rw [mul_def]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q r : ℚ
⊢ q * r = mkRat (q.num * r.num) (q.den * r.den)
have rw : normalize (q.num * r.num) (q.den * r.den) sorry = mkRat (q.num * r.num) (q.den * r.den)
Tactic: rw [mul_def, normalize_eq_mkRat]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q r : ℚ
rw : normalize (q.num * r.num) (q.den * r.den) ⋯ = mkRat (q.num * r.num) (q.den * r.den)
⊢ q * r = mkRat (q.num * r.num) (q.den * r.den)
have rw₁ : mkRat (q.num * r.num) (q.den * r.den) = mkRat (q.num * r.num) (q.den * r.den)
Tactic: rw [mul_def, normalize_eq_mkRat]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
n : ℕ
⊢ q ^ n = mkRat (q.num ^ n) (q.den ^ n)
have rw : { num := q.num ^ n, den := q.den ^ n, den_nz := sorry, reduced := sorry : ℚ } = mkRat (q.num ^ n) (q.den ^ n)
Tactic: rw [pow_def, mk_eq_mkRat]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
n : ℕ
rw : { num := q.num ^ n, den := q.den ^ n, den_nz := ⋯, reduced := ⋯ : ℚ } = mkRat (q.num ^ n) (q.den ^ n)
⊢ q ^ n = mkRat (q.num ^ n) (q.den ^ n)
have rw₁ : mkRat (q.num ^ n) (q.den ^ n) = mkRat (q.num ^ n) (q.den ^ n)
Tactic: rw [pow_def, mk_eq_mkRat]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
n : ℕ
⊢ q ^ n = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
have rw : { num := q.num ^ n, den := q.den ^ n, den_nz := sorry, reduced := sorry : ℚ } = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
Tactic: rw [pow_def, mk_eq_divInt, Int.natCast_pow]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
n : ℕ
rw :
  { num := q.num ^ n, den := q.den ^ n, den_nz := ⋯, reduced := ⋯ : ℚ } = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
⊢ q ^ n = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
have rw₁ : q.num ^ n /. (↑(q.den ^ n) : ℤ) = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
Tactic: rw [pow_def, mk_eq_divInt, Int.natCast_pow]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
n : ℕ
rw :
  { num := q.num ^ n, den := q.den ^ n, den_nz := ⋯, reduced := ⋯ : ℚ } = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
rw₁ : q.num ^ n /. (↑(q.den ^ n) : ℤ) = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
⊢ q ^ n = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
have rw₂ : q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n = q.num ^ n /. HPow.hPow (α := ℤ) (↑q.den : ℤ) n
Tactic: rw [pow_def, mk_eq_divInt, Int.natCast_pow]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q : ℚ
num : ℤ
den : ℕ
hd : den ≠ 0
hdn : num.natAbs.Coprime den
n : ℕ
⊢ (num ^ n).natAbs.Coprime (den ^ n)
have rw : (num.natAbs ^ n).Coprime (den ^ n)
Tactic: rw [Int.natAbs_pow]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
a : ℤ
b : ℕ
⊢ (mkRat a b)⁻¹ = (↑b : ℤ) /. a
have rw : (a /. (↑b : ℤ))⁻¹ = (↑b : ℤ) /. a
Tactic: rw [mkRat_eq_divInt, inv_divInt]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
a : ℤ
b : ℕ
rw : (a /. (↑b : ℤ))⁻¹ = (↑b : ℤ) /. a
⊢ (mkRat a b)⁻¹ = (↑b : ℤ) /. a
have rw₁ : (↑b : ℤ) /. a = (↑b : ℤ) /. a
Tactic: rw [mkRat_eq_divInt, inv_divInt]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ / (n₂ /. d₂) = n₁ * d₂ /. (d₁ * n₂)
have rw : n₁ /. d₁ * (n₂ /. d₂)⁻¹ = n₁ * d₂ /. (d₁ * n₂)
Tactic: rw [div_def, inv_divInt, divInt_mul_divInt]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
n₁ d₁ n₂ d₂ : ℤ
rw : n₁ /. d₁ * (n₂ /. d₂)⁻¹ = n₁ * d₂ /. (d₁ * n₂)
⊢ n₁ /. d₁ / (n₂ /. d₂) = n₁ * d₂ /. (d₁ * n₂)
have rw₁ : n₁ /. d₁ * (d₂ /. n₂) = n₁ * d₂ /. (d₁ * n₂)
Tactic: rw [div_def, inv_divInt, divInt_mul_divInt]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
n₁ d₁ n₂ d₂ : ℤ
rw : n₁ /. d₁ * (n₂ /. d₂)⁻¹ = n₁ * d₂ /. (d₁ * n₂)
rw₁ : n₁ /. d₁ * (d₂ /. n₂) = n₁ * d₂ /. (d₁ * n₂)
⊢ n₁ /. d₁ / (n₂ /. d₂) = n₁ * d₂ /. (d₁ * n₂)
have rw₂ : n₁ * d₂ /. (d₁ * n₂) = n₁ * d₂ /. (d₁ * n₂)
Tactic: rw [div_def, inv_divInt, divInt_mul_divInt]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q r : ℚ
⊢ q / r = q.num * (↑r.den : ℤ) /. ((↑q.den : ℤ) * r.num)
have rw : q / r = q.num /. (↑q.den : ℤ) / (r.num /. (↑r.den : ℤ))
Tactic: rw [← divInt_div_divInt, num_divInt_den, num_divInt_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q r : ℚ
rw : q / r = q.num /. (↑q.den : ℤ) / (r.num /. (↑r.den : ℤ))
⊢ q / r = q.num * (↑r.den : ℤ) /. ((↑q.den : ℤ) * r.num)
have rw₁ : q / r = q / (r.num /. (↑r.den : ℤ))
Tactic: rw [← divInt_div_divInt, num_divInt_den, num_divInt_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q r : ℚ
rw : q / r = q.num /. (↑q.den : ℤ) / (r.num /. (↑r.den : ℤ))
rw₁ : q / r = q / (r.num /. (↑r.den : ℤ))
⊢ q / r = q.num * (↑r.den : ℤ) /. ((↑q.den : ℤ) * r.num)
have rw₂ : q / r = q / r
Tactic: rw [← divInt_div_divInt, num_divInt_den, num_divInt_den]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
⊢ 1 /. 1 = 1
have rw : Eq (α := ℚ) (↑1 : ℚ) 1
Tactic: rw [divInt_one, Rat.intCast_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
rw : Eq (α := ℚ) (↑1 : ℚ) 1
⊢ 1 /. 1 = 1
have rw₁ : Eq (α := ℚ) 1 1
Tactic: rw [divInt_one, Rat.intCast_one]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
⊢ Ne (α := ℚ) 0 1
have rw : Ne (α := ℤ) 1 0
Tactic: rw [ne_comm, ← divInt_one_one, divInt_ne_zero]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q_1 a b c : ℚ
n : ℕ
q : ℚ
⊢ (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℚ) * q = (↑n : ℚ) * q + q
have rw : (↑(↑n : ℤ) : ℚ) * q + q = (↑n : ℚ) * q + q
Tactic: rw [Rat.intCast_add, Rat.add_mul, Rat.intCast_one, Rat.one_mul]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
q a b c : ℚ
x : ℕ
x_1 : ℚ
⊢ (↑(Int.negSucc x) : ℚ) * x_1 = -((↑(↑x.succ : ℤ) : ℚ) * x_1)
have rw : -((↑(HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) : ℚ) * x_1) = -((↑(↑x.succ : ℤ) : ℚ) * x_1)
Tactic: rw [Int.negSucc_eq, Rat.intCast_neg, Rat.neg_mul]
-- Lean 4 proof step from Mathlib.Data.Rat.Defs (goal)
Goal:
a b c : ℤ
h : ¬c = 0
⊢ (a + b) /. c = a /. c + b /. c
have rw : (a + b) * (c * c) = (a * c + b * c) * c
Tactic: rw [divInt_add_divInt _ _ h h, divInt_eq_divInt_iff h (Int.mul_ne_zero h h)]