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

Goal state before:
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}

Tactic:
grind

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

Goal state before:
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:
grind

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

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : ∀ (hfi : (Set.ofPred p).Finite), 0 < #hfi.toFinset
⊢ f (sInf {i | p (f i)}) = sInf (Set.ofPred p)

Tactic:
replace h := nth_mem _ h

Goal state after:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
h : p (nth p 0)
⊢ f (sInf {i | p (f i)}) = sInf (Set.ofPred p)
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · rcases id ll with _ | lls
      · rcases lr with _ | ⟨_, _, lrx⟩
        · exact node 2 l x nil
        · exact node 3 (ι lx) lrx ι x
      · rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)
    · refine
        if delta * ls < rs then ?_ else if delta * rs < ls then ?_ else node (ls + rs + 1) l x r
      · rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact nil
        --should not happen
        rcases id rr with _ | rrs
        · exact nil
        --should not happen
        exact
          if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
          else
            node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx
              (node (size rlr + rrs + 1) rlr rx rr)
      · rcases id ll with _ | lls
        · exact nil
        --should not happen
        rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact nil
        --should not happen
        exact
          if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (lrs + rs + 1) lr x r)
          else
            node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
              (node (size lrr + rs + 1) lrr x r)

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

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

Tactic:
rfl

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

Goal state before:
pp: case pos
a✝ : PosNum
⊢ - -pos a✝ = pos a✝

Tactic:
rfl

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

Goal state before:
pp: case neg
a✝ : PosNum
⊢ - -neg a✝ = neg a✝

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case neg
a✝ : PosNum
⊢ a✝.pred'.toZNum = (-neg a✝).pred

Tactic:
rfl

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

Goal state before:
pp: a : PosNum
⊢ a.bit0.pred'.toZNumNeg = (neg a).bit1

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case mk
P : PFunctor.{uA, uB}
fst✝ : P.A
snd✝ : P.B fst✝ → P.W
⊢ (mk ⟨fst✝, snd✝⟩).dest = ⟨fst✝, snd✝⟩

Tactic:
rfl

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

Goal state before:
pp: case mk
P : PFunctor.{uA, uB}
a✝ : P.A
f✝ : P.B a✝ → WType P.B
⊢ mk (dest (WType.mk a✝ f✝)) = WType.mk a✝ f✝

Tactic:
rfl

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

Goal state before:
pp: case mk
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
f : α → β
fst✝ : P.A
snd✝ : P.B fst✝ → α
⊢ (P.map f ⟨fst✝, snd✝⟩).fst = ⟨fst✝, snd✝⟩.fst

Tactic:
rfl

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

Goal state before:
pp: case mk
P : PFunctor.{uA, uB}
α : Type v₁
β : Type v₂
inst✝² : DecidableEq P.A
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
i : P.Idx
fst✝ : P.A
snd✝ : P.B fst✝ → α
h : i.fst = ⟨fst✝, snd✝⟩.fst
⊢ (P.map f ⟨fst✝, snd✝⟩).snd (cast ⋯ i.snd) = f (⟨fst✝, snd✝⟩.snd (cast ⋯ i.snd))

Tactic:
rfl

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

Goal state before:
pp: case h
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
a : P.A
f : P.B a → α
xeq : x = ⟨a, f⟩
pf : ∀ (i : P.B a), p (f i)
⊢ Subtype.val <$> ⟨a, fun i ↦ ⟨f i, ⋯⟩⟩ = ⟨a, f⟩

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case pos
a✝ : PosNum
⊢ pos a✝ + 0 = pos a✝

Tactic:
rfl

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

Goal state before:
pp: case neg
a✝ : PosNum
⊢ neg a✝ + 0 = neg a✝

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case pos
a✝ : PosNum
⊢ 0 + pos a✝ = pos a✝

Tactic:
rfl

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

Goal state before:
pp: case neg
a✝ : PosNum
⊢ 0 + neg a✝ = neg a✝

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case h.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).1) <$> ⟨a, f⟩ = ⟨a, fun i ↦ (↑(f i)).1⟩

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: p : PosNum
⊢ (pos p).toZNumNeg = ZNum.neg p

Tactic:
rfl

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

Goal state before:
pp: ⊢ toZNum 0 = (0 + 1).toZNumNeg + 1

Tactic:
rfl

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

Goal state before:
pp: case h.right.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t ↦ (↑t).1) <$> u = x
yeq : (fun t ↦ (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t ↦ (↑t).2) <$> ⟨a, f⟩ = ⟨a, fun i ↦ (↑(f i)).2⟩

Tactic:
rfl

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:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case h.left
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).1) <$> ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = ⟨a, f₀⟩

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case h.right
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ (fun t ↦ (↑t).2) <$> ⟨a, fun i ↦ ⟨(f₀ i, f₁ i), ⋯⟩⟩ = ⟨a, f₁⟩

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rw [← cast_to_nat, ofZNum_toNat]

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

Goal state before:
pp: ⊢ Num.toZNum 0 = -Num.toZNum 0

Tactic:
rfl

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

Goal state before:
pp: ⊢ (Num.ofNat' 0).toZNum = 0

Tactic:
simp only [Num.ofNat'_zero, Num.toZNum]

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

Goal state before:
pp: a : PosNum
⊢ (Num.pos a).toZNum = pos a

Tactic:
rfl

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

Goal state before:
pp: a : PosNum
⊢ -(Num.pos a).toZNum = neg a

Tactic:
rfl

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

Goal state before:
pp: case mk
n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
fst✝ : (const n A).A
snd✝ : (const n A).B fst✝ ⟹ α
⊢ get (f <$$> ⟨fst✝, snd✝⟩) = get ⟨fst✝, snd✝⟩

Tactic:
rfl

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:
rfl

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:
rfl

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:
rfl

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

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
y : ↑P fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : P.A
f : P.B a ⟹ fun i ↦ Subtype p
h : y = ⟨a, f⟩
⊢ ⟨a, (fun i ↦ Subtype.val) ⊚ f⟩ = ⟨a, fun i j ↦ ↑(f i j)⟩

Tactic:
rfl

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

Goal state before:
pp: case h
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
a : P.A
f : P.B a ⟹ α
xeq : x = ⟨a, f⟩
pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ (fun i ↦ Subtype.val) <$$> ⟨a, fun i j ↦ ⟨f i j, ⋯⟩⟩ = ⟨a, f⟩

Tactic:
rfl

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
⊢ l.realSize + r.realSize + 1 = (node (l.realSize + r.realSize + 1) l x r).realSize

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
⊢ Num.toZNum 0 = 0

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
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:
rfl

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

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

Tactic:
Num.zneg_toZNumNeg,

Goal state after:
n : ℕ
⊢ (↑n).succ.toZNum = ↑(n + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : ℕ
⊢ (↑n).toZNum.succ = (↑n).succ

Tactic:
rfl

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

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

Tactic:
← Int.cast_natCast,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ℕ
⊢ ↑↑↑n = ↑n
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case h.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).1) <$$> ⟨a, f⟩ = ⟨a, fun i j ↦ (↑(f i j)).1⟩

Tactic:
rfl

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

Goal state before:
pp: case h.right.left
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
r : ⦃i : Fin2 n⦄ → α i → α i → Prop
x y : ↑P α
u : ↑P fun i ↦ { p // r p.1 p.2 }
xeq : (fun i t ↦ (↑t).1) <$$> u = x
yeq : (fun i t ↦ (↑t).2) <$$> u = y
a : P.A
f : P.B a ⟹ fun i ↦ { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun i t ↦ (↑t).2) <$$> ⟨a, f⟩ = ⟨a, fun i j ↦ (↑(f i j)).2⟩

Tactic:
rfl

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

Goal state before:
pp: case intro
F : PFunctor.{uA, uB}
n : ℕ
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F n
⊢ CofixA.intro a✝¹ a✝ = CofixA.intro (head' (CofixA.intro a✝¹ a✝)) (children' (CofixA.intro a✝¹ a✝))

Tactic:
rfl

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

Goal state before:
pp: case zero.continue.intro
F : PFunctor.{uA, uB}
a✝¹ : F.A
a✝ : F.B a✝¹ → CofixA F 0
h : Agree CofixA.continue (CofixA.intro a✝¹ a✝)
⊢ truncate (CofixA.intro a✝¹ a✝) = CofixA.continue

Tactic:
rfl

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

Goal state before:
pp: case continue.continue
F : PFunctor.{uA, uB}
X : Type w
f : X → ↑F X
⊢ «continue» = «continue»

Tactic:
rfl

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

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

Tactic:
grind

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

Goal state before:
pp: case nil.nil
α : Type u_1
x : α
⊢ (casesOn (id nil)
        (casesOn (id nil) (Ordnode.singleton x) fun ls ll lx lr ↦
          casesOn (id ll)
            (casesOn lr (node 2 nil x nil) fun size l lrx r ↦ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x))
            fun lls l x_1 r ↦
            casesOn (id lr) (node 3 ll lx (Ordnode.singleton x)) fun lrs lrl lrx lrr ↦
              if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
              else node (ls + 1) (node (lls + lrl.size + 1) ll lx lrl) lrx (node (lrr.size + 1) lrr x nil))
        fun rs l x_1 r ↦
        casesOn (id nil) (node (rs + 1) nil x nil) fun ls ll lx lr ↦
          if ls > delta * rs then
            casesOn (id ll) nil fun lls l x_2 r ↦
              casesOn (id lr) nil fun lrs lrl lrx lrr ↦
                if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (rs + lrs + 1) lr x nil)
                else node (ls + rs + 1) (node (lls + lrl.size + 1) ll lx lrl) lrx (node (lrr.size + rs + 1) lrr x nil)
          else node (ls + rs + 1) nil x nil).dual =
    casesOn (id nil.dual)
      (casesOn (id nil.dual) (Ordnode.singleton x) fun rs rl rx rr ↦
        casesOn (id rr)
          (casesOn rl (node 2 nil x nil.dual) fun size l rlx r ↦
            node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun rrs l x_1 r ↦
          casesOn (id rl) (node 3 (Ordnode.singleton x) rx rr) fun rls rll rlx rlr ↦
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else node (rs + 1) (node (rll.size + 1) nil x rll) rlx (node (rlr.size + rrs + 1) rlr rx rr))
      fun ls l x_1 r ↦
      casesOn (id nil.dual) (node (ls + 1) nil.dual x nil) fun rs rl rx rr ↦
        if rs > delta * ls then
          casesOn (id rr) nil fun rrs l x_2 r ↦
            casesOn (id rl) nil fun rls rll rlx rlr ↦
              if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) nil.dual x rl) rx rr
              else
                node (ls + rs + 1) (node (ls + rll.size + 1) nil.dual x rll) rlx (node (rlr.size + rrs + 1) rlr rx rr)
        else node (ls + rs + 1) nil.dual x nil.dual

Tactic:
rfl

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

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

Tactic:
← IH.1

Goal state after:
case bit0.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * (↑r + ↑d * ↑q) = 2 * (↑r + ↑d * ↑q)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case zero
⊢ zero.div 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case zero
⊢ zero.mod 0 = zero

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ (↑b % ↑(pos a)).gcd ↑(pos a) = (↑b % ↑a).gcd ↑a

Tactic:
rfl

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

Goal state before:
pp: case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) * 2 ≤ ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a)))

Tactic:
rw [mul_two, mul_add]

Goal state after:
case a
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : ↑(pos a) * (↑b % ↑(pos a) + ↑(pos a) * (↑b / ↑(pos a))) < 2 ^ n * 2
⊢ ↑(pos a) * (↑b % ↑(pos a)) + ↑(pos a) * (↑b % ↑(pos a)) ≤
    ↑(pos a) * (↑b % ↑(pos a)) + ↑(pos a) * (↑(pos a) * (↑b / ↑(pos a)))
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.inr
α : 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₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rcases Nat.eq_zero_or_pos (size r) with r0 | r0
    · rw [r0] at mr₂; cases not_le_of_gt Hm mr₂
    rw [hm.2.size_eq] at lr₁ lr₂ mr₁ mr₂
    by_cases mm : size ml + size mr ≤ 1
    · dsimp [delta, ratio] at lr₁ mr₁
      have r1 : r.size = 1 := by lia
      have l1 : l.size = 1 := by lia
      rw [r1, add_assoc] at lr₁
      rw [l1, r1]
      revert mm; cases size ml <;> cases size mr <;> intro mm
      · decide
      · rw [zero_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)
        decide
      · rcases mm with (_ | ⟨⟨⟩⟩); decide
      · rw [Nat.succ_add] at mm; rcases mm with (_ | ⟨⟨⟩⟩)
    rcases hm.3.1.resolve_left mm with ⟨mm₁, mm₂⟩
    rcases Nat.eq_zero_or_pos (size ml) with ml0 | ml0
    · rw [ml0, mul_zero, Nat.le_zero] at mm₂
      rw [ml0, mm₂] at mm; cases mm (by decide)
    have : 2 * size l ≤ size ml + size mr + 1 := by
      have := Nat.mul_le_mul_left ratio lr₁
      rw [mul_left_comm, mul_add] at this
      have := le_trans this (add_le_add_right mr₁ _)
      rw [← Nat.succ_mul] at this
      exact (mul_le_mul_iff_right₀ (by decide)).1 this
    refine ⟨Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩, Or.inr ⟨?_, ?_⟩⟩
    · refine (mul_le_mul_iff_right₀ (by decide)).1 (le_trans this ?_)
      rw [two_mul, Nat.succ_le_iff]
      refine add_lt_add_of_lt_of_le ?_ mm₂
      simpa using! mul_lt_mul_of_pos_right (by decide : 1 < 3) ml0
    · exact Nat.le_of_lt_succ (Valid'.node4L_lemma₁ lr₂ mr₂ mm₁)
    · exact Valid'.node4L_lemma₂ mr₂
    · exact Valid'.node4L_lemma₃ mr₁ mm₁
    · exact Valid'.node4L_lemma₄ lr₁ mr₂ mm₁
    · exact Valid'.node4L_lemma₅ lr₂ mr₁ mm₂

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

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

Tactic:
rfl

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

Goal state before:
pp: case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨?succ.f.a✝, ?succ.f.x⟩

Tactic:
rfl

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

Goal state before:
pp: case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ M.mk ⟨a✝, f✝⟩ = M.mk ⟨a✝, ?succ.f.y⟩

Tactic:
rfl

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

Goal state before:
pp: case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝ i) (f✝ i)

Tactic:
rfl

Goal state after:
case succ.f.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
a✝ : F.A
f✝ : F.B a✝ → F.M
⊢ ∀ (i : F.B a✝), Agree' n✝ (f✝ i) (f✝ i)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m n : Num
⊢ ↑n % ↑m = 0 ↔ ↑n % ↑m = ↑0

Tactic:
rfl

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

Goal state before:
pp: case pos
a✝ : PosNum
⊢ (pos a✝).div 0 = 0

Tactic:
rfl

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

Goal state before:
pp: case neg
a✝ : PosNum
⊢ (neg a✝).div 0 = 0

Tactic:
rfl

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

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑(↑(Num.pos n) % (↑d).natAbs) = ↑↑n % ↑d

Tactic:
rfl

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

Goal state before:
pp: case mp.succ.f.f.intro.a
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree (x.approx n✝) (y.approx (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ : F.B a✝ → F.M
n : ℕ
f✝ : F.B a✝ → F.M
hagree : ∀ (i : F.B a✝), Agree ((fun j ↦ (f✝¹ j).approx n✝) i) ((fun j ↦ (f✝ j).approx (n✝ + 1)) i)
⊢ M.mk ⟨a✝, f✝¹⟩ = M.mk ⟨?mp.succ.f.f.intro.a✝, ?mp.succ.f.f.intro.x⟩

Tactic:
rfl

Goal state after: