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

Goal state before:
pp: case case2
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ decide
      ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
        { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr) =
    decide (s₁.curr < s₂.curr)

pp: case case2.hnc
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ ¬{ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr = { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr

Tactic:
·

Goal state after:
case case2
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ decide
      ({ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr <
        { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr) =
    decide (s₁.curr < s₂.curr)
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:
·

Goal state after:
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
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case case2.hnc
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ ¬{ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr = { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr

Tactic:
·

Goal state after:
case case2.hnc
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : ¬s₁.curr = s₂.curr
⊢ ¬{ s := ofList (c :: s₁.s.toList), i := s₁.i + c }.curr = { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.curr
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

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:
·

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')
h' : a' = a
⊢ ∃ 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 α)
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:
·

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')
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
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case nil.nil
⊢ ltb { s := ofList [], i := 0 } { s := ofList [], i := 0 } = true ↔ [] < []

pp: case nil.cons
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔ [] < head✝ :: tail✝

pp: case cons.nil
head✝ : Char
tail✝ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝ < s₂
⊢ ltb { s := ofList (head✝ :: tail✝), i := 0 } { s := ofList [], i := 0 } = true ↔ head✝ :: tail✝ < []

pp: case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝¹, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList (head✝¹ :: tail✝¹), i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝

Tactic:
·

Goal state after:
case nil.nil
⊢ ltb { s := ofList [], i := 0 } { s := ofList [], i := 0 } = true ↔ [] < []
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case nil.cons
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔ [] < head✝ :: tail✝

pp: case cons.nil
head✝ : Char
tail✝ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝ < s₂
⊢ ltb { s := ofList (head✝ :: tail✝), i := 0 } { s := ofList [], i := 0 } = true ↔ head✝ :: tail✝ < []

pp: case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝¹, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList (head✝¹ :: tail✝¹), i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝

Tactic:
·

Goal state after:
case nil.cons
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔ [] < head✝ :: tail✝
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (c₂ :: cs₂), i := 0 } = true

pp: case nil.cons.hb
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂

Tactic:
·

Goal state after:
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (c₂ :: cs₂), i := 0 } = true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case nil.cons.hb
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂

Tactic:
·

Goal state after:
case nil.cons.hb
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case cons.nil
head✝ : Char
tail✝ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝ < s₂
⊢ ltb { s := ofList (head✝ :: tail✝), i := 0 } { s := ofList [], i := 0 } = true ↔ head✝ :: tail✝ < []

pp: case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝¹, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList (head✝¹ :: tail✝¹), i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝

Tactic:
·

Goal state after:
case cons.nil
head✝ : Char
tail✝ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝ < s₂
⊢ ltb { s := ofList (head✝ :: tail✝), i := 0 } { s := ofList [], i := 0 } = true ↔ head✝ :: tail✝ < []
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case cons.nil.ha
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬ltb { s := ofList (c₁ :: cs₁), i := 0 } { s := ofList [], i := 0 } = true

pp: case cons.nil.hb
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬c₁ :: cs₁ < []

Tactic:
·

Goal state after:
case cons.nil.ha
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬ltb { s := ofList (c₁ :: cs₁), i := 0 } { s := ofList [], i := 0 } = true
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case cons.nil.hb
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬c₁ :: cs₁ < []

Tactic:
·

Goal state after:
case cons.nil.hb
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬c₁ :: cs₁ < []
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝¹, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList (head✝¹ :: tail✝¹), i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝

Tactic:
·

Goal state after:
case cons.cons
head✝¹ : Char
tail✝¹ : List Char
tail_ih✝ : ∀ (s₂ : List Char), ltb { s := ofList tail✝¹, i := 0 } { s := ofList s₂, i := 0 } = true ↔ tail✝¹ < s₂
head✝ : Char
tail✝ : List Char
⊢ ltb { s := ofList (head✝¹ :: tail✝¹), i := 0 } { s := ofList (head✝ :: tail✝), i := 0 } = true ↔
    head✝¹ :: tail✝¹ < head✝ :: tail✝
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 ↦
    ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct

pp: case r
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ ∃ s_1,
    (map f s).destruct = (map f s_1).destruct ∧
      Computation.map (Option.map (Prod.map f (map f))) s.destruct =
        Computation.map (Option.map (Prod.map f (map f))) s_1.destruct

Tactic:
·

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 ↦
    ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case pos
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : c₁ = c₂
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ } { s := ofList (c₂ :: cs₂), i := 0 + c₂ } = true ↔ c₁ :: cs₁ < c₂ :: cs₂

pp: case neg
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂

Tactic:
·

Goal state after:
case pos
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : c₁ = c₂
⊢ ltb { s := ofList (c₁ :: cs₁), i := 0 + c₁ } { s := ofList (c₂ :: cs₂), i := 0 + c₂ } = true ↔ c₁ :: cs₁ < c₂ :: cs₂
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: 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

pp: 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

Tactic:
·

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
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case neg
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂

Tactic:
·

Goal state after:
case neg
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
⊢ c₁ < c₂ ↔ c₁ :: cs₁ < c₂ :: cs₂
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: 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

Tactic:
·

Goal state after:
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.String.Basic

Goal state before:
pp: case neg.rel
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
h' : c₁ < c₂
⊢ c₁ < c₂

pp: case neg.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
h : ¬c₁ = c₁
h' : List.Lex (fun x1 x2 ↦ x1 < x2) cs₁ cs₂
⊢ c₁ < c₁

Tactic:
·

Goal state after:
case neg.rel
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
c₂ : Char
cs₂ : List Char
h : ¬c₁ = c₂
h' : c₁ < c₂
⊢ c₁ < c₂
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case neg.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
h : ¬c₁ = c₁
h' : List.Lex (fun x1 x2 ↦ x1 < x2) cs₁ cs₂
⊢ c₁ < c₁

Tactic:
·

Goal state after:
case neg.cons
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
cs₂ : List Char
h : ¬c₁ = c₁
h' : List.Lex (fun x1 x2 ↦ x1 < x2) cs₁ cs₂
⊢ c₁ < c₁
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case r
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ ∃ s_1,
    (map f s).destruct = (map f s_1).destruct ∧
      Computation.map (Option.map (Prod.map f (map f))) s.destruct =
        Computation.map (Option.map (Prod.map f (map f))) s_1.destruct

Tactic:
·

Goal state after:
case r
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ ∃ s_1,
    (map f s).destruct = (map f s_1).destruct ∧
      Computation.map (Option.map (Prod.map f (map f))) s.destruct =
        Computation.map (Option.map (Prod.map f (map f))) s_1.destruct
Module: Mathlib.Data.SubtypeNeLift

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

pp: case neg
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i₀ i : ι
h : ¬i = i₀
⊢ subtypeNeLift i₀ (fun i ↦ φ ↑i) (φ i₀) i = φ i

Tactic:
·

Goal state after:
case pos
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i₀ i : ι
h : i = i₀
⊢ subtypeNeLift i₀ (fun i ↦ φ ↑i) (φ i₀) i = φ i
Module: Mathlib.Data.SubtypeNeLift

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

Tactic:
·

Goal state after:
case neg
ι : Type u_1
inst✝ : DecidableEq ι
M : ι → Type u_2
φ : (i : ι) → M i
i₀ i : ι
h : ¬i = i₀
⊢ subtypeNeLift i₀ (fun i ↦ φ ↑i) (φ i₀) i = φ i
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join

pp: case r
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join

Tactic:
·

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim.nil
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (nil.append (map f S.join))) (Seq.destruct (nil.append (map (map f) S).join))

pp: case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
x✝ : β
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct ((cons x✝ s✝).append (map f S.join))) (Seq.destruct ((cons x✝ s✝).append (map (map f) S).join))

pp: case bisim.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s✝.think.append (map f S.join))) (Seq.destruct (s✝.think.append (map (map f) S).join))

Tactic:
·

Goal state after:
case bisim.nil
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (nil.append (map f S.join))) (Seq.destruct (nil.append (map (map f) S).join))
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
x✝ : β
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct ((cons x✝ s✝).append (map f S.join))) (Seq.destruct ((cons x✝ s✝).append (map (map f) S).join))

pp: case bisim.think
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s✝.think.append (map f S.join))) (Seq.destruct (s✝.think.append (map (map f) S).join))

Tactic:
·

Goal state after:
case bisim.cons
α : Type u
β : Type v
f : α → β
S✝ S : WSeq (WSeq α)
x✝ : β
s✝ : WSeq β
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct ((cons x✝ s✝).append (map f S.join))) (Seq.destruct ((cons x✝ s✝).append (map (map f) S).join))