awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.W.Basic
Goal:
α : Type u_1
β : α → Type u_2
inst : (a : α) → Fintype (β a)
inst_1 : (a : α) → Encodable (β a)
inst_2 : Encodable α
h' : (n : ℕ) → Encodable (WType' β n)
f : WType β → (n : ℕ) × WType' β n :=
  fun (t : WType β) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ WType' β n) (t.depth (β := β))
      (Subtype.mk (p := fun (t_1 : WType β) ↦ t_1.depth (β := β) ≤ t.depth (β := β)) t ⋯)
finv : (n : ℕ) × WType' β n → WType β :=
  fun (p : (n : ℕ) × WType' β n) ↦ (↑(p.snd (β := fun (n : ℕ) ↦ WType' β n)) : WType β)
this : ∀ (t : WType β), finv (f t) = t
⊢ Encodable (WType β)

Tactic:
exact Encodable.ofLeftInverse f finv this

Premises used: Encodable.ofLeftInverse
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
simp_rw :
  (sum fun (i : α) ↦ lift.{v, max u v} #(WType β) ^ lift.{max u v, v} #(β i)) =
    sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)
⊢ #((a : α) × (β a → WType β)) = sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)

Tactic:
simp_rw [mk_sigma, mk_arrow]

Premises used: Cardinal.mk_arrow, Cardinal.mk_sigma
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
rw : (sum fun (i : α) ↦ #(WType β) ^ lift.{max u v, v} #(β i)) = sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)
rw₁ rw₂ : (sum fun (i : α) ↦ #(WType β) ^ lift.{u, v} #(β i)) = sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)
⊢ (sum fun (i : α) ↦ lift.{v, max u v} #(WType β) ^ lift.{max u v, v} #(β i)) =
    sum fun (a : α) ↦ #(WType β) ^ lift.{u, v} #(β a)

Tactic:
rw [lift_id'.{v, u}, lift_umax.{v, u}]
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
κ : Cardinal.{max u v}
hκ : (sum fun (a : α) ↦ κ ^ lift.{u, v} #(β a)) ≤ κ
mk : ∀ (γ : Type (max u v)) (hκ : (sum fun (a : α) ↦ #γ ^ lift.{u, v} #(β a)) ≤ #γ), #(WType β) ≤ #γ
⊢ #(WType β) ≤ κ

Tactic:
induction κ using Cardinal.inductionOn with | _ γ
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun (a : α) ↦ #γ ^ lift.{u, v} #(β a)) ≤ #γ
⊢ (sum fun (a : α) ↦ #γ ^ lift.{max u v, v} #(β a)) ≤ #γ

Tactic:
simp_rw [← lift_umax.{v, u}] at hκ
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun (a : α) ↦ #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ (sum fun (a : α) ↦ lift.{v, max v u} #γ ^ lift.{max u v, v} #(β a)) ≤ #γ

Tactic:
nth_rewrite 1 [← lift_id'.{v, u} #γ] at hκ
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (sum fun (a : α) ↦ lift.{v, max v u} #γ ^ lift.{max u v, v} #(β a)) ≤ #γ
⊢ Nonempty ((i : α) × (β i → γ) ↪ γ)

Tactic:
simp_rw [← mk_arrow, ← mk_sigma, le_def] at hκ

Premises used: Cardinal.mk_arrow, Cardinal.mk_sigma, Cardinal.le_def
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : Nonempty ((i : α) × (β i → γ) ↪ γ)
mk : ∀ (hκ : (i : α) × (β i → γ) ↪ γ), #(WType β) ≤ #γ
⊢ #(WType β) ≤ #γ

Tactic:
obtain ⟨hκ⟩ := hκ
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (i : α) × (β i → γ) ↪ γ
⊢ #(WType β) ≤ #γ

Tactic:
Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)

Premises used: Function.Embedding.inj', WType.elim_injective, Cardinal.mk_le_of_injective, Function.Embedding.toFun
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
γ : Type (max u v)
hκ : (i : α) × (β i → γ) ↪ γ
⊢ #(WType β) ≤ #γ

Tactic:
exact Cardinal.mk_le_of_injective (elim_injective _ hκ.1 hκ.2)

Premises used: Function.Embedding.inj', WType.elim_injective, Cardinal.mk_le_of_injective, Function.Embedding.toFun
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
h : IsEmpty α
⊢ #(WType β) ≤ max (lift.{v, u} #α) ℵ₀

Tactic:
simp
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
hn : Nonempty α
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
rw : LE.le (α := Cardinal.{max u v}) 1 (⨆ (a : α), m ^ lift.{u, v} #(β a))
⊢ LE.le (α := Cardinal.{max u v}) (Order.succ 0) (⨆ (a : α), m ^ lift.{u, v} #(β a))

Tactic:
rw [succ_zero]

Premises used: Cardinal.succ_zero
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
hn : Nonempty α
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
⊢ Nonempty α

Tactic:
hn
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
hn : Nonempty α
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
obtain : ∀ (a : α), LE.le (α := Cardinal.{max u v}) 1 (⨆ (a : α), m ^ lift.{u, v} #(β a))
⊢ LE.le (α := Cardinal.{max u v}) 1 (⨆ (a : α), m ^ lift.{u, v} #(β a))

Tactic:
obtain ⟨a⟩ : Nonempty α := hn

Premises used: Nonempty
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
⊢ LE.le (α := Cardinal.{max u v}) 1 (⨆ (a : α), m ^ lift.{u, v} #(β a))

Tactic:
le_trans ?_ (le_ciSup bddAbove_of_small a)

Premises used: le_ciSup, Cardinal.bddAbove_of_small, le_trans
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
refine : 1 ≤ m ^ lift.{u, v} #(β a)
⊢ LE.le (α := Cardinal.{max u v}) 1 (⨆ (a : α), m ^ lift.{u, v} #(β a))

Tactic:
refine le_trans ?_ (le_ciSup bddAbove_of_small a)

Premises used: le_ciSup, Cardinal.bddAbove_of_small, le_trans
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
rw : HPow.hPow (β := Cardinal.{max u v}) m 0 ≤ m ^ lift.{u, v} #(β a)
rw₁ : Cardinal.{max u v}
⊢ 1 ≤ m ^ lift.{u, v} #(β a)

Tactic:
rw [← power_zero]

Premises used: Cardinal.power_zero
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type v
inst : ∀ (a : α), Finite.{v + 1} (β a)
m : Cardinal.{max u v} := max (lift.{v, u} #α) ℵ₀
a : α
⊢ HPow.hPow (β := Cardinal.{max u v}) m 0 ≤ m ^ lift.{u, v} #(β a)

Tactic:
power_le_power_left
                      (pos_iff_ne_zero.1 (aleph0_pos.trans_le (le_max_right _ _))) zero_le

Premises used: le_max_right, zero_le, LT.lt.trans_le, Iff.mp, Cardinal.aleph0_pos, pos_iff_ne_zero, Cardinal.power_le_power_left
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type u
⊢ (sum fun (a : α) ↦ #(WType β) ^ lift.{u, u} #(β a)) = sum fun (a : α) ↦ #(WType β) ^ #(β a)

Tactic:
simp_rw [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ simp_rw : (sum fun (a : α) ↦ κ ^ #(β a)) ≤ κ
⊢ (sum fun (a : α) ↦ κ ^ lift.{u, u} #(β a)) ≤ κ

Tactic:
simp_rw [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun (a : α) ↦ κ ^ #(β a)) ≤ κ
⊢ (sum fun (a : α) ↦ κ ^ #(β a)) ≤ κ

Tactic:
hκ
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun (a : α) ↦ κ ^ #(β a)) ≤ κ
⊢ (sum fun (a : α) ↦ κ ^ #(β a)) ≤ κ

Tactic:
exact hκ
-- Module: Mathlib.Data.W.Cardinal
Goal:
α : Type u
β : α → Type u
inst : ∀ (a : α), Finite.{u + 1} (β a)
rw rw₁ : max #α ℵ₀ = max #α ℵ₀
⊢ max (lift.{u, u} #α) ℵ₀ = max #α ℵ₀

Tactic:
rw [lift_id]

Premises used: Cardinal.lift_id
-- Module: Mathlib.Data.W.Constructions
Goal:
f : Natβ Natα.zero → WType Natβ
e_f : Empty.elim = f
⊢ mk (β := Natβ) Natα.zero Empty.elim = mk (β := Natβ) Natα.zero f

Tactic:
congr
-- Module: Mathlib.Data.W.Constructions
Goal:
f : Natβ Natα.zero → WType Natβ
e_f : ∀ (x : Empty), x.elim = f x
⊢ Empty.elim = f

Tactic:
ext x
-- Module: Mathlib.Data.W.Constructions
Goal:
f : Natβ Natα.zero → WType Natβ
x : Empty
⊢ x.elim = f x

Tactic:
cases x
-- Module: Mathlib.Data.W.Constructions
Goal:
f : Natβ Natα.succ → WType Natβ
simp : (fun (x : Natβ Natα.succ) ↦ f ()) = f
⊢ ofNat (mk (β := Natβ) Natα.succ f).toNat = mk (β := Natβ) Natα.succ f

Tactic:
simp only [toNat, ofNat, leftInverse_nat (f ()), mk.injEq, heq_eq_eq, true_and]

Premises used: Unit.unit, WType.toNat, WType.mk.injEq, heq_eq_eq, WType.ofNat, true_and
-- Module: Mathlib.Data.W.Constructions
Goal:
f : Natβ Natα.succ → WType Natβ
⊢ (fun (x : Natβ Natα.succ) ↦ f ()) = f

Tactic:
rfl
-- Module: Mathlib.Data.W.Constructions
Goal:
n : ℕ
rw : toNat (mk (β := Natβ) Natα.succ fun (x : Natβ Natα.succ) ↦ ofNat n) = n.succ
rw₁ : (ofNat n).toNat.succ = n.succ
rw₂ rw₃ : n.succ = n.succ
⊢ (ofNat n.succ).toNat = n.succ

Tactic:
rw [ofNat, toNat, rightInverse_nat n]

Premises used: WType.toNat, WType.ofNat
-- Module: Mathlib.Data.W.Constructions
Goal:
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
simp : PEmpty.elim = f
⊢ ofList γ (toList γ (mk (β := Listβ γ) Listα.nil f)) = mk (β := Listβ γ) Listα.nil f

Tactic:
simp only [toList, ofList, mk.injEq, heq_eq_eq, true_and]

Premises used: WType.ofList, WType.toList, WType.mk.injEq, heq_eq_eq, true_and
-- Module: Mathlib.Data.W.Constructions
Goal:
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
h : ∀ (x : PEmpty.{u + 1}), x.elim = f x
⊢ PEmpty.elim = f

Tactic:
ext x
-- Module: Mathlib.Data.W.Constructions
Goal:
γ : Type u
f : Listβ γ Listα.nil → WType (Listβ γ)
x : PEmpty.{u + 1}
⊢ x.elim = f x

Tactic:
cases x
-- Module: Mathlib.Data.W.Constructions
Goal:
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
simp : (fun (x : Listβ γ (Listα.cons x)) ↦ f PUnit.unit) = f
⊢ ofList γ (toList γ (mk (β := Listβ γ) (Listα.cons x) f)) = mk (β := Listβ γ) (Listα.cons x) f

Tactic:
simp only [toList, ofList, leftInverse_list (f PUnit.unit), mk.injEq, heq_eq_eq, true_and]

Premises used: WType.ofList, WType.toList, WType.mk.injEq, heq_eq_eq, PUnit.unit, true_and
-- Module: Mathlib.Data.W.Constructions
Goal:
γ : Type u
x : γ
f : Listβ γ (Listα.cons x) → WType (Listβ γ)
⊢ (fun (x : Listβ γ (Listα.cons x)) ↦ f PUnit.unit) = f

Tactic:
rfl
-- Module: Mathlib.Data.W.Constructions
Goal:
γ : Type u
hd : γ
tl : List γ
⊢ toList γ (ofList γ (hd :: tl)) = hd :: tl

Tactic:
simp [rightInverse_list tl]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
⊢ a ∉ nil

Tactic:
Seq.notMem_nil (some a)

Premises used: Option.some, Stream'.Seq.notMem_nil, Stream'.WSeq.nil, Stream'.WSeq.Mem
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Computation (Option (α × WSeq α))) (destruct nil) (Computation.pure none)

Tactic:
Computation.destruct_eq_pure rfl

Premises used: Computation.destruct_eq_pure, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
⊢ (cons a s).destruct.destruct = Sum.inl (some (a, s))

Tactic:
simp [destruct, cons, Computation.rmap]

Premises used: Stream'.WSeq.destruct, Stream'.WSeq.cons, Computation.rmap
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ s.think.destruct.destruct = Sum.inr s.destruct

Tactic:
simp [destruct, think, Computation.rmap]

Premises used: Stream'.WSeq.destruct, Computation.rmap, Stream'.WSeq.think
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Option (Seq1 (Option α))) (Seq.destruct nil) none

Tactic:
rfl

Premises used: Stream'.Seq.destruct, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
⊢ Seq.destruct (cons a s) = some (some a, s)

Tactic:
Seq.destruct_cons _ _

Premises used: Stream'.WSeq.cons, Stream'.WSeq, Stream'.Seq.destruct_cons
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ Seq.destruct s.think = some (none, s)

Tactic:
Seq.destruct_cons _ _

Premises used: Stream'.WSeq.think, Stream'.WSeq, Stream'.Seq.destruct_cons
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Computation (Option α)) (head nil) (Computation.pure none)

Tactic:
simp [head]

Premises used: Stream'.WSeq.head
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
a : α
s : WSeq α
⊢ (cons a s).head = Computation.pure (some a)

Tactic:
simp [head]

Premises used: Stream'.WSeq.head
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ s.think.head = s.head.think

Tactic:
simp [head]

Premises used: Stream'.WSeq.head
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
⊢ flatten (Computation.pure s) = s

Tactic:
Seq.eq_of_bisim (fun s1 s2 => flatten (Computation.pure s2) = s1) ?_ rfl

Premises used: Stream'.Seq.eq_of_bisim, Stream'.WSeq.flatten, Computation.pure, Stream'.WSeq, Eq, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s : WSeq α
refine : Seq.IsBisimulation.{u} (α := Option α) fun (s1 s2 : Seq (Option α)) ↦ flatten (Computation.pure s2) = s1
⊢ flatten (Computation.pure s) = s

Tactic:
refine Seq.eq_of_bisim (fun s1 s2 => flatten (Computation.pure s2) = s1) ?_ rfl

Premises used: Stream'.Seq.eq_of_bisim, Stream'.WSeq.flatten, Computation.pure, Eq, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
rw :
  Seq.BisimO (fun (s1 s2 : Seq (Option α)) ↦ flatten (Computation.pure s2) = s1)
    (Seq.destruct (flatten (Computation.pure s))) s.destruct
⊢ Seq.BisimO (fun (s1 s2 : Seq (Option α)) ↦ flatten (Computation.pure s2) = s1) s'.destruct s.destruct

Tactic:
rw [← h]
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
simp :
  match (motive := Option (Seq1 (Option α)) → Option (Seq1 (Option α)) → Prop)
    match (motive := Option (Option α × Computation (WSeq α)) → Option (Option α × Seq (Option α)))
      match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α))) s.destruct with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun (c : Computation (WSeq α)) ↦
              match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
              | Sum.inl s =>
                match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                  Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun (c : Computation (WSeq α)) ↦
            match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
            | Sum.inl s =>
              match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False
⊢ Seq.BisimO (fun (s1 s2 : Seq (Option α)) ↦ flatten (Computation.pure s2) = s1)
    (Seq.destruct (flatten (Computation.pure s))) s.destruct

Tactic:
simp only [Seq.BisimO, flatten, Seq.omap, pure_def, Seq.corec_eq, destruct_pure]

Premises used: Computation.destruct_pure, Stream'.Seq.omap, Stream'.WSeq.flatten, Stream'.Seq.corec_eq, Computation.pure_def, Stream'.Seq.BisimO
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 : WSeq α
s' s : Seq (Option α)
h : flatten (Computation.pure s) = s'
⊢ match (motive := Option (Seq1 (Option α)) → Option (Seq1 (Option α)) → Prop)
    match (motive := Option (Option α × Computation (WSeq α)) → Option (Option α × Seq (Option α)))
      match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α))) none with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun (c : Computation (WSeq α)) ↦
              match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
              | Sum.inl s =>
                match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                  Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    none with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun (c : Computation (WSeq α)) ↦
            match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
            | Sum.inl s =>
              match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
s_1 : WSeq α
s'_1 s : Seq (Option α)
h : flatten (Computation.pure s) = s'_1
o : Option α
s' : Seq (Option α)
⊢ match (motive := Option (Seq1 (Option α)) → Option (Seq1 (Option α)) → Prop)
    match (motive := Option (Option α × Computation (WSeq α)) → Option (Option α × Seq (Option α)))
      match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α))) some (o, s') with
      | none => none
      | some (a, b) => some (a, Computation.pure b) with
    | none => none
    | some (a, b) =>
      some
        (a,
          Seq.corec
            (fun (c : Computation (WSeq α)) ↦
              match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
              | Sum.inl s =>
                match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                  Seq.destruct s with
                | none => none
                | some (a, b) => some (a, Computation.pure b)
              | Sum.inr c' => some (none, c'))
            b),
    some (o, s') with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      Seq.corec
          (fun (c : Computation (WSeq α)) ↦
            match (motive := WSeq α ⊕ Computation (WSeq α) → Option (Option α × Computation (WSeq α))) c.destruct with
            | Sum.inl s =>
              match (motive := Option (Option α × WSeq α) → Option (Option α × Computation (WSeq α)))
                Seq.destruct s with
              | none => none
              | some (a, b) => some (a, Computation.pure b)
            | Sum.inr c' => some (none, c'))
          (Computation.pure s') =
        s
  | x, x_1 => False

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c : Computation (WSeq α)
⊢ Seq.destruct (flatten c.think) = some (none, flatten c)

Tactic:
simp [flatten]

Premises used: Stream'.WSeq.flatten
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c : Computation (WSeq α)
⊢ (flatten c).destruct = c >>= destruct

Tactic:
Computation.eq_of_bisim
      (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct) ?_
      (Or.inr ⟨c, rfl, rfl⟩)

Premises used: Stream'.WSeq.destruct, Exists, Stream'.WSeq.flatten, And, And.intro, Exists.intro, Or, Computation.eq_of_bisim, Computation.bind, Eq, Or.inr, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c : Computation (WSeq α)
c1 :
  Computation.IsBisimulation.{u} (α := Option (α × WSeq α)) fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
    c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
⊢ (flatten c).destruct = c >>= destruct

Tactic:
refine
    Computation.eq_of_bisim
      (fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = destruct (flatten c) ∧ c2 = Computation.bind c destruct) ?_
      (Or.inr ⟨c, rfl, rfl⟩)

Premises used: Stream'.WSeq.destruct, Exists, Stream'.WSeq.flatten, And, And.intro, Exists.intro, Or, Computation.eq_of_bisim, Computation.bind, Eq, Or.inr, rfl
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c_1 : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (Option (α × WSeq α))
inl :
  ∀ (val : Option (α × WSeq α)),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
      (Sum.inl val) (Sum.inl val)
inr :
  ∀ (val : Computation (Option (α × WSeq α))),
    BisimO
      (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
        c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
      (Sum.inr val) (Sum.inr val)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    c.destruct c.destruct

Tactic:
cases c.destruct

Premises used: Computation.destruct
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c_1 : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c : Computation (Option (α × WSeq α))
val : Option (α × WSeq α)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (Sum.inl val) (Sum.inl val)

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c_1 : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
c val : Computation (Option (α × WSeq α))
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (Sum.inr val) (Sum.inr val)

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
pure :
  match (motive :=
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
    a.destruct.destruct, a.destruct.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct)
    (flatten (Computation.pure a)).destruct.destruct ((Computation.pure a).bind destruct).destruct

Tactic:
simp
-- Module: Mathlib.Data.WSeq.Basic
Goal:
α : Type u
c : Computation (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ (c : Computation (WSeq α)), c1 = (flatten c).destruct ∧ c2 = c.bind destruct
a : WSeq α
pure :
  ∀ (val : Option (α × WSeq α)),
    match (motive :=
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
        Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
      Sum.inl val, Sum.inl val with
    | Sum.inl a, Sum.inl a' => a = a'
    | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
    | x, x_1 => False
pure₁ :
  ∀ (val : Computation (Option (α × WSeq α))),
    match (motive :=
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
        Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
      Sum.inr val, Sum.inr val with
    | Sum.inl a, Sum.inl a' => a = a'
    | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
    | x, x_1 => False
⊢ match (motive :=
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) →
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)) → Prop)
    a.destruct.destruct, a.destruct.destruct with
  | Sum.inl a, Sum.inl a' => a = a'
  | Sum.inr s, Sum.inr s' => s = s' ∨ ∃ (c : Computation (WSeq α)), s = (flatten c).destruct ∧ s' = c.bind destruct
  | x, x_1 => False

Tactic:
cases (destruct a).destruct

Premises used: Stream'.WSeq.destruct, Computation.destruct