mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
bs : List β
⊢ as.zipRight bs = (as.zipRight' bs).fst

Tactic:
induction as generalizing bs <;> cases bs

Goal state after:
case nil.nil
α : Type u
β : Type v
⊢ [].zipRight [] = ([].zipRight' []).fst

case nil.cons
α : Type u
β : Type v
head✝ : β
tail✝ : List β
⊢ [].zipRight (head✝ :: tail✝) = ([].zipRight' (head✝ :: tail✝)).fst

case cons.nil
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (bs : List β), tail✝.zipRight bs = (tail✝.zipRight' bs).fst
⊢ (head✝ :: tail✝).zipRight [] = ((head✝ :: tail✝).zipRight' []).fst

case cons.cons
α : Type u
β : Type v
head✝¹ : α
tail✝¹ : List α
tail_ih✝ : ∀ (bs : List β), tail✝¹.zipRight bs = (tail✝¹.zipRight' bs).fst
head✝ : β
tail✝ : List β
⊢ (head✝¹ :: tail✝¹).zipRight (head✝ :: tail✝) = ((head✝¹ :: tail✝¹).zipRight' (head✝ :: tail✝)).fst
Module: Mathlib.Data.List.Lemmas

Goal state before:
pp: case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k ↦ (hd :: tl).insertIdx k x) (n✝¹ + 1) = (fun k ↦ (hd :: tl).insertIdx k x) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
simp only [insertIdx_succ_cons, cons.injEq, true_and] at h

Goal state after:
case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH :
  ¬x ∈ tl →
    ∀ ⦃n : ℕ⦄,
      n ∈ {n | n ≤ tl.length} →
        ∀ ⦃m : ℕ⦄, m ∈ {n | n ≤ tl.length} → (fun k ↦ tl.insertIdx k x) n = (fun k ↦ tl.insertIdx k x) m → n = m
hx : ¬x = hd ∧ ¬x ∈ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : tl.insertIdx n✝¹ x = tl.insertIdx n✝ x
⊢ n✝¹ + 1 = n✝ + 1
Module: Mathlib.Data.List.Sections

Goal state before:
pp: case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f tail✝
f : List α
h : ∃ a, a ∈ tail✝.sections ∧ ∃ a_1, a_1 ∈ head✝ ∧ a_1 :: a = f
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f (head✝ :: tail✝)

Tactic:
rcases h with ⟨_, _, _, _, rfl⟩

Goal state after:
case refine_1.cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ {f : List α}, f ∈ tail✝.sections → Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f tail✝
w✝¹ : List α
left✝¹ : w✝¹ ∈ tail✝.sections
w✝ : α
left✝ : w✝ ∈ head✝
⊢ Forall₂ (fun x1 x2 ↦ x1 ∈ x2) (w✝ :: w✝¹) (head✝ :: tail✝)
Module: Mathlib.Data.List.Sections

Goal state before:
pp: case refine_2.cons
α : Type u_1
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L
fs : f ∈ L.sections
⊢ a :: f ∈ (l :: L).sections

Tactic:
simp only [sections, mem_flatMap, mem_map]

Goal state after:
case refine_2.cons
α : Type u_1
L✝ : List (List α)
f✝ : List α
a : α
l f : List α
L : List (List α)
al : a ∈ l
fL : Forall₂ (fun x1 x2 ↦ x1 ∈ x2) f L
fs : f ∈ L.sections
⊢ ∃ a_1, a_1 ∈ L.sections ∧ ∃ a_2, a_2 ∈ l ∧ a_2 :: a_1 = a :: f
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case inr.inr.eq
α : Type u_1
w : List α
p q : ℕ
per_p : w.HasPeriod p
per_q : w.HasPeriod q
len : p + q - p.gcd q ≤ w.length
p_pos : p > 0
q_pos : q > 0
hyp : compare p q = Ordering.eq
⊢ w.HasPeriod (p.gcd q)

Tactic:
| eq =>

Goal state after:
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (Y + (X - {a}))

Tactic:
add_comm Y,

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : Preorder α
M : Multiset α
a : α
X Y : Multiset α
b : α
h0 : M + {a} = X + {b}
h2 : ∀ (y : α), y ∈ Y → y < b
hab : a ≠ b
⊢ X + Y = a ::ₘ (X - {a} + Y)
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case hf
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ FiniteMultiplicity p n

Tactic:
exact finiteMultiplicity_iff.mpr ⟨hp.out.ne_one, hn⟩

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

Goal state before:
pp: n k : ℕ
⊢ hyperoperation (n + 3) 1 k = 1

Tactic:
induction n generalizing k with

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

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

Tactic:
rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_notMem,
      ← count_eq_card_filter_range, ihk fun hf => lt_of_succ_lt (hn hf)]
    simp

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

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

Tactic:
PosNum.cast_add,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ -(↑a + ↑b) = -↑a + -↑b
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ ↑r = ↑r₂ + ↑(Num.pos d) ↔ ↑r = ↑r₂ + ↑d

Tactic:
← Int.natCast_inj

Goal state after:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ ↑r = ↑r₂ + ↑(Num.pos d) ↔ ↑↑r = ↑(↑r₂ + ↑d)
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
h : ∃ y, f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x

Tactic:
simp only [liftP_iff']
    cases h
    subst x
    tauto

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

Goal state before:
pp: case succ.intro
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
h' : hd = head' (x.approx 1)
⊢ (CofixA.intro (head' (x.approx 1)) fun i ↦ (x.children i).approx n) = CofixA.intro hd ch

Tactic:
revert ch

Goal state after:
case succ.intro
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 hd → CofixA F n),
    x.approx n.succ = CofixA.intro hd ch →
      (CofixA.intro (head' (x.approx 1)) fun i ↦ (x.children i).approx n) = CofixA.intro hd ch
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
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:
| succ _ n_ih =>

Goal state after:
case succ
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x : F.M), Agree' n✝ x x
x : F.M
⊢ Agree' (n✝ + 1) x x
Module: Mathlib.Data.PFunctor.Univariate.M

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

Tactic:
| succ _ n_ih =>

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

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

Tactic:
| succ _ n_ih =>

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

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.node4L x (node size✝ l✝ x✝ r✝) y r).Sized

Tactic:
exact (hl.node' hm.2.1).node' (hm.2.2.node' hr)

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 α
⊢ (TypeVec.id ::: Quot.mk R) <$$> ⟨ax, fx⟩ = (TypeVec.id ::: Quot.mk R) <$$> dest P y →
    ∃ a f f₁ f₂, ⟨ax, fx⟩ = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)

Tactic:
rcases M.dest P y with ⟨ay, fy⟩

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 α
⊢ (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.Ordmap.Invariants

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
hm : nil.Sized
⊢ l.size + 1 + r.size = l.size + r.size + 1

Tactic:
abel

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

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x y : α
r : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ ((match l with
          | nil => 0
          | node sz l x r => sz) +
          match l✝ with
          | nil => 0
          | node sz l x r => sz) +
        1 +
      (((match r✝ with
          | nil => 0
          | node sz l x r => sz) +
          match r with
          | nil => 0
          | node sz l x r => sz) +
        1) =
    ((match l with
          | nil => 0
          | node sz l x r => sz) +
          (((match l✝ with
              | nil => 0
              | node sz l x r => sz) +
              match r✝ with
              | nil => 0
              | node sz l x r => sz) +
            1) +
        match r with
        | nil => 0
        | node sz l x r => sz) +
      1

Tactic:
abel

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hm : r.Sized
⊢ (l.rotateL x r).size = l.size + r.size + 1

Tactic:
cases r <;> simp [Ordnode.rotateL]

Goal state after:
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).size = l.size + size✝ + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
h✝ : l✝.size < ratio * r✝.size
⊢ l.size + l✝.size + r✝.size + 1 = l.size + (l✝.size + r✝.size + 1)

Tactic:
abel

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

Goal state before:
pp: case neg
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : (node size✝ l✝ x✝ r✝).Sized
h✝ : ¬l✝.size < ratio * r✝.size
⊢ l.size + l✝.size + r✝.size + 1 = l.size + (l✝.size + r✝.size + 1)

Tactic:
abel

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

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableLE α
x : α
h : nil.Sized
h_mem : x ∈ nil
⊢ 0 < nil.size

Tactic:
{ contradiction }

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
⊢ Valid' o₁
      (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr))
      o₂ ∧
    (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
          ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
      ls + rs

Tactic:
obtain ⟨v, e⟩ := Valid'.eraseMax_aux hl

Goal state after:
case pos
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
⊢ Valid' o₁
      (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
        ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr))
      o₂ ∧
    (((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).1.balanceR
          ((Ordnode.node ?pos.s✝ ll lx lr).eraseMax, findMax' lx lr).2 (Ordnode.node rs rl rx rr)).size =
      ls + rs
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
h✝ : rls < ratio * rrs
⊢ rls + 1 + rrs = rls + rrs + 1

Tactic:
abel

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

Goal state before:
pp: case neg
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
h✝ : ¬rls < ratio * rrs
⊢ rll.size + 1 + (rlr.size + rrs + 1) = rll.size + rlr.size + 1 + rrs + 1

Tactic:
abel

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

Goal state before:
pp: case neg
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
h✝ : ¬rls < ratio * rrs
⊢ nil.node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

Tactic:
· simp [node4L, node', sr.2.1.1]; abel

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t ↑rx
e : t.size = ls + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
rw [hl.2.1] at e

Goal state after:
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
h✝ : lrs < ratio * lls
⊢ lls + (lrs + 1) = lls + lrs + 1

Tactic:
abel

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

Goal state before:
pp: case neg
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
h✝ : ¬lrs < ratio * lls
⊢ lls + lrl.size + 1 + (lrr.size + 1) = lls + (lrl.size + lrr.size + 1) + 1

Tactic:
abel

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
H₁ : t.size = 0 → rr.size ≤ 1
⊢ ll.size + lr.size + 1 + rl.size + rr.size + 1 = ll.size + lr.size + 1 + (rl.size + rr.size + 1)

Tactic:
abel

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

Goal state before:
pp: case pos
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h✝ : rls < ratio * rrs
⊢ ls + rls + 1 + rrs = ls + (rls + rrs + 1)

Tactic:
abel

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

Goal state before:
pp: case neg
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h✝ : ¬rls < ratio * rrs
⊢ ls + rll.size + 1 + (rlr.size + rrs + 1) = ls + (rll.size + rlr.size + 1 + rrs + 1)

Tactic:
abel

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

Goal state before:
pp: u : XgcdType
hr : u.r ≠ 0
⊢ sizeOf u.step < sizeOf u

Tactic:
change u.r - 1 < u.bp
  have h₀ : u.r - 1 + 1 = u.r := Nat.succ_pred_eq_of_pos (Nat.pos_of_ne_zero hr)
  have h₁ : u.r < u.bp + 1 := Nat.mod_lt (u.ap + 1) u.bp.succ_pos
  rw [← h₀] at h₁
  exact lt_of_succ_lt_succ h₁

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

Goal state before:
pp: case pos
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
h✝ : lrs < ratio * lls
⊢ lls + (lrs + rs + 1) = lls + lrs + 1 + rs

Tactic:
abel

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

Goal state before:
pp: case neg
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
h✝ : ¬lrs < ratio * lls
⊢ lls + lrl.size + 1 + (lrr.size + rs + 1) = lls + (lrl.size + lrr.size + 1) + 1 + rs

Tactic:
abel

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case refine_1
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀) ((P F).wMk a₁ f'₁ f₁)
⊢ ∀ (a : (P F).A) (f' : (P F).drop.B a ⟹ α) (f₀ f₁ : (P F).last.B a → (P F).W α),
    (∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)) →
      (∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)) → recF u ((P F).wMk a f' f₀) = recF u ((P F).wMk a f' f₁)

Tactic:
intro a f' f₀ f₁ _h ih

Goal state after:
case refine_1
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
a₀ : (P F).A
f'₀ : (P F).drop.B a₀ ⟹ α
f₀✝ : (P F).last.B a₀ → (P F).W α
a₁ : (P F).A
f'₁ : (P F).drop.B a₁ ⟹ α
f₁✝ : (P F).last.B a₁ → (P F).W α
h : WEquiv ((P F).wMk a₀ f'₀ f₀✝) ((P F).wMk a₁ f'₁ f₁✝)
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
_h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), recF u (f₀ x) = recF u (f₁ x)
⊢ recF u ((P F).wMk a f' f₀) = recF u ((P F).wMk a f' f₁)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ l', Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ r', Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
⊢ Raised
    (match Ordering.lt with
      | Ordering.lt => (erase x t_l).balanceR t_x t_r
      | Ordering.eq => t_l.glue t_r
      | Ordering.gt => t_l.balanceL t_x (erase x t_r)).size
    (t_l.size + t_r.size + 1)

Tactic:
rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable]
          repeat apply Raised.add_right
          exact t_l_size

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

Goal state before:
pp: F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
x✝ : F₂ (F₁ α)
a : (P F₂).A
f : (P F₂).B a → F₁ α
x : (P F₂).B a
b : (P F₁).A
g : (P F₁).B b → α
h' : repr (f x) = ⟨b, g⟩
⊢ abs ⟨b, fun y ↦ g y⟩ = f x

Tactic:
← h',

Goal state after:
F₂ : Type u → Type u
q₂ : QPF F₂
F₁ : Type u → Type u
q₁ : QPF F₁
α : Type u
x✝ : F₂ (F₁ α)
a : (P F₂).A
f : (P F₂).B a → F₁ α
x : (P F₂).B a
b : (P F₁).A
g : (P F₁).B b → α
h' : repr (f x) = ⟨b, g⟩
⊢ abs (repr (f x)) = f x
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case cons
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a ∈ c :: l
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a

Tactic:
simp only [List.mem_cons] at m

Goal state after:
case cons
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
m : pure a = c ∨ pure a ∈ l
⊢ ∃ a, parallel.aux2 (c :: l) = Sum.inl a