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

Goal state before:
pp: case succ.refine_2.ha
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ n ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

pp: case succ.refine_2.hb
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

pp: case succ.refine_2.h
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ f n < f m

Tactic:
<;>

Goal state after:
case succ.refine_2.ha
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ n ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

case succ.refine_2.hb
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}

case succ.refine_2.h
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ f n < f m
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ - -zero = zero

pp: case pos
a✝ : PosNum
⊢ - -pos a✝ = pos a✝

pp: case neg
a✝ : PosNum
⊢ - -neg a✝ = neg a✝

Tactic:
<;>

Goal state after:
case zero
⊢ - -zero = zero

case pos
a✝ : PosNum
⊢ - -pos a✝ = pos a✝

case neg
a✝ : PosNum
⊢ - -neg a✝ = neg a✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ -zero.bit1 = (-zero).bitm1

pp: case pos
a✝ : PosNum
⊢ -(pos a✝).bit1 = (-pos a✝).bitm1

pp: case neg
a✝ : PosNum
⊢ -(neg a✝).bit1 = (-neg a✝).bitm1

Tactic:
<;>

Goal state after:
case zero
⊢ -zero.bit1 = (-zero).bitm1

case pos
a✝ : PosNum
⊢ -(pos a✝).bit1 = (-pos a✝).bitm1

case neg
a✝ : PosNum
⊢ -(neg a✝).bit1 = (-neg a✝).bitm1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ -zero.bitm1 = (-zero).bit1

pp: case pos
a✝ : PosNum
⊢ -(pos a✝).bitm1 = (-pos a✝).bit1

pp: case neg
a✝ : PosNum
⊢ -(neg a✝).bitm1 = (-neg a✝).bit1

Tactic:
<;>

Goal state after:
case zero
⊢ -zero.bitm1 = (-zero).bit1

case pos
a✝ : PosNum
⊢ -(pos a✝).bitm1 = (-pos a✝).bit1

case neg
a✝ : PosNum
⊢ -(neg a✝).bitm1 = (-neg a✝).bit1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ -zero.succ = (-zero).pred

pp: case pos
a✝ : PosNum
⊢ -(pos a✝).succ = (-pos a✝).pred

pp: case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred

Tactic:
<;>

Goal state after:
case zero
⊢ -zero.succ = (-zero).pred

case pos
a✝ : PosNum
⊢ -(pos a✝).succ = (-pos a✝).pred

case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1

pp: case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1

case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)) → ∀ (i : P.B a), p (f i)

pp: case mpr
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∀ (i : P.B a), p (f i)) → ∃ a_2 f_1, ⟨a, f⟩ = ⟨a_2, f_1⟩ ∧ ∀ (i : P.B a_2), p (f_1 i)

Tactic:
<;>

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)) → ∀ (i : P.B a), p (f i)

case mpr
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∀ (i : P.B a), p (f i)) → ∃ a_2 f_1, ⟨a, f⟩ = ⟨a_2, f_1⟩ ∧ ∀ (i : P.B a_2), p (f_1 i)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ zero + 0 = zero

pp: case pos
a✝ : PosNum
⊢ pos a✝ + 0 = pos a✝

pp: case neg
a✝ : PosNum
⊢ neg a✝ + 0 = neg a✝

Tactic:
<;>

Goal state after:
case zero
⊢ zero + 0 = zero

case pos
a✝ : PosNum
⊢ pos a✝ + 0 = pos a✝

case neg
a✝ : PosNum
⊢ neg a✝ + 0 = neg a✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ 0 + zero = zero

pp: case pos
a✝ : PosNum
⊢ 0 + pos a✝ = pos a✝

pp: case neg
a✝ : PosNum
⊢ 0 + neg a✝ = neg a✝

Tactic:
<;>

Goal state after:
case zero
⊢ 0 + zero = zero

case pos
a✝ : PosNum
⊢ 0 + pos a✝ = pos a✝

case neg
a✝ : PosNum
⊢ 0 + neg a✝ = neg a✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case one
⊢ neg one + 1 = (neg one).succ

pp: case bit1
a✝ : PosNum
⊢ neg a✝.bit1 + 1 = (neg a✝.bit1).succ

pp: case bit0
a✝ : PosNum
⊢ neg a✝.bit0 + 1 = (neg a✝.bit0).succ

Tactic:
<;>

Goal state after:
case one
⊢ neg one + 1 = (neg one).succ

case bit1
a✝ : PosNum
⊢ neg a✝.bit1 + 1 = (neg a✝.bit1).succ

case bit0
a✝ : PosNum
⊢ neg a✝.bit0 + 1 = (neg a✝.bit0).succ
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.zero
α : 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 + 1)
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
r1 : r.size = 1
l1 : l.size = 1
⊢ 0 + mr.size ≤ 1 → BalancedSz 1 0 ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + 0 + 1) (mr.size + 1 + 1)

pp: case pos.succ
α : 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 + 1)
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
r1 : r.size = 1
l1 : l.size = 1
n✝ : ℕ
⊢ n✝ + 1 + mr.size ≤ 1 → BalancedSz 1 (n✝ + 1) ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + (n✝ + 1) + 1) (mr.size + 1 + 1)

Tactic:
<;>

Goal state after:
case pos.zero
α : 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 + 1)
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
r1 : r.size = 1
l1 : l.size = 1
⊢ 0 + mr.size ≤ 1 → BalancedSz 1 0 ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + 0 + 1) (mr.size + 1 + 1)

case pos.succ
α : 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 + 1)
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
r1 : r.size = 1
l1 : l.size = 1
n✝ : ℕ
⊢ n✝ + 1 + mr.size ≤ 1 → BalancedSz 1 (n✝ + 1) ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + (n✝ + 1) + 1) (mr.size + 1 + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
p : PosNum
⊢ pos p = zero ↔ ZNum.pos p = zero.toZNum

pp: case pos
p a✝ : PosNum
⊢ pos p = pos a✝ ↔ ZNum.pos p = (pos a✝).toZNum

Tactic:
<;>

Goal state after:
case zero
p : PosNum
⊢ pos p = zero ↔ ZNum.pos p = zero.toZNum

case pos
p a✝ : PosNum
⊢ pos p = pos a✝ ↔ ZNum.pos p = (pos a✝).toZNum
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero.mp
p : PosNum
⊢ pos p = zero → ZNum.pos p = zero.toZNum

pp: case zero.mpr
p : PosNum
⊢ ZNum.pos p = zero.toZNum → pos p = zero

pp: case pos.mp
p a✝ : PosNum
⊢ pos p = pos a✝ → ZNum.pos p = (pos a✝).toZNum

pp: case pos.mpr
p a✝ : PosNum
⊢ ZNum.pos p = (pos a✝).toZNum → pos p = pos a✝

Tactic:
<;>

Goal state after:
case zero.mp
p : PosNum
⊢ pos p = zero → ZNum.pos p = zero.toZNum

case zero.mpr
p : PosNum
⊢ ZNum.pos p = zero.toZNum → pos p = zero

case pos.mp
p a✝ : PosNum
⊢ pos p = pos a✝ → ZNum.pos p = (pos a✝).toZNum

case pos.mpr
p a✝ : PosNum
⊢ ZNum.pos p = (pos a✝).toZNum → pos p = pos a✝
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero.mp
p : PosNum
h : pos p = zero
⊢ ZNum.pos p = zero.toZNum

pp: case zero.mpr
p : PosNum
h : ZNum.pos p = zero.toZNum
⊢ pos p = zero

pp: case pos.mp
p a✝ : PosNum
h : pos p = pos a✝
⊢ ZNum.pos p = (pos a✝).toZNum

pp: case pos.mpr
p a✝ : PosNum
h : ZNum.pos p = (pos a✝).toZNum
⊢ pos p = pos a✝

Tactic:
<;>

Goal state after:
case zero.mp
p : PosNum
h : pos p = zero
⊢ ZNum.pos p = zero.toZNum

case zero.mpr
p : PosNum
h : ZNum.pos p = zero.toZNum
⊢ pos p = zero

case pos.mp
p a✝ : PosNum
h : pos p = pos a✝
⊢ ZNum.pos p = (pos a✝).toZNum

case pos.mpr
p a✝ : PosNum
h : ZNum.pos p = (pos a✝).toZNum
⊢ pos p = pos a✝
Module: Mathlib.Data.Num.ZNum

Goal state before:

Tactic:
<;>

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

Goal state before:
pp: case pos.mp.refl
p : PosNum
⊢ ZNum.pos p = (pos p).toZNum

Tactic:
<;>

Goal state after:
case pos.mp.refl
p : PosNum
⊢ ZNum.pos p = (pos p).toZNum
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case pos.mpr.refl
p : PosNum
⊢ pos p = pos p

Tactic:
<;>

Goal state after:
case pos.mpr.refl
p : PosNum
⊢ pos p = pos p
Module: Mathlib.Data.Num.ZNum

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

pp: case pos
p a✝ : PosNum
h : ZNum.neg p = (pos a✝).toZNum
⊢ pos a✝ ∈ ofZNum' (ZNum.neg p)

Tactic:
<;>

Goal state after:
case zero
p : PosNum
h : ZNum.neg p = zero.toZNum
⊢ zero ∈ ofZNum' (ZNum.neg p)

case pos
p a✝ : PosNum
h : ZNum.neg p = (pos a✝).toZNum
⊢ pos a✝ ∈ ofZNum' (ZNum.neg p)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ castNum <$> ofZNum' (ZNum.pos p) = (↑p).toNat?

Tactic:
rw [← PosNum.to_nat_to_int p]

Goal state after:
p : PosNum
⊢ castNum <$> ofZNum' (ZNum.pos p) = (↑↑p).toNat?
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: p : PosNum
⊢ ↑(ofZNum (ZNum.pos p)) = (↑p).toNat

Tactic:
rw [← PosNum.to_nat_to_int p]

Goal state after:
p : PosNum
⊢ ↑(ofZNum (ZNum.pos p)) = (↑↑p).toNat
Module: Mathlib.Data.Num.ZNum

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

pp: case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(0 + pos a✝) = ↑0 + ↑(pos a✝)

pp: case neg
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(0 + neg a✝) = ↑0 + ↑(neg a✝)

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑(0 + zero) = ↑0 + ↑zero

case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(0 + pos a✝) = ↑0 + ↑(pos a✝)

case neg
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(0 + neg a✝) = ↑0 + ↑(neg a✝)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x) → ∃ y, f y = x

pp: case mpr
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∃ y, f y = x) → ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x

Tactic:
<;>

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x) → ∃ y, f y = x

case mpr
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∃ y, f y = x) → ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
Module: Mathlib.Data.Num.ZNum

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

pp: case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(pos a✝ + 0) = ↑(pos a✝) + ↑0

pp: case neg
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(neg a✝ + 0) = ↑(neg a✝) + ↑0

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
⊢ ↑(zero + 0) = ↑zero + ↑0

case pos
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(pos a✝ + 0) = ↑(pos a✝) + ↑0

case neg
α : Type u_1
inst✝ : AddGroupWithOne α
a✝ : PosNum
⊢ ↑(neg a✝ + 0) = ↑(neg a✝) + ↑0
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ ↑(0 * zero) = ↑0 * ↑zero

pp: case pos
a✝ : PosNum
⊢ ↑(0 * pos a✝) = ↑0 * ↑(pos a✝)

pp: case neg
a✝ : PosNum
⊢ ↑(0 * neg a✝) = ↑0 * ↑(neg a✝)

Tactic:
<;>

Goal state after:
case zero
⊢ ↑(0 * zero) = ↑0 * ↑zero

case pos
a✝ : PosNum
⊢ ↑(0 * pos a✝) = ↑0 * ↑(pos a✝)

case neg
a✝ : PosNum
⊢ ↑(0 * neg a✝) = ↑0 * ↑(neg a✝)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ ↑(zero * 0) = ↑zero * ↑0

pp: case pos
a✝ : PosNum
⊢ ↑(pos a✝ * 0) = ↑(pos a✝) * ↑0

pp: case neg
a✝ : PosNum
⊢ ↑(neg a✝ * 0) = ↑(neg a✝) * ↑0

Tactic:
<;>

Goal state after:
case zero
⊢ ↑(zero * 0) = ↑zero * ↑0

case pos
a✝ : PosNum
⊢ ↑(pos a✝ * 0) = ↑(pos a✝) * ↑0

case neg
a✝ : PosNum
⊢ ↑(neg a✝ * 0) = ↑(neg a✝) * ↑0
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
⊢ nil.dual.size = nil.size

pp: case node
α : Type u_1
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (node size✝ l✝ x✝ r✝).dual.size = (node size✝ l✝ x✝ r✝).size

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
⊢ nil.dual.size = nil.size

case node
α : Type u_1
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (node size✝ l✝ x✝ r✝).dual.size = (node size✝ l✝ x✝ r✝).size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
⊢ (l.node4L x nil y r).dual = r.dual.node4R y nil.dual x l.dual

pp: case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.node4L x (node size✝ l✝ x✝ r✝) y r).dual = r.dual.node4R y (node size✝ l✝ x✝ r✝).dual x l.dual

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
⊢ (l.node4L x nil y r).dual = r.dual.node4R y nil.dual x l.dual

case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.node4L x (node size✝ l✝ x✝ r✝) y r).dual = r.dual.node4R y (node size✝ l✝ x✝ r✝).dual x l.dual
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
⊢ (l.node4R x nil y r).dual = r.dual.node4L y nil.dual x l.dual

pp: case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.node4R x (node size✝ l✝ x✝ r✝) y r).dual = r.dual.node4L y (node size✝ l✝ x✝ r✝).dual x l.dual

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
⊢ (l.node4R x nil y r).dual = r.dual.node4L y nil.dual x l.dual

case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.node4R x (node size✝ l✝ x✝ r✝) y r).dual = r.dual.node4L y (node size✝ l✝ x✝ r✝).dual x l.dual
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x : α
⊢ (l.rotateL x nil).dual = nil.dual.rotateR x l.dual

pp: case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).dual = (node size✝ l✝ x✝ r✝).dual.rotateR x l.dual

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : Ordnode α
x : α
⊢ (l.rotateL x nil).dual = nil.dual.rotateR x l.dual

case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).dual = (node size✝ l✝ x✝ r✝).dual.rotateR x l.dual
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h✝ : l✝.size < ratio * r✝.size
⊢ (l.node3L x l✝ x✝ r✝).dual = r✝.dual.node3R x✝ l✝.dual x l.dual

pp: case neg
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).dual = r✝.dual.node4R x✝ l✝.dual x l.dual

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h✝ : l✝.size < ratio * r✝.size
⊢ (l.node3L x l✝ x✝ r✝).dual = r✝.dual.node3R x✝ l✝.dual x l.dual

case neg
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
h✝ : ¬l✝.size < ratio * r✝.size
⊢ (l.node4L x l✝ x✝ r✝).dual = r✝.dual.node4R x✝ l✝.dual x l.dual
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : l.size + r.size ≤ 1
⊢ (l.node' x r).dual = r.dual.node' x l.dual

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : delta * r.size < l.size
⊢ (l.rotateL x r).dual = r.dual.rotateL x l.dual

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : ¬delta * r.size < l.size
⊢ (l.rotateL x r).dual = r.dual.rotateR x l.dual

pp: case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : ¬delta * l.size < r.size
h✝ : delta * r.size < l.size
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual

pp: case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : ¬delta * l.size < r.size
h✝ : ¬delta * r.size < l.size
⊢ (l.node' x r).dual = r.dual.node' x l.dual

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : l.size + r.size ≤ 1
⊢ (l.node' x r).dual = r.dual.node' x l.dual

case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : delta * r.size < l.size
⊢ (l.rotateL x r).dual = r.dual.rotateL x l.dual

case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : ¬delta * r.size < l.size
⊢ (l.rotateL x r).dual = r.dual.rotateR x l.dual

case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : ¬delta * l.size < r.size
h✝ : delta * r.size < l.size
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual

case neg
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : ¬delta * l.size < r.size
h✝ : ¬delta * r.size < l.size
⊢ (l.node' x r).dual = r.dual.node' x l.dual
Module: Mathlib.Data.PFunctor.Multivariate.Basic

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

pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
⊢ (∃ y, f i y = x) → ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x

Tactic:
<;>

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
⊢ (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x) → ∃ y, f i y = x

case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
⊢ (∃ y, f i y = x) → ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : CofixA F n) (y : CofixA F n.succ), Agree x y → truncate y = x
x : CofixA F (n + 1)
y : CofixA F (n + 1).succ
h : Agree x y
⊢ truncate y = x

Tactic:
| succ n n_ih =>

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

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
X : Type w
f : X → ↑F X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)
i : X
⊢ Agree (sCorec f i (n + 1)) (sCorec f i (n + 1).succ)

Tactic:
| succ n n_ih =>

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

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
n✝ m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
n_ih : head' (x n.succ) = head' (x 1)
⊢ head' (x (n + 1).succ) = head' (x 1)

Tactic:
| succ n n_ih =>

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

Goal state before:
pp: F : PFunctor.{uA, uB}
x y : F.M
H : ∀ (i : ℕ), x.approx i = y.approx i
⊢ x = y

Tactic:
cases x
  cases y
  congr with n
  apply H

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

Goal state before:
pp: case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit1 + ↑d * (↑q + ↑q) = ↑n.bit1

pp: case bit1.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit1 < 2 * ↑d

Tactic:
<;>

Goal state after:
case bit1.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit1 + ↑d * (↑q + ↑q) = ↑n.bit1

case bit1.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit1 < 2 * ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ hd = head' (x.approx 1)

Tactic:
← head_succ' n,

Goal state after:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ hd = head' (x.approx n.succ)

case Hconsistent
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ AllAgree x.approx
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
x : F.M
⊢ Agree' 0 x x

pp: case succ
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
x : F.M
⊢ Agree' (n✝ + 1) x x

Tactic:
<;>

Goal state after:
case zero
F : PFunctor.{uA, uB}
x : F.M
⊢ Agree' 0 x x

case succ
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
x : F.M
⊢ Agree' (n✝ + 1) x x