awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
zero : ∀ {a : α}, Membership.mem (γ := Multiset α) 0 a → ∃ (b : β), Membership.mem (γ := Multiset β) 0 b ∧ r a b
cons :
  ∀ {x : α} {y : β} {s : Multiset α} {t : Multiset β} (hxy : r x y),
    Rel r s t →
      ∀ (ih : ∀ {a : α}, a ∈ s → ∃ (b : β), b ∈ t ∧ r a b) {a : α}, a ∈ x ::ₘ s → ∃ (b : β), b ∈ y ::ₘ t ∧ r a b
⊢ ∀ {a : α}, a ∈ s → ∃ (b : β), b ∈ t ∧ r a b

Tactic:
induction h with
  | zero => simp
  | @cons x y s t hxy _ ih =>
    intro a ha
    rcases mem_cons.1 ha with ha | ha
    · exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩
    · rcases ih ha with ⟨b, hbt, hab⟩
      exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩

Premises used: Multiset.cons, Nat.zero
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
m1 m2 : Multiset α
r : α → α → Prop
h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b
hc : m1.card = m2.card
revert : ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) (hc : m1.card = m2.card), Rel r m1 m2
⊢ Rel r m1 m2

Tactic:
revert m1
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) (hc : m1.card = m2.card), Rel r m1 m2

Tactic:
@(m2.induction_on ?_ ?_)

Premises used: Multiset.induction_on
-- Module: Mathlib.Data.Multiset.ZeroCons
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
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)
⊢ ∀ {m1 : Multiset α} (h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b) (hc : m1.card = m2.card), Rel r m1 m2

Tactic:
refine @(m2.induction_on ?_ ?_)
-- Module: Mathlib.Data.Multiset.ZeroCons
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
refine_1₃ refine_1₄ : Eq (α := ℕ) 0 0
⊢ Rel r m 0

Tactic:
rw [rel_zero_right, ← card_eq_zero, hc, card_zero]

Premises used: Multiset.card_eq_zero, Multiset.card_zero, Multiset.rel_zero_right
-- Module: Mathlib.Data.Multiset.ZeroCons
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
⊢ m.card = t.card + 1

Tactic:
rw [card_cons] at hc

Premises used: Multiset.card_cons
-- Module: Mathlib.Data.Multiset.ZeroCons
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
refine_2 : ∀ (b : α) (hb : b ∈ m), Rel r m (a ::ₘ t)
⊢ 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 _)

Premises used: Eq.rec, Nat.succ_pos, Iff.mp, Multiset.card, Multiset.card_pos_iff_exists_mem, Eq.symm
-- Module: Mathlib.Data.Multiset.ZeroCons
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
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)
⊢ Rel r m (a ::ₘ t)

Tactic:
obtain ⟨m', rfl⟩ := exists_cons_of_mem hb

Premises used: Multiset.exists_cons_of_mem, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
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)

Tactic:
rel_cons_right.mpr ⟨b, m', h _ _ hb (mem_cons_self _ _), ih ?_ ?_, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Multiset.rel_cons_right, Multiset.mem_cons_self, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
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
refine_2₁ : m'.card = t.card
⊢ Rel r (b ::ₘ m') (a ::ₘ t)

Tactic:
refine rel_cons_right.mpr ⟨b, m', h _ _ hb (mem_cons_self _ _), ih ?_ ?_, rfl⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Multiset.rel_cons_right, Multiset.mem_cons_self, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
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'
⊢ ∀ (a b : α), a ∈ m' → b ∈ t → r a b

Tactic:
fun _ _ ha hb => h _ _ (mem_cons_of_mem ha) (mem_cons_of_mem hb)

Premises used: Multiset.mem_cons_of_mem
-- Module: Mathlib.Data.Multiset.ZeroCons
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'
⊢ ∀ (a b : α), a ∈ m' → b ∈ t → r a b

Tactic:
exact fun _ _ ha hb => h _ _ (mem_cons_of_mem ha) (mem_cons_of_mem hb)

Premises used: Multiset.mem_cons_of_mem
-- Module: Mathlib.Data.Multiset.ZeroCons
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'
⊢ m'.card = t.card

Tactic:
simpa using hc
-- Module: Mathlib.Data.Multiset.ZeroCons
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
empty₂ empty₃ : Eq.{u_1 + 1} (α := Multiset α) 0 0
⊢ Rel r s u

Tactic:
rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]

Premises used: Iff.mp, Multiset.rel_zero_right, Multiset.rel_zero_left
-- Module: Mathlib.Data.Multiset.ZeroCons
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
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
⊢ Rel r s u

Tactic:
obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1

Premises used: Iff.mp, Multiset.rel_cons_right, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
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)
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)
⊢ Rel r (a ::ₘ as) u

Tactic:
obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2

Premises used: Multiset.rel_cons_left, Iff.mp, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
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
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
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:
Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)

Premises used: trans, Multiset.Rel.cons
-- Module: Mathlib.Data.Multiset.ZeroCons
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
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
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:
exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)

Premises used: trans, Multiset.Rel.cons
-- Module: Mathlib.Data.Multiset.ZeroCons
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
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
⊢ 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)

Premises used: Multiset.rel_cons_left, Multiset.Rel.cons, Iff.mp, Multiset.rel_cons_right, Multiset.rel_zero_right, Multiset.rel_zero_left, rfl
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
r : α → α → Prop
⊢ Pairwise r 0

Tactic:
⟨[], rfl, List.Pairwise.nil⟩

Premises used: List.Pairwise.nil, And.intro, Exists.intro, Multiset.Pairwise, rfl, List.nil
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
⊢ Nodup.{u_1} (α := α) 0

Tactic:
Pairwise.nil

Premises used: Multiset.Nodup, List.Nodup, List.Pairwise.nil
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
a : α
s : Multiset α
⊢ (a ::ₘ s).Nodup ↔ ¬a ∈ s ∧ s.Nodup

Tactic:
Quot.induction_on s fun _ => List.nodup_cons

Premises used: Quot.induction_on
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
m : ¬a ∈ s
n : s.Nodup
⊢ (a ::ₘ s).Nodup

Tactic:
nodup_cons.2 ⟨m, n⟩

Premises used: Iff.mpr, Multiset.nodup_cons, And.intro
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
h : (a ::ₘ s).Nodup
⊢ s.Nodup

Tactic:
(nodup_cons.1 h).2

Premises used: Multiset.nodup_cons, And.right, Iff.mp
-- Module: Mathlib.Data.Multiset.ZeroCons
Goal:
α : Type u_1
s : Multiset α
a : α
h : (a ::ₘ s).Nodup
⊢ ¬a ∈ s

Tactic:
(nodup_cons.1 h).1

Premises used: Multiset.nodup_cons, And.left, Iff.mp
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : CharZero K
l : List ℚ≥0
⊢ Eq.{u_2 + 1} (α := K) (↑l.sum : K) (List.sum (List.map NNRat.cast l))

Tactic:
map_list_sum (castHom _) _

Premises used: map_list_sum, NNRat.castHom
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : CharZero K
l : List ℚ≥0
⊢ Eq.{u_2 + 1} (α := K) (↑l.prod : K) (List.prod (List.map NNRat.cast l))

Tactic:
map_list_prod (castHom _) _

Premises used: map_list_prod, NNRat.castHom
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
K : Type u_2
inst : DivisionSemiring K
inst_1 : CharZero K
s : Multiset ℚ≥0
⊢ Eq.{u_2 + 1} (α := K) (↑s.sum : K) (Multiset.sum (Multiset.map NNRat.cast s))

Tactic:
map_multiset_sum (castHom _) _

Premises used: map_multiset_sum, NNRat.castHom
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
α : Type u_1
K : Type u_2
inst : DivisionSemiring K
inst_1 : CharZero K
s : Finset α
f : α → ℚ≥0
⊢ Eq.{u_2 + 1} (α := K) (↑(∑ a ∈ s, f a) : K) (∑ a ∈ s, (↑(f a) : K))

Tactic:
map_sum (castHom _) _ _

Premises used: map_sum, NNRat.castHom
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
K : Type u_2
inst : Semifield K
inst_1 : CharZero K
s : Multiset ℚ≥0
⊢ Eq.{u_2 + 1} (α := K) (↑s.prod : K) (Multiset.prod (Multiset.map NNRat.cast s))

Tactic:
map_multiset_prod (castHom _) _

Premises used: NNRat.castHom, map_multiset_prod
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
α : Type u_1
K : Type u_2
inst : Semifield K
inst_1 : CharZero K
s : Finset α
f : α → ℚ≥0
⊢ Eq.{u_2 + 1} (α := K) (↑(∏ a ∈ s, f a) : K) (∏ a ∈ s, (↑(f a) : K))

Tactic:
map_prod (castHom _) _ _

Premises used: map_prod, NNRat.castHom
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
rw : Eq (α := ℚ) (∑ i ∈ s, f i) (∑ a ∈ s, (↑(f a).toNNRat : ℚ))
⊢ Rat.toNNRat (∑ a ∈ s, f a) = ∑ a ∈ s, (f a).toNNRat

Tactic:
rw [← coe_inj, cast_sum, Rat.coe_toNNRat _ (Finset.sum_nonneg hf)]

Premises used: NNRat.cast_sum, Finset.sum_nonneg, NNRat.coe_inj, Rat.coe_toNNRat
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
x : α
hxs : x ∈ s
rw rw₁ : f x = f x
⊢ f x = (↑(f x).toNNRat : ℚ)

Tactic:
rw [Rat.coe_toNNRat _ (hf x hxs)]

Premises used: Rat.coe_toNNRat
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ Eq (α := ℚ) (∑ i ∈ s, f i) (∑ a ∈ s, (↑(f a).toNNRat : ℚ))

Tactic:
exact Finset.sum_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
rw : Eq (α := ℚ) (∏ i ∈ s, f i) (∏ a ∈ s, (↑(f a).toNNRat : ℚ))
⊢ Rat.toNNRat (∏ a ∈ s, f a) = ∏ a ∈ s, (f a).toNNRat

Tactic:
rw [← coe_inj, cast_prod, Rat.coe_toNNRat _ (Finset.prod_nonneg hf)]

Premises used: NNRat.cast_prod, NNRat.coe_inj, Finset.prod_nonneg, Rat.coe_toNNRat
-- Module: Mathlib.Data.NNRat.BigOperators
Goal:
α : Type u_1
s : Finset α
f : α → ℚ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ Eq (α := ℚ) (∏ i ∈ s, f i) (∏ a ∈ s, (↑(f a).toNNRat : ℚ))

Tactic:
exact Finset.prod_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
r : ℚ
hr : 0 ≤ r
p q : ℚ
hpq : p ≤ q
⊢ r * p ≤ r * q

Tactic:
simpa [mul_sub, sub_nonneg] using Rat.mul_nonneg hr (sub_nonneg.2 hpq)

Premises used: Iff.mpr, mul_sub, Rat.mul_nonneg, sub_nonneg
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
⊢ Ne (α := ℚ≥0) 1 0

Tactic:
decide
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ (↑q : ℚ) = (↑q : ℚ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
a b : ℕ
hab : Eq (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)
⊢ a = b

Tactic:
simpa using congr_arg num hab

Premises used: NNRat.num, congr_arg
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
⊢ Eq (α := ℚ) (↑p : ℚ) (↑q : ℚ) → p = q

Tactic:
Subtype.ext

Premises used: NNRat, Subtype.ext
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ Injective (β := ℚ) NNRat.cast

Tactic:
Subtype.coe_injective

Premises used: NNRat, Subtype.coe_injective
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
⊢ Eq (α := ℚ) (↑p : ℚ) (↑q : ℚ) ↔ p = q

Tactic:
Subtype.coe_inj

Premises used: Subtype.coe_inj, NNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
x y : ℚ≥0
⊢ Ne (α := ℚ) (↑x : ℚ) (↑y : ℚ) ↔ x ≠ y

Tactic:
NNRat.coe_inj.not

Premises used: Iff.not, NNRat.coe_inj
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ
hq : 0 ≤ q
⊢ (↑(Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) q hq) : ℚ) = q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p : ℚ≥0 → Prop
⊢ (∀ (q : ℚ≥0), p q) ↔ ∀ (q : ℚ) (hq : 0 ≤ q), p (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) q hq)

Tactic:
Subtype.forall

Premises used: Subtype.forall, NNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p : ℚ≥0 → Prop
⊢ (∃ (q : ℚ≥0), p q) ↔ ∃ (q : ℚ), ∃ (hq : 0 ≤ q), p (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) q hq)

Tactic:
Subtype.exists

Premises used: Subtype.exists, NNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ
hq : 0 ≤ q
⊢ (↑q.toNNRat : ℚ) = q

Tactic:
max_eq_left hq

Premises used: max_eq_left, ite
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ
⊢ q ≤ (↑q.toNNRat : ℚ)

Tactic:
le_max_left _ _

Premises used: le_max_left, ite
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ LE.le (α := ℚ) 0 (↑q : ℚ)

Tactic:
q.2

Premises used: Subtype.property
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ Eq (α := ℚ) (↑0 : ℚ) 0

Tactic:
rfl

Premises used: Rat.ofInt, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ num 0 = 0

Tactic:
rfl

Premises used: NNRat.num, Int.natAbs, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ den 0 = 1

Tactic:
rfl

Premises used: NNRat.den, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ Eq (α := ℚ) (↑1 : ℚ) 1

Tactic:
rfl

Premises used: Rat.ofInt, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ num 1 = 1

Tactic:
rfl

Premises used: NNRat.num, Int.natAbs, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ den 1 = 1

Tactic:
rfl

Premises used: NNRat.den, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
⊢ (↑(p + q) : ℚ) = HAdd.hAdd (α := ℚ) (↑p : ℚ) (↑q : ℚ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
⊢ (↑(p * q) : ℚ) = HMul.hMul (α := ℚ) (↑p : ℚ) (↑q : ℚ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
n : ℕ
⊢ (↑(q ^ n) : ℚ) = HPow.hPow (α := ℚ) (↑q : ℚ) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
n : ℕ
⊢ (q ^ n).num = q.num ^ n

Tactic:
simp [num, Int.natAbs_pow]

Premises used: NNRat.num, Int.natAbs_pow
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
n : ℕ
⊢ (q ^ n).den = q.den ^ n

Tactic:
rfl

Premises used: NNRat.den, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
h : q ≤ p
rwa rwa₁ rwa₂ rwa₃ : (↑q : ℚ) ≤ (↑p : ℚ)
⊢ (↑q : ℚ) ≤ (↑p : ℚ) - 0

Tactic:
rwa [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : q = 0 ↔ q = 0
⊢ Eq (α := ℚ) (↑q : ℚ) 0 ↔ q = 0

Tactic:
norm_cast
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ Ne (α := ℚ) (↑q : ℚ) 0 ↔ q ≠ 0

Tactic:
coe_eq_zero.not

Premises used: NNRat.coe_eq_zero, Iff.not
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ Eq (α := { q : ℚ // 0 ≤ q }) (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) 0 ⋯) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
⊢ LE.le (α := ℚ) (↑p : ℚ) (↑q : ℚ) ↔ p ≤ q

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
⊢ LT.lt (α := ℚ) (↑p : ℚ) (↑q : ℚ) ↔ p < q

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ LT.lt (α := ℚ) 0 (↑q : ℚ) ↔ 0 < q

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ Monotone (β := ℚ) NNRat.cast

Tactic:
fun _ _ ↦ coe_le_coe.2

Premises used: Iff.mpr, Monotone, NNRat.coe_le_coe
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ Monotone toNNRat

Tactic:
fun _ _ h ↦ max_le_max h le_rfl

Premises used: le_rfl, Monotone, max_le_max
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ toNNRat (↑q : ℚ) = q

Tactic:
ext <| max_eq_left q.2

Premises used: max_eq_left, NNRat.ext, Subtype.property
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n : ℕ
simp : Eq (α := ℚ) (↑n : ℚ) (↑(↑n : ℚ≥0) : ℚ)
⊢ Eq (α := ℚ) (↑(toNNRat (↑n : ℚ)) : ℚ) (↑(↑n : ℚ≥0) : ℚ)

Tactic:
simp only [Nat.cast_nonneg', Rat.coe_toNNRat]

Premises used: Nat.cast_nonneg', Rat.coe_toNNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n : ℕ
⊢ Eq (α := ℚ) (↑n : ℚ) (↑(↑n : ℚ≥0) : ℚ)

Tactic:
rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n : ℕ
⊢ Eq (α := ℚ) (↑(↑n : ℚ≥0) : ℚ) (↑n : ℚ)

Tactic:
rfl

Premises used: Rat.ofInt, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
n : ℕ
⊢ Eq (α := ℚ≥0) (Subtype.mk (p := fun (q : ℚ) ↦ 0 ≤ q) (↑n : ℚ) ⋯) (↑n : ℚ≥0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ Eq (α := (a : ℚ≥0) → ℚ) (⇑coeHom : (a : ℚ≥0) → ℚ) NNRat.cast

Tactic:
rfl

Premises used: NNRat, rfl
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
n : ℕ
⊢ (↑(n • q) : ℚ) = HSMul.hSMul (β := ℚ) n (↑q : ℚ)

Tactic:
coeHom.toAddMonoidHom.map_nsmul _ _

Premises used: NNRat.coeHom, AddMonoidHom.map_nsmul, RingHom.toAddMonoidHom
-- Module: Mathlib.Data.NNRat.Defs
Goal:
s : Set ℚ≥0
⊢ BddAbove (α := ℚ) (NNRat.cast '' s) ↔ BddAbove s

Tactic:
⟨fun ⟨b, hb⟩ ↦
    ⟨toNNRat b, fun ⟨y, _⟩ hys ↦
      show y ≤ max b 0 from (hb <| Set.mem_image_of_mem _ hys).trans <| le_max_left _ _⟩,
    fun ⟨b, hb⟩ ↦ ⟨b, fun _ ⟨_, hx, Eq⟩ ↦ Eq ▸ hb hx⟩⟩

Premises used: _private.0.NNRat.bddAbove_coe.match_3, Eq.rec, _private.0.NNRat.bddAbove_coe.match_2, _private.0.NNRat.bddAbove_coe.match_1, LE.le, BddAbove, Set.mem_image_of_mem, Rat.toNNRat, Iff.intro, Exists.intro, Set.image, LE.le.trans, OfNat.ofNat, le_max_left, NNRat.cast, _private.0.NNRat.bddAbove_coe.match_4
-- Module: Mathlib.Data.NNRat.Defs
Goal:
s : Set ℚ≥0
⊢ BddBelow (α := ℚ) (NNRat.cast '' s)

Tactic:
⟨0, fun _ ⟨q, _, h⟩ ↦ h ▸ q.2⟩

Premises used: _private.0.NNRat.bddBelow_coe.match_1, Eq.rec, LE.le, Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat, Subtype.property
-- Module: Mathlib.Data.NNRat.Defs
Goal:
x y : ℚ≥0
⊢ Eq (α := ℚ) (↑(max x y) : ℚ) (max (↑x : ℚ) (↑y : ℚ))

Tactic:
coe_mono.map_max

Premises used: Monotone.map_max, NNRat.coe_mono
-- Module: Mathlib.Data.NNRat.Defs
Goal:
x y : ℚ≥0
⊢ Eq (α := ℚ) (↑(min x y) : ℚ) (min (↑x : ℚ) (↑y : ℚ))

Tactic:
coe_mono.map_min

Premises used: Monotone.map_min, NNRat.coe_mono
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ≥0
⊢ p - q = (HSub.hSub (α := ℚ) (↑p : ℚ) (↑q : ℚ)).toNNRat

Tactic:
rfl

Premises used: Rat.toNNRat, rfl, Nonneg.toNonneg
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ Eq (α := ℚ) |(↑q : ℚ)| (↑q : ℚ)

Tactic:
abs_of_nonneg q.2

Premises used: abs_of_nonneg, Subtype.property
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ≥0
⊢ q ≤ 0 ↔ q = 0

Tactic:
⟨fun h => le_antisymm h q.2, fun h => h.symm ▸ q.2⟩

Premises used: Eq.rec, le_antisymm, Iff.intro, Eq.symm, Subtype.property
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ toNNRat 0 = 0

Tactic:
rfl

Premises used: Rat.toNNRat, rfl, ite
-- Module: Mathlib.Data.NNRat.Defs
Goal:
⊢ toNNRat 1 = 1

Tactic:
rfl

Premises used: Rat.toNNRat, rfl, ite
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ
⊢ 0 < q.toNNRat ↔ 0 < q

Tactic:
simp [toNNRat, ← coe_lt_coe]

Premises used: NNRat.coe_lt_coe, Rat.toNNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
q : ℚ
⊢ q.toNNRat = 0 ↔ q ≤ 0

Tactic:
simpa [-toNNRat_pos] using (@toNNRat_pos q).not

Premises used: Iff.not, Rat.toNNRat_pos
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
hp : 0 ≤ p
⊢ q.toNNRat ≤ p.toNNRat ↔ q ≤ p

Tactic:
simp [← coe_le_coe, toNNRat, hp]

Premises used: NNRat.coe_le_coe, Rat.toNNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
⊢ q.toNNRat < p.toNNRat ↔ q < p ∧ 0 < p

Tactic:
simp [← coe_lt_coe, toNNRat]

Premises used: NNRat.coe_lt_coe, Rat.toNNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
h : 0 < p
⊢ q.toNNRat < p.toNNRat ↔ q < p

Tactic:
toNNRat_lt_toNNRat_iff'.trans (and_iff_left h)

Premises used: and_iff_left, Rat.toNNRat_lt_toNNRat_iff', Iff.trans
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
hq : 0 ≤ q
⊢ q.toNNRat < p.toNNRat ↔ q < p

Tactic:
toNNRat_lt_toNNRat_iff'.trans ⟨And.left, fun h ↦ ⟨h, hq.trans_lt h⟩⟩

Premises used: Rat.toNNRat_lt_toNNRat_iff', And.left, And.intro, Iff.intro, Iff.trans, LE.le.trans_lt
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
hq : 0 ≤ q
hp : 0 ≤ p
⊢ Eq (α := ℚ) (↑(q + p).toNNRat : ℚ) (↑(q.toNNRat + p.toNNRat) : ℚ)

Tactic:
simp [toNNRat, hq, hp, add_nonneg]

Premises used: add_nonneg, Rat.toNNRat
-- Module: Mathlib.Data.NNRat.Defs
Goal:
p q : ℚ
⊢ (q + p).toNNRat ≤ q.toNNRat + p.toNNRat

Tactic:
coe_le_coe.1 <| max_le (add_le_add (le_max_left _ _) (le_max_left _ _)) <| coe_nonneg _

Premises used: add_le_add, NNRat.coe_le_coe, NNRat.coe_nonneg, max_le, Iff.mp, le_max_left