mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simp

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.think.destruct t.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.think.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
simp

Goal state after:
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:
simp

Goal state after:
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: α : Type u_1
x : αᵒᵖ
⊢ {x}.unop = {unop x}

Tactic:
by
  ext
  constructor
  · apply op_injective
  · apply unop_injective

Goal state after:
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: α : Type u_1
x : α
⊢ {op x}.unop = {x}

Tactic:
by
  ext
  constructor
  · apply op_injective
  · apply unop_injective

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
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
⊢ a ∈ cons a' s' ↔ a = a' ∨ a ∈ s'

Tactic:
dsimp only [cons, Membership.mem, WSeq.Mem, Seq.Mem, Seq.cons]

Goal state after:
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
i1 : x✝ = a'
i2 : s✝ = s'
⊢ Any (fun b ↦ some (some a) = b) (some (some a') :: ↑s') ↔ a = a' ∨ Any (fun b ↦ some (some a) = b) ↑s'
Module: Mathlib.Data.WSeq.Basic

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

Tactic:
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:
simp

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

Goal state before:
pp: α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h✝ : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : some (some c) = S.get? 0
H : S.destruct = some (some c, S.tail)
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
C :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match some (some c, S.tail) with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ c ∈ c :: l'

Tactic:
simp

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ Seq.map some ↑(a :: l) = Seq.cons (some a) (Seq.map some ↑l)

Tactic:
simp

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

Goal state before:
pp: case none.none
α : 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
h : LiftRelO R (LiftRel R) none none
⊢ 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)) none) (Option.map (Prod.map f2 (map f2)) none)

Tactic:
simp

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

Goal state before:
pp: α : Type u
l : List α
s : WSeq α
s1 s2 : Computation (List α)
l' : List α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, nil) ∧
    s2 =
      Computation.map (fun x ↦ l.reverse ++ x)
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', nil))
⊢ BisimO
    (fun c1 c2 ↦
      ∃ l' s,
        c1 =
            Computation.corec
              (fun x ↦
                match x with
                | (l, s) =>
                  match Seq.destruct s with
                  | none => Sum.inl l.reverse
                  | some (none, s') => Sum.inr (l, s')
                  | some (some a, s') => Sum.inr (a :: l, s'))
              (l' ++ l, s) ∧
          c2 =
            Computation.map (fun x ↦ l.reverse ++ x)
              (Computation.corec
                (fun x ↦
                  match x with
                  | (l, s) =>
                    match Seq.destruct s with
                    | none => Sum.inl l.reverse
                    | some (none, s') => Sum.inr (l, s')
                    | some (some a, s') => Sum.inr (a :: l, s'))
                (l', s)))
    (Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, nil)).destruct
    (Computation.map (fun x ↦ l.reverse ++ x)
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', nil))).destruct

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Setoid.Partition.Card

Goal state before:
pp: case hj
α : Type u_1
P : Set (Set α)
hP : IsPartition P
s : Set α
hs : s.Finite
hst : ∀ (t : Set α), (s ∩ t).Finite
hst' : ∀ (t : Set α), Nat.card ↑(s ∩ t) = ⋯.toFinset.card
hs' : Function.HasFiniteSupport fun t ↦ (s ∩ ↑t).ncard
⊢ Set.MapsTo (fun x ↦ ⟨⟨⋯.choose, ⋯⟩, x⟩) ↑hs.toFinset ↑(⋯.toFinset.sigma fun t ↦ ⋯.toFinset)

Tactic:
intro x
      simp only [Set.Finite.mem_toFinset, Finset.mem_sigma, Function.mem_support, Set.mem_inter_iff,
        Finset.mem_coe]
      intro hx
      refine ⟨Nat.card_ne_zero.mpr ⟨?_, hst (hP.right x).exists.choose⟩,
        hx, (hP.2 x).exists.choose_spec.2⟩
      simp only [nonempty_subtype, Set.mem_inter_iff]
      use x, hx, (hP.2 x).exists.choose_spec.2

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

Goal state before:
pp: case refine_1
α : Type u
l : List α
s✝ : WSeq α
s1 s2 : Computation (List α)
l' : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, cons a s) ∧
    s2 =
      Computation.map (fun x ↦ l.reverse ++ x)
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', cons a s))
⊢ (Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, cons a s)).tail =
    Computation.corec
      (fun x ↦
        match x with
        | (l, s) =>
          match Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (a :: l' ++ l, s)

Tactic:
simp

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

Goal state before:
pp: case refine_2
α : Type u
l : List α
s✝ : WSeq α
s1 s2 : Computation (List α)
l' : List α
a : α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, cons a s) ∧
    s2 =
      Computation.map (fun x ↦ l.reverse ++ x)
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', cons a s))
⊢ (Computation.map (fun x ↦ l.reverse ++ x)
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', cons a s))).tail =
    Computation.map (fun x ↦ l.reverse ++ x)
      (Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (a :: l', s))

Tactic:
simp

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x✝¹ x✝ : (i : ι) × α i
⊢ x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹ → x✝¹ < x✝

Tactic:
rintro ⟨⟨i, a, b, hab⟩, h⟩
        rw [mk_le_mk_iff] at h
        exact mk_lt_mk_iff.2 (hab.lt_of_not_ge h)

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

Goal state before:
pp: case inr.inr.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
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val✝
ad : a' ∈ c'
e : d = c'
⊢ a' ∈ c

Tactic:
rw [destruct_eq_think h]

Goal state after:
case inr.inr.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
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
a' : α
d : Computation α
dm : d ∈ c' :: val✝
ad : a' ∈ c'
e : d = c'
⊢ a' ∈ c'.think
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case refine_1
α : Type u
l : List α
s✝ : WSeq α
s1 s2 : Computation (List α)
l' : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s.think) ∧
    s2 =
      Computation.map (fun x ↦ l.reverse ++ x)
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s.think))
⊢ (Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s.think)).tail =
    Computation.corec
      (fun x ↦
        match x with
        | (l, s) =>
          match Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l' ++ l, s)

Tactic:
simp

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

Goal state before:
pp: case refine_2
α : Type u
l : List α
s✝ : WSeq α
s1 s2 : Computation (List α)
l' : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l' ++ l, s.think) ∧
    s2 =
      Computation.map (fun x ↦ l.reverse ++ x)
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s.think))
⊢ (Computation.map (fun x ↦ l.reverse ++ x)
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l', s.think))).tail =
    Computation.map (fun x ↦ l.reverse ++ x)
      (Computation.corec
        (fun x ↦
          match x with
          | (l, s) =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a :: l, s'))
        (l', s))

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u
⊢ [] ∈ (↑[]).toList

Tactic:
simp

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

Goal state before:
pp: case some
α : Type u
s : Seq α
a : α
⊢ (match
      match Option.map (fun a' ↦ (a', (Seq.map some s).tail)) (Option.map some (some a)) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun s ↦
            match Option.map (fun a' ↦ (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b)) =
    Sum.inl (Option.map (fun a ↦ (a, Seq.map some s.tail)) (some a))

Tactic:
simp

Goal state after:
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:
simp

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iic a)) ↔
    ⟨i, b⟩ ≤ ⟨i, a⟩

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Iio a)) ↔
    ⟨i, b⟩ < ⟨i, a⟩

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ici a)) ↔
    ⟨i, a⟩ ≤ ⟨i, b⟩

Tactic:
simp

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

Goal state before:
pp: case inr
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ (⟨j, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ici a)) ↔
    ⟨i, a⟩ ≤ ⟨j, b⟩

Tactic:
· simp [hij, le_def]

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

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderTop (α i)
x✝¹ x✝ : (i : ι) × α i
i : ι
a b : α i
⊢ (⟨i, b⟩ ∈
      match ⟨i, a⟩ with
      | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk i) (Ioi a)) ↔
    ⟨i, a⟩ < ⟨i, b⟩

Tactic:
simp

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

Goal state before:
pp: c : Char
cs₁ cs₂ : List Char
i₁ i₂ : Pos.Raw
⊢ ltb { s := ofList (c :: { s := ofList cs₁, i := i₁ }.s.toList), i := { s := ofList cs₁, i := i₁ }.i + c }
      { s := ofList (c :: { s := ofList cs₂, i := i₂ }.s.toList), i := { s := ofList cs₂, i := i₂ }.i + c } =
    ltb { s := ofList (c :: cs₁), i := i₁ + c } { s := ofList (c :: cs₂), i := i₂ + c }

Tactic:
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 β))
h : c1 = (map f nil).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) nil.destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f nil).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) nil.destruct).destruct

Tactic:
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 β))
x✝ : α
s✝ : WSeq α
h : c1 = (map f (cons x✝ s✝)).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (cons x✝ s✝).destruct
⊢ BisimO (fun c1 c2 ↦ ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f (cons x✝ s✝)).destruct.destruct
    (Computation.map (Option.map (Prod.map f (map f))) (cons x✝ s✝).destruct).destruct

Tactic:
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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: l : List Char
⊢ (ofList l).length = l.length

Tactic:
simp

Goal state after:
Module: Mathlib.Data.SubtypeNeLift

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i : ι
⊢ subtypeNeLift i (fun i_1 ↦ φ ↑i_1) (φ i) i = φ i

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = (nil.append nil).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux nil)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (nil.append nil).destruct.destruct (nil.destruct.bind (destruct_append.aux nil)).destruct

Tactic:
simp

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

Goal state before:
pp: α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
x✝ : α
s✝ : WSeq α
h : c1 = (nil.append (cons x✝ s✝)).destruct ∧ c2 = nil.destruct.bind (destruct_append.aux (cons x✝ s✝))
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    (nil.append (cons x✝ s✝)).destruct.destruct (nil.destruct.bind (destruct_append.aux (cons x✝ s✝))).destruct

Tactic:
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:
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 α
x✝ : α
s✝ : WSeq α
h : c1 = ((cons x✝ s✝).append t).destruct ∧ c2 = (cons x✝ s✝).destruct.bind (destruct_append.aux t)
⊢ BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    ((cons x✝ s✝).append t).destruct.destruct ((cons x✝ s✝).destruct.bind (destruct_append.aux t)).destruct

Tactic:
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:
simp

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

Goal state before:
pp: case inl
α : 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
c : Computation (Option (α × WSeq α))
val✝ : Option (α × WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) (Sum.inl val✝)
    (Sum.inl val✝)

Tactic:
simp

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

Goal state before:
pp: case inr
α : 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
c val✝ : Computation (Option (α × WSeq α))
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) (Sum.inr val✝)
    (Sum.inr val✝)

Tactic:
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
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    nil.join.destruct.destruct (nil.destruct.bind destruct_join.aux).destruct

Tactic:
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
x✝ : WSeq α
s✝ : WSeq (WSeq α)
⊢ BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    (cons x✝ s✝).join.destruct.destruct ((cons x✝ s✝).destruct.bind destruct_join.aux).destruct

Tactic:
simp

Goal state after: