awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
refine_1 :
  ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → Membership.mem (γ := Multiset α) 0 b → r a b)
    (hc : m1.card = card.{u_1} (α := α) 0), Rel r m1 0
⊢ ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) (hc : m1.card = m2.card), Rel r m1 m2
have refine_2 : ∀ (a : α) (s : Multiset α),
  (∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ s → r a b) (hc : m1.card = s.card), Rel r m1 s) →
    ∀ {m1 : Multiset α} (h : ∀ (a_2 b : α), a_2 ∈ m1 → b ∈ a ::ₘ s → r a_2 b) (hc : m1.card = (a ::ₘ s).card),
      Rel r m1 (a ::ₘ s)
Tactic: refine @(m2.induction_on ?_ ?_)
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → Membership.mem (γ := Multiset α) 0 b → r a b
hc : m.card = card.{u_1} (α := α) 0
⊢ Rel r m 0
have refine_1 : m = 0
Tactic: rw [rel_zero_right, ← card_eq_zero, hc, card_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → Membership.mem (γ := Multiset α) 0 b → r a b
hc : m.card = card.{u_1} (α := α) 0
refine_1 : m = 0
⊢ Rel r m 0
have refine_1₁ : m.card = 0
Tactic: rw [rel_zero_right, ← card_eq_zero, hc, card_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → Membership.mem (γ := Multiset α) 0 b → r a b
hc : m.card = card.{u_1} (α := α) 0
refine_1 : m = 0
refine_1₁ : m.card = 0
⊢ Rel r m 0
have refine_1₂ : card.{u_1} (α := α) 0 = 0
Tactic: rw [rel_zero_right, ← card_eq_zero, hc, card_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → Membership.mem (γ := Multiset α) 0 b → r a b
hc : m.card = card.{u_1} (α := α) 0
refine_1 : m = 0
refine_1₁ : m.card = 0
refine_1₂ : card.{u_1} (α := α) 0 = 0
⊢ Rel r m 0
have refine_1₃ : Eq (α := ℕ) 0 0
Tactic: rw [rel_zero_right, ← card_eq_zero, hc, card_zero]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (hypothesis)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ t → r a b) (hc : m1.card = t.card), Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = (a ::ₘ t).card
⊢ Rel r m (a ::ₘ t)
have hc₁ : m.card = t.card + 1
Tactic: rw [card_cons] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ t → r a b) (hc : m1.card = t.card), Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = t.card + 1
⊢ Rel r m (a ::ₘ t)
have refine_2 : ∀ (b : α) (hb : b ∈ m), Rel r m (a ::ₘ t)
Tactic: obtain ⟨b, hb⟩ := card_pos_iff_exists_mem.1 (show 0 < card m from hc.symm ▸ Nat.succ_pos _)
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ t → r a b) (hc : m1.card = t.card), Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
hc : m.card = t.card + 1
b : α
hb : b ∈ m
⊢ Rel r m (a ::ₘ t)
have refine_2 : ∀ (m' : Multiset α) (h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1)
  (hc : (b ::ₘ m').card = t.card + 1) (hb : b ∈ b ::ₘ m'), Rel r (b ::ₘ m') (a ::ₘ t)
Tactic: obtain ⟨m', rfl⟩ := exists_cons_of_mem hb
Cleared hypotheses: m, h, hc, hb
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ t → r a b) (hc : m1.card = t.card), Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
⊢ Rel r (b ::ₘ m') (a ::ₘ t)
have refine_2 : ∀ (a b : α), a ∈ m' → b ∈ t → r a b
Tactic: refine rel_cons_right.mpr ⟨b, m', h _ _ hb (mem_cons_self _ _), ih ?_ ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ t → r a b) (hc : m1.card = t.card), Rel r m1 t
b : α
m' : Multiset α
h : ∀ (a_1 b_1 : α), a_1 ∈ b ::ₘ m' → b_1 ∈ a ::ₘ t → r a_1 b_1
hc : (b ::ₘ m').card = t.card + 1
hb : b ∈ b ::ₘ m'
refine_2 : ∀ (a b : α), a ∈ m' → b ∈ t → r a b
⊢ Rel r (b ::ₘ m') (a ::ₘ t)
have refine_2₁ : m'.card = t.card
Tactic: refine rel_cons_right.mpr ⟨b, m', h _ _ hb (mem_cons_self _ _), ih ?_ ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
s u : Multiset α
r1 : Rel r s 0
r2 empty : Rel r 0 u
⊢ Rel r s u
have empty₁ : Rel r 0 0
Tactic: rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
s u : Multiset α
r1 : Rel r s 0
r2 empty : Rel r 0 u
empty₁ : Rel r 0 0
⊢ Rel r s u
have empty₂ : Eq.{u_1 + 1} (α := Multiset α) 0 0
Tactic: rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α} (r1 : Rel r s t) (r2 : Rel r t u), Rel r s u
s u : Multiset α
r1 : Rel r s (x ::ₘ t)
r2 : Rel r (x ::ₘ t) u
⊢ Rel r s u
have cons : ∀ (a : α) (as : Multiset α) (ha1 : r a x) (ha2 : Rel r as t) (r1 : Rel r (a ::ₘ as) (x ::ₘ t)), Rel r (a ::ₘ as) u
Tactic: obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1
Cleared hypotheses: s, r1
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α} (r1 : Rel r s t) (r2 : Rel r t u), Rel r s u
u : Multiset α
r2 : Rel r (x ::ₘ t) u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
⊢ Rel r (a ::ₘ as) u
have cons : ∀ (b : α) (bs : Multiset α) (hb1 : r x b) (hb2 : Rel r t bs) (r2 : Rel r (x ::ₘ t) (b ::ₘ bs)),
  Rel r (a ::ₘ as) (b ::ₘ bs)
Tactic: obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2
Cleared hypotheses: u, r2
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
s t u : Multiset α
r1 : Rel r s t
r2 : Rel r t u
⊢ Rel r s u
have empty : ∀ {s u : Multiset α} (r1 : Rel r s 0) (r2 : Rel r 0 u), Rel r s u
Tactic: induction t using Multiset.induction_on generalizing s u with
  | empty => rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]
  | cons x t ih =>
    obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1
    obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2
    exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)
Cleared hypotheses: s, t, u, r1, r2
-- Lean 4 proof step from Mathlib.Data.Multiset.ZeroCons (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
s t u : Multiset α
r1 : Rel r s t
r2 : Rel r t u
empty : ∀ {s u : Multiset α} (r1 : Rel r s 0) (r2 : Rel r 0 u), Rel r s u
⊢ Rel r s u
have cons : ∀ (x : α) (t : Multiset α) (ih : ∀ {s u : Multiset α} (r1 : Rel r s t) (r2 : Rel r t u), Rel r s u) {s u : Multiset α}
  (r1 : Rel r s (x ::ₘ t)) (r2 : Rel r (x ::ₘ t) u), Rel r s u
Tactic: induction t using Multiset.induction_on generalizing s u with
  | empty => rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]
  | cons x t ih =>
    obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1
    obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2
    exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)
Cleared hypotheses: s, t, u, r1, r2
-- Lean 4 proof step from Mathlib.Data.NNRat.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ Rat.toNNRat (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toNNRat
have rw : Eq (α := ℚ) (∑ i ∈ s, f i) (∑ a ∈ s, (↑(f a).toNNRat : ℚ))
Tactic: rw [← coe_inj, cast_sum, Rat.coe_toNNRat _ (Finset.sum_nonneg hf)]
-- Lean 4 proof step from Mathlib.Data.NNRat.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
x : α
hxs : x ∈ s
⊢ f x = (↑(f x).toNNRat : ℚ)
have rw : f x = f x
Tactic: rw [Rat.coe_toNNRat _ (hf x hxs)]
-- Lean 4 proof step from Mathlib.Data.NNRat.BigOperators (goal)
Goal:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ Rat.toNNRat (∏ a ∈ s, f a) = ∏ a ∈ s, (f a).toNNRat
have rw : Eq (α := ℚ) (∏ i ∈ s, f i) (∏ a ∈ s, (↑(f a).toNNRat : ℚ))
Tactic: rw [← coe_inj, cast_prod, Rat.coe_toNNRat _ (Finset.prod_nonneg hf)]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ≥0
h : q ≤ p
⊢ (↑q : ℚ) ≤ (↑p : ℚ) - 0
have rwa : (↑q : ℚ) ≤ (↑p : ℚ)
Tactic: rwa [sub_zero]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
q : ℚ≥0
⊢ Eq (α := ℚ) (↑q : ℚ) 0 ↔ q = 0
have norm_cast : q = 0 ↔ q = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ) (↑(toNNRat (↑n : ℚ)) : ℚ) (↑(↑n : ℚ≥0) : ℚ)
have simp : Eq (α := ℚ) (↑n : ℚ) (↑(↑n : ℚ≥0) : ℚ)
Tactic: simp only [Nat.cast_nonneg', Rat.coe_toNNRat]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p : ℚ
q : ℚ≥0
hp : 0 ≤ p
⊢ q ≤ p.toNNRat ↔ (↑q : ℚ) ≤ p
have rw : LE.le (α := ℚ) (↑q : ℚ) (↑p.toNNRat : ℚ) ↔ (↑q : ℚ) ≤ p
Tactic: rw [← coe_le_coe, Rat.coe_toNNRat p hp]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p : ℚ
q : ℚ≥0
hp : 0 ≤ p
rw : LE.le (α := ℚ) (↑q : ℚ) (↑p.toNNRat : ℚ) ↔ (↑q : ℚ) ≤ p
⊢ q ≤ p.toNNRat ↔ (↑q : ℚ) ≤ p
have rw₁ : (↑q : ℚ) ≤ p ↔ (↑q : ℚ) ≤ p
Tactic: rw [← coe_le_coe, Rat.coe_toNNRat p hp]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ q.toNNRat < p ↔ q < (↑p : ℚ)
have rw : LT.lt (α := ℚ) (↑q.toNNRat : ℚ) (↑p : ℚ) ↔ q < (↑p : ℚ)
Tactic: rw [← coe_lt_coe, Rat.coe_toNNRat q hq]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
q : ℚ
p : ℚ≥0
hq : 0 ≤ q
rw : LT.lt (α := ℚ) (↑q.toNNRat : ℚ) (↑p : ℚ) ↔ q < (↑p : ℚ)
⊢ q.toNNRat < p ↔ q < (↑p : ℚ)
have rw₁ : q < (↑p : ℚ) ↔ q < (↑p : ℚ)
Tactic: rw [← coe_lt_coe, Rat.coe_toNNRat q hq]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ
hp : 0 ≤ p
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
have inl : ∀ (hq : 0 ≤ q), (p * q).toNNRat = p.toNNRat * q.toNNRat
Tactic: rcases le_total 0 q with hq | hq
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ
hp : 0 ≤ p
inl : ∀ (hq : 0 ≤ q), (p * q).toNNRat = p.toNNRat * q.toNNRat
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
have inr : ∀ (hq : q ≤ 0), (p * q).toNNRat = p.toNNRat * q.toNNRat
Tactic: rcases le_total 0 q with hq | hq
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
have inl : Eq (α := ℚ) (↑(p * q).toNNRat : ℚ) (↑(p.toNNRat * q.toNNRat) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (hypothesis)
Goal:
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
have hpq : p * q ≤ 0
Tactic: have hpq := mul_nonpos_of_nonneg_of_nonpos hp hq
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
have inr : (p * q).toNNRat = p.toNNRat * 0
Tactic: rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
inr : (p * q).toNNRat = p.toNNRat * 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
have inr₁ : 0 = p.toNNRat * 0
Tactic: rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ
hp : 0 ≤ p
hq : q ≤ 0
hpq : p * q ≤ 0
inr : (p * q).toNNRat = p.toNNRat * 0
inr₁ : 0 = p.toNNRat * 0
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat
have inr₂ : Eq (α := ℚ≥0) 0 0
Tactic: rw [toNNRat_eq_zero.2 hq, toNNRat_eq_zero.2 hpq, mul_zero]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ≥0
hn : p.num = q.num
hd : p.den = q.den
⊢ p = q
have refine : Rat.num (↑p : ℚ) = Rat.num (↑q : ℚ)
Tactic: refine ext <| Rat.ext ?_ hd
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁
have rw : Eq (α := ℚ) (↑(divNat n₁ d₁) : ℚ) (↑(divNat n₂ d₂) : ℚ) ↔ n₁ * d₂ = n₂ * d₁
Tactic: rw [← coe_inj]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ Eq (α := ℚ) (↑(divNat n₁ d₁) : ℚ) (↑(divNat n₂ d₂) : ℚ) ↔ n₁ * d₂ = n₂ * d₁
have simp : HMul.hMul (α := ℤ) (↑n₁ : ℤ) (↑d₂ : ℤ) = HMul.hMul (α := ℤ) (↑n₂ : ℤ) (↑d₁ : ℤ) ↔ n₁ * d₂ = n₂ * d₁
Tactic: simp [Rat.mkRat_eq_iff, h₁, h₂]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ HMul.hMul (α := ℤ) (↑n₁ : ℤ) (↑d₂ : ℤ) = HMul.hMul (α := ℤ) (↑n₂ : ℤ) (↑d₁ : ℤ) ↔ n₁ * d₂ = n₂ * d₁
have norm_cast : n₁ * d₂ = n₂ * d₁ ↔ n₁ * d₂ = n₂ * d₁
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
q : ℚ≥0
⊢ Eq (α := ℚ) (↑(divNat q.num q.den) : ℚ) (↑q : ℚ)
have rw : (↑(divNat q.num q.den) : ℚ) = mkRat (Rat.num (↑q : ℚ)) (Rat.den (↑q : ℚ))
Tactic: rw [← (q : ℚ).mkRat_num_den']
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
n₁ n₂ d₁ d₂ : ℕ
⊢ divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)
have a : Eq (α := ℚ) (↑(divNat n₁ d₁ * divNat n₂ d₂) : ℚ) (↑(divNat (n₁ * n₂) (d₁ * d₂)) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
n₁ n₂ d₁ d₂ : ℕ
⊢ Eq (α := ℚ) (↑(divNat n₁ d₁ * divNat n₂ d₂) : ℚ) (↑(divNat (n₁ * n₂) (d₁ * d₂)) : ℚ)
have a : Rat.divInt (↑n₁ : ℤ) (↑d₁ : ℤ) * Rat.divInt (↑n₂ : ℤ) (↑d₂ : ℤ) =
  Rat.divInt (HMul.hMul (α := ℤ) (↑n₁ : ℤ) (↑n₂ : ℤ)) (HMul.hMul (α := ℤ) (↑d₁ : ℤ) (↑d₂ : ℤ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (a * n) (a * d) = divNat n d
have a₁ : Eq (α := ℚ) (↑(divNat (a * n) (a * d)) : ℚ) (↑(divNat n d) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Eq (α := ℚ) (↑(divNat (a * n) (a * d)) : ℚ) (↑(divNat n d) : ℚ)
have a₁ : Rat.divInt (HMul.hMul (α := ℤ) (↑a : ℤ) (↑n : ℤ)) (HMul.hMul (α := ℤ) (↑a : ℤ) (↑d : ℤ)) = Rat.divInt (↑n : ℤ) (↑d : ℤ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (n * a) (d * a) = divNat n d
have a₁ : Eq (α := ℚ) (↑(divNat (n * a) (d * a)) : ℚ) (↑(divNat n d) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Eq (α := ℚ) (↑(divNat (n * a) (d * a)) : ℚ) (↑(divNat n d) : ℚ)
have a₁ : Rat.divInt (HMul.hMul (α := ℤ) (↑n : ℤ) (↑a : ℤ)) (HMul.hMul (α := ℤ) (↑d : ℤ) (↑a : ℤ)) = Rat.divInt (↑n : ℤ) (↑d : ℤ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
q : ℚ≥0
⊢ q * (↑q.den : ℚ≥0) = (↑q.num : ℚ≥0)
have a : Eq (α := ℚ) (↑(q * (↑q.den : ℚ≥0)) : ℚ) (↑(↑q.num : ℚ≥0) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
q : ℚ≥0
⊢ HMul.hMul (α := ℚ) (↑q : ℚ) (↑q.den : ℚ) = (↑q.num : ℚ)
have a : HMul.hMul (α := ℚ) (↑q : ℚ) (↑(↑(Rat.den (↑q : ℚ)) : ℤ) : ℚ) = (↑(Rat.num (↑q : ℚ)) : ℚ)
Tactic: rw [← Int.cast_natCast, ← den_coe, ← Int.cast_natCast q.num, ← num_coe]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
q : ℚ≥0
⊢ (↑q.den : ℚ≥0) * q = (↑q.num : ℚ≥0)
have rw : q * (↑q.den : ℚ≥0) = (↑q.num : ℚ≥0)
Tactic: rw [mul_comm, mul_den_eq_num]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
q : ℚ≥0
rw : q * (↑q.den : ℚ≥0) = (↑q.num : ℚ≥0)
⊢ (↑q.den : ℚ≥0) * q = (↑q.num : ℚ≥0)
have rw₁ : Eq (α := ℚ≥0) (↑q.num : ℚ≥0) (↑q.num : ℚ≥0)
Tactic: rw [mul_comm, mul_den_eq_num]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q_1 : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C q
have rw : C (divNat q.num q.den)
Tactic: rw [← q.num_divNat_den]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
q r : ℚ≥0
⊢ q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den)
have a : Eq (α := ℚ) (↑(q + r) : ℚ) (↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den)) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
q r : ℚ≥0
⊢ q * r = divNat (q.num * r.num) (q.den * r.den)
have a : Eq (α := ℚ) (↑(q * r) : ℚ) (↑(divNat (q.num * r.num) (q.den * r.den)) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ≥0
⊢ p < q ↔ p.num * q.den < q.num * p.den
have rw : Rat.num (↑p : ℚ) * (↑(Rat.den (↑q : ℚ)) : ℤ) < Rat.num (↑q : ℚ) * (↑(Rat.den (↑p : ℚ)) : ℤ) ↔
  p.num * q.den < q.num * p.den
Tactic: rw [← NNRat.coe_lt_coe, Rat.lt_iff]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ≥0
⊢ Rat.num (↑p : ℚ) * (↑(Rat.den (↑q : ℚ)) : ℤ) < Rat.num (↑q : ℚ) * (↑(Rat.den (↑p : ℚ)) : ℤ) ↔
    p.num * q.den < q.num * p.den
have norm_cast : p.num * q.den < q.num * p.den ↔ p.num * q.den < q.num * p.den
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ≥0
⊢ p ≤ q ↔ p.num * q.den ≤ q.num * p.den
have rw : Rat.num (↑p : ℚ) * (↑(Rat.den (↑q : ℚ)) : ℤ) ≤ Rat.num (↑q : ℚ) * (↑(Rat.den (↑p : ℚ)) : ℤ) ↔
  p.num * q.den ≤ q.num * p.den
Tactic: rw [← NNRat.coe_le_coe, Rat.le_iff]
-- Lean 4 proof step from Mathlib.Data.NNRat.Defs (goal)
Goal:
p q : ℚ≥0
⊢ Rat.num (↑p : ℚ) * (↑(Rat.den (↑q : ℚ)) : ℤ) ≤ Rat.num (↑q : ℚ) * (↑(Rat.den (↑p : ℚ)) : ℤ) ↔
    p.num * q.den ≤ q.num * p.den
have norm_cast : p.num * q.den ≤ q.num * p.den ↔ p.num * q.den ≤ q.num * p.den
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Encodable (goal)
Goal:
x : ℚ≥0
num : ℤ
den : ℕ
den_nz : den ≠ 0
reduced : num.natAbs.Coprime den
hq : 0 ≤ { num := num, den := den, den_nz := den_nz, reduced := reduced : ℚ }
⊢ (fun (x : (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d }) ↦
        (match (motive := (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d } → ℚ≥0) x with
          | ⟨num, ⟨den, prop⟩⟩ =>
            Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := ⋯, reduced := ⋯ } ⋯ :
          ℚ≥0))
      ((fun (q : ℚ≥0) ↦
          (Sigma.mk (β := fun (n : ℕ) ↦ { d : ℕ // 0 < d ∧ n.Coprime d }) q.num
              (Subtype.mk (p := fun (d : ℕ) ↦ 0 < d ∧ q.num.Coprime d) q.den ⋯) :
            (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d }))
        (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := num, den := den, den_nz := den_nz, reduced := reduced } hq)) =
    Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := num, den := den, den_nz := den_nz, reduced := reduced : ℚ } hq
have lift : ∀ (num : ℕ) (reduced : (Int.natAbs (↑num : ℤ)).Coprime den)
  (hq : 0 ≤ { num := (↑num : ℤ), den := den, den_nz := den_nz, reduced := reduced : ℚ }),
  (fun (x : (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d }) ↦
        (match (motive := (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d } → ℚ≥0) x with
          | ⟨num, ⟨den, prop⟩⟩ =>
            Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := sorry, reduced := sorry } sorry :
          ℚ≥0))
      ((fun (q : ℚ≥0) ↦
          (Sigma.mk (β := fun (n : ℕ) ↦ { d : ℕ // 0 < d ∧ n.Coprime d }) q.num
              (Subtype.mk (p := fun (d : ℕ) ↦ 0 < d ∧ q.num.Coprime d) q.den sorry) :
            (n : ℕ) × { d : ℕ // 0 < d ∧ n.Coprime d }))
        (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := den_nz, reduced := reduced }
          hq)) =
    Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) { num := (↑num : ℤ), den := den, den_nz := den_nz, reduced := reduced : ℚ } hq
Tactic: lift num to ℕ using Rat.num_nonneg.mpr hq
Cleared hypotheses: num, reduced, hq
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ n ≤ ⌊(↑a : ℚ)⌋₊ ↔ (↑n : ℚ≥0) ≤ a
have rw : (↑n : ℚ) ≤ (↑a : ℚ) ↔ LE.le (α := ℚ) (↑(↑n : ℚ≥0) : ℚ) (↑a : ℚ)
Tactic: rw [← NNRat.coe_le_coe, Nat.le_floor_iff]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
a : ℚ≥0
n : ℕ
h : 0 ≤ a
rw : (↑n : ℚ) ≤ (↑a : ℚ) ↔ LE.le (α := ℚ) (↑(↑n : ℚ≥0) : ℚ) (↑a : ℚ)
⊢ n ≤ ⌊(↑a : ℚ)⌋₊ ↔ (↑n : ℚ≥0) ≤ a
have rw₁ : 0 ≤ (↑a : ℚ)
Tactic: rw [← NNRat.coe_le_coe, Nat.le_floor_iff]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
a : ℚ≥0
n : ℕ
h : 0 ≤ a
⊢ (↑n : ℚ) ≤ (↑a : ℚ) ↔ LE.le (α := ℚ) (↑(↑n : ℚ≥0) : ℚ) (↑a : ℚ)
have norm_cast : (↑n : ℚ) ≤ (↑a : ℚ) ↔ (↑n : ℚ≥0) ≤ a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
a : ℚ≥0
b : ℕ
⊢ (fun (q : ℚ≥0) ↦ ⌈(↑q : ℚ)⌉₊) a ≤ b ↔ a ≤ (↑b : ℚ≥0)
have rw : (↑a : ℚ) ≤ (↑b : ℚ) ↔ LE.le (α := ℚ) (↑a : ℚ) (↑(↑b : ℚ≥0) : ℚ)
Tactic: rw [← NNRat.coe_le_coe, Nat.ceil_le]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
a : ℚ≥0
b : ℕ
⊢ (↑a : ℚ) ≤ (↑b : ℚ) ↔ LE.le (α := ℚ) (↑a : ℚ) (↑(↑b : ℚ≥0) : ℚ)
have norm_cast : (↑a : ℚ) ≤ (↑b : ℚ) ↔ a ≤ (↑b : ℚ≥0)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
q : ℚ≥0
⊢ ⌊q⌋₊ = q.num / q.den
have rw : Eq (α := ℤ) (↑⌊q⌋₊ : ℤ) (↑(q.num / q.den) : ℤ)
Tactic: rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def', Int.natCast_ediv, den_coe, num_coe]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
q : ℚ≥0
rw : Eq (α := ℤ) (↑⌊q⌋₊ : ℤ) (↑(q.num / q.den) : ℤ)
⊢ ⌊q⌋₊ = q.num / q.den
have rw₁ : Int.floor (α := ℚ) (↑q : ℚ) = (↑(q.num / q.den) : ℤ)
Tactic: rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def', Int.natCast_ediv, den_coe, num_coe]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
q : ℚ≥0
rw : Eq (α := ℤ) (↑⌊q⌋₊ : ℤ) (↑(q.num / q.den) : ℤ)
rw₁ : Int.floor (α := ℚ) (↑q : ℚ) = (↑(q.num / q.den) : ℤ)
⊢ ⌊q⌋₊ = q.num / q.den
have rw₂ : Rat.num (↑q : ℚ) / (↑(Rat.den (↑q : ℚ)) : ℤ) = (↑(q.num / q.den) : ℤ)
Tactic: rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def', Int.natCast_ediv, den_coe, num_coe]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
q : ℚ≥0
rw : Eq (α := ℤ) (↑⌊q⌋₊ : ℤ) (↑(q.num / q.den) : ℤ)
rw₁ : Int.floor (α := ℚ) (↑q : ℚ) = (↑(q.num / q.den) : ℤ)
rw₂ : Rat.num (↑q : ℚ) / (↑(Rat.den (↑q : ℚ)) : ℤ) = (↑(q.num / q.den) : ℤ)
⊢ ⌊q⌋₊ = q.num / q.den
have rw₃ : Rat.num (↑q : ℚ) / (↑(Rat.den (↑q : ℚ)) : ℤ) = HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ)
Tactic: rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def', Int.natCast_ediv, den_coe, num_coe]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
q : ℚ≥0
rw : Eq (α := ℤ) (↑⌊q⌋₊ : ℤ) (↑(q.num / q.den) : ℤ)
rw₁ : Int.floor (α := ℚ) (↑q : ℚ) = (↑(q.num / q.den) : ℤ)
rw₂ : Rat.num (↑q : ℚ) / (↑(Rat.den (↑q : ℚ)) : ℤ) = (↑(q.num / q.den) : ℤ)
rw₃ : Rat.num (↑q : ℚ) / (↑(Rat.den (↑q : ℚ)) : ℤ) = HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ)
⊢ ⌊q⌋₊ = q.num / q.den
have rw₄ : Rat.num (↑q : ℚ) / (↑q.den : ℤ) = HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ)
Tactic: rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def', Int.natCast_ediv, den_coe, num_coe]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
q : ℚ≥0
rw : Eq (α := ℤ) (↑⌊q⌋₊ : ℤ) (↑(q.num / q.den) : ℤ)
rw₁ : Int.floor (α := ℚ) (↑q : ℚ) = (↑(q.num / q.den) : ℤ)
rw₂ : Rat.num (↑q : ℚ) / (↑(Rat.den (↑q : ℚ)) : ℤ) = (↑(q.num / q.den) : ℤ)
rw₃ : Rat.num (↑q : ℚ) / (↑(Rat.den (↑q : ℚ)) : ℤ) = HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ)
rw₄ : Rat.num (↑q : ℚ) / (↑q.den : ℤ) = HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ)
⊢ ⌊q⌋₊ = q.num / q.den
have rw₅ : HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ) = HDiv.hDiv (α := ℤ) (↑q.num : ℤ) (↑q.den : ℤ)
Tactic: rw [← Int.natCast_inj, NNRat.coe_floor, Rat.floor_def', Int.natCast_ediv, den_coe, num_coe]
-- Lean 4 proof step from Mathlib.Data.NNRat.Floor (goal)
Goal:
K : Type u_1
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
x : ℚ≥0
⊢ Nat.ceil.{u_1} (α := K) (↑x : K) = ⌈x⌉₊
have inl : Nat.ceil.{u_1} (α := K) (↑0 : K) = Nat.ceil (α := ℚ≥0) 0
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x