mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
x y : ↑F F.M
h : M.mk x = M.mk y
⊢ x = y

Tactic:
by rw [← dest_mk x, h, dest_mk]

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

Goal state before:
pp: case zero.f.f
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
z : F.M
a✝ : F.A
f✝¹ : F.B a✝ → F.M
hx : Agree' 0 z (M.mk ⟨a✝, f✝¹⟩)
f✝ : F.B a✝ → F.M
hy : Agree' 0 z (M.mk ⟨a✝, f✝⟩)
⊢ (M.mk ⟨a✝, f✝¹⟩).approx (0 + 1) = (M.mk ⟨a✝, f✝⟩).approx (0 + 1)

Tactic:
simp only [approx_mk, heq_iff_eq, CofixA.intro.injEq,
      eq_iff_true_of_subsingleton, and_self]

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

Goal state before:
pp: case pos.inr.refine_2
α : 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
⊢ rl.size ≤ delta * l.size

Tactic:
exact Nat.le_of_lt_succ (Valid'.rotateL_lemma₂ H3 h)

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 fy : P.B ax ⟹ α ::: P.M α
Hdrop : dropFun fx = dropFun fy
i : (P.B ax).last
h₁ : Relation.EqvGen R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)

Tactic:
h₀.eqvGen_iff

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
Hdrop : dropFun fx = dropFun fy
i : (P.B ax).last
h₁ : R (fx Fin2.fz i) (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
s₁ s₂ : F.M
ps : Path F
⊢ R s₁ s₂ →
    IsPath ps s₁ ∨ IsPath ps s₂ →
      iselect ps s₁ = iselect ps s₂ ∧
        ∃ a f f', isubtree ps s₁ = M.mk ⟨a, f⟩ ∧ isubtree ps s₂ = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)

Tactic:
intro h₀ hh
  induction s₁ using PFunctor.M.casesOn' with | _ a f
  induction s₂ using PFunctor.M.casesOn' with | _ a' f'
  obtain rfl : a = a' := bisim.head h₀
  induction ps generalizing a f f' with
  | nil =>
    exists rfl, a, f, f', rfl, rfl
    apply bisim.tail h₀
  | cons i ps ps_ih => ?_
  obtain ⟨a', i⟩ := i
  obtain rfl : a = a' := by rcases hh with hh | hh <;> cases isPath_cons hh <;> rfl
  dsimp only [iselect] at ps_ih ⊢
  have h₁ := bisim.tail h₀ i
  induction h : f i using PFunctor.M.casesOn' with | _ a₀ f₀
  induction h' : f' i using PFunctor.M.casesOn' with | _ a₁ f₁
  simp only [h, h', isubtree_cons] at ps_ih ⊢
  rw [h, h'] at h₁
  obtain rfl : a₀ = a₁ := bisim.head h₁
  apply ps_ih _ _ _ h₁
  rw [← h, ← h']
  apply Or.imp isPath_cons' isPath_cons' hh

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

Goal state before:
pp: F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
⊢ iselect ps s₁ = iselect ps s₂

Tactic:
by_cases h : IsPath ps s₁ ∨ IsPath ps s₂

Goal state after:
case pos
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂

case neg
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝ : Nonempty F.M
bisim : IsBisimulation R
inhabited_h : Inhabited F.M
s₁ s₂ : F.M
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
t : Ordnode α
⊢ t.merge nil = t

Tactic:
cases t <;> rfl

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

Goal state before:
pp: case refine_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
⊢ p ⟨↑n, ⋯⟩

Tactic:
obtain ⟨n', hn', pn'⟩ := n.prop.1

Goal state after:
case refine_2
p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
this : ∃ n' n x, p n
n : { n // (∃ n_1 x, p n_1) ∧ ∀ (m : ℕ), m < n → ¬∃ n x, p n }
n' : ℕ+
hn' : ↑n = ↑n'
pn' : p n'
⊢ p ⟨↑n, ⋯⟩
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: case e'_3.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • PrimeMultiset.ofPrime p
⊢ q = p

Tactic:
PrimeMultiset.ofPrime,

Goal state after:
case e'_3.right
m : ℕ+
p : Nat.Primes
k : ℕ
e_1✝ : PrimeMultiset = Multiset Nat.Primes
q : Nat.Primes
h : q ∈ k • {p}
⊢ q = p
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
this : (node lls lll llx llr).size ≤ 1
⊢ lll.size = 0 ∧ llr.size = 0

Tactic:
rwa [size, sl.2.1.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this

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

Goal state before:
pp: case fst
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := ⋯
hr : u.r - 1 + 1 = u.r := ⋯
⊢ u.step.v.1 = u.v.swap.1

Tactic:
change ((u.y * u.q + u.z) * u.b + u.y * (u.r - 1 + 1) : ℕ) = u.y * u.a + u.z * u.b

Goal state after:
case fst
u : XgcdType
hr✝ : u.r ≠ 0
ha : u.r + ↑u.b * u.q = ↑u.a := rq_eq u
hr : u.r - 1 + 1 = u.r := Eq.trans (add_comm (u.r - 1) 1) (add_tsub_cancel_of_le (Nat.pos_of_ne_zero hr✝))
⊢ (u.y * u.q + ↑u.z) * ↑u.b + u.y * (u.r - 1 + 1) = u.y * ↑u.a + ↑u.z * ↑u.b
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: a b : ℕ+
⊢ (a.xgcd b).y + (a.xgcd b).zp + 1 = (a.xgcd b).y + ((a.xgcd b).zp + 1)

Tactic:
rw [add_assoc]

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

Goal state before:
pp: case pos
α : 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
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
IHrl :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
      Valid' o₁ rl o₂ →
        All (fun x ↦ All (fun y ↦ x < y) rl) (Ordnode.node ls ll lx lr) →
          Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) o₂ ∧
            ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
r_ih✝ :
  ∀ {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ (Ordnode.node ls ll lx lr) o₂ →
      Valid' o₁ rr o₂ →
        All (fun x ↦ All (fun y ↦ x < y) rr) (Ordnode.node ls ll lx lr) →
          Valid' o₁ ((Ordnode.node ls ll lx lr).merge rr) o₂ ∧
            ((Ordnode.node ls ll lx lr).merge rr).size = (Ordnode.node ls ll lx lr).size + rr.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
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)
h : delta * ls < rs
v : Valid' o₁ ((Ordnode.node ls ll lx lr).merge rl) ↑rx
e : ((Ordnode.node ls ll lx lr).merge rl).size = (Ordnode.node ls ll lx lr).size + rl.size
⊢ Valid' o₁ (((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr) o₂ ∧
    (((Ordnode.node ls ll lx lr).merge rl).balanceL rx rr).size =
      (Ordnode.node ls ll lx lr).size + (Ordnode.node rs rl rx rr).size

Tactic:
exact Valid'.merge_aux₁ hl hr h v e

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

Goal state before:
pp: case right.right.right.right.left
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
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' + 1

Tactic:
hwb'

Goal state after:
case right.right.right.right.left
a b : ℕ+
d : ℕ+ := a.gcdD b
w : ℕ+ := a.gcdW b
x : ℕ := a.gcdX b
y : ℕ := a.gcdY b
z : ℕ+ := a.gcdZ b
a' : ℕ+ := a.gcdA' b
b' : ℕ+ := a.gcdB' b
u : XgcdType := XgcdType.start a b
ur : XgcdType := u.reduce
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
⊢ y * ↑a' + 1 = y * ↑a' + 1
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} (x : Comp F G α),
    (Comp.mk ∘ (MvFunctor.map fun x ↦ abs) ∘ abs ∘ comp.get)
        ((comp.mk ∘ repr ∘ (MvFunctor.map fun i ↦ repr) ∘ Comp.get) x) =
      x

Tactic:
intros
    simp +unfoldPartialApp only [Function.comp_def, comp.get_mk, abs_repr,
      map_map, TypeVec.comp, MvFunctor.id_map', Comp.mk_get]

Goal state after:
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 ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₁) = abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₂)

Tactic:
b₁eq,

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 ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) (g <$$> a₁)) =
    abs ((TypeVec.id ::: Quot.mk r') <$$> M.dest (P F) b₂)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Quot

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u
q : MvQPF F
G : TypeVec.{u} n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec.{u} n} → F α → G α
FG_repr : {α : TypeVec.{u} n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ β✝ : TypeVec.{u} n
f : α✝ ⟹ β✝
p : ↑(P F) α✝
⊢ FG_abs (f <$$> abs p) = f <$$> FG_abs (abs p)

Tactic:
FG_abs_map

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u
q : MvQPF F
G : TypeVec.{u} n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec.{u} n} → F α → G α
FG_repr : {α : TypeVec.{u} n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ β✝ : TypeVec.{u} n
f : α✝ ⟹ β✝
p : ↑(P F) α✝
⊢ f <$$> FG_abs (abs p) = f <$$> FG_abs (abs p)
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
G : Type u → Type u
inst✝ : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α β : Type u
f : α → β
x : ↑(P F) α
⊢ FG_abs (f <$> abs x) = f <$> FG_abs (abs x)

Tactic:
FG_abs_map

Goal state after:
F : Type u → Type u
q : QPF F
G : Type u → Type u
inst✝ : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α β : Type u
f : α → β
x : ↑(P F) α
⊢ f <$> FG_abs (abs x) = f <$> FG_abs (abs x)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: Cofix.corec (g ∘ f)) <$$> g (f x))
    ((TypeVec.id ::: Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g)) <$$>
      (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x))

Tactic:
Function.comp_apply

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: Cofix.corec (g ∘ f)) <$$> g (f x))
    ((TypeVec.id ::: Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g)) <$$> (TypeVec.id ::: f) <$$> g (f x))
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : WSeq α
a : α
h : some a ∈ s.tail.head
⊢ ∃ a', some a' ∈ s.head

Tactic:
by
  unfold head at h
  rcases Computation.exists_of_mem_map h with ⟨o, md, e⟩; clear h
  rcases o with - | o <;> [injection e; injection e with h']; clear h'
  obtain ⟨a, am⟩ := destruct_some_of_destruct_tail_some md
  exact ⟨_, Computation.mem_map (@Prod.fst α (WSeq α) <$> ·) am⟩

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

Goal state before:
pp: α : Type u
C : WSeq α → Prop
a : α
s : WSeq α
M : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), a = b ∨ C s' → C (cons b s')
h2 : ∀ (s : WSeq α), C s → C s.think
s' : Seq (Option α)
b : α
h✝ : some a = some b ∨ C s'
h : some a = some b
⊢ a = b

Tactic:
injection h

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 := 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 β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ S s t

Tactic:
refine ⟨Computation.pure s, Computation.pure t, ?_, ?_, ?_⟩

Goal state after:
case refine_1
α : 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 β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ s = flatten (Computation.pure s)

case refine_2
α : 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 β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ t = flatten (Computation.pure t)

case refine_3
α : 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 β)
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ Computation.LiftRel (LiftRel R) (Computation.pure s) (Computation.pure t)
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
⊢ ∀ (a : Σₗ (i : ι), α i), ∃ b, b < a

Tactic:
rintro ⟨i, a⟩
    obtain ⟨b, h⟩ := exists_lt a
    exact ⟨⟨i, b⟩, right _ _ h⟩

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

Goal state before:
pp: case h1
α : 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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
e' : (corec parallel.aux1 (l, S)).destruct = (pure a).destruct
this : F l (parallel.aux2 l)
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e'

Goal state after:
case h1
α : 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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = pure a
this : F l (parallel.aux2 l)
e' :
  rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)) =
    Sum.inl a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
x✝¹ : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
x✝ : S.destruct.Results none m
rs2 : (destruct_join.aux none).Results a k
mT : none ∈ T.destruct
⊢ LiftRelO R U a none

Tactic:
rw [eq_of_pure_mem rs2.mem]

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
ra : (S.destruct.bind destruct_join.aux).Results a n
o : Option (WSeq α × WSeq (WSeq α))
m k : ℕ
rs1 : S.destruct.Results o m
rs2✝ : (destruct_join.aux o).Results a k
en : n = k + m
p : Option (WSeq β × WSeq (WSeq β))
mT✝ : p ∈ T.destruct
rop : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) o p
x✝¹ : LiftRelO (LiftRel R) (LiftRel (LiftRel R)) none none
x✝ : S.destruct.Results none m
rs2 : (destruct_join.aux none).Results a k
mT : none ∈ T.destruct
⊢ LiftRelO R U none none
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2
α : 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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
e' : (corec parallel.aux1 (l, S)).destruct = C'.think.destruct
this : F l (parallel.aux2 l)
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
simp only [parallel.aux1, corec_eq, destruct_pure, destruct_think] at e'

Goal state after:
case h2
α : 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
lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)
C : Computation α
aC : a ∈ C
C' : Computation α
IH :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
l : List (Computation α)
S : WSeq (Computation α)
e : corec parallel.aux1 (l, S) = C'.think
this : F l (parallel.aux2 l)
e' :
  rmap (corec parallel.aux1)
      (rmap
        (fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        (parallel.aux2 l)) =
    Sum.inr C'
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c