α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
⊢ destruct ({ hOrElse := fun a b => OrElse.orElse a b }.1 (think c₁) fun x => think c₂) =
    Sum.inr ({ hOrElse := fun a b => OrElse.orElse a b }.1 c₁ fun x => c₂)
α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
⊢ destruct (HOrElse.hOrElse (think c₁) fun x => think c₂) = Sum.inr (HOrElse.hOrElse c₁ fun x => c₂)
unfold HOrElse.hOrElse instHOrElse
α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
⊢ destruct
      ({
            hOrElse := fun a b =>
              {
                    orElse :=
                      (let src := monad;
                        Alternative.mk empty @orElse).3 }.1
                a b }.1
        (think c₁) fun x => think c₂) =
    Sum.inr
      ({
            hOrElse := fun a b =>
              {
                    orElse :=
                      (let src := monad;
                        Alternative.mk empty @orElse).3 }.1
                a b }.1
        c₁ fun x => c₂)
α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
⊢ destruct ({ hOrElse := fun a b => OrElse.orElse a b }.1 (think c₁) fun x => think c₂) =
    Sum.inr ({ hOrElse := fun a b => OrElse.orElse a b }.1 c₁ fun x => c₂)
unfold OrElse.orElse instOrElse Alternative.orElse instAlternativeComputation
no goals
α : Type u
β : Type v
γ : Type w
c₁ c₂ : Computation α
⊢ destruct
      ({
            hOrElse := fun a b =>
              {
                    orElse :=
                      (let src := monad;
                        Alternative.mk empty @orElse).3 }.1
                a b }.1
        (think c₁) fun x => think c₂) =
    Sum.inr
      ({
            hOrElse := fun a b =>
              {
                    orElse :=
                      (let src := monad;
                        Alternative.mk empty @orElse).3 }.1
                a b }.1
        c₁ fun x => c₂)
simp [orElse]