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

Goal state before:
pp: case node.bal.right.right
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
t_l_valid : Valid' (Option.map f a₁) (map f l✝) (Option.map f ↑x✝)
t_l_size : (map f l✝).size = l✝.size
t_r_valid : Valid' (Option.map f ↑x✝) (map f r✝) (Option.map f a₂)
t_r_size : (map f r✝).size = r✝.size
⊢ (map f r✝).Balanced

Tactic:
exact t_r_valid.bal

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

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ l', Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ r', Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
⊢ Raised ((erase x t_l).size + t_r.size + 1) (t_l.size + t_r.size + 1)

Tactic:
repeat apply Raised.add_right

Goal state after:
case right
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ t_l t_x t_r) a₂
t_l_valid : Valid' a₁ (erase x t_l) ↑t_x
t_l_size : Raised (erase x t_l).size t_l.size
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
h_balanceable :
  (∃ l', Raised (erase x t_l).size l' ∧ BalancedSz l' t_r.size) ∨
    ∃ r', Raised r' t_r.size ∧ BalancedSz (erase x t_l).size r'
⊢ Raised (erase x t_l).size t_l.size
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h
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 → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
r'xy : r' x y
⊢ (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest

Tactic:
cases r'xy with
    | inl h =>
      rw [h]
    | inr r'xy =>
      have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
      rw [← Quot.factor_mk_eq _ _ this]
      dsimp [r']
      rw [appendFun_comp_id]
      rw [@comp_map _ _ q _ _ _ (appendFun id (Quot.mk r)),
        @comp_map _ _ q _ _ _ (appendFun id (Quot.mk r))]
      rw [h _ _ r'xy]

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

Goal state before:
pp: case mk.mk
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x✝ : Fix F
a : (P F).A
f : (P F).B a → WType (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid) (f a))
⊢ ∀ (i : (P F).B a), p ⟦f i⟧

Tactic:
convert! ih

Goal state after:
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 : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
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)
⊢ IsPrecongr r'

Tactic:
intro a b r'ab

Goal state after:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h' : ∀ (x : Cofix F), r x x
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
x✝ : Cofix F
x : (P F).M
y✝ : Cofix F
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)
a b : (P F).M
r'ab : r' a b
⊢ abs ((P F).map (Quot.mk r') a.dest) = abs ((P F).map (Quot.mk r') b.dest)
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: ⊢ 0 < 1

Tactic:
by simp

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

Goal state before:
pp: case inr.inr
z : ℤ
hp : 0 < z
⊢ (↑z).sign = ↑z.sign

Tactic:
· rw [sign_of_pos (Int.cast_pos.mpr hp), Int.sign_eq_one_of_pos hp, Int.cast_one]

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

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

Tactic:
by simp

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

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

pp: case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ) →
    ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u

Tactic:
· intro h
    have : Liftp (· ∈ supp x) x := by rw [h]; intro u; exact id
    rw [liftp_iff] at this
    rcases this with ⟨a, f, xeq, h'⟩
    refine ⟨a, f, xeq.symm, ?_⟩
    intro a' f' h''
    rintro u ⟨i, _, hfi⟩
    have : u ∈ supp x := by rw [← hfi]; apply h'
    exact (mem_supp x u).mp this _ _ h''

Goal state after:
case mpr
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ (∃ a f, abs ⟨a, f⟩ = x ∧ ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ) →
    ∀ (p : α → Prop), Liftp p x ↔ ∀ u ∈ supp x, p u
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : 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 : α
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, pure a ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
l

Goal state after:
α : 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 : α
l : List (Computation α)
⊢ ∀ {S : WSeq (Computation α)}, pure a ∈ l → (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : 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 α)}, s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates

Tactic:
l

Goal state after:
α : 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 α)}, s.think ∈ l → (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s✝¹ : WSeq α
t✝ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝¹.destruct t✝.destruct
s✝ : WSeq α
t : WSeq β
h✝ : (fun s t ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s✝ t
h : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t.destruct
s : WSeq α
⊢ ∀ (t : WSeq β), LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
t

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s✝¹ : WSeq α
t✝¹ : WSeq β
h✝¹ : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝¹.destruct t✝¹.destruct
s✝ : WSeq α
t✝ : WSeq β
h✝ : (fun s t ↦ LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct) s✝ t✝
h : Computation.LiftRel (LiftRelO R (LiftRel R)) s✝.destruct t✝.destruct
s : WSeq α
t : WSeq β
⊢ LiftRel R s t → LiftRel R s t ∨ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case succ
α : Type u_1
sel : Set α → Option α
a : α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
m k : ℕ
ih : ∀ {s : Set α}, enumerate sel s k = some a → enumerate sel s (k + m) = some a → k = k + m
s : Set α
h₁ : enumerate sel s (k + 1) = some a
h₂ : enumerate sel s (k + 1 + m) = some a
⊢ k + 1 = k + 1 + m

Tactic:
| succ k ih =>

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
n : ℕ
a : Option (α × WSeq α)
b : Option (β × WSeq β)
o : LiftRelO R (LiftRel R) a b
x✝ : LiftRelO R (LiftRel R) none none
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (tail.aux none) (tail.aux none)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
s : WSeq α
⊢ ∀ {t : WSeq α}, s ~ʷ t → ∀ {o : Option α}, o ∈ s.head → o ∈ t.head

Tactic:
t

Goal state after:
α : Type u
s t : WSeq α
⊢ s ~ʷ t → ∀ {o : Option α}, o ∈ s.head → o ∈ t.head
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: α : Type u_1
s✝ : Set α
K : s✝.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty ↑s
n : ℕ
⊢ ∅ ⊆ ∅

Tactic:
by simp

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

Goal state before:
pp: α : Type u
s : WSeq α
b a : α
⊢ some (b, s) ∈ (cons b s).destruct

Tactic:
by simp

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 β), LiftRel R s t → S s t

Tactic:
t

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

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
n : ℕ
⊢ s.drop n ~ʷ t.drop n

Tactic:
induction n <;> simp [*, tail_congr, drop]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h : LiftRel R s t
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)},
    LiftRelO R (LiftRel R) a b →
      LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x)
        (Option.map (Prod.map f1 (map f1)) a) (Option.map (Prod.map f2 (map f2)) b)

Tactic:
intro o p h

Goal state after:
α : Type u
β : Type v
γ : Type w
δ : Type u_1
R : α → β → Prop
S : γ → δ → Prop
s1✝ : WSeq α
s2✝ : WSeq β
f1 : α → γ
f2 : β → δ
h1 : LiftRel R s1✝ s2✝
h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)
s1 : WSeq γ
s2 : WSeq δ
h✝¹ : (fun s1 s2 ↦ ∃ s t, s1 = map f1 s ∧ s2 = map f2 t ∧ LiftRel R s t) s1 s2
s : WSeq α
t : WSeq β
h✝ : LiftRel R s t
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
⊢ LiftRelO S (fun s1 s2 ↦ ∃ s, s1 = map f1 s ∧ ∃ x, s2 = map f2 x ∧ LiftRel R s x) (Option.map (Prod.map f1 (map f1)) o)
    (Option.map (Prod.map f2 (map f2)) p)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? (n + 1)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
have C : corec parallel.aux1 (l, S) = _ := destruct_eq_think (by
        simp only [corec_eq, rmap, parallel.aux1.eq_1]
        rw [h])
      rw [C]
      refine @Computation.think_terminates _ _ ?_
      have TT : ∀ l', Terminates (corec parallel.aux1 (l', S.tail)) := by
        intro
        apply IH _ _ _ (Or.inr _) T
        rw [a, Seq.get?_tail]
      rcases e : Seq.get? S 0 with - | o
      · grind [Seq.get?_zero_eq_none, Seq.get?_nil]
      · have D : Seq.destruct S = some (o, S.tail) := by
          dsimp [Seq.destruct]
          rw [e]
          rfl
        rw [D]
        cases o <;> simp [TT]

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

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

Tactic:
t

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

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

Tactic:
intro o p h

Goal state after:
α : Type u
β : Type v
R : α → β → Prop
s1✝ s2 : WSeq α
t1✝ t2 : WSeq β
h1 : LiftRel R s1✝ t1✝
h2 : LiftRel R s2 t2
s : WSeq α
t : WSeq β
h✝¹ : (fun s t ↦ LiftRel R s t ∨ ∃ s1 t1, s = s1.append s2 ∧ t = t1.append t2 ∧ LiftRel R s1 t1) s t
s1 : WSeq α
t1 : WSeq β
h✝ : LiftRel R s1 t1
o : Option (α × WSeq α)
p : Option (β × WSeq β)
h : LiftRelO R (LiftRel R) o p
⊢ Computation.LiftRel
    (LiftRelO R fun s t ↦ LiftRel R s t ∨ ∃ s1, s = s1.append s2 ∧ ∃ x, t = x.append t2 ∧ LiftRel R s1 x)
    (destruct_append.aux s2 o) (destruct_append.aux t2 p)
Module: Mathlib.Data.WSeq.Relation

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

Tactic:
t

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

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

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s✝ : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s.think).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.think.destruct
⊢ (map f s.think).destruct.tail = (map f s).destruct ∧
    (Computation.map (Option.map (Prod.map f (map f))) s.think.destruct).tail =
      Computation.map (Option.map (Prod.map f (map f))) s.destruct

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.String.Lemmas

Goal state before:
pp: a b : String
⊢ a ++ b = ofList (a.toList ++ b.toList)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
s t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t : WSeq α
h : c1 = (nil.append t.think).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux t.think)
⊢ (nil.append t.think).destruct.tail = (nil.append t).destruct ∧
    (nil.destruct.bind (destruct_append.aux t.think)).tail = nil.destruct.bind (destruct_append.aux t)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
s✝ t✝ : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
t s : WSeq α
h : c1 = (s.think.append t).destruct ∧ c2 = s.think.destruct.bind (destruct_append.aux t)
⊢ (s.think.append t).destruct.tail = (s.append t).destruct ∧
    (s.think.destruct.bind (destruct_append.aux t)).tail = s.destruct.bind (destruct_append.aux t)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
S✝ : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
S : WSeq (WSeq α)
⊢ S.think.join.destruct.tail = S.join.destruct ∧
    (S.think.destruct.bind destruct_join.aux).tail = S.destruct.bind destruct_join.aux

Tactic:
by simp

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

Goal state before:
pp: case think
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
s✝ : WSeq (WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    s✝.think.join.destruct.destruct (s✝.think.destruct.bind destruct_join.aux).destruct

Tactic:
case think S => exact Or.inr ⟨S, by simp⟩

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ map f S.join = nil.append (map f S.join)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ (map (map f) S).join = nil.append (map (map f) S).join

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ map f S.join = nil.append (map f S.join)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ (map (map f) S).join = nil.append (map (map f) S).join

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h : LiftRel (LiftRel R) S T
⊢ S.join = nil.append S.join

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h : LiftRel (LiftRel R) S T
⊢ T.join = nil.append T.join

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
S : WSeq (WSeq α)
T : WSeq (WSeq β)
h : LiftRel (LiftRel R) S T
⊢ LiftRel R nil nil

Tactic:
by simp

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

Goal state before:
pp: α : Type u
S T : WSeq (WSeq α)
⊢ (S.append T).join = nil.append (S.append T).join

Tactic:
by simp

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

Goal state before:
pp: α : Type u
S T : WSeq (WSeq α)
⊢ S.join.append T.join = nil.append (S.join.append T.join)

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
e : ℕ ↪ α := Infinite.natEmbedding α
n : ℕ
⊢ ¬s(e 0, e (n + 1)).IsDiag

Tactic:
by simp

Goal state after:
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
e : ℕ ↪ α := Infinite.natEmbedding α
x✝¹ x✝ : ℕ
⊢ (fun n ↦ ⟨s(e 0, e (n + 1)), ⋯⟩) x✝¹ = (fun n ↦ ⟨s(e 0, e (n + 1)), ⋯⟩) x✝ → x✝¹ = x✝

Tactic:
by simp

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

Goal state before:
pp: α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ SS.join.join = nil.append (nil.append SS.join).join

Tactic:
by simp

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

Goal state before:
pp: α : Type u
SS : WSeq (WSeq (WSeq α))
⊢ (map join SS).join = nil.append (nil.join.append (map join SS).join)

Tactic:
by simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : WSeq α
f : α → WSeq β
g : β → WSeq γ
⊢ (s.bind f).bind g ~ʷ s.bind fun x ↦ (f x).bind g

Tactic:
exact bind_assoc_comp s f g

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝ : ℕ
x : α
s : σ
xs : Vector α n✝
C : {n : ℕ} → Vector α n → Sort u_5
n : ℕ
v : Vector α n
nil : C Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (xs.snoc x)
⊢ C v.reverse.reverse = C v

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝¹ : ℕ
x✝ : α
s : σ
xs✝ : Vector α n✝¹
C : {n : ℕ} → Vector α n → Sort u_5
n✝ : ℕ
v : Vector α n✝
nil : C Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (x : α) → C xs → C (xs.snoc x)
n : ℕ
x : α
xs : Vector α n
r : C xs.reverse
⊢ C (xs.reverse.snoc x) = C (x ::ᵥ xs).reverse

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝ : ℕ
x : α
s : σ
xs : Vector α n✝
C : {n : ℕ} → Vector α n → Vector β n → Sort u_5
n : ℕ
v : Vector α n
w : Vector β n
nil : C Vector.nil Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C xs ys → C (xs.snoc x) (ys.snoc y)
⊢ C v.reverse.reverse w.reverse.reverse = C v w

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n✝¹ : ℕ
x✝ : α
s : σ
xs✝ : Vector α n✝¹
C : {n : ℕ} → Vector α n → Vector β n → Sort u_5
n✝ : ℕ
v : Vector α n✝
w : Vector β n✝
nil : C Vector.nil Vector.nil
snoc : {n : ℕ} → (xs : Vector α n) → (ys : Vector β n) → (x : α) → (y : β) → C xs ys → C (xs.snoc x) (ys.snoc y)
n : ℕ
x : α
y : β
xs : Vector α n
ys : Vector β n
r : C xs.reverse ys.reverse
⊢ C (xs.reverse.snoc x) (ys.reverse.snoc y) = C (x ::ᵥ xs).reverse (y ::ᵥ ys).reverse

Tactic:
by simp

Goal state after: