[GOAL]
α : Sort u_1
a : α
⊢ out (mk a) = a
[PROOFSTEP]
let h := (mk a).2
[GOAL]
α : Sort u_1
a : α
h : ∃ a_1, (fun b => a_1 = b) = (mk a).fst := (mk a).snd
⊢ out (mk a) = a
[PROOFSTEP]
show Classical.choose h = a
[GOAL]
α : Sort u_1
a : α
h : ∃ a_1, (fun b => a_1 = b) = (mk a).fst := (mk a).snd
⊢ Classical.choose h = a
[PROOFSTEP]
have := Classical.choose_spec h
[GOAL]
α : Sort u_1
a : α
h : ∃ a_1, (fun b => a_1 = b) = (mk a).fst := (mk a).snd
this : (fun b => Classical.choose h = b) = (mk a).fst
⊢ Classical.choose h = a
[PROOFSTEP]
exact cast (congr_fun this a).symm rfl
[GOAL]
α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ mk (out { fst := s, snd := h }) = { fst := s, snd := h }
[PROOFSTEP]
simp [mk]
[GOAL]
α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ { fst := fun b => out { fst := s, snd := h } = b,
      snd := (_ : ∃ a, (fun b => a = b) = fun b => out { fst := s, snd := h } = b) } =
    { fst := s, snd := h }
[PROOFSTEP]
congr
[GOAL]
case e_fst
α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ (fun b => out { fst := s, snd := h } = b) = s
[PROOFSTEP]
exact Classical.choose_spec h
[GOAL]
α : Sort u_1
a b : Erased α
h : out a = out b
⊢ a = b
[PROOFSTEP]
simpa using congr_arg mk h
[GOAL]
α : Sort u_1
β : Sort u_2
f : α → β
a : Erased α
⊢ out (map f a) = f (out a)
[PROOFSTEP]
simp [map]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529}, Functor.mapConst = Functor.map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
ext
[GOAL]
case h.h.h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝¹ : α✝
x✝ : Erased β✝
⊢ out (Functor.mapConst x✝¹ x✝) = out ((Functor.map ∘ Function.const β✝) x✝¹ x✝)
[PROOFSTEP]
simp [Functor.mapConst]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α : Type ?u.5529} (x : Erased α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ : Type ?u.5529
x✝ : Erased α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ : Type ?u.5529
x✝ : Erased α✝
⊢ out (id <$> x✝) = out x✝
[PROOFSTEP]
simp
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (x : Erased α) (y : Erased β),
    (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Seq.seq (Function.const β✝ <$> x✝) fun x => y✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : Erased α✝
y✝ : Erased β✝
⊢ out (SeqLeft.seqLeft x✝ fun x => y✝) = out (Seq.seq (Function.const β✝ <$> x✝) fun x => y✝)
[PROOFSTEP]
simp [Seq.seq, Functor.mapConst, SeqLeft.seqLeft]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (x : Erased α) (y : Erased β),
    (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : Erased α✝
y✝ : Erased β✝
⊢ out (SeqRight.seqRight x✝ fun x => y✝) = out (Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝)
[PROOFSTEP]
simp [Seq.seq, Functor.mapConst, SeqRight.seqRight]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (g : α → β) (x : Erased α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (Seq.seq (pure g✝) fun x => x✝) = g✝ <$> x✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ out (Seq.seq (pure g✝) fun x => x✝) = out (g✝ <$> x✝)
[PROOFSTEP]
simp [Seq.seq, Functor.mapConst, SeqRight.seqRight]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (f : α → β) (x : Erased α),
    (do
        let a ← x
        pure (f a)) =
      f <$> x
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (do
      let a ← x✝
      pure (f✝ a)) =
    f✝ <$> x✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (out do
      let a ← x✝
      pure (f✝ a)) =
    out (f✝ <$> x✝)
[PROOFSTEP]
simp
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (f : Erased (α → β)) (x : Erased α),
    (do
        let x_1 ← f
        x_1 <$> x) =
      Seq.seq f fun x_1 => x
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (do
      let x ← f✝
      x <$> x✝) =
    Seq.seq f✝ fun x => x✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (out do
      let x ← f✝
      x <$> x✝) =
    out (Seq.seq f✝ fun x => x✝)
[PROOFSTEP]
simp [Seq.seq]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (x : α) (f : α → Erased β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ out (pure x✝ >>= f✝) = out (f✝ x✝)
[PROOFSTEP]
simp
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β γ : Type ?u.5529} (x : Erased α) (f : α → Erased β) (g : β → Erased γ),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ γ✝ : Type ?u.5529
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ γ✝ : Type ?u.5529
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ out (x✝ >>= f✝ >>= g✝) = out (x✝ >>= fun x => f✝ x >>= g✝)
[PROOFSTEP]
simp
