-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem Seq.monotone_seq [LawfulMonad m] (f : γ → m α) (g : γ → m (α → β))
  (hmono₁ : monotone g) (hmono₂ : monotone f) :
    monotone (fun x => g x <*> f x)

Proof state:
case hmono₂.h.hmono
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
y : α → β
⊢ monotone f

Tactic:
assumption

Result:
no goals

Proof state:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => g x <*> f x

Tactic:
simp only [← LawfulMonad.bind_map ]

Result:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => do
    let x_1 ← g x
    x_1 <$> f x

Proof state:
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x => do
    let x_1 ← g x
    x_1 <$> f x

Tactic:
apply monotone_bind

Result:
case hmono₁
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone g

case hmono₂
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x x_1 => x_1 <$> f x

Proof state:
case hmono₂.h
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
y : α → β
⊢ monotone fun x => y <$> f x

Tactic:
apply Functor.monotone_map

Result:
case hmono₂.h.hmono
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
y : α → β
⊢ monotone f

Proof state:
case hmono₁
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone g

Tactic:
assumption

Result:
no goals

Proof state:
case hmono₂.h
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
⊢ ∀ (y : α → β), monotone fun x => y <$> f x

Tactic:
intro y

Result:
case hmono₂.h
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
y : α → β
⊢ monotone fun x => y <$> f x

Proof state:
case hmono₂
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
⊢ monotone fun x x_1 => x_1 <$> f x

Tactic:
apply monotone_of_monotone_apply

Result:
case hmono₂.h
m : Type u → Type v
inst✝⁴ : Monad m
inst✝³ : (α : Type u) → PartialOrder (m α)
inst✝² : MonoBind m
α β : Type u
γ : Type w
inst✝¹ : PartialOrder γ
inst✝ : LawfulMonad m
f : γ → m α
g : γ → m (α → β)
hmono₁ : monotone g
hmono₂ : monotone f
⊢ ∀ (y : α → β), monotone fun x => y <$> f x