mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = lt) = if c then a = lt else b = lt

Tactic:
by_cases c <;> simp [*]

Goal state after:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = eq) = if c then a = eq else b = eq

Tactic:
by_cases c <;> simp [*]

Goal state after:
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: c : Prop
inst✝ : Decidable c
a b : Ordering
⊢ ((if c then a else b) = gt) = if c then a = gt else b = gt

Tactic:
by_cases c <;> simp [*]

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

Goal state before:
pp: fuel : ℕ
n k : PosNum
h : (↑n).sqrt < fuel + ↑k.bit1
⊢ ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1

Tactic:
induction fuel generalizing k <;> rw [minFacAux, Nat.minFacAux]

Goal state after:
case zero
n k : PosNum
h : (↑n).sqrt < 0 + ↑k.bit1
⊢ ↑n = if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)

case succ
n : PosNum
n✝ : ℕ
a✝ : ∀ {k : PosNum}, (↑n).sqrt < n✝ + ↑k.bit1 → ↑(n.minFacAux n✝ k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < n✝ + 1 + ↑k.bit1
⊢ ↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux n✝ k.succ) =
    if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hm : Valid' (↑x) m ↑y
hr : Valid' (↑y) r o₂
Hm : 0 < m.size
H :
  l.size = 0 ∧ m.size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ m.size ∧
        delta * l.size ≤ m.size + r.size ∧ 3 * (m.size + r.size) ≤ 16 * l.size + 9 ∧ m.size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x m y r) o₂

Tactic:
obtain - | ⟨s, ml, z, mr⟩ := m

Goal state after:
case nil
α : 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₂
hm : Valid' (↑x) nil ↑y
Hm : 0 < nil.size
H :
  l.size = 0 ∧ nil.size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ nil.size ∧
        delta * l.size ≤ nil.size + r.size ∧ 3 * (nil.size + r.size) ≤ 16 * l.size + 9 ∧ nil.size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x nil y r) o₂

case node
α : 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
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x (Ordnode.node s ml z mr) y r) o₂
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:
cases x

Goal state after:
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
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).snd (cast ⋯ i.snd) = f (x.snd (cast ⋯ i.snd))

Tactic:
cases x

Goal state after:
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))
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)

Tactic:
intro h

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∃ 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)
Module: Mathlib.Data.PFunctor.Univariate.Basic

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

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

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

Tactic:
intro h

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

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

Tactic:
intro h

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

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

Tactic:
intro h

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

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

Tactic:
intro h

Goal state after:
case pos.mpr
p a✝ : PosNum
h : ZNum.pos p = (pos a✝).toZNum
⊢ pos p = pos 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

Tactic:
intro h

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

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

Goal state after:
case mpr
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
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:
cases x

Goal state after:
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✝⟩
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:
cases x

Goal state after:
case mk
n : ℕ
A : Type u
α : TypeVec.{u} n
fst✝ : (const n A).A
snd✝ : (const n A).B fst✝ ⟹ α
⊢ mk n (get ⟨fst✝, snd✝⟩) = ⟨fst✝, snd✝⟩
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
by decide

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 decide

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

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

Tactic:
rw [add_comm]; exact id

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

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

Tactic:
by decide

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

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

Tactic:
by decide

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

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

Tactic:
intro h

Goal state after:
α : Type u_1
a b c : ZNum
h : ↑a ≤ ↑b
⊢ ↑a + ↑c ≤ ↑b + ↑c
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₁
h : ¬l + r₂ ≤ 1
⊢ l ≤ delta * r₂

Tactic:
cases H with
  | inl H =>
    cases r₂
    · cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)
    · exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)
  | inr H =>
    exact le_trans H.1 (Nat.mul_le_mul_left _ h₁)

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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * 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 : ¬0 + 0 ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size = 0
ml0 : ml.size = 0
⊢ 0 + 0 ≤ 1

Tactic:
by decide

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

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

Tactic:
simp [balance', add_comm]

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else 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

Tactic:
intro h

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
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
⊢ ∃ y, f i y = x
Module: Mathlib.Data.PFunctor.Multivariate.Basic

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

Goal state after:
case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∃ y, f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * 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
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this✝ : delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + ratio * r.size
this : delta * (ratio * l.size) ≤ ratio.succ * (ml.size + mr.size + 1)
⊢ 0 < delta

Tactic:
by decide

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

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x : CofixA F (n + 1)
⊢ x = CofixA.intro (head' x) (children' x)

Tactic:
cases x

Goal state after:
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✝))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case zero
F : PFunctor.{uA, uB}
x : CofixA F 0
y : CofixA F (succ 0)
h : Agree x y
⊢ truncate y = x

Tactic:
cases x

Goal state after:
case zero.continue
F : PFunctor.{uA, uB}
y : CofixA F (succ 0)
h : Agree CofixA.continue y
⊢ truncate y = CofixA.continue
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

Goal state after:
case mk
F : PFunctor.{uA, uB}
y : F.M
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H : ∀ (i : ℕ), { approx := approx✝, consistent := consistent✝ }.approx i = y.approx i
⊢ { approx := approx✝, consistent := consistent✝ } = y
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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * 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
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ 0 < 2

Tactic:
by decide

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₁ : ratio * r.size ≤ ml.size + mr.size + 1
lr₁ : delta * 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
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this : 2 * l.size ≤ ml.size + mr.size + 1
⊢ 1 < 3

Tactic:
by decide

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

Goal state before:
pp: case mp
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree (x.approx n) (y.approx (n + 1)) → Agree' n x y

Tactic:
intro h

Goal state after:
case mp
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
h : Agree (x.approx n) (y.approx (n + 1))
⊢ Agree' n x y
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case mpr
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree' n x y → Agree (x.approx n) (y.approx (n + 1))

Tactic:
intro h

Goal state after:
case mpr
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
h : Agree' n x y
⊢ Agree (x.approx n) (y.approx (n + 1))
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
l0 : l.size > 0
hb : rl.size + rr.size ≤ 1
⊢ ¬delta * Nat.succ 0 ≤ 1

Tactic:
by decide

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

Goal state before:
pp: m n : ZNum
⊢ m ∣ n ↔ n % m = 0

Tactic:
rw [← dvd_to_int, Int.dvd_iff_emod_eq_zero, ← to_int_inj, mod_to_int]; rfl

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

Goal state before:
pp: case mpr.succ.step.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
y : F.M
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : y = M.mk ⟨a, y'⟩
x_a : F.A
x_f : F.B x_a → F.M
a✝ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))

Tactic:
induction y using PFunctor.M.casesOn' with | _ y_a y_f
       =>  _ 

Goal state after:
case mpr.succ.step.f.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) ((M.mk ⟨y_a, y_f⟩).approx (n✝ + 1 + 1))
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : rl.size < ratio * rr.size
⊢ 0 < ratio

Tactic:
by decide

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
h : ratio = 0 ∨ rr.size = 0
rl0 : rl.size = 0
⊢ ¬ratio = 0

Tactic:
by decide

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (0 + 0 + 1) ≤ 1
H2 : delta = 0 ∨ l.size = 0
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
rl0 : rl.size = 0
h : rr.size = 0
⊢ ¬delta = 0

Tactic:
by decide

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬0 + (0 + 0 + 1) ≤ 1
H2 : delta = 0 ∨ l.size = 0
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
rl0 : rl.size = 0
h : rr.size = 0
⊢ 0 + (0 + 0 + 1) ≤ 1

Tactic:
by decide

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx : P.B ax ⟹ α ::: P.M α
ay : P.A
fy : P.B ay ⟹ α ::: P.M α
⊢ (TypeVec.id ::: Quot.mk R) <$$> ⟨ax, fx⟩ = (TypeVec.id ::: Quot.mk R) <$$> ⟨ay, fy⟩ →
    ∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ay, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)

Tactic:
intro h

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx : P.B ax ⟹ α ::: P.M α
ay : P.A
fy : P.B ay ⟹ α ::: P.M α
h : (TypeVec.id ::: Quot.mk R) <$$> ⟨ax, fx⟩ = (TypeVec.id ::: Quot.mk R) <$$> ⟨ay, fy⟩
⊢ ∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ay, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
⊢ ∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ax, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)

Tactic:
have Hdrop : dropFun fx = dropFun fy := by
    replace h₁ := congr_arg dropFun h₁
    simpa using! h₁

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
h₁ : (TypeVec.id ::: Quot.mk R) ⊚ fx = (TypeVec.id ::: Quot.mk R) ⊚ fy
Hdrop : dropFun fx = dropFun fy
⊢ ∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ ⟨ax, fy⟩ = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ 1 ≤ 3

Tactic:
by decide

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : l.size = 0 → r.size ≤ 1
H₂ : 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size
H₃ : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
r0 : r.size > 0
l0 : l.size = 0
⊢ 2 * 1 ≤ 9 * 0 + 5

Tactic:
by decide

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk a f) i
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) i x = h i x

Tactic:
cases x

Goal state after:
case root
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
i : Fin2 n
c✝ : P.drop.B a i
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) i (WPath.root a f i c✝) = h i (WPath.root a f i c✝)

case child
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
a : P.A
f : P.last.B a → P.last.W
h : P.WPath (WType.mk a f) ⟹ α
i : Fin2 n
j✝ : P.last.B a
c✝ : P.WPath (f j✝) i
⊢ P.wPathCasesOn (P.wPathDestLeft h) (P.wPathDestRight h) i (WPath.child a f i j✝ c✝) = h i (WPath.child a f i j✝ c✝)
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
x : P.WPath (WType.mk a f) i
⊢ (h ⊚ P.wPathCasesOn g' g) i x = P.wPathCasesOn (h ⊚ g') (fun i ↦ h ⊚ g i) i x

Tactic:
cases x

Goal state after:
case root
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
c✝ : P.drop.B a i
⊢ (h ⊚ P.wPathCasesOn g' g) i (WPath.root a f i c✝) = P.wPathCasesOn (h ⊚ g') (fun i ↦ h ⊚ g i) i (WPath.root a f i c✝)

case child
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u_1} n
β : TypeVec.{u_2} n
h : α ⟹ β
a : P.A
f : P.last.B a → P.last.W
g' : P.drop.B a ⟹ α
g : (j : P.last.B a) → P.WPath (f j) ⟹ α
i : Fin2 n
j✝ : P.last.B a
c✝ : P.WPath (f j✝) i
⊢ (h ⊚ P.wPathCasesOn g' g) i (WPath.child a f i j✝ c✝) =
    P.wPathCasesOn (h ⊚ g') (fun i ↦ h ⊚ g i) i (WPath.child a f i j✝ c✝)
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
⊢ MvFunctor P.W

Tactic:
delta MvPFunctor.W; infer_instance

Goal state after:
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case mp
m n : ℕ+
⊢ m.factorMultiset ≤ n.factorMultiset → m ∣ n

Tactic:
intro h

Goal state after:
case mp
m n : ℕ+
h : m.factorMultiset ≤ n.factorMultiset
⊢ m ∣ n