mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ η✝.app (bicompl t F G β✝ β'✝) (bitraverse (traverse f✝) (traverse f'✝) x✝) =
    bitraverse (traverse (η✝.app β✝ ∘ f✝)) (traverse (η✝.app β'✝ ∘ f'✝)) x✝

Tactic:
dsimp only [bicompl]

Goal state after:
case binaturality
t : Type u → Type u → Type u
inst✝⁹ : Bitraversable t
F G : Type u → Type u
inst✝⁸ : Traversable F
inst✝⁷ : Traversable G
inst✝⁶ : LawfulTraversable F
inst✝⁵ : LawfulTraversable G
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompl t F G α✝ α'✝
⊢ η✝.app (t (F β✝) (G β'✝)) (bitraverse (traverse f✝) (traverse f'✝) x✝) =
    bitraverse (traverse (η✝.app β✝ ∘ f✝)) (traverse (η✝.app β'✝ ∘ f'✝)) x✝
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: F : Type u → Type u
inst✝¹ : Applicative F
α' β' : Type u
f : α' → F β'
inst✝ : LawfulApplicative F
a : α'
as bs : List α'
⊢ traverse f (a :: as ++ bs) = (fun x1 x2 ↦ x1 ++ x2) <$> traverse f (a :: as) <*> traverse f bs

Tactic:
by simp [traverse_append as bs, functor_norm]; congr

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
⊢ prod.fst i (prod.mk i a b) = a

Tactic:
induction i with
  | fz => simp_all only [prod.fst, prod.mk]
  | fs _ i_ih => apply i_ih

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
⊢ prod.snd i (prod.mk i a b) = b

Tactic:
by
  induction i with
  | fz => simp_all [prod.snd, prod.mk]
  | fs _ i_ih => apply i_ih

Goal state after:
Module: Mathlib.Data.Fin.Init

Goal state before:
pp: n k : ℕ
h : k = 2 ^ n
a b c : Fin k
⊢ a ^^^ b ^^^ c = a ^^^ (b ^^^ c)

Tactic:
by
  grind [Fin.xor_val, Nat.xor_mod_two_pow, Nat.mod_mod]

Goal state after:
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: case cons
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ go f (hd :: tl) acc = acc.toListAppend (go f (hd :: tl) #[])

Tactic:
go,

Goal state after:
case cons
α : Type u_1
f : α → Option α
acc : Array α
hd : α
tl : List α
⊢ (match f hd with
    | some b => acc.toListAppend (b :: tl)
    | none => go f tl (acc.push hd)) =
    acc.toListAppend (go f (hd :: tl) #[])
Module: Mathlib.Data.List.Lookmap

Goal state before:
pp: α : Type u_1
f : α → Option α
a : α
l : List α
⊢ lookmap f (a :: l) =
    match f a with
    | none => a :: lookmap f l
    | some b => b :: l

Tactic:
by
  cases h : f a <;> simp_all

Goal state after:
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
p : l₁ ~ l₂
⊢ dlookup a l₁ = dlookup a l₂

Tactic:
by
  have nd₂ := (perm_nodupKeys p).mp nd₁
  ext b; simp only [← Option.mem_def, mem_dlookup_iff nd₁, mem_dlookup_iff nd₂, p.mem_iff]

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

Goal state before:
pp: case swap
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : CommApplicative F
α' β' : Type u
f : α' → F β'
a b : List α'
x y : α'
l : List α'
this : (fun a b l ↦ ↑(a :: b :: l)) <$> f y <*> f x = (fun a b l ↦ ↑(a :: b :: l)) <$> f x <*> f y
⊢ ofList <$> Traversable.traverse f (y :: x :: l) = ofList <$> Traversable.traverse f (x :: y :: l)

Tactic:
simp [Function.comp_def, this, functor_norm]

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ a ∈ (filter (fun x ↦ decide (x.snd ≠ 0)) l.entries).keys ↔ (lookup a l).getD 0 ≠ 0

Tactic:
List.mem_keys,

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : Zero M
l : AList fun _x ↦ M
a : α
⊢ (∃ b, ⟨a, b⟩ ∈ filter (fun x ↦ decide (x.snd ≠ 0)) l.entries) ↔ (lookup a l).getD 0 ≠ 0
Module: Mathlib.Data.Holor

Goal state before:
pp: case refine_1
α : Type
d : ℕ
ds : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x ∈ ∅, (f x).slice i hid = (∑ x ∈ ∅, f x).slice i hid

Tactic:
simp [slice_zero]

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ v ≡ x [ZMOD r] ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v

Tactic:
modEq_iff_dvd,

Goal state after:
a b r v x : ℤ
⊢ (a ≤ x ∧ x < b) ∧ r ∣ x - v ↔ (a - v ≤ x - v ∧ x - v < b - v) ∧ r ∣ x - v
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ v ≡ x [ZMOD r] ↔ (a - v < x - v ∧ x - v ≤ b - v) ∧ r ∣ x - v

Tactic:
modEq_iff_dvd,

Goal state after:
a b r v x : ℤ
⊢ (a < x ∧ x ≤ b) ∧ r ∣ x - v ↔ (a - v < x - v ∧ x - v ≤ b - v) ∧ r ∣ x - v
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case mpr
a b r v : ℕ
x : ℤ
⊢ (↑a < x ∧ x ≤ ↑b) ∧ x ≡ ↑v [ZMOD ↑r] → ∃ a_2, ((a < a_2 ∧ a_2 ≤ b) ∧ a_2 ≡ v [MOD r]) ∧ ↑a_2 = x

Tactic:
intro h; lift x to ℕ using (by lia); exact ⟨x, by simp_all [natCast_modEq_iff]⟩

Goal state after:
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r : ℕ
hr : 0 < r
v : ℕ
⊢ ↑(#({x ∈ Ico a b | x ≡ v [MOD r]})) = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0

Tactic:
← Ico_filter_modEq_cast _ _ ▸ card_map _,

Goal state after:
a b r : ℕ
hr : 0 < r
v : ℕ
⊢ ↑(#({x ∈ Ico ↑a ↑b | x ≡ ↑v [ZMOD ↑r]})) = max (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) 0
Module: Mathlib.Data.List.Map2

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

Tactic:
by
  rw [zipLeft, zipLeft']
  cases as with
  | nil => rfl
  | cons _ atl =>
    cases bs with
    | nil => rfl
    | cons _ btl =>
      rw [zipWithLeft, zipWithLeft', cons_inj_right]
      exact zipLeft_eq_zipLeft' atl btl

Goal state after:
Module: Mathlib.Data.List.SplitLengths

Goal state before:
pp: α : Type u_1
l : List α
sz : List ℕ
i : ℕ
⊢ take i (sz.splitLengths l) = (take i sz).splitLengths l

Tactic:
induction i generalizing sz l

Goal state after:
case zero
α : Type u_1
l : List α
sz : List ℕ
⊢ take 0 (sz.splitLengths l) = (take 0 sz).splitLengths l

case succ
α : Type u_1
n✝ : ℕ
a✝ : ∀ (l : List α) (sz : List ℕ), take n✝ (sz.splitLengths l) = (take n✝ sz).splitLengths l
l : List α
sz : List ℕ
⊢ take (n✝ + 1) (sz.splitLengths l) = (take (n✝ + 1) sz).splitLengths l
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
s : List α
h1 : t₁.length < t₂.length
⊢ Shortlex r (s ++ t₁) (s ++ t₂)

Tactic:
apply of_length_lt
    rw [List.length_append, List.length_append]
    lia

Goal state after:
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
l : List α
hn : l ≠ []
h : IsChain (fun x y ↦ r x y = true) l
⊢ splitBy r l = [l]

Tactic:
cases l with
  | nil => contradiction
  | cons a l => rw [splitBy, ← append_nil l, splitByLoop_append] <;> simp [h]

Goal state after:
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h.a
α : Type u_1
r : α → α → Bool
l m : List α
ha : ∀ (x : α), x ∈ l.getLast? → ∀ (y : α), y ∈ m.head? → r x y = false
hl : l ≠ []
hm : m ≠ []
x : List α
hx : x ∈ (splitBy r l).getLast?
y : List α
hy : y ∈ (splitBy r m).head?
⊢ l.getLast hl ∈ l.getLast?

Tactic:
exact getLast_mem_getLast? _

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
M N : Multiset α
⊢ M.OneStep N → M.IsDershowitzMannaLT N

Tactic:
by
  rintro ⟨X, Y, a, M_def, N_def, ys_lt_a⟩
  use X, Y, {a}, by simp, M_def, N_def
  · simpa

Goal state after:
Module: Mathlib.Data.NNRat.Floor

Goal state before:
pp: case right
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ x ≤ ↑⌈x⌉₊

Tactic:
exact Nat.le_ceil _

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

Goal state before:
pp: case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
j : ι
hj : j ∈ l
⊢ ¬s j = 0

Tactic:
exact hs j (List.mem_cons_of_mem _ hj)

Goal state after:
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ (b'.digits n).sum

Tactic:
← ofDigits_one

Goal state after:
b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ n ↔ b ∣ ofDigits 1 (b'.digits n)
Module: Mathlib.Data.Nat.Digits.Div

Goal state before:
pp: b b' : ℕ
h : b' % b = 1
n : ℕ
⊢ b ∣ ofDigits b' (b'.digits n) ↔ b ∣ ofDigits 1 (b'.digits n)

Tactic:
rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, ofDigits_mod, h]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a n : ℕ
⊢ n.floorRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun x1 x2 ↦ x1 ^ x2

Tactic:
by
  unfold floorRoot; split_ifs with h <;> simp [Finsupp.floorDiv_def, prod_mapRange_index pow_zero]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
⊢ (∑ x ∈ range (n % p + 1) ×ˢ range (n / p + 1),
      if k = x.1 + p * x.2 then 1 * ↑((n % p).choose x.1 * (n / p).choose x.2) else 0) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))

Tactic:
sum_congr rfl (fun a ha ↦ if_congr (h_iff a ha) rfl rfl),

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
h_iff : ∀ x ∈ range (n % p + 1) ×ˢ range (n / p + 1), k = x.1 + p * x.2 ↔ (k % p, k / p) = x
⊢ (∑ a ∈ range (n % p + 1) ×ˢ range (n / p + 1),
      if (k % p, k / p) = a then 1 * ↑((n % p).choose a.1 * (n / p).choose a.2) else 0) =
    (Int.castRingHom (ZMod p)) ↑((n % p).choose (k % p) * (n / p).choose (k / p))
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: case inr
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib

Tactic:
rw [zeckendorf_of_pos h, cons_append, head?_cons, Option.mem_some_iff] at ha

Goal state after:
case inr
n a : ℕ
ha : (n + 1 - fib (n + 1).greatestFib).greatestFib = a
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: case zero
k a b p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑((p ^ 0 * a).choose (p ^ 0 * b)) ≡ ↑(a.choose b) [ZMOD ↑p]

Tactic:
simp [Int.ModEq.refl]

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

Goal state before:
pp: p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ nth p n = (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩

Tactic:
nth_eq_getD_sort hf,

Goal state after:
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).getD n 0 = (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case pos
p : ℕ → Prop
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
exact (isLeast_nth hn).csInf_eq.symm

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

Goal state before:
pp: case node.node.refine_1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
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)

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

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

Tactic:
rw [sub'_one, Num.cast_toZNum, ← Num.cast_to_nat, pred'_to_nat, ← Nat.sub_one]
    simp

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

Goal state before:
pp: p : PosNum
⊢ p.pred'.succ.toZNum = ZNum.pos p

Tactic:
Num.succ,

Goal state after:
p : PosNum
⊢ (pos p.pred'.succ').toZNum = ZNum.pos p
Module: Mathlib.Data.Num.ZNum

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

Tactic:
← of_nat_toZNum,

Goal state after:
n : ℕ
⊢ (↑n).toZNumNeg = -(↑n).toZNum
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 : ratio * (delta * l.size) ≤ ratio * (ml.size + mr.size + 1 + r.size)
⊢ 2 * l.size ≤ ml.size + mr.size + 1

Tactic:
rw [mul_left_comm, mul_add] at this

Goal state after:
α : 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
⊢ 2 * l.size ≤ ml.size + mr.size + 1
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
⊢ ↑r.bit0 + ↑d * (↑q + ↑q) = ↑n.bit0

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

Tactic:
· simp only [Num.cast_bit0, cast_bit0]
      rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]

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

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

Tactic:
· exact PosNum.cast_pos _

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
β : Type u
g : β → ↑P (α ::: β)
x : β
⊢ dest P (corec P g x) = (TypeVec.id ::: corec P g) <$$> g x

Tactic:
by
  trans
  · apply M.dest_corec'
  obtain ⟨a, f⟩ := g x; dsimp
  rw [MvPFunctor.map_eq]; congr
  conv_rhs => rw [← split_dropFun_lastFun f, appendFun_comp_splitFun]
  rfl

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

Goal state before:
pp: case pos.inr
α : 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_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
rr0 : rr.size > 0
l0 : l.size > 0
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
⊢ BalancedSz l.size rl.size ∧ BalancedSz (l.size + rl.size + 1) rr.size

Tactic:
rcases hr.3.1.resolve_left (hlp l0) with ⟨_, hb₂⟩

Goal state after:
case pos.inr
α : 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_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
rr0 : rr.size > 0
l0 : l.size > 0
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
left✝ : rl.size ≤ delta * rr.size
hb₂ : rr.size ≤ delta * rl.size
⊢ BalancedSz l.size rl.size ∧ BalancedSz (l.size + rl.size + 1) rr.size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node3L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
by
  simp [node3L, all_node', and_assoc]

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

Goal state before:
pp: case e_a
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = lastFun (dropFun g ::: fun x ↦ dropFun g <$$> x)

Tactic:
simp only [lastFun_appendFun]

Goal state after:
case e_a
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ lastFun g = fun x ↦ dropFun g <$$> x
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case a
m n : ℕ+
⊢ (m.gcd n).factorMultiset ≤ m.factorMultiset ⊓ n.factorMultiset

pp: case a
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset

Tactic:
· apply le_inf_iff.mpr; constructor <;> apply factorMultiset_le_iff.mpr
    · exact gcd_dvd_left m n
    · exact gcd_dvd_right m n

Goal state after:
case a
m n : ℕ+
⊢ m.factorMultiset ⊓ n.factorMultiset ≤ (m.gcd n).factorMultiset
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ ⟨⊥, ⊥⟩ ≤ ⟨a, b⟩

Tactic:
by
    obtain rfl | ha := eq_bot_or_bot_lt a
    · exact Lex.right _ bot_le
    · exact Lex.left _ _ ha

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

Goal state before:
pp: u : XgcdType
hs : u.IsSpecial
⊢ u.finish.IsSpecial

Tactic:
dsimp [IsSpecial, finish] at hs ⊢
  rw [add_mul _ _ u.y, add_comm _ (u.x * u.y), ← hs]
  ring

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h

Goal state after:
case right
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h

Goal state after:
case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h

Goal state after:
case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
c : α i
ha : a < c
hb : c < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩
Module: Mathlib.Data.QPF.Multivariate.Constructions.Comp

Goal state before:
pp: n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst✝¹ : MvQPF F
inst✝ : (i : Fin2 n) → MvQPF (G i)
α✝ β✝ : TypeVec.{u} m
f✝ : α✝ ⟹ β✝
p✝ : ↑((P F).comp fun i ↦ P (G i)) α✝
⊢ Comp.mk ((fun x ↦ abs) <$$> abs (comp.get (f✝ <$$> p✝))) = f✝ <$$> Comp.mk ((fun x ↦ abs) <$$> abs (comp.get p✝))

Tactic:
rw [← abs_map]

Goal state after:
n m : ℕ
F : TypeVec.{u} n → Type u_1
G : Fin2 n → TypeVec.{u} m → Type u
α β : TypeVec.{u} m
f : α ⟹ β
inst✝¹ : MvQPF F
inst✝ : (i : Fin2 n) → MvQPF (G i)
α✝ β✝ : TypeVec.{u} m
f✝ : α✝ ⟹ β✝
p✝ : ↑((P F).comp fun i ↦ P (G i)) α✝
⊢ Comp.mk (abs ((fun x ↦ abs) <$$> comp.get (f✝ <$$> p✝))) = f✝ <$$> Comp.mk ((fun x ↦ abs) <$$> abs (comp.get p✝))
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
⊢ id <$> abs ⟨a, f⟩ = abs ⟨a, f⟩

Tactic:
rw [← abs_map]

Goal state after:
F : Type u → Type v
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
⊢ abs ((P F).map id ⟨a, f⟩) = abs ⟨a, f⟩
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case trans
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
x✝ y✝ x y z : (P F).W α
a✝¹ : WEquiv x y
a✝ : WEquiv y z
ih₁ : WEquiv (g <$$> x) (g <$$> y)
ih₂ : WEquiv (g <$$> y) (g <$$> z)
⊢ WEquiv (g <$$> x) (g <$$> z)

Tactic:
| trans x y z _ _ ih₁ ih₂ =>

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

Goal state before:
pp: case trans
F : Type u → Type v
q : QPF F
α : Type u
u : F α → α
x✝ y✝ x y z : (P F).W
a✝¹ : Wequiv x y
a✝ : Wequiv y z
ih₁ : recF u x = recF u y
ih₂ : recF u y = recF u z
⊢ recF u x = recF u z

Tactic:
| trans x y z _ _ ih₁ ih₂ =>

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

Goal state before:
pp: case trans
F : Type u → Type v
q : QPF F
x✝ y✝ x y z : (P F).W
a✝¹ : Wequiv x y
a✝ : Wequiv y z
ih₁ : Wequiv y x
ih₂ : Wequiv z y
⊢ Wequiv z x

Tactic:
| trans x y z _ _ ih₁ ih₂ =>

Goal state after: