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

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: α : Type u
s t : WSeq α
c1 : Computation (Option (α × WSeq α))
⊢ ∀ ⦃s₂ : Computation (Option (α × WSeq α))⦄,
    (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)) c1 s₂ →
      BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)) c1.destruct
        s₂.destruct

Tactic:
c2

Goal state after:
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
⊢ (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)) c1 c2 →
    BisimO (fun c1 c2 ↦ ∃ s t, c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)) c1.destruct
      c2.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
S : WSeq (WSeq α)
c1 : Computation (Option (α × WSeq α))
⊢ ∀ ⦃s₂ : Computation (Option (α × WSeq α))⦄,
    (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) c1 s₂ →
      BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) c1.destruct
        s₂.destruct

Tactic:
c2

Goal state after:
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
⊢ (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) c1 c2 →
    BisimO (fun c1 c2 ↦ c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux) c1.destruct
      c2.destruct
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✝)

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

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

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✝)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 : Computation β
⊢ ∀ ⦃s₂ : Computation β⦄,
    (fun c1 c2 ↦
          ∃ l S,
            c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
        c1 s₂ →
      BisimO
        (fun c1 c2 ↦
          ∃ l S,
            c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
        c1.destruct s₂.destruct

Tactic:
c2

Goal state after:
α : Type u
β : Type v
f : α → β
S : WSeq (Computation α)
c1 c2 : Computation β
⊢ (fun c1 c2 ↦
        ∃ l S,
          c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
      c1 c2 →
    BisimO
      (fun c1 c2 ↦
        ∃ l S,
          c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
      c1.destruct c2.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret nil).join.destruct.destruct
    nil.destruct.destruct

pp: case cons
α : Type u
s✝¹ s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
x✝ : α
s✝ : WSeq α
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret (cons x✝ s✝)).join.destruct.destruct
    (cons x✝ s✝).destruct.destruct

pp: case think
α : Type u
s✝¹ s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
s✝ : WSeq α
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s✝.think).join.destruct.destruct
    s✝.think.destruct.destruct

Tactic:
<;>

Goal state after:
case nil
α : Type u
s✝ s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret nil).join.destruct.destruct
    nil.destruct.destruct

case cons
α : Type u
s✝¹ s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
x✝ : α
s✝ : WSeq α
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret (cons x✝ s✝)).join.destruct.destruct
    (cons x✝ s✝).destruct.destruct

case think
α : Type u
s✝¹ s' s : WSeq α
h : (map ret s).join = s'
c1 c2 : Computation (Option (α × WSeq α))
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
s✝ : WSeq α
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s✝.think).join.destruct.destruct
    s✝.think.destruct.destruct
Module: Mathlib.Data.Sym.NatCard

Goal state before:
pp: case inr.zero
α : Type u_1
h✝ : Infinite α
⊢ Nat.card (Sym α 0) = (Nat.card α).multichoose 0

pp: case inr.succ
α : Type u_1
h✝ : Infinite α
n✝ : ℕ
⊢ Nat.card (Sym α (n✝ + 1)) = (Nat.card α).multichoose (n✝ + 1)

Tactic:
<;>

Goal state after:
case inr.zero
α : Type u_1
h✝ : Infinite α
⊢ Nat.card (Sym α 0) = (Nat.card α).multichoose 0

case inr.succ
α : Type u_1
h✝ : Infinite α
n✝ : ℕ
⊢ Nat.card (Sym α (n✝ + 1)) = (Nat.card α).multichoose (n✝ + 1)
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil.cons.refine_1
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
T : WSeq (WSeq α)
⊢ (s.append T.join).destruct = (s.append (nil.append T).join).destruct

pp: case nil.nil.cons.refine_2
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
T : WSeq (WSeq α)
⊢ (s.append T.join).destruct = (s.append (nil.join.append T.join)).destruct

Tactic:
<;>

Goal state after:
case nil.nil.cons.refine_1
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
T : WSeq (WSeq α)
⊢ (s.append T.join).destruct = (s.append (nil.append T).join).destruct

case nil.nil.cons.refine_2
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
s : WSeq α
T : WSeq (WSeq α)
⊢ (s.append T.join).destruct = (s.append (nil.join.append T.join)).destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil.think.refine_1
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ T.join.destruct = (nil.append (nil.append T).join).destruct

pp: case nil.nil.think.refine_2
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ T.join.destruct = (nil.append (nil.join.append T.join)).destruct

Tactic:
<;>

Goal state after:
case nil.nil.think.refine_1
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ T.join.destruct = (nil.append (nil.append T).join).destruct

case nil.nil.think.refine_2
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ T.join.destruct = (nil.append (nil.join.append T.join)).destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.think.refine_1
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T S : WSeq (WSeq α)
⊢ (nil.append (S.think.append T).join).destruct.tail = (nil.append (S.append T).join).destruct

pp: case nil.think.refine_2
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T S : WSeq (WSeq α)
⊢ (nil.append (S.think.join.append T.join)).destruct.tail = (nil.append (S.join.append T.join)).destruct

Tactic:
<;>

Goal state after:
case nil.think.refine_1
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T S : WSeq (WSeq α)
⊢ (nil.append (S.think.append T).join).destruct.tail = (nil.append (S.append T).join).destruct

case nil.think.refine_2
α : Type u
S✝ T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T S : WSeq (WSeq α)
⊢ (nil.append (S.think.join.append T.join)).destruct.tail = (nil.append (S.join.append T.join)).destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 : Computation (Option (α × WSeq α))
⊢ ∀ {cb : Computation (Option (α × WSeq α))},
    (∃ s S SS,
        c1 = (s.append (S.append SS.join).join).destruct ∧
          cb = (s.append (S.join.append (map join SS).join)).destruct) →
      LiftRelAux
        (LiftRelO Eq fun s1 s2 ↦
          ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
        (fun c1 c2 ↦
          ∃ s S SS,
            c1 = (s.append (S.append SS.join).join).destruct ∧
              c2 = (s.append (S.join.append (map join SS).join)).destruct)
        c1.destruct cb.destruct

Tactic:
c2

Goal state after:
α : Type u
SS : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
⊢ (∃ s S SS,
      c1 = (s.append (S.append SS.join).join).destruct ∧ c2 = (s.append (S.join.append (map join SS).join)).destruct) →
    LiftRelAux
      (LiftRelO Eq fun s1 s2 ↦
        ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join))
      (fun c1 c2 ↦
        ∃ s S SS,
          c1 = (s.append (S.append SS.join).join).destruct ∧
            c2 = (s.append (S.join.append (map join SS).join)).destruct)
      c1.destruct c2.destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil.cons.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ (cons S SS).join.join.destruct.tail = (nil.append (S.append SS.join).join).destruct

pp: case nil.nil.cons.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ (map join (cons S SS)).join.destruct.tail = (nil.append (S.join.append (map join SS).join)).destruct

Tactic:
<;>

Goal state after:
case nil.nil.cons.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ (cons S SS).join.join.destruct.tail = (nil.append (S.append SS.join).join).destruct

case nil.nil.cons.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
S : WSeq (WSeq α)
SS : WSeq (WSeq (WSeq α))
⊢ (map join (cons S SS)).join.destruct.tail = (nil.append (S.join.append (map join SS).join)).destruct
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.nil.think.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ SS.think.join.join.destruct.tail = (nil.append (nil.append SS.join).join).destruct

pp: case nil.nil.think.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ (map join SS.think).join.destruct.tail = (nil.append (nil.join.append (map join SS).join)).destruct

Tactic:
<;>

Goal state after:
case nil.nil.think.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ SS.think.join.join.destruct.tail = (nil.append (nil.append SS.join).join).destruct

case nil.nil.think.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
⊢ (map join SS.think).join.destruct.tail = (nil.append (nil.join.append (map join SS).join)).destruct
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case mp.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₁
⊢ c ∈ sumLift₂ f g (inl a) b →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

pp: case mp.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₂
⊢ c ∈ sumLift₂ f g (inr a) b →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
<;>

Goal state after:
case mp.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₁
⊢ c ∈ sumLift₂ f g (inl a) b →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

case mp.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
c : γ₁ ⊕ γ₂
a : α₂
⊢ c ∈ sumLift₂ f g (inr a) b →
    (∃ a₁ b₁ c₁, inr a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inr a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case nil.think.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ (nil.append (S.think.append SS.join).join).destruct.tail = (nil.append (S.append SS.join).join).destruct

pp: case nil.think.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ (nil.append (S.think.join.append (map join SS).join)).destruct.tail =
    (nil.append (S.join.append (map join SS).join)).destruct

Tactic:
<;>

Goal state after:
case nil.think.refine_1
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ (nil.append (S.think.append SS.join).join).destruct.tail = (nil.append (S.append SS.join).join).destruct

case nil.think.refine_2
α : Type u
SS✝ : WSeq (WSeq (WSeq α))
s1 s2 : WSeq α
h : ∃ s S SS, s1 = s.append (S.append SS.join).join ∧ s2 = s.append (S.join.append (map join SS).join)
c1 c2 : Computation (Option (α × WSeq α))
SS : WSeq (WSeq (WSeq α))
S : WSeq (WSeq α)
⊢ (nil.append (S.think.join.append (map join SS).join)).destruct.tail =
    (nil.append (S.join.append (map join SS).join)).destruct
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this✝ : c.Terminates
this : (parallel S).Terminates
⊢ a ∈ parallel S

Tactic:
exact mem_of_promises _ (parallel_promises H)

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

Goal state before:
pp: case mpr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
h : c ∈ f a b
⊢ inl c ∈ sumLift₂ f g (inl a) (inl b)

pp: case mpr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
h : c ∈ g a b
⊢ inr c ∈ sumLift₂ f g (inr a) (inr b)

Tactic:
<;>

Goal state after:
case mpr.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
h : c ∈ f a b
⊢ inl c ∈ sumLift₂ f g (inl a) (inl b)

case mpr.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₂
b : β₂
c : γ₂
h : c ∈ g a b
⊢ inr c ∈ sumLift₂ f g (inr a) (inr b)
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_1.left
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅

pp: case refine_1.right
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅

Tactic:
<;>

Goal state after:
case refine_1.left
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₁ : α₁) (b₁ : β₁), a = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅

case refine_1.right
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
h : sumLift₂ f g a b = ∅
⊢ ∀ (a₂ : α₂) (b₂ : β₂), a = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
Module: Mathlib.Data.Sum.Interval

Goal state before:
pp: case refine_2.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val✝ : α₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝ = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝ = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝) b = ∅

pp: case refine_2.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val✝ : α₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝ = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝ = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝) b = ∅

Tactic:
<;>

Goal state after:
case refine_2.inl
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val✝ : α₁
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inl val✝ = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inl val✝ = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inl val✝) b = ∅

case refine_2.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
b : β₁ ⊕ β₂
val✝ : α₂
h :
  (∀ (a₁ : α₁) (b₁ : β₁), inr val✝ = inl a₁ → b = inl b₁ → f a₁ b₁ = ∅) ∧
    ∀ (a₂ : α₂) (b₂ : β₂), inr val✝ = inr a₂ → b = inr b₂ → g a₂ b₂ = ∅
⊢ sumLift₂ f g (inr val✝) b = ∅