[GOAL]
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ (Seq.seq x fun x => f <$> y) = Seq.seq ((fun x => x ∘ f) <$> x) fun x => y
[PROOFSTEP]
simp [← pure_seq]
[GOAL]
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ (Seq.seq x fun x => Seq.seq (pure f) fun x => y) = Seq.seq (Seq.seq (pure fun x => x ∘ f) fun x_1 => x) fun x => y
[PROOFSTEP]
simp [seq_assoc, ← comp_map, (· ∘ ·)]
[GOAL]
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
x : F (α → β)
f : γ → α
y : F γ
⊢ (Seq.seq ((fun x x_1 => x (f x_1)) <$> x) fun x => y) =
    Seq.seq (Seq.seq (pure fun x x_1 => x (f x_1)) fun x_1 => x) fun x => y
[PROOFSTEP]
simp [pure_seq]
[GOAL]
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ (f <$> Seq.seq x fun x => y) = Seq.seq ((fun x => f ∘ x) <$> x) fun x => y
[PROOFSTEP]
simp only [← pure_seq]
[GOAL]
α β γ : Type u
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
f : β → γ
x : F (α → β)
y : F α
⊢ (Seq.seq (pure f) fun x_1 => Seq.seq x fun x => y) = Seq.seq (Seq.seq (pure fun x => f ∘ x) fun x_1 => x) fun x => y
[PROOFSTEP]
simp [seq_assoc]
[GOAL]
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : α → m β
f : β → γ
⊢ f <$> (x >>= g) = do
    let a ← x
    f <$> g a
[PROOFSTEP]
rw [← bind_pure_comp, bind_assoc]
[GOAL]
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : α → m β
f : β → γ
⊢ (do
      let x ← x
      let a ← g x
      pure (f a)) =
    do
    let a ← x
    f <$> g a
[PROOFSTEP]
simp [bind_pure_comp]
[GOAL]
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : β → m γ
f : α → β
⊢ f <$> x >>= g = x >>= g ∘ f
[PROOFSTEP]
rw [← bind_pure_comp, bind_assoc]
[GOAL]
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : β → m γ
f : α → β
⊢ (x >>= fun x => pure (f x) >>= g) = x >>= g ∘ f
[PROOFSTEP]
simp [pure_bind, (· ∘ ·)]
[GOAL]
α✝ β✝ γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β : Type u
f : α → m β
⊢ f >=> pure = f
[PROOFSTEP]
simp only [(· >=> ·), functor_norm]
[GOAL]
α✝ β✝ γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → m β
⊢ pure >=> f = f
[PROOFSTEP]
simp only [(· >=> ·), functor_norm]
[GOAL]
α✝ β✝ γ✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_1
β γ φ : Type u
f : α → m β
g : β → m γ
h : γ → m φ
⊢ (f >=> g) >=> h = f >=> g >=> h
[PROOFSTEP]
simp only [(· >=> ·), functor_norm]
[GOAL]
α✝ β✝ γ : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
f : α → β
a : m (m α)
⊢ joinM (Functor.map f <$> a) = f <$> joinM a
[PROOFSTEP]
simp only [joinM, (· ∘ ·), id.def, ← bind_pure_comp, bind_assoc, map_bind, pure_bind]
[GOAL]
α✝ β γ : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
a : m (m (m α))
⊢ joinM (joinM <$> a) = joinM (joinM a)
[PROOFSTEP]
simp only [joinM, (· ∘ ·), id.def, map_bind, ← bind_pure_comp, bind_assoc, pure_bind]
[GOAL]
α✝ β γ : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
a : m α
⊢ joinM (pure <$> a) = a
[PROOFSTEP]
simp only [joinM, (· ∘ ·), id.def, map_bind, ← bind_pure_comp, bind_assoc, pure_bind, bind_pure]
[GOAL]
α β γ : Type u
F : Type → Type v
inst✝ : Alternative F
h : Decidable True
⊢ guard True = pure ()
[PROOFSTEP]
simp [guard, if_pos]
[GOAL]
α β γ : Type u
F : Type → Type v
inst✝ : Alternative F
h : Decidable False
⊢ guard False = failure
[PROOFSTEP]
simp [guard, if_neg not_false]
[GOAL]
α β γ : Type u
e : Type v
⊢ LawfulFunctor (Sum e)
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
case refine'_2
α β γ : Type u
e : Type v
⊢ ∀ {α : Type u} (x : e ⊕ α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α β γ : Type u
e : Type v
⊢ ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : e ⊕ α), (h ∘ g) <$> x = h <$> g <$> x
[PROOFSTEP]
intros
[GOAL]
case refine'_1
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
try casesm Sum _ _
[GOAL]
case refine'_1
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case refine'_2
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e ⊕ α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
try casesm Sum _ _
[GOAL]
case refine'_2
α β γ : Type u
e : Type v
α✝ : Type u
x✝ : e ⊕ α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case refine'_3
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e ⊕ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
try casesm Sum _ _
[GOAL]
case refine'_3
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : e ⊕ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case refine'_1
α β γ : Type u
e : Type v
α✝ β✝ : Type u
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inl
α β γ : Type u
e : Type v
α✝ : Type u
val✝ : e
⊢ id <$> inl val✝ = inl val✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2.inr
α β γ : Type u
e : Type v
α✝ : Type u
val✝ : α✝
⊢ id <$> inr val✝ = inr val✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3.inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
val✝ : e
⊢ (h✝ ∘ g✝) <$> inl val✝ = h✝ <$> g✝ <$> inl val✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_3.inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
val✝ : α✝
⊢ (h✝ ∘ g✝) <$> inr val✝ = h✝ <$> g✝ <$> inr val✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : e ⊕ α) (y : e ⊕ β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
y✝ : e ⊕ β✝
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Seq.seq (Function.const β✝ <$> x✝) fun x => y✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
val✝ : e
⊢ (SeqLeft.seqLeft (inl val✝) fun x => y✝) = Seq.seq (Function.const β✝ <$> inl val✝) fun x => y✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
val✝ : α✝
⊢ (SeqLeft.seqLeft (inr val✝) fun x => y✝) = Seq.seq (Function.const β✝ <$> inr val✝) fun x => y✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : e ⊕ α) (y : e ⊕ β),
    (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
y✝ : e ⊕ β✝
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
val✝ : e
⊢ (SeqRight.seqRight (inl val✝) fun x => y✝) = Seq.seq (Function.const α✝ id <$> inl val✝) fun x => y✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
y✝ : e ⊕ β✝
val✝ : α✝
⊢ (SeqRight.seqRight (inr val✝) fun x => y✝) = Seq.seq (Function.const α✝ id <$> inr val✝) fun x => y✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl.inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
val✝¹ val✝ : e
⊢ (SeqRight.seqRight (inl val✝¹) fun x => inl val✝) = Seq.seq (Function.const α✝ id <$> inl val✝¹) fun x => inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
val✝¹ : e
val✝ : β✝
⊢ (SeqRight.seqRight (inl val✝¹) fun x => inr val✝) = Seq.seq (Function.const α✝ id <$> inl val✝¹) fun x => inr val✝
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
val✝¹ : α✝
val✝ : e
⊢ (SeqRight.seqRight (inr val✝¹) fun x => inl val✝) = Seq.seq (Function.const α✝ id <$> inr val✝¹) fun x => inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
val✝¹ : α✝
val✝ : β✝
⊢ (SeqRight.seqRight (inr val✝¹) fun x => inr val✝) = Seq.seq (Function.const α✝ id <$> inr val✝¹) fun x => inr val✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (g : α → β) (x : e ⊕ α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
g✝ : α✝ → β✝
x✝ : e ⊕ α✝
⊢ (Seq.seq (pure g✝) fun x => x✝) = g✝ <$> x✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (f : α → β) (x : e ⊕ α),
    (do
        let a ← x
        pure (f a)) =
      f <$> x
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
x✝ : e ⊕ α✝
⊢ (do
      let a ← x✝
      pure (f✝ a)) =
    f✝ <$> x✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
val✝ : e
⊢ (do
      let a ← inl val✝
      pure (f✝ a)) =
    f✝ <$> inl val✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : α✝ → β✝
val✝ : α✝
⊢ (do
      let a ← inr val✝
      pure (f✝ a)) =
    f✝ <$> inr val✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (f : e ⊕ (α → β)) (x : e ⊕ α),
    (do
        let x_1 ← f
        x_1 <$> x) =
      Seq.seq f fun x_1 => x
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
f✝ : e ⊕ (α✝ → β✝)
x✝ : e ⊕ α✝
⊢ (do
      let x ← f✝
      x <$> x✝) =
    Seq.seq f✝ fun x => x✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
val✝ : e
⊢ (do
      let x ← inl val✝
      x <$> x✝) =
    Seq.seq (inl val✝) fun x => x✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : e ⊕ α✝
val✝ : α✝ → β✝
⊢ (do
      let x ← inr val✝
      x <$> x✝) =
    Seq.seq (inr val✝) fun x => x✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β : Type u} (x : α) (f : α → e ⊕ β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ : Type u
x✝ : α✝
f✝ : α✝ → e ⊕ β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
rfl
[GOAL]
α β γ : Type u
e : Type v
⊢ ∀ {α β γ : Type u} (x : e ⊕ α) (f : α → e ⊕ β) (g : β → e ⊕ γ), x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
x✝ : e ⊕ α✝
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
casesm Sum _ _
[GOAL]
case inl
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
val✝ : e
⊢ inl val✝ >>= f✝ >>= g✝ = inl val✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rfl
[GOAL]
case inr
α β γ : Type u
e : Type v
α✝ β✝ γ✝ : Type u
f✝ : α✝ → e ⊕ β✝
g✝ : β✝ → e ⊕ γ✝
val✝ : α✝
⊢ inr val✝ >>= f✝ >>= g✝ = inr val✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
rfl
[GOAL]
α✝ β✝ γ✝ : Type u
m✝ : ?m.20624
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (Seq.seq (f <$> a) fun x => b) = (fun p => f p.fst p.snd) <$> Seq.seq (Prod.mk <$> a) fun x => b
[PROOFSTEP]
simp [seq_map_assoc, map_seq, seq_assoc, seq_pure, map_map]
[GOAL]
α✝ β✝ γ✝ : Type u
m✝ : ?m.20624
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (Seq.seq (f <$> a) fun x => b) = Seq.seq (((fun x => (fun p => f p.fst p.snd) ∘ x) ∘ Prod.mk) <$> a) fun x => b
[PROOFSTEP]
rfl
[GOAL]
α✝ β✝ γ✝ : Type u
m✝ : ?m.20624
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ ((fun p => f p.fst p.snd) <$> Seq.seq (Prod.mk <$> a) fun x => b) = Seq.seq ((fun b a => f a b) <$> b) fun x => a
[PROOFSTEP]
rw [@CommApplicative.commutative_prod m h]
[GOAL]
α✝ β✝ γ✝ : Type u
m✝ : ?m.20624
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ ((fun p => f p.fst p.snd) <$> Seq.seq ((fun b a => (a, b)) <$> b) fun x => a) =
    Seq.seq ((fun b a => f a b) <$> b) fun x => a
[PROOFSTEP]
simp [seq_map_assoc, map_seq, seq_assoc, seq_pure, map_map, (· ∘ ·)]
