mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case pos.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
⊢ (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).rotateR x (node rs rl rx rr) =
    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) (node lls lll llx llr) lx
                (node (size_1 + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          (node lrs lrl lrx lrr))
      (node lls lll llx llr)

Tactic:
dsimp [rotateR]

Goal state after:
case pos.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
⊢ (if lrs < ratio * lls then (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x (node rs rl rx rr)
    else (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x (node rs rl rx rr)) =
    if lrs < ratio * lls then
      node (ls + rs + 1) (node lls lll llx llr) lx (node (lrs + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
    else
      node (ls + rs + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + rs + 1) lrr x (node rs rl rx rr))
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
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⟩
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p (f i j)

Tactic:
use a, fun i j => (f i j).val

Goal state after:
case h
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)⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p ((fun i j ↦ ↑(f i j)) i j)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l r : Ordnode α
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (∃ l', Raised l' r.dual.size ∧ BalancedSz l' l.dual.size) ∨ ∃ r', Raised l.dual.size r' ∧ BalancedSz r.dual.size r'

Tactic:
rw [size_dual, size_dual]

Goal state after:
α : Type u_1
l r : Ordnode α
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (∃ l', Raised l' r.size ∧ BalancedSz l' l.size) ∨ ∃ r', Raised l.size r' ∧ BalancedSz r.size r'
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.dual.dual.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂

Tactic:
dual_dual,

Goal state after:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ((P F).map fixToW ⟨a, fun x ↦ ⟦f x⟧⟩) = abs (Wrepr (WType.mk a f)).dest

Tactic:
PFunctor.map_eq

Goal state after:
F : Type u → Type u
q : QPF F
a : (P F).A
f : (P F).B a → (P F).W
⊢ abs ⟨a, fixToW ∘ fun x ↦ ⟦f x⟧⟩ = abs (Wrepr (WType.mk a f)).dest
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ abs ⟨a, g₁ ∘ fun x ↦ ⟦f x⟧⟩ = abs ((P F).map g₂ ⟨a, fun x ↦ ⟦f x⟧⟩)

Tactic:
PFunctor.map_eq

Goal state after:
case mk.mk
F : Type u → Type u
q : QPF F
α : Type u
g₁ g₂ : Fix F → α
h : ∀ (x : F (Fix F)), g₁ <$> x = g₂ <$> x → g₁ (mk x) = g₂ (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), g₁ (Quot.mk (⇑Wsetoid) (f a)) = g₂ (Quot.mk (⇑Wsetoid) (f a))
⊢ abs ⟨a, g₁ ∘ fun x ↦ ⟦f x⟧⟩ = abs ⟨a, g₂ ∘ fun x ↦ ⟦f x⟧⟩
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
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih : (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' = x'
| x'

Tactic:
rw [← ih]

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Fix F α → Type u
g : (x : F (α ::: Sigma β)) → β (mk ((TypeVec.id ::: Sigma.fst) <$$> x))
x : Fix F α
y : Sigma β := rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x
x' : F (α ::: Fix F α)
ih : (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x' = x'
| (TypeVec.id ::: fun x ↦ (rec (fun i ↦ ⟨mk ((TypeVec.id ::: Sigma.fst) <$$> i), g i⟩) x).fst) <$$> x'
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs ⟨a, f₀⟩
dyeq : y.dest = abs ⟨a, f₁⟩
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ abs ⟨a, Quot.mk r ∘ f₀⟩ = abs ((P F).map (Quot.mk r) ⟨a, f₁⟩)

Tactic:
PFunctor.map_eq

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs ⟨a, f₀⟩
dyeq : y.dest = abs ⟨a, f₁⟩
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ abs ⟨a, Quot.mk r ∘ f₀⟩ = abs ⟨a, Quot.mk r ∘ f₁⟩
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⟩ →
    α
⊢ (P F₂).map (fun x ↦ f <$> x) ⟨b, fun x ↦ abs ⟨h x, fun y ↦ g ⟨x, y⟩⟩⟩ =
    ⟨({ 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) }.map
            f ⟨⟨b, h⟩, g⟩).fst.fst,
      fun x ↦
      abs
        ⟨({ 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) }.map
                  f ⟨⟨b, h⟩, g⟩).fst.snd
            x,
          fun y ↦
          ({ 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) }.map
                f ⟨⟨b, h⟩, g⟩).snd
            ⟨x, y⟩⟩⟩

Tactic:
PFunctor.map_eq

Goal state after:
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⟩ →
    α
⊢ ⟨b, (fun x ↦ f <$> x) ∘ fun x ↦ abs ⟨h x, fun y ↦ g ⟨x, y⟩⟩⟩ =
    ⟨({ 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) }.map
            f ⟨⟨b, h⟩, g⟩).fst.fst,
      fun x ↦
      abs
        ⟨({ 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) }.map
                  f ⟨⟨b, h⟩, g⟩).fst.snd
            x,
          fun y ↦
          ({ 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) }.map
                f ⟨⟨b, h⟩, g⟩).snd
            ⟨x, y⟩⟩⟩
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ((P F).map g ⟨a, f⟩)) = g '' supp (abs ⟨a, f⟩)

Tactic:
PFunctor.map_eq

Goal state after:
F : Type u → Type u
q : QPF F
h : IsUniform
α β : Type u
g : α → β
x : F α
a : (P F).A
f : (P F).B a → α
⊢ supp (abs ⟨a, g ∘ f⟩) = g '' supp (abs ⟨a, f⟩)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h1.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
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
a' : α
⊢ F l (Sum.inl a') →
    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'))
            (Sum.inl a')) =
        Sum.inl a →
      ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
intro this

Goal state after:
case h1.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
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
a' : α
this : F l (Sum.inl a')
⊢ 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'))
          (Sum.inl a')) =
      Sum.inl a →
    ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h1.inr
α : 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
l' : List (Computation α)
⊢ F l (Sum.inr l') →
    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'))
            (Sum.inr l')) =
        Sum.inl a →
      ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
intro this

Goal state after:
case h1.inr
α : 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
l' : List (Computation α)
this : F l (Sum.inr l')
⊢ 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'))
          (Sum.inr l')) =
      Sum.inl a →
    ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2.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
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
a' : α
⊢ F l (Sum.inl a') →
    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'))
            (Sum.inl a')) =
        Sum.inr C' →
      ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
intro this

Goal state after:
case h2.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
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
a' : α
this : F l (Sum.inl a')
⊢ 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'))
          (Sum.inl a')) =
      Sum.inr C' →
    ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h2.inr
α : 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
l' : List (Computation α)
⊢ F l (Sum.inr l') →
    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'))
            (Sum.inr l')) =
        Sum.inr C' →
      ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
intro this

Goal state after:
case h2.inr
α : 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
l' : List (Computation α)
this : F l (Sum.inr l')
⊢ 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'))
          (Sum.inr l')) =
      Sum.inr C' →
    ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case h1.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
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
a' : α
this : F l (Sum.inl a)
h' : a' = a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rcases this with ⟨c, cl, ac⟩

Goal state after:
case h1.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
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
a' : α
h' : a' = a
c : Computation α
cl : c ∈ l
ac : a ∈ c
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h2
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
⊢ ∀ (s : WSeq α),
    (∀ (s_1 : WSeq α) (S : WSeq (WSeq α)), s_1.append S.join = s → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s) →
      ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)),
        s_1.append S.join = s.think → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s

Tactic:
intro ss IH s S ej m
    induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip] <;>
      have := congr_arg Seq.destruct ej
    case nil.cons | nil.think | think => simp at this; simp_all
    case nil.nil | cons => simp at this

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

Goal state before:
pp: case h2.inr
α : 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
l' : List (Computation α)
this : F l (Sum.inr l')
h' :
  corec parallel.aux1
      ((fun l' ↦
          match Seq.destruct S with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c

Tactic:
rcases e : Seq.destruct S with - | a <;> rw [e] at h'

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

case h2.inr.some
α : 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
l' : List (Computation α)
this : F l (Sum.inr l')
a : Seq1 (Option (Computation α))
h' :
  corec parallel.aux1
      ((fun l' ↦
          match some a with
          | none => (l', Seq.nil)
          | some (none, S') => (l', S')
          | some (some c, S') => (c :: l', S'))
        l') =
    C'
e : Seq.destruct S = some a
⊢ ∃ c, (c ∈ l ∨ c ∈ S) ∧ a✝ ∈ c
Module: Mathlib.Data.Tree.Traversable

Goal state before:
pp: case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : BinaryTree α
hl : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r)
⊢ traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (node v l r) =
    Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g (node v l r))

Tactic:
rw [traverse, hl, hr, traverse]

Goal state after:
case node
α : Type u_1
F : Type u → Type v
G : Type v → Type w
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
β : Type v
γ : Type u
f : β → F γ
g : α → G β
v : α
l r : BinaryTree α
hl : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) l = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l)
hr : traverse (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) r = Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r)
⊢ node <$> (Functor.Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) v <*> Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g l) <*>
      Functor.Comp.mk ((fun x ↦ traverse f x) <$> traverse g r) =
    Functor.Comp.mk ((fun x ↦ traverse f x) <$> (node <$> g v <*> traverse g l <*> traverse g r))
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
h : S.head ~> none
x✝ : (parallel S).Terminates
a : α
m : a ∈ parallel S
⊢ False

Tactic:
by
    let ⟨c, cs, _⟩ := exists_of_mem_parallel m
    let ⟨n, nm⟩ := WSeq.exists_get?_of_mem cs
    let ⟨c', h'⟩ := WSeq.head_some_of_get?_some nm
    injection h h'

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
⊢ mapAccumr f xs s = (s, map (fun x ↦ (f x s).2) xs)

Tactic:
induction xs using revInductionOn

Goal state after:
case nil
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
⊢ mapAccumr f nil s = (s, map (fun x ↦ (f x s).2) nil)

case snoc
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
s : σ
h : ∀ (a : α), (f a s).1 = s
n✝ : ℕ
xs✝ : Vector α n✝
x✝ : α
a✝ : mapAccumr f xs✝ s = (s, map (fun x ↦ (f x s).2) xs✝)
⊢ mapAccumr f (xs✝.snoc x✝) s = (s, map (fun x ↦ (f x s).2) (xs✝.snoc x✝))
Module: Mathlib.Data.WSeq.Productive

Goal state before:
pp: α : Type u
s : WSeq α
inst✝ : s.Productive
n : ℕ
h : (fun n ↦ (s.get? n).get) n = none
⊢ (fun n ↦ (s.get? n).get) (n + 1) = none

Tactic:
by
    cases e : Computation.get (get? s (n + 1))
    · assumption
    have := Computation.mem_of_get_eq _ e
    simp only [get?] at this h
    obtain ⟨a', h'⟩ := head_some_of_head_tail_some this
    have := mem_unique h' (@Computation.mem_of_get_eq _ _ _ _ h)
    contradiction

Goal state after: