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

Goal state before:
pp: case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
⊢ Valid' o₁ (l.rotateL x (Ordnode.node rs rl rx rr)) o₂

Tactic:
Ordnode.rotateL_node

Goal state after:
case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : Valid' (↑x) (Ordnode.node rs rl rx rr) o₂
H1 : ¬l.size + (Ordnode.node rs rl rx rr).size ≤ 1
H2 : delta * l.size ≤ rl.size + rr.size
H3 : 2 * (rl.size + rr.size) ≤ 9 * l.size + 3 ∨ rl.size + rr.size ≤ 2
H3_0 : l.size = 0 → rl.size + rr.size ≤ 2
H3p : l.size > 0 → 2 * (rl.size + rr.size) ≤ 9 * l.size + 3
ablem : ∀ {a b : ℕ}, 1 ≤ a → a + b ≤ 2 → b ≤ 1
hlp : l.size > 0 → ¬rl.size + rr.size ≤ 1
⊢ Valid' o₁ (if rl.size < ratio * rr.size then l.node3L x rl rx rr else l.node4L x rl rx rr) o₂
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (l.rotateL x (node size✝ l✝ x✝ r✝)).Sized

Tactic:
Ordnode.rotateL_node

Goal state after:
case node
α : Type u_1
l : Ordnode α
x : α
hl : l.Sized
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : (node size✝ l✝ x✝ r✝).Sized
⊢ (if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).Sized
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
unfold balance'

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
hr : r.Sized
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if r.size > delta * l.size then l.rotateL x r
        else if l.size > delta * r.size then l.rotateR x r else l.node' x r).size =
    l.size + r.size + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P r.dual ∧ P x ∧ All P l.dual ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_dual, and_comm, and_left_comm, and_assoc]

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

Goal state before:
pp: α : Type u_1
x✝ ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
⊢ (node ls ll lx lr).splitMin' x r = ((node ls ll lx lr).findMin' x, (node x✝ (node ls ll lx lr) x r).eraseMin)

Tactic:
rw [splitMin', splitMin_eq ls ll lx lr, findMin', eraseMin]

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ::: P.M α ⟹ β ::: P.M β
x : P.M α
h : ∀ (x : P.M α), lastFun g x = dropFun g <$$> x
⊢ dropFun g = dropFun (dropFun g ::: fun x ↦ dropFun g <$$> x)

Tactic:
simp

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

Goal state before:
pp: case tail
P : PFunctor.{uA, uB}
R : P.M → P.M → Prop
this : Inhabited P.A
a : P.A
f f' : P.B a → P.M
ih : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : P.B a
a'' : P.A
g g' : P.B a'' → P.M
h₀ : (M.mk ⟨a, f⟩).dest = ⟨a'', g⟩
h₁ : (M.mk ⟨a, f'⟩).dest = ⟨a'', g'⟩
h₂ : ∀ (i : P.B a''), R (g i) (g' i)
⊢ R (f i) (f' i)

Tactic:
· simp only [dest_mk] at h₀ h₁
    cases h₀
    cases h₁
    apply h₂

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
⊢ ∃ a f_1 f',
    (f x).dest = ⟨a, f_1⟩ ∧
      (M.corec g x).dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), ∃ x', True ∧ f_1 i = f x' ∧ f' i = M.corec g x'

Tactic:
refine ⟨_, _, _, h₀, h₁, ?_⟩

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
h₁ : (M.corec g x).dest = ⟨a, M.corec g ∘ f'⟩
⊢ ∀ (i : P.B a), ∃ x', True ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: p : ℕ+
s : Multiset ℕ
hs : ∀ (p : ℕ), p ∈ s → Nat.Prime p
⊢ (∃ a h, ↑⟨a, ⋯⟩ = ↑p) ↔ ↑p ∈ s

Tactic:
simp

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

Goal state before:
pp: p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ 1 < PNat.find h ↔ ¬p 1

Tactic:
simp

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

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
by
  rw [← card_uIcc, Fintype.card_ofFinset]

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

Goal state before:
pp: case a
m n : ℕ+
⊢ m.factorMultiset ⊔ n.factorMultiset ≤ (m.lcm n).factorMultiset

Tactic:
· apply sup_le_iff.mpr; constructor <;> apply factorMultiset_le_iff.mpr
    · exact dvd_lcm_left m n
    · exact dvd_lcm_right m n

Goal state after:
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
⊢ ∀ (a b c : Σₗ' (i : ι), α i), a ≤ b → b ≤ c → a ≤ c

Tactic:
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨a₃, b₃⟩ ⟨h₁r⟩ ⟨h₂r⟩

Goal state after:
case left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a₃ : ι
b₃ : α a₃
a✝¹ : a₁ < a₂
a✝ : a₂ < a₃
⊢ ⟨a₁, b₁⟩ ≤ ⟨a₃, b₃⟩

case left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
a✝¹ : a₁ < a₂
b₂✝ : α a₂
a✝ : b₂ ≤ b₂✝
⊢ ⟨a₁, b₁⟩ ≤ ⟨a₂, b₂✝⟩

case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ : α a₁
a₃ : ι
b₃ : α a₃
b₂✝ : α a₁
a✝¹ : b₁ ≤ b₂✝
a✝ : a₁ < a₃
⊢ ⟨a₁, b₁⟩ ≤ ⟨a₃, b₃⟩

case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a₁ : ι
b₁ b₂✝¹ : α a₁
a✝¹ : b₁ ≤ b₂✝¹
b₂✝ : α a₁
a✝ : b₂✝¹ ≤ b₂✝
⊢ ⟨a₁, b₁⟩ ≤ ⟨a₁, b₂✝⟩
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r < u.bp + 1
⊢ u.r - 1 < u.bp

Tactic:
rw [← h₀] at h₁

Goal state after:
u : XgcdType
hr : u.r ≠ 0
h₀ : u.r - 1 + 1 = u.r
h₁ : u.r - 1 + 1 < u.bp + 1
⊢ u.r - 1 < u.bp
Module: Mathlib.Data.QPF.Multivariate.Basic

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

Tactic:
intro j

Goal state after:
case mpr.mpr
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
a : (P F).A
f : (P F).B a ⟹ α
xeq : abs ⟨a, f⟩ = x
h : ∀ (i : Fin2 n) (a' : (P F).A) (f' : (P F).B a' ⟹ α), abs ⟨a', f'⟩ = x → f i '' univ ⊆ f' i '' univ
p : (i : Fin2 n) → α i → Prop
h' : ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u
j : Fin2 n
⊢ ∀ (j_1 : (P F).B a j), p j (f j j_1)
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
⊢ mk (abs ⟨a, fun x ↦ ⟦f x⟧⟩) = ⟦WType.mk a f⟧

Tactic:
have : Fix.mk (abs ⟨a, fun x => ⟦f x⟧⟩) = ⟦Wrepr ⟨a, f⟩⟧ := by
    apply Quot.sound; apply Wequiv.abs'
    rw [PFunctor.W.dest_mk, abs_map, abs_repr, ← abs_map, PFunctor.map_eq]
    simp only [Wrepr, recF_eq, PFunctor.W.dest_mk, abs_repr, Function.comp]
    rfl

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

Goal state before:
pp: case isTrue
K : Type u_1
inst✝¹ : _root_.Field K
inst✝ : CharZero K
m : ℕ
s : Bool
e : ℕ
h✝ : s = true
⊢ ↑⟨↑m / ↑(10 ^ e), ⋯⟩ = ↑m / ↑(10 ^ e)

Tactic:
simp

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

Goal state before:
pp: case fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩
vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩
h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
a✝ : Fin2 n
⊢ ∀ (j : (P F).B a a✝.fs), α.RelLast R ((P F).appendContents f' f₀ a✝.fs j) ((P F).appendContents f' f₁ a✝.fs j)

Tactic:
intro j

Goal state after:
case fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u_1
Q : β → Prop
u v : β → Cofix F α
h :
  ∀ (x : β),
    Q x →
      ∃ a f' f₀ f₁,
        (u x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩ ∧
          (v x).dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩ ∧
            ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
x✝¹ : β
Qx : Q x✝¹
R : Cofix F α → Cofix F α → Prop := fun w z ↦ ∃ x', Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F α
x✝ : R x y
x' : β
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → Cofix F α
ux'eq : (u x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₀⟩
vx'eq : (v x').dest = MvQPF.abs ⟨a, (P F).appendContents f' f₁⟩
h' : ∀ (i : (P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x'
a✝ : Fin2 n
j : (P F).B a a✝.fs
⊢ α.RelLast R ((P F).appendContents f' f₀ a✝.fs j) ((P F).appendContents f' f₁ a✝.fs j)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: ⊢ 0 < 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
hn : r < 0
⊢ -1 ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
r : ℝ
hn : r.sign = -1
⊢ (-1)⁻¹ = -1

Tactic:
simp

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

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h :
  ∀ ⦃α : Type u⦄ (x : ↑(P F) α), {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ (∀ u ∈ f '' univ, p u) ↔ ∀ (i : (P F).B a), p (f i)

Tactic:
simp

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

Goal state before:
pp: case h_1
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
o✝ : α ⊕ List (Computation α)
a✝ : α
heq✝ :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a✝
⊢ ∃ a, Sum.inl a✝ = Sum.inl a

Tactic:
simp

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

Goal state before:
pp: case h_2
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
a : α
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH : pure a ∈ l → ∃ a, parallel.aux2 l = Sum.inl a
e : pure a = c
o✝ : α ⊕ List (Computation α)
ls✝ : List (Computation α)
heq✝ :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls✝
⊢ ∃ a_1, Sum.inl a = Sum.inl a_1

Tactic:
simp

Goal state after:
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
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ (corec' (fun x ↦ g Sum.inl Sum.inr x) x).dest = g _root_.id (corec₁ g) x

Tactic:
Cofix.dest_corec',

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ (TypeVec.id ::: Sum.elim _root_.id (corec' fun x ↦ g Sum.inl Sum.inr x)) <$$> g Sum.inl Sum.inr x =
    g _root_.id (corec₁ g) x
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
⊢ Function.swap (LiftRelO R C) none y = LiftRelO (Function.swap R) (Function.swap C) none y

Tactic:
rcases y with ⟨⟩ | ⟨hy, jy⟩

Goal state after:
case none.none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
⊢ Function.swap (LiftRelO R C) none none = LiftRelO (Function.swap R) (Function.swap C) none none

case none.some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hy : α
jy : WSeq α
⊢ Function.swap (LiftRelO R C) none (some (hy, jy)) = LiftRelO (Function.swap R) (Function.swap C) none (some (hy, jy))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
y : Option (α × WSeq α)
hx : β
jx : WSeq β
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) y = LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) y

Tactic:
rcases y with ⟨⟩ | ⟨hy, jy⟩

Goal state after:
case some.none
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) none = LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) none

case some.some
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
hx : β
jx : WSeq β
hy : α
jy : WSeq α
⊢ Function.swap (LiftRelO R C) (some (hx, jx)) (some (hy, jy)) =
    LiftRelO (Function.swap R) (Function.swap C) (some (hx, jx)) (some (hy, jy))
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case none
α : Type u
s✝ : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ match
    match
      match none with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c ↦
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    none with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c ↦
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
simp

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

Goal state before:
pp: case none
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : Std.Refl R
⊢ LiftRelO R (fun x1 x2 ↦ x1 = x2) none none

Tactic:
simp

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

Goal state before:
pp: case h_1
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
e : s.think = c
o✝ : α ⊕ List (Computation α)
a✝ : α
heq✝ :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inl a✝
⊢ Sum.inl a✝ = Sum.inr l' → s ∈ l'

Tactic:
simp

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

Goal state before:
pp: case some
α : Type u
s✝ : WSeq α
s'✝ s : Seq (Option α)
h : flatten (Computation.pure s) = s'✝
o : Option α
s' : Seq (Option α)
⊢ match
    match
      match some (o, s') with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun c ↦
              match c.destruct with
              | Sum.inl s =>
                match Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some (o, s') with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun c ↦
            match c.destruct with
            | Sum.inl s =>
              match Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
simp

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

Goal state before:
pp: case h_2
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c✝ : Computation α
T : c✝.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
S : WSeq (Computation α)
c : Computation α
l : List (Computation α)
IH' : s.think ∈ l → ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
e : s.think = c
o✝ : α ⊕ List (Computation α)
ls✝ : List (Computation α)
heq✝ :
  List.foldr
      (fun c o ↦
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls =>
          match c.destruct with
          | Sum.inl a => Sum.inl a
          | Sum.inr b => Sum.inr (b :: ls))
      (Sum.inr []) l =
    Sum.inr ls✝
⊢ s ∈ s :: ls✝

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
case pure
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
⊢ match a.destruct.destruct, a.destruct.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case pure.inl
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
val✝ : Option (α × WSeq α)
⊢ match Sum.inl val✝, Sum.inl val✝ with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

Tactic:
simp

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

Goal state before:
pp: case pure.inr
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
val✝ : Computation (Option (α × WSeq α))
⊢ match Sum.inr val✝, Sum.inr val✝ with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ c, s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

Tactic:
simp

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ (Option.rec nil Prod.snd none).destruct = tail.aux none

Tactic:
simp

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

Goal state before:
pp: α : Type u
s✝ : WSeq α
a : α
s : WSeq α
⊢ (Option.rec nil Prod.snd (some (a, s))).destruct = tail.aux (some (a, s))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Set.Finite.List

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
n : ℕ
x✝ : List α
⊢ x✝ ∈ {l | l.length < n} ↔ x✝ ∈ ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}

Tactic:
simp

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

Goal state before:
pp: case inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
have H2 : corec parallel.aux1 (l, S) = think _ := destruct_eq_think (by
        simp only [parallel.aux1, rmap, corec_eq]
        rw [h])

Goal state after:
case inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1 (l, S)).Terminates