mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
⊢ LiftP (fun i x ↦ ∃ y, f i y = x) ⟨a, f⟩

Tactic:
rw [liftP_iff']

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
⊢ ∀ (i : Fin2 n) (x : P.B a i), ∃ y, f i y = f i x
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case some.left
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + ↑d + ↑d * (↑q + ↑q) = ↑n

Tactic:
← this

Goal state after:
case some.left
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r + ↑d * (↑q + ↑q) = ↑n
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.inl.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 : rl.size + rr.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size > 0
rr1 : rr.size = 1
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size

Tactic:
add_comm

Goal state after:
case pos.inl.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 : rr.size + rl.size ≤ 2
this : BalancedSz rl.size rr.size
rl0 : rl.size > 0
rr1 : rr.size = 1
⊢ BalancedSz 0 rl.size ∧ BalancedSz (0 + rl.size + 1) rr.size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : 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
rl0 : rl.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
rr0 : rr.size > 0
⊢ rr.size + rl.size ≤ 2

Tactic:
add_comm

Goal state after:
α : 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
rl0 : rl.size > 0
l0 : l.size = 0
H3 : rl.size + rr.size ≤ 2
rr0 : rr.size > 0
⊢ rl.size + rr.size ≤ 2
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ ¬r.size + l.size ≤ 1

Tactic:
add_comm

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬l.size + r.size ≤ 1
H2 : delta * r.size < l.size
H3 : 2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3
⊢ ¬l.size + r.size ≤ 1
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ (ofPNatMultiset v h).toPNatMultiset = v

Tactic:
dsimp [ofPNatMultiset, toPNatMultiset]

Goal state after:
v : Multiset ℕ+
h : ∀ (p : ℕ+), p ∈ v → p.Prime
⊢ Multiset.map Nat.Primes.toPNat (Multiset.pmap (fun p hp ↦ ⟨↑p, hp⟩) v h) = v
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ nil.Bounded (↑((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).2) o₂

Tactic:
refine findMax'_all (P := fun a : α => Bounded nil (a : WithTop α) o₂)
            lx lr hl.1.2.to_nil (sep.2.2.imp ?_)

Goal state after:
case refine_1
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
sep : All (fun x ↦ All (fun y ↦ x < y) (Ordnode.node rs rl rx rr)) (Ordnode.node ls ll lx lr)
bal : BalancedSz (Ordnode.node ls ll lx lr).size (Ordnode.node rs rl rx rr).size
h✝ : ls > rs
v : Valid' o₁ (ll.node' lx lr).eraseMax ↑(findMax' lx lr)
e : (ll.node' lx lr).size = (ll.node' lx lr).eraseMax.size + 1
H :
  (∃ l',
      Raised ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size l' ∧
        BalancedSz l' (Ordnode.node rs rl rx rr).size) ∨
    ∃ r',
      Raised r' (Ordnode.node rs rl rx rr).size ∧
        BalancedSz ((Ordnode.node (ll.size + lr.size + 1) ll lx lr).eraseMax, findMax' lx lr).1.size r'
⊢ ∀ (a : α), All (fun y ↦ a < y) (Ordnode.node rs rl rx rr) → nil.Bounded (↑a) o₂
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
⊢ ∀ (i : Fin2 n), supp (abs ⟨a, f⟩) i = f i '' univ

Tactic:
intro; ext u; rw [mem_supp]; constructor
  · intro h'
    apply h' _ _ rfl
  intro h' a' f' e
  rw [← h _ _ _ _ e.symm]; apply h'

Goal state after:
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
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ (P F).wRec (fun a f' _f rec ↦ g (abs ⟨a, splitFun f' rec⟩)) ((P F).wMk a f' f) = g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)

Tactic:
MvPFunctor.wRec_eq

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
a : (P F).A
f' : (P F).drop.B a ⟹ α
f : (P F).last.B a → (P F).W α
⊢ g (abs ⟨a, splitFun f' fun i ↦ (P F).wRec (fun a f' _f rec ↦ g (abs ⟨a, splitFun f' rec⟩)) (f i)⟩) =
    g (abs ⟨a, splitFun f' (recF g ∘ f)⟩)
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
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
⊢ ∀ (a : (P F).M α) (b : Cofix F α),
    r (Quot.mk Mcongr a) b → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr a) = Quot.lift (Quot.mk r') h₁ b

Tactic:
intro c d

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h' : ∀ (x : Cofix F α), r x x
h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
x y : (P F).M α
rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
r' : (P F).M α → (P F).M α → Prop := fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
hr' : r' = fun x y ↦ r (Quot.mk Mcongr x) (Quot.mk Mcongr y)
a b : (P F).M α
r'ab : r' a b
h₀ :
  (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) a) =
    (TypeVec.id ::: Quot.mk r ∘ Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) b)
h₁ : ∀ (u v : (P F).M α), Mcongr u v → Quot.mk r' u = Quot.mk r' v
c : (P F).M α
d : Cofix F α
⊢ r (Quot.mk Mcongr c) d → Quot.lift (Quot.mk r') h₁ (Quot.mk Mcongr c) = Quot.lift (Quot.mk r') h₁ d
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α β γ : Type u
f : α → β
g : β → γ
x : F α
⊢ (g ∘ f) <$> x = g <$> f <$> x

Tactic:
rw [← abs_repr x]
  rw [← abs_map, ← abs_map, ← abs_map]
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
t : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ t a₂
⊢ Valid' a₁ (erase x t) a₂ ∧ Raised (erase x t).size t.size

Tactic:
induction t generalizing a₁ a₂ with
  | nil =>
    simpa [erase, Raised]
  | node _ t_l t_x t_r t_ih_l t_ih_r =>
    simp only [erase, size_node]
    have t_ih_l' := t_ih_l h.left
    have t_ih_r' := t_ih_r h.right
    clear t_ih_l t_ih_r
    obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
    obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
    cases cmpLE x t_x <;> rw [h.sz.1]
    · suffices h_balanceable : _ by
        constructor
        · exact Valid'.balanceR t_l_valid h.right h_balanceable
        · rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable]
          repeat apply Raised.add_right
          exact t_l_size
      left; exists t_l.size; exact And.intro t_l_size h.bal.1
    · have h_glue := Valid'.glue h.left h.right h.bal.1
      obtain ⟨h_glue_valid, h_glue_sized⟩ := h_glue
      constructor
      · exact h_glue_valid
      · right; rw [h_glue_sized]
    · suffices h_balanceable : _ by
        constructor
        · exact Valid'.balanceL h.left t_r_valid h_balanceable
        · rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz h_balanceable]
          apply Raised.add_right
          apply Raised.add_left
          exact t_r_size
      right; exists t_r.size; exact And.intro t_r_size h.bal.1

Goal state after:
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 α
⊢ abs ((P F).wDest' ((P F).wMk' ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)))) =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))

Tactic:
MvPFunctor.wDest'_wMk',

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 α
⊢ abs ((TypeVec.id ::: fixToW) <$$> repr (abs ⟨a, (P F).appendContents f' fun x ↦ ⟦f x⟧⟩)) =
    abs ((P F).wDest' (wrepr ((P F).wMk a f' f)))
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
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 α
a✝ : r x✝ y✝
⊢ LiftR (α.RelLast r) x✝.dest y✝.dest

Tactic:
rw [← LiftR_RelLast_iff]

Goal state after:
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 α
a✝ : r x✝ y✝
⊢ LiftR' (α.RelLast' r) x✝.dest y✝.dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mpr.mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
a' : (P F).A
f' : (P F).B a' → α
xeq' : x = abs ⟨a', f'⟩
h' : ∀ (i : (P F).B a'), p (f' i)
u : α
usuppx : u ∈ supp x
⊢ p u

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

Goal state after:
case mpr.mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
xeq : abs ⟨a, f⟩ = x
h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ
p : α → Prop
a' : (P F).A
f' : (P F).B a' → α
xeq' : x = abs ⟨a', f'⟩
h' : ∀ (i : (P F).B a'), p (f' i)
u : α
usuppx : u ∈ supp x
i : (P F).B a'
left✝ : i ∈ univ
f'ieq : f' i = u
⊢ p u
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (swap (LiftRelO R (LiftRel R))) s.destruct t.destruct

Tactic:
Computation.LiftRel.swap

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1 : WSeq α
s2 : WSeq β
h✝ : LiftRel R s1 s2
s : WSeq β
t : WSeq α
h : LiftRel R t s
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct s.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
⊢ Computation.LiftRel (LiftRelO R fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) s.destruct u.destruct

Tactic:
refine
    Computation.liftRel_def.2
      ⟨(Computation.terminates_of_liftRel h1).trans (Computation.terminates_of_liftRel h2),
        fun {a c} ha hc => ?_⟩

Goal state after:
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
a c : Option (α × WSeq α)
ha : a ∈ s.destruct
hc : c ∈ u.destruct
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) a c
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
m : nil.destruct = Computation.pure (some (a', s'))
this : nil.destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

Tactic:
simp at this

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

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s✝ : WSeq α
m : s✝.think.destruct = Computation.pure (some (a', s'))
this : s✝.think.destruct.destruct = (Computation.pure (some (a', s'))).destruct
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'

Tactic:
simp at this

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

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
m : nil.destruct = c.think
this : nil.destruct.destruct = c.think.destruct
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

Tactic:
simp at this

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

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = c.think
this : (cons x✝ s✝).destruct.destruct = c.think.destruct
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

Tactic:
simp at this

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

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s✝ : WSeq α
m : s✝.think.destruct = c.think
this : s✝.think.destruct.destruct = c.think.destruct
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'

Tactic:
simp at this

Goal state after:
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s✝ : WSeq α
m : s✝.think.destruct = c.think
this : s✝.destruct = c
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (s : WSeq α), (∃ n, some a ∈ s.get? n) → ∃ n, some a ∈ s.think.get? n

Tactic:
intro s' h
    obtain ⟨n, h⟩ := h
    exists n
    simp only [get?, dropn_think, head_think]
    apply think_mem h

Goal state after:
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
ej : nil.append nil.join = cons b ss
m : a ∈ nil.append nil.join
this : Seq.destruct (nil.append nil.join) = Seq.destruct (cons b ss)
⊢ a ∈ nil ∨ ∃ s ∈ nil, a ∈ s

Tactic:
simp at this

Goal state after:
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
x✝ : WSeq α
s✝ : WSeq (WSeq α)
ej : nil.append (cons x✝ s✝).join = cons b ss
m : a ∈ nil.append (cons x✝ s✝).join
this : Seq.destruct (nil.append (cons x✝ s✝).join) = Seq.destruct (cons b ss)
⊢ a ∈ nil ∨ ∃ s ∈ cons x✝ s✝, a ∈ s

Tactic:
simp at this

Goal state after:
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 α)
ej : nil.append s✝.think.join = cons b ss
m : a ∈ nil.append s✝.think.join
this : Seq.destruct (nil.append s✝.think.join) = Seq.destruct (cons b ss)
⊢ a ∈ nil ∨ ∃ s ∈ s✝.think, a ∈ s

Tactic:
simp at this

Goal state after:
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 α)
s✝ : WSeq α
ej : s✝.think.append S.join = cons b ss
m : a ∈ s✝.think.append S.join
this : Seq.destruct (s✝.think.append S.join) = Seq.destruct (cons b ss)
⊢ a ∈ s✝.think ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp at this

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

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

Tactic:
simp at this

Goal state after:
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x✝ : WSeq α
s✝ : WSeq (WSeq α)
ej : nil.append (cons x✝ s✝).join = ss.think
m : a ∈ nil.append (cons x✝ s✝).join
this : x✝.append s✝.join = ss
⊢ a ∈ nil ∨ ∃ s ∈ cons x✝ s✝, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s✝ : WSeq (WSeq α)
ej : nil.append s✝.think.join = ss.think
m : a ∈ nil.append s✝.think.join
this : Seq.destruct (nil.append s✝.think.join) = Seq.destruct ss.think
⊢ a ∈ nil ∨ ∃ s ∈ s✝.think, a ∈ s

Tactic:
simp at this

Goal state after:
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s✝ : WSeq (WSeq α)
ej : nil.append s✝.think.join = ss.think
m : a ∈ nil.append s✝.think.join
this : s✝.join = ss
⊢ a ∈ nil ∨ ∃ s ∈ s✝.think, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s✝ : WSeq α
ej : s✝.think.append S.join = ss.think
m : a ∈ s✝.think.append S.join
this : Seq.destruct (s✝.think.append S.join) = Seq.destruct ss.think
⊢ a ∈ s✝.think ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp at this

Goal state after:
α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
s✝ : WSeq α
ej : s✝.think.append S.join = ss.think
m : a ∈ s✝.think.append S.join
this : s✝.append S.join = ss
⊢ a ∈ s✝.think ∨ ∃ s ∈ S, a ∈ s
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
ej : nil.append nil.join = ss.think
m : a ∈ nil.append nil.join
this : Seq.destruct (nil.append nil.join) = Seq.destruct ss.think
⊢ a ∈ nil ∨ ∃ s ∈ nil, a ∈ s

Tactic:
simp at this

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

Goal state before:
pp: α : Type u
a : α
ss✝ : WSeq α
h : a ∈ ss✝
ss : WSeq α
IH : ∀ (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 = ss.think
m : a ∈ (cons x✝ s✝).append S.join
this : Seq.destruct ((cons x✝ s✝).append S.join) = Seq.destruct ss.think
⊢ a ∈ cons x✝ s✝ ∨ ∃ s ∈ S, a ∈ s

Tactic:
simp at this

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

Goal state before:
pp: α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ Computation.LiftRel (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1) (map ret s).join.destruct s.destruct

Tactic:
apply liftRel_rec fun c1 c2 => ∃ s, c1 = destruct (join (map ret s)) ∧ c2 = destruct s

Goal state after:
case H
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∀ {ca cb : Computation (Option (α × WSeq α))},
    (∃ s, ca = (map ret s).join.destruct ∧ cb = s.destruct) →
      LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
        (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) ca.destruct cb.destruct

case Hc
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
⊢ ∃ s_1, (map ret s).join.destruct = (map ret s_1).join.destruct ∧ s.destruct = s_1.destruct