-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_mapM (xs : Array α) (f : γ → α → m β) (hmono : monotone f) :
    monotone (fun x => xs.mapM (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 γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
⊢ monotone fun x __do_lift => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)

Tactic:
intro y

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 γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
y : γ
⊢ ∀ (y_1 : γ),
    y ⊑ y_1 →
      (fun x __do_lift => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)) y ⊑
        (fun x __do_lift => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)) y_1

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : ¬i✝ < xs.size
⊢ monotone fun x => pure r✝

Tactic:
apply monotone_const

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 γ
xs : Array α
f : γ → α → m β
hmono : monotone f
⊢ ∀ (i : Nat) (r : Array β), monotone fun x => Array.mapM.map (f x) xs i r

Tactic:
intros i r

Result:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i : Nat
r : Array β
⊢ monotone fun x => Array.mapM.map (f x) xs i r

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
⊢ monotone fun x => do
    let __do_lift ← f x xs[i✝]
    Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)

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 γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
⊢ monotone fun x => f x xs[i✝]

case hmono₂
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
⊢ monotone fun x __do_lift => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)

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 γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
y : γ
⊢ ∀ (y_1 : γ),
    y ⊑ y_1 →
      (fun x __do_lift => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)) y ⊑
        (fun x __do_lift => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)) y_1

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 γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
y : γ
⊢ ∀ (y : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push y)

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
⊢ monotone fun x => Array.mapM (f x) xs

Tactic:
suffices ∀ i r, monotone (fun x => Array.mapM.map (f x) xs i r) by apply this

Result:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
⊢ ∀ (i : Nat) (r : Array β), monotone fun x => Array.mapM.map (f x) xs i r

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
⊢ monotone fun x =>
    if hlt : i✝ < xs.size then do
      let __do_lift ← f x xs[i✝]
      Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
    else pure r✝

Tactic:
simp only [↓reduceDIte, *]

Result:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
⊢ monotone fun x => do
    let __do_lift ← f x xs[i✝]
    Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : ¬i✝ < xs.size
⊢ monotone fun x =>
    if hlt : i✝ < xs.size then do
      let __do_lift ← f x xs[i✝]
      Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
    else pure r✝

Tactic:
simp only [↓reduceDIte, *]

Result:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : ¬i✝ < xs.size
⊢ monotone fun x => pure r✝

Proof state:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
⊢ monotone fun x => Array.mapM.map (f x) xs i✝ r✝

Tactic:
unfold Array.mapM.map

Result:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
xs : Array α
f : γ → α → m β
hmono : monotone f
i✝ : Nat
r✝ : Array β
h✝ : i✝ < xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
⊢ monotone fun x =>
    if hlt : i✝ < xs.size then do
      let __do_lift ← f x xs[i✝]
      Array.mapM.map (f x) xs (i✝ + 1) (r✝.push __do_lift)
    else pure r✝