mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p (nth p 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
⊢ Valid' o₁ t o₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
⊢ {n ∈ range (nth p (k + 1)) | p n} ⊆ insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: a b c d : ℕ
lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9
mr₂ : b + c + 1 ≤ 3 * d
mm₁ : b ≤ 3 * c
⊢ b < 3 * a + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
k : ℕ
hlt : ∀ (hf : (Set.ofPred p).Finite), k + 1 < #hf.toFinset
⊢ {n ∈ range (nth p (k + 1)) | p n} = insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: b c d : ℕ
mr₂ : b + c + 1 ≤ 3 * d
⊢ c ≤ 3 * d

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: b c d : ℕ
mr₁ : 2 * d ≤ b + c + 1
mm₁ : b ≤ 3 * c
⊢ d ≤ 3 * c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: a b c d : ℕ
lr₁ : 3 * a ≤ b + c + 1 + d
mr₂ : b + c + 1 ≤ 3 * d
mm₁ : b ≤ 3 * c
⊢ a + b + 1 ≤ 3 * (c + d + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: a b c d : ℕ
lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9
mr₁ : 2 * d ≤ b + c + 1
mm₂ : c ≤ 3 * b
⊢ c + d + 1 ≤ 3 * (a + b + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ -n.succ = (-n).pred

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ -n.pred = (-n).succ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ count p (nth p n) = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑↑0 = ↑0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ count p (nth p n + 1) = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑↑(pos p) = ↑(pos p)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Infinite
n : ℕ
⊢ count p (nth p n + 1) = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n k : ℕ
h : k < count p n
⊢ nth p k < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
n : ℕ
⊢ count p n = 0 ↔ n ≤ nth p 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑↑(neg p) = ↑(neg p)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(pos p).bit0 = ↑(pos p) + ↑(pos p)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ nth p (count p n) = sInf {i | p i ∧ n ≤ i}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(neg p).bit0 = ↑(neg p) + ↑(neg p)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≤ n, p n'
⊢ nth p n = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑(ZNum.bit1 0) = ↑0 + ↑0 + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(pos p).bit1 = ↑(pos p) + ↑(pos p) + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ Set.ofPred p
hp : n' ∉ ↑(range n)
⊢ n' ≥ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
⊢ Set.ofPred p ⊆ ↑(range n)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
⊢ nth p n = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
p : ↑P P.W
⊢ (mk p).dest = p

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
p : P.W
⊢ mk p.dest = p

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
x : ↑P α
f : α → β
⊢ (P.map f x).fst = x.fst

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
inst✝² : DecidableEq P.A
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : ↑P α
f : α → β
i : P.Idx
h : i.fst = x.fst
⊢ (P.map f x).iget i = f (x.iget i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
⊢ Liftp p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
⊢ ↑(-↑a) = -1 + ↑(-↑a + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(neg p).bit1 = ↑(neg p) + ↑(neg p) + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑n.bitm1 = ↑n + ↑n - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ n + 0 = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ 0 + n = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ neg p + 1 = (neg p).succ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ ↑p.bit0 = ZNum.pos p.bit0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ ↑p.bit1 = ZNum.pos p.bit1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑(a.sub' 1) = ↑a - ↑1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑(sub' 1 b) = ↑1 - ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(↑a + -↑b + (↑a + -↑b)) = ↑a + ↑a + (-↑b + -↑b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit0.sub' b.bit0) = ↑a.bit0 - ↑b.bit0

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ Liftp p ⟨a, f⟩ ↔ ∀ (i : P.B a), p (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(-↑b + (↑a + (-↑b + -1))) = ↑(↑a + -1 + (-↑b + -↑b))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
⊢ r.size = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit0.sub' b.bit1) = ↑a.bit0 - ↑b.bit1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
⊢ l.size = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(-↑b + (↑a + (-↑b + 1))) = ↑(↑a + 1 + (-↑b + -↑b))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit1.sub' b.bit0) = ↑a.bit1 - ↑b.bit0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(-↑b + (↑a + -↑b)) = ↑a + (-↑b + -↑b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(a.bit1.sub' b.bit1) = ↑a.bit1 - ↑b.bit1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
⊢ ↑n = ↑n.pred' + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
⊢ ↑n = ↑↑n.pred' + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ (ZNum.pos p).pred.succ = ZNum.pos p

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ ZNum.ofInt' (↑n + 1) = ZNum.ofInt' ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ZNum.ofInt' (-[0+1] + 1) = ZNum.ofInt' -[0+1] + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ ZNum.ofInt' (-[n + 1+1] + 1) = ZNum.ofInt' -[n + 1+1] + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (↑(n + 1)).toZNum = ZNum.ofInt' ↑(n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m : Num
p : PosNum
⊢ pos p = m ↔ ZNum.pos p = m.toZNum

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m : Num
p : PosNum
h : ZNum.neg p = m.toZNum
⊢ m ∈ ofZNum' (ZNum.neg p)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ ↑(↑p.pred' + 1) = ↑p

Tactic:
rw [← succ'_to_nat]; simp

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ Liftr r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
n : ZNum
⊢ ↑(ofZNum n) = ↑(↑n).toNat

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : ZNum
⊢ ↑(0 + a) = ↑0 + ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
b : ZNum
⊢ ↑(b + 0) = ↑b + ↑0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(pos a + neg b) = ↑(pos a) + ↑(neg b)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑b + -↑a = -↑a + ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ ↑n.succ = ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : ZNum
⊢ ↑(0 * a) = ↑0 * ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: b : ZNum
⊢ ↑(b * 0) = ↑b * ↑0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocRing α
m n : ZNum
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
⊢ supp ⟨a, f⟩ = f '' univ

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ofInt' ↑0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : PosNum
⊢ ofInt' ↑(pos a) = pos a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a : PosNum
⊢ ofInt' ↑(neg a) = neg a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
x : ↑(const n A) α
⊢ get (f <$$> x) = get x

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
A : Type u
α : TypeVec.{u} n
x : ↑(const n A) α
⊢ mk n (get x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n m : ℕ
P : MvPFunctor.{u} n
Q : Fin2 n → MvPFunctor.{u} m
α β : TypeVec.{u} m
f : α ⟹ β
x : ↑(P.comp Q) α
⊢ get (f <$$> x) = (fun i x ↦ f <$$> x) <$$> get x

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n m : ℕ
P : MvPFunctor.{u} n
Q : Fin2 n → MvPFunctor.{u} m
α : TypeVec.{u} m
x : ↑P fun i ↦ ↑(Q i) α
⊢ get (mk x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n m : ℕ
P : MvPFunctor.{u} n
Q : Fin2 n → MvPFunctor.{u} m
α : TypeVec.{u} m
x : ↑(P.comp Q) α
⊢ mk (get x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
⊢ LiftP p x ↔ ∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a b : PosNum
⊢ Ordering.casesOn ((neg a).cmp (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
h : Ordering.casesOn Ordering.lt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.lt = Ordering.lt

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
h : Ordering.casesOn Ordering.eq (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.eq = Ordering.lt

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ 0 < delta

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
h : Ordering.casesOn Ordering.gt (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ ↑m < ↑n ↔ Ordering.gt = Ordering.lt

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ 1 ≤ delta * delta

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ a ≤ delta * (delta * a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ node s l x r = l.node' x r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m < ↑n ↔ m < n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
hl : t.Sized
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
⊢ C t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
m n : ZNum
⊢ ↑m = ↑n ↔ m = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), a ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), a ≤ b → b ≤ c → a ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a ≤ b → b ≤ a → a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ (node s l x r).size = (node s l x r).realSize

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a ≤ b ∨ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), a + b + c = a + (b + c)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), -a + a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a + b = b + a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
ht : t.Sized
⊢ t.size = 0 ↔ t = nil

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h : (node s l x r).Sized
⊢ 0 < s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ∀ (a b : ZNum), a * b = b * a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a b c : ZNum
⊢ a * b * c = a * (b * c)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), 1 * a = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), a * 1 = a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), 0 * a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ (node s l x r).dual.dual = node s l x r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a : ZNum), a * 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), a * (b + c) = a * b + a * c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.dual.size = t.size

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), (a + b) * c = a * c + b * c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ 0 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: l r : ℕ
⊢ l + r ≤ 1 → r + l ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ 0 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: l : ℕ
⊢ BalancedSz l 0 ↔ l ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a b : ZNum
h : a ≤ b
c : ZNum
⊢ a + c ≤ b + c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a b : ZNum
⊢ 0 < a → 0 < b → 0 < a * b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroupWithOne α
m n : ZNum
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: ⊢ ↑(-0) = -↑0

Tactic:
by

Goal state after:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
a : P.A
f : P.B a ⟹ α
⊢ LiftP p ⟨a, f⟩ ↔ ∀ (i : Fin2 n) (x : P.B a i), p (f i x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ ofInt' -[n+1] = ↑-[n+1]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ZNum
⊢ ↑↑n = n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℤ
⊢ ↑↑0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℤ
⊢ ∀ (k : ℤ), 0 ≤ k → ↑↑k = k → ↑↑(k + 1) = k + 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℤ
⊢ ∀ (k : ℤ), k ≤ 0 → ↑↑k = k → ↑↑(k - 1) = k - 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
H : BalancedSz l r₁
⊢ BalancedSz l r₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (↑n).toZNumNeg = -↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.dual.size l.dual.size

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.node' x r).dual = r.dual.node' x l.dual

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
x✝ : ↑m ∣ ↑n
k : ℤ
e : ↑n = ↑m * k
⊢ n = m * ↑k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3L x m y r).dual = r.dual.node3R y m.dual x l.dual

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : ZNum
x✝ : m ∣ n
k : ZNum
e : n = m * k
⊢ ↑n = ↑m * ↑k

Tactic:
by

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3R x m y r).dual = r.dual.node3L y m.dual x l.dual

Tactic:
by

Goal state after: