mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: case neg
κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : AddMonoid M
k : κ
f g : ι k →₀ M
k' : κ
i : ι k'
hk : ¬k' = k
⊢ (f + g).embSigma ⟨k', i⟩ = (f.embSigma + g.embSigma) ⟨k', i⟩

Tactic:
· simp [embSigma_apply_of_ne _ hk]

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)

Tactic:
rw [Nat.add_comm]

Goal state after:
α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: a b r v : ℤ
⊢ {x ∈ Ioc a b | x ≡ v [ZMOD r]} = map { toFun := fun x ↦ x + v, inj' := ⋯ } ({x ∈ Ioc (a - v) (b - v) | r ∣ x})

Tactic:
ext x
  simp_rw [mem_map, mem_filter, mem_Ioc, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
    exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]

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

Goal state before:
pp: a b r : ℤ
hr : 0 < r
x : ℤ
⊢ ((a ≤ x ∧ x < b) ∧ ∃ c, x = c * r) ↔
    ∃ a_1, (a ≤ a_1 * r ∧ a_1 * r < b) ∧ { toFun := fun x ↦ x * r, inj' := ⋯ } a_1 = x

Tactic:
aesop

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

Goal state before:
pp: a b r : ℤ
hr : 0 < r
x : ℤ
⊢ ((a < x ∧ x ≤ b) ∧ ∃ c, x = c * r) ↔
    ∃ a_1, (a < a_1 * r ∧ a_1 * r ≤ b) ∧ { toFun := fun x ↦ x * r, inj' := ⋯ } a_1 = x

Tactic:
aesop

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
⊢ map₂Left' f as [] = (map (fun a ↦ f a none) as, [])

Tactic:
cases as

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
⊢ map₂Left' f [] [] = (map (fun a ↦ f a none) [], [])

case cons
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : α
tail✝ : List α
⊢ map₂Left' f (head✝ :: tail✝) [] = (map (fun a ↦ f a none) (head✝ :: tail✝), [])
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
⊢ as.zipLeft' [] = (map (fun a ↦ (a, none)) as, [])

Tactic:
cases as

Goal state after:
case nil
α : Type u
β : Type v
⊢ [].zipLeft' [] = (map (fun a ↦ (a, none)) [], [])

case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).zipLeft' [] = (map (fun a ↦ (a, none)) (head✝ :: tail✝), [])
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
⊢ map₂Left f as [] = map (fun a ↦ f a none) as

Tactic:
cases as

Goal state after:
case nil
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
⊢ map₂Left f [] [] = map (fun a ↦ f a none) []

case cons
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : α
tail✝ : List α
⊢ map₂Left f (head✝ :: tail✝) [] = map (fun a ↦ f a none) (head✝ :: tail✝)
Module: Mathlib.Data.List.Map2

Goal state before:
pp: α : Type u
β : Type v
as : List α
⊢ as.zipLeft [] = map (fun a ↦ (a, none)) as

Tactic:
cases as

Goal state after:
case nil
α : Type u
β : Type v
⊢ [].zipLeft [] = map (fun a ↦ (a, none)) []

case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).zipLeft [] = map (fun a ↦ (a, none)) (head✝ :: tail✝)
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
⊢ Acc (Shortlex r) (xa :: xb)

Tactic:
| intro xb _ ihb =>

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

Goal state before:
pp: case neg.inr
α : Type u_1
p i : ℕ
w : List α
per : ∀ i < w.length - p, w[i]? = w[i + p]?
less : i < w.length
p_zero : ¬p = 0
large : p ≤ i
len' : i - p < w.length
IH : w[(i - p) % p]? = w[i - p]?
minus : i - p < w.length - p
per' : w[i - p]? = w[i]?
mod : i % p = (i - p) % p
⊢ w[i % p]? = w[i]?

Tactic:
aesop

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

Goal state before:
pp: case inr.inr
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
less_mod : i % p < n + w.length
⊢ w[i % p]? = (take n w ++ w)[i % p]?

Tactic:
mod_p (i % p) less_mod,

Goal state after:
case inr.inr
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
mod_p : ∀ j < n + w.length, (take n w ++ w)[j]? = w[j % p]?
less_mod : i % p < n + w.length
⊢ w[i % p]? = w[i % p % p]?
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case inl
b n : ℕ
hn : n ≠ 0
⊢ 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b

Tactic:
aesop

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

Goal state before:
pp: case hn
p : ℕ → Prop
hf : (Set.ofPred p).Finite
n : ℕ
hn : #hf.toFinset ≤ n
⊢ (hf.toFinset.sort fun a b ↦ a ≤ b).length ≤ n

Tactic:
rwa [Finset.length_sort]

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

Goal state before:
pp: n : ZNum
⊢ ↑↑n = n

Tactic:
← ofInt'_eq,

Goal state after:
n : ZNum
⊢ ofInt' ↑n = n
Module: Mathlib.Data.Num.ZNum

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

Tactic:
by rw [← of_nat_toZNum, Num.zneg_toZNum]

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

Goal state before:
pp: case node
α : 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 < (Ordnode.node rs rl rx rr).size
H3 : 2 * (Ordnode.node rs rl rx rr).size ≤ 9 * l.size + 5 ∨ (Ordnode.node rs rl rx rr).size ≤ 3
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂

Tactic:
hr.2.size_eq,

Goal state after:
case node
α : 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 + 1
H3 : 2 * (Ordnode.node rs rl rx rr).size ≤ 9 * l.size + 5 ∨ (Ordnode.node rs rl rx rr).size ≤ 3
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case neg.inl
α : 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 = 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
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂

Tactic:
hr.2.size_eq,

Goal state after:
case neg.inl
α : 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 + (rl.size + rr.size + 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
⊢ Valid' o₁ (l.node4L x rl rx rr) o₂
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 :
  ∀ (x y : P.M α),
    R x y →
      ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)
x y : P.M α
r : R x y
⊢ x = y

Tactic:
obtain ⟨a₁, f₁⟩ := x
  obtain ⟨a₂, f₂⟩ := y
  dsimp [mp] at *
  have : a₁ = a₂ := by
    refine
      PFunctor.M.bisim (fun a₁ a₂ => ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) ?_ _ _
        ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
    rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩
    rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h'⟩
    rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩
    rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩
    rw [e₁', e₂']
    exact ⟨_, _, _, rfl, rfl, fun b => ⟨_, _, h' b, rfl, rfl⟩⟩
  subst this
  congr with (i p)
  induction p with (
    obtain ⟨a', f', f₁', f₂', e₁, e₂, h''⟩ := h _ _ r
    obtain ⟨g₁', e₁', rfl, rfl⟩ := M.bisim_lemma P e₁
    obtain ⟨g₂', e₂', e₃, rfl⟩ := M.bisim_lemma P e₂
    cases h'.symm.trans e₁'
    cases h'.symm.trans e₂')
  | root x a f h' i c =>
    exact congr_fun (congr_fun e₃ i) c
  | child x a f h' i c p IH =>
    exact IH _ _ (h'' _)

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

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.dual.findMax = t.findMin

Tactic:
← findMin_dual,

Goal state after:
α : Type u_1
t : Ordnode α
⊢ t.dual.dual.findMin = t.findMin
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
⊢ (u + v).prod = u.prod * v.prod

Tactic:
by
  change (coePNatMonoidHom (u + v)).prod = _
  rw [coePNatMonoidHom.map_add]
  exact Multiset.prod_add _ _

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

Goal state before:
pp: case right.right.right.right.left
a b : ℕ+
d : ℕ+ := ⋯
w : ℕ+ := ⋯
x : ℕ := ⋯
y : ℕ := ⋯
z : ℕ+ := ⋯
a' : ℕ+ := ⋯
b' : ℕ+ := ⋯
u : XgcdType := ⋯
ur : XgcdType := ⋯
hb : d = ur.b
ha' : ↑a' = ↑w + x
hb' : ↑b' = y + ↑z
hdet : w * z = (x * y).succPNat
hdet' : ↑w * ↑z = x * y + 1
hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)
ha'' : ↑a = ↑a' * ↑d
hb'' : ↑b = ↑b' * ↑d
hza' : ↑z * ↑a' = x * ↑b' + 1
hwb' : ↑w * ↑b' = y * ↑a' + 1
⊢ ↑(w * b') = ↑(y * ↑a').succPNat

Tactic:
rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hwb']

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

Goal state before:
pp: case mpr.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : x = abs ⟨a', f'⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
i : Fin2 n
u : α i
usuppx : u ∈ supp x i
⊢ p i u

Tactic:
rcases (mem_supp x _ u).mp (@usuppx) a' f' xeq'.symm with ⟨i, _, f'ieq⟩

Goal state after:
case mpr.mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
a' : (P F).A
f' : (P F).B a' ⟹ α
xeq' : x = abs ⟨a', f'⟩
h' : ∀ (i : Fin2 n) (j : (P F).B a' i), p i (f' i j)
i✝ : Fin2 n
u : α i✝
usuppx : u ∈ supp x i✝
i : (P F).B a' i✝
left✝ : i ∈ univ
f'ieq : f' i✝ i = u
⊢ p i✝ u
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.left
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := ⋯
⊢ IsPrecongr r'

pp: case h.right
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := ⋯
⊢ r' (g <$$> aa₁) (g <$$> aa₂)

Tactic:
· show IsPrecongr r'
        rintro b₁ b₂ ⟨a₁, a₂, ra₁a₂, b₁eq, b₂eq⟩
        let u : Quot r → Quot r' :=
          Quot.lift (fun x : q.P.M α => Quot.mk r' (g <$$> x))
            (by
              intro a₁ a₂ ra₁a₂
              apply Quot.sound
              exact ⟨a₁, a₂, ra₁a₂, rfl, rfl⟩)
        have hu : (Quot.mk r' ∘ fun x : q.P.M α => g <$$> x) = u ∘ Quot.mk r := by
          ext x
          rfl
        rw [b₁eq, b₂eq, M.dest_map, M.dest_map, ← q.P.comp_map, ← q.P.comp_map]
        rw [← appendFun_comp, id_comp, hu, ← comp_id g, appendFun_comp]
        rw [q.P.comp_map, q.P.comp_map, abs_map, pr ra₁a₂, ← abs_map]

Goal state after:
case h.right
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α β : TypeVec.{u} n
g : α ⟹ β
aa₁ aa₂ : (P F).M α
r : (P F).M α → (P F).M α → Prop
pr : IsPrecongr r
ra₁a₂ : r aa₁ aa₂
r' : (P F).M β → (P F).M β → Prop := ⋯
⊢ r' (g <$$> aa₁) (g <$$> aa₂)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : DecidableLE α
x : α
t : Ordnode α
h : t.Valid
⊢ (Ordnode.insert x t).Valid

Tactic:
by
  rw [insert_eq_insertWith]; exact insertWith.valid _ _ (fun _ _ => ⟨le_rfl, le_rfl⟩) h

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

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
⊢ LiftPPreservation ↔ IsUniform

Tactic:
rw [← suppPreservation_iff_liftpPreservation, suppPreservation_iff_isUniform]

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

Goal state before:
pp: case ih
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
u : F (α ::: β) → β
y : (P F).W α
a✝ : (P F).A
f'✝ : (P F).drop.B a✝ ⟹ α
f✝ : (P F).last.B a✝ → (P F).W α
⊢ WEquiv ((P F).wMk a✝ f'✝ f✝) y → recF u ((P F).wMk a✝ f'✝ f✝) = recF u y

Tactic:
case ih a₀ f'₀ f₀ =>
    induction y using q.P.wCases
    case ih a₁ f'₁ f₁ =>
      intro h
      -- Porting note: induction on h doesn't work.
      refine @WEquiv.recOn _ _ _ _ (fun a a' _ ↦ recF u a = recF u a') _ _ h ?_ ?_ ?_
      · intro a f' f₀ f₁ _h ih; simp only [recF_eq]
        congr 4; funext; apply ih
      · intro a₀ f'₀ f₀ a₁ f'₁ f₁ h; simp only [recF_eq', abs_map, MvPFunctor.wDest'_wMk, h]
      · intro x y z _e₁ _e₂ ih₁ ih₂; exact Eq.trans ih₁ ih₂

Goal state after:
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:
size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable

Goal state after:
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 ((erase x t_l).size + t_r.size + 1) (t_l.size + t_r.size + 1)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
h_pos_t_l_size : 0 < t_l.size
⊢ t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1

Tactic:
revert h_pos_t_l_size

Goal state after:
case node.lt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_l = true
t_ih_l : (erase x t_l).size = t_l.size - 1
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
⊢ 0 < t_l.size → t_l.size - 1 + t_r.size + 1 = (node (t_l.size + t_r.size + 1) t_l t_x t_r).size - 1
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ ((TypeVec.id ::: fixToW) ⊚ splitFun f' fun x ↦ ⟦f x⟧) = (TypeVec.id ::: wrepr) ⊚ splitFun f' f

Tactic:
rw [appendFun, appendFun, ← splitFun_comp, ← splitFun_comp]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ splitFun (TypeVec.id ⊚ f') (fixToW ∘ fun x ↦ ⟦f x⟧) = splitFun (TypeVec.id ⊚ f') (wrepr ∘ f)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
j : (P F).B a Fin2.fz
⊢ splitFun (dropFun f₀) (Quot.mk r ∘ lastFun f₀) Fin2.fz j = splitFun (dropFun f₁) (Quot.mk r ∘ lastFun f₁) Fin2.fz j

pp: case fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
i : Fin2 n
j : (P F).B a i.fs
⊢ splitFun (dropFun f₀) (Quot.mk r ∘ lastFun f₀) i.fs j = splitFun (dropFun f₁) (Quot.mk r ∘ lastFun f₁) i.fs j

Tactic:
· apply Quot.sound
    apply h' _ j

Goal state after:
case fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest
x y : Cofix F α
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a ⟹ fun a ↦ (α ::: Cofix F α) a
dxeq : x.dest = MvQPF.abs ⟨a, f₀⟩
dyeq : y.dest = MvQPF.abs ⟨a, f₁⟩
h' : ∀ (i : Fin2 (n + 1)) (j : (P F).B a i), α.RelLast r (f₀ i j) (f₁ i j)
i : Fin2 n
j : (P F).B a i.fs
⊢ splitFun (dropFun f₀) (Quot.mk r ∘ lastFun f₀) i.fs j = splitFun (dropFun f₁) (Quot.mk r ∘ lastFun f₁) i.fs j
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
f : α → β
b : (P F₂).A
h : (P F₂).B b → (P F₁).A
g :
  { A := (a₂ : (P F₂).A) × ((P F₂).B a₂ → (P F₁).A), B := fun a₂a₁ ↦ (u : (P F₂).B a₂a₁.fst) × (P F₁).B (a₂a₁.snd u) }.B
      ⟨b, h⟩ →
    α
⊢ ?a = f <$> abs ⟨b, fun x ↦ abs ⟨h x, fun y ↦ g ⟨x, y⟩⟩⟩

Tactic:
apply abs_map

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : 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 : α) {l : List (Computation α)} {S : WSeq (Computation α)}, pure a ∈ l → (corec parallel.aux1 (l, S)).Terminates

pp: α : 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
⊢ ∀ (s : Computation α),
    (∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates) →
      ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
· intro a l S m
    apply lem1
    induction l with | nil => simp at m | cons c l IH => ?_
    simp only [List.mem_cons] at m
    rcases m with e | m
    · rw [← e]
      simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
      split <;> simp
    · obtain ⟨a', e⟩ := IH m
      simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
      rw [e]
      exact ⟨a', rfl⟩

Goal state after:
α : 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
⊢ ∀ (s : Computation α),
    (∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates) →
      ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (n + 1)

Tactic:
rw [Nat.add_comm]

Goal state after:
α : Type u
s : WSeq α
n : ℕ
⊢ s.tail.drop n = s.drop (1 + n)
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).drop n).tail = ↑(s.drop n).tail

Tactic:
dropn_ofSeq s n,

Goal state after:
α : Type u
s : Seq α
n : ℕ
⊢ (↑(s.drop n)).tail = ↑(s.drop n).tail
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
x✝ : α
s✝ : WSeq α
ej : (cons x✝ s✝).append S.join = cons b ss
m : a ∈ (cons x✝ s✝).append S.join
this : x✝ = b ∧ s✝.append S.join = ss
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s

Tactic:
cases this with

Goal state after:
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S✝ : WSeq (WSeq α)
T✝ : WSeq (WSeq β)
h : LiftRel (LiftRel R) S✝ T✝
s1 : WSeq α
s2 : WSeq β
x✝ :
  (fun s1 s2 ↦ ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) s1 s2
s : WSeq α
t : WSeq β
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h1 : s1 = s.append S.join
h2 : s2 = t.append T.join
st : LiftRel R s t
ST : LiftRel (LiftRel R) S T
⊢ Computation.LiftRel
    (LiftRelO R fun s1 s2 ↦
      ∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T)
    s1.destruct s2.destruct

Tactic:
by
    rw [h1, h2]; rw [destruct_append, destruct_append]
    apply Computation.liftRel_bind _ _ (liftRel_destruct st)
    exact fun {o p} h =>
      match o, p, h with
      | some (a, s), some (b, t), ⟨h1, h2⟩ => by
        simpa using ⟨h1, s, t, S, rfl, T, rfl, h2, ST⟩
      | none, none, _ => by
        -- We do not `dsimp` with `LiftRelO` since `liftRel_join.lem` uses `LiftRelO`.
        dsimp only [destruct_append.aux, Computation.LiftRel]; constructor
        · intro
          apply liftRel_join.lem _ ST fun _ _ => id
        · intro b mb
          rw [← LiftRelO.swap]
          apply liftRel_join.lem (swap R)
          · rw [← LiftRel.swap R, ← LiftRel.swap]
            apply ST
          · rw [← LiftRel.swap R, ← LiftRel.swap (LiftRel R)]
            exact fun s1 s2 ⟨s, t, S, T, h1, h2, st, ST⟩ => ⟨t, s, T, S, h2, h1, st, ST⟩
          · exact mb

Goal state after: