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

Goal state before:
pp: α : Type u_1
l : List α
x : α
hx : ¬x ∈ l
⊢ Set.InjOn (fun k ↦ l.insertIdx k x) {n | n ≤ l.length}

Tactic:
intro n hn m hm h
  induction l generalizing n m with
  | nil =>
    simp_all [Set.mem_singleton_iff, Set.ofPred_eq_eq_singleton, length]
  | cons hd tl IH =>
    simp only [length, Set.mem_ofPred_eq] at hn hm
    simp only [mem_cons, not_or] at hx
    cases n <;> cases m
    · rfl
    · simp [hx.left] at h
    · simp [Ne.symm hx.left] at h
    · simp only [insertIdx_succ_cons, cons.injEq, true_and] at h
      rw [Nat.succ_inj]
      refine IH hx.right ?_ ?_ h
      · simpa [Nat.succ_le_succ_iff] using hn
      · simpa [Nat.succ_le_succ_iff] using hm

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

Goal state before:
pp: case mp
α : Type u_1
p : ℕ
w : List α
⊢ w.HasPeriod p → ∀ i < w.length, w[i]? = w[i % p]?

Tactic:
intro per i len

Goal state after:
case mp
α : Type u_1
p : ℕ
w : List α
per : w.HasPeriod p
i : ℕ
len : i < w.length
⊢ w[i]? = w[i % p]?
Module: Mathlib.Data.Multiset.DershowitzManna

Goal state before:
pp: case cons.inr.refine_2
α : Type u_1
inst✝ : Preorder α
z : α
Z : Multiset α
ih :
  ∀ {M N : Multiset α} (X Y : Multiset α),
    Z ≠ ∅ → M = X + Y → N = X + Z → (∀ (y : α), y ∈ Y → ∃ z, z ∈ Z ∧ y < z) → TransGen OneStep M N
M N X Y : Multiset α
hZ✝ : z ::ₘ Z ≠ ∅
hM : M = X + Y
hN : N = X + z ::ₘ Z
hYZ : ∀ (y : α), y ∈ Y → ∃ z_1, z_1 ∈ z ::ₘ Z ∧ y < z_1
hZ : Z ≠ 0
Y' : Multiset α := filter (fun x ↦ x < z) Y
y : α
hy : y ∈ Y - Y'
⊢ ∃ z, z ∈ Z ∧ y < z

Tactic:
· simp only [sub_filter_eq_filter_not, mem_filter, Y'] at hy
    simpa [hy.2] using hYZ y (by simp_all)

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ⌊↑x⌋ = ⌊↑x⌋

Tactic:
by
  rw [Int.floor_eq_iff, ← coe_floor]
  norm_cast
  norm_cast
  rw [Nat.cast_add_one, ← Nat.floor_eq_iff zero_le]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ IsChain (fun a b ↦ b + 2 ≤ a) ((n + 1).greatestFib :: (n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0])

Tactic:
List.cons_append

Goal state after:
n : ℕ
⊢ IsChain (fun a b ↦ b + 2 ≤ a) ((n + 1).greatestFib :: ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]))
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_2.inl
p : ℕ → Prop
h₀ : p 0
⊢ nth p 0 = 0

pp: case refine_2.inr
p : ℕ → Prop
n : ℕ
hf : (Set.ofPred p).Finite
hle : #hf.toFinset ≤ n
⊢ nth p n = 0

Tactic:
exacts [nth_zero_of_zero h₀, nth_of_card_le hf hle]

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

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : Set.ofPred p ⊆ ↑(range n)
⊢ #⋯.toFinset ≤ n

Tactic:
· refine (Finset.card_le_card ?_).trans_eq (Finset.card_range n)
    exact Set.Finite.toFinset_subset.mpr this

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

Tactic:
by
  simp only [Obj.iget, fst_map, *, dif_pos]
  cases x
  rfl

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

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

Tactic:
← hy,

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ Subtype.val <$> y = ⟨a, fun i ↦ ↑(f i)⟩
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mpr
P : PFunctor.{uA, uB}
α : Type u
r : α → α → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ Liftr r x y

Tactic:
use ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩

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

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

Tactic:
← hy,

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

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
intro a b

Goal state after:
α : Type u_1
a b : ZNum
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a ≤ b → b ≤ a → a = b

Tactic:
intro a b

Goal state after:
α : Type u_1
a b : ZNum
⊢ a ≤ b → b ≤ a → a = b
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b : ZNum), a ≤ b ∨ b ≤ a

Tactic:
intro a b

Goal state after:
α : Type u_1
a b : ZNum
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
e₁ : dest P ⟨a₁, f₁⟩ = ⟨a', ff⟩
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = ⟨a₁', g₁'⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Tactic:
M.dest_eq_dest' _ e₁'

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = ⟨a₁', g₁'⟩
e₁ : dest' P e₁' f₁ = ⟨a', ff⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case neg
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ¬ls > delta * rs
⊢ (node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)).dual =
    node (rs + ls + 1) (node rs rr.dual rx rl.dual) x (node ls lr.dual lx ll.dual)

pp: case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ls > delta * rs
⊢ (rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l x_2 r l_ih r_ih ↦
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll).dual =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual

Tactic:
· simp [add_comm]

Goal state after:
case pos
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h✝ : ls > delta * rs
⊢ (rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l x_2 r l_ih r_ih ↦
              if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll).dual =
    rec nil
      (fun size l x_1 r l_ih r_ih ↦
        rec nil
          (fun size_1 l x_2 r l_ih r_ih ↦
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.hrec
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), (isubtree ps x).head = (isubtree ps y).head
i : ℕ
i_ih : x.approx i = y.approx i
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y

Tactic:
cases H'

Goal state after:
case succ.hrec.refl
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), (isubtree ps x).head = (isubtree ps y).head
ps : Path F
i_ih : x.approx (length ps) = y.approx (length ps)
⊢ iselect ps x = iselect ps y
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
⊢ r.size + l.size + 1 = l.size + r.size + 1

Tactic:
add_comm (size l)

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
⊢ r.size + l.size + 1 = r.size + l.size + 1
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ Multiset.map Subtype.val (Multiset.pmap (fun p hp ↦ ⟨p, hp⟩) v h) = v

Tactic:
Multiset.map_pmap,

Goal state after:
v : Multiset ℕ
h : ∀ (p : ℕ), p ∈ v → Nat.Prime p
⊢ Multiset.pmap (fun a h ↦ ↑⟨a, h⟩) v h = v
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
this : (fun p h ↦ ↑⟨↑p, h⟩) = fun p x ↦ id p
⊢ Multiset.map Nat.Primes.toPNat (Multiset.pmap (fun p hp ↦ ⟨↑p, hp⟩) v h) = v

Tactic:
Multiset.map_pmap,

Goal state after:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
this : (fun p h ↦ ↑⟨↑p, h⟩) = fun p x ↦ id p
⊢ Multiset.pmap (fun a h ↦ ↑⟨↑a, h⟩) v h = v
Module: Mathlib.Data.PFunctor.Multivariate.W

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : ↑P (α ::: P.W α)
⊢ P.wDest' (P.wMk' x) = x

Tactic:
obtain ⟨a, f⟩ := x; rw [wMk', wDest'_wMk, split_dropFun_lastFun]

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

Goal state before:
pp: case node.node
α : 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 : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ (node ls ll lx lr).balance x (node rs rl rx rr) = (node ls ll lx lr).balance' x (node rs rl rx rr)

Tactic:
simp only [balance, id_eq, balance', size_node, gt_iff_lt]

Goal state after:
case node.node
α : 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 : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ (if delta * ls < rs then
      rec nil
        (fun size l x_1 r l_ih r_ih ↦
          rec nil
            (fun size_1 l_1 x_2 r_1 l_ih r_ih ↦
              if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x rl) rx rr
              else
                node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                  (node (r.size + size_1 + 1) r rx rr))
            rr)
        rl
    else
      if delta * rs < ls then
        rec nil
          (fun size l x_1 r l_ih r_ih ↦
            rec nil
              (fun size_1 l x_2 r l_ih r_ih ↦
                if size_1 < ratio * size then node (ls + rs + 1) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                    (node (r.size + rs + 1) r x (node rs rl rx rr)))
              lr)
          ll
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)) =
    if ls + rs ≤ 1 then (node ls ll lx lr).node' x (node rs rl rx rr)
    else
      if delta * ls < rs then (node ls ll lx lr).rotateL x (node rs rl rx rr)
      else
        if delta * rs < ls then (node ls ll lx lr).rotateR x (node rs rl rx rr)
        else (node ls ll lx lr).node' x (node rs rl rx rr)
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case refine_2.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
i : ι
b₁✝ b₂✝ : α i
hab : b₁✝ ≤ b₂✝
hba : ¬⟨i, b₂✝⟩ ≤ ⟨i, b₁✝⟩
⊢ ⟨i, b₁✝⟩ < ⟨i, b₂✝⟩

Tactic:
exact Lex.right _ (hab.lt_of_not_ge fun h => hba <| Lex.right _ h)

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l o₂
hr : Valid' o₁ r o₂
sep : All (fun x ↦ All (fun y ↦ x < y) r) l
⊢ Valid' o₁ (l.merge r) o₂ ∧ (l.merge r).size = l.size + r.size

Tactic:
induction l generalizing o₁ o₂ r with
  | nil => exact ⟨hr, (zero_add _).symm⟩
  | node ls ll lx lr _ IHlr => ?_

Goal state after:
case node
α : Type u_1
inst✝ : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih✝ :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ ll o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) ll → Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ lr o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) lr → Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ r o₂
sep : All (fun x ↦ All (fun y ↦ x < y) r) (Ordnode.node ls ll lx lr)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge r) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge r).size = (Ordnode.node ls ll lx lr).size + r.size
Module: Mathlib.Data.QPF.Multivariate.Basic

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

Tactic:
← hy,

Goal state after:
case h.left
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : F α
y : F fun i ↦ Subtype p
hy : (fun i ↦ Subtype.val) <$$> y = x
a : (P F).A
f : (P F).B a ⟹ fun i ↦ Subtype p
h : repr y = ⟨a, f⟩
⊢ (fun i ↦ Subtype.val) <$$> y = abs ⟨a, fun i j ↦ ↑(f i j)⟩
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 := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((g ::: Quot.mk r' ∘ fun x ↦ g <$$> x) <$$> M.dest (P F) a₁) =
    abs ((g ::: Quot.mk r' ∘ fun x ↦ g <$$> x) <$$> M.dest (P F) a₂)

Tactic:
hu,

Goal state after:
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 := fun b₁ b₂ ↦ ∃ a₁ a₂, r a₁ a₂ ∧ b₁ = g <$$> a₁ ∧ b₂ = g <$$> a₂
b₁ b₂ : (P F).M β
a₁ a₂ : (P F).M α
ra₁a₂ : r a₁ a₂
b₁eq : b₁ = g <$$> a₁
b₂eq : b₂ = g <$$> a₂
u : Quot r → Quot r' := Quot.lift (fun x ↦ Quot.mk r' (g <$$> x)) ⋯
hu : (Quot.mk r' ∘ fun x ↦ g <$$> x) = u ∘ Quot.mk r
⊢ abs ((g ::: u ∘ Quot.mk r) <$$> M.dest (P F) a₁) = abs ((g ::: u ∘ Quot.mk r) <$$> M.dest (P F) a₂)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i ↦ ↑(f i)⟩

Tactic:
← hy,

Goal state after:
case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ Subtype.val <$> y = abs ⟨a, fun i ↦ ↑(f i)⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = x

Tactic:
← hy,

Goal state after:
case h.left
F : Type u → Type v
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ⟨a, fun i ↦ ↑(f i)⟩ = Subtype.val <$> y
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ Liftr r x y ↔ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

Tactic:
constructor
  · rintro ⟨u, xeq, yeq⟩
    rcases h : repr u with ⟨a, f⟩
    use a, fun i => (f i).val.fst, fun i => (f i).val.snd
    constructor
    · rw [← xeq, ← abs_repr u, h, ← abs_map]
      rfl
    constructor
    · rw [← yeq, ← abs_repr u, h, ← abs_map]
      rfl
    intro i
    exact (f i).property
  rintro ⟨a, f₀, f₁, xeq, yeq, h⟩
  use abs ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩
  constructor
  · rw [xeq, ← abs_map]
    rfl
  rw [yeq, ← abs_map]; rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Ordset α
h : s = ∅
⊢ (↑s).empty = true

Tactic:
by cases h; exact rfl

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

Goal state before:
pp: case e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ x y : Cofix F α
h : x = mk y.dest
⊢ (((Quot.mk fun x y ↦ x = mk y.dest) ∘ mk) ∘ fun i ↦ i.dest) = Quot.mk fun x y ↦ x = mk y.dest

Tactic:
funext x

Goal state after:
case e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝¹ x✝ y : Cofix F α
h : x✝ = mk y.dest
x : Cofix F α
⊢ (((Quot.mk fun x y ↦ x = mk y.dest) ∘ mk) ∘ fun i ↦ i.dest) x = Quot.mk (fun x y ↦ x = mk y.dest) x
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case think
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c' : Computation (WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten c'.think).destruct.destruct (c'.think.bind destruct).destruct

Tactic:
simpa using Or.inr ⟨c', rfl, rfl⟩

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := ⋯
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a : WSeq α
b : WSeq β
ab : LiftRel R a b
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R (LiftRel R) a b → LiftRelO R S a b

Tactic:
intro a b

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
c1✝ : Computation (WSeq α)
c2✝ : Computation (WSeq β)
h✝¹ : Computation.LiftRel (LiftRel R) c1✝ c2✝
S : WSeq α → WSeq β → Prop := fun s t ↦ ∃ c1 c2, s = flatten c1 ∧ t = flatten c2 ∧ Computation.LiftRel (LiftRel R) c1 c2
s : WSeq α
t : WSeq β
h✝ : S s t
c1 : Computation (WSeq α)
c2 : Computation (WSeq β)
h : Computation.LiftRel (LiftRel R) c1 c2
a✝ : WSeq α
b✝ : WSeq β
ab : LiftRel R a✝ b✝
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b → LiftRelO R S a b
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case zero.nil
α : Type u
a : α
m : a ∈ nil.tail
e : some (some a) = (↑nil.tail).get 0
⊢ a ∈ nil

pp: case zero.cons
α : Type u
a x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get 0
⊢ a ∈ cons x✝ s✝

pp: case zero.think
α : Type u
a : α
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get 0
⊢ a ∈ s✝.think

pp: case succ.nil
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
m : a ∈ nil.tail
e : some (some a) = (↑nil.tail).get (n✝ + 1)
⊢ a ∈ nil

pp: case succ.cons
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get (n✝ + 1)
⊢ a ∈ cons x✝ s✝

pp: case succ.think
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get (n✝ + 1)
⊢ a ∈ s✝.think

Tactic:
case zero.nil | succ.nil => simpa using m

Goal state after:
case zero.cons
α : Type u
a x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get 0
⊢ a ∈ cons x✝ s✝

case zero.think
α : Type u
a : α
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get 0
⊢ a ∈ s✝.think

case succ.cons
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
x✝ : α
s✝ : WSeq α
m : a ∈ (cons x✝ s✝).tail
e : some (some a) = (↑(cons x✝ s✝).tail).get (n✝ + 1)
⊢ a ∈ cons x✝ s✝

case succ.think
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {s : WSeq α}, a ∈ s.tail → some (some a) = (↑s.tail).get n✝ → a ∈ s
s✝ : WSeq α
m : a ∈ s✝.think.tail
e : some (some a) = (↑s✝.think.tail).get (n✝ + 1)
⊢ a ∈ s✝.think
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO R (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) a b

Tactic:
intro a b

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1 s2 : WSeq α
t1 t2 : WSeq β
h1 : LiftRel R s1 t1
h2 : LiftRel R s2 t2
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s✝ t✝
s : WSeq α
t : WSeq β
h : LiftRel R s t
a : Option (α × WSeq α)
b : Option (β × WSeq β)
⊢ LiftRelO R (LiftRel R) a b →
    LiftRelO R (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) a b
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inl
α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l : List (Computation α)
val✝ : α
c' : Computation α
cl : c' ∈ l
ac : val✝ ∈ c'
⊢ F (c :: l) (Sum.inl val✝)

Tactic:
exact ⟨c', List.Mem.tail _ cl, ac⟩

Goal state after: