m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ (Seq.seq (const α id <$> x) fun x => y) = do
    let _ ← x
    y
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ (SeqRight.seqRight x fun x => y) = do
    let _ ← x
    y
rw [seqRight_eq]
no goals
m : Type u_1 → Type u_2
α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
y : m β
⊢ (Seq.seq (const α id <$> x) fun x => y) = do
    let _ ← x
    y
simp [map_eq_pure_bind, seq_eq_bind_map, const]