-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_modifyM (a : Array α) (i : Nat) (f : γ → α → m α) (hmono : monotone f) :
    monotone (fun x => a.modifyM i (f x))

Proof state:
case isTrue.hmono₁.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
a : Array α
i : Nat
f : γ → α → m α
hmono : monotone f
h✝ : i < a.size
⊢ monotone f

Tactic:
apply hmono

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 γ
a : Array α
i : Nat
f : γ → α → m α
hmono : monotone f
⊢ monotone fun x =>
    if h : i < a.size then
      let v := a[i];
      do
      let v ← f x v
      pure (a.set i v h)
    else pure a

Tactic:
split

Result:
case isTrue
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
a : Array α
i : Nat
f : γ → α → m α
hmono : monotone f
h✝ : i < a.size
⊢ monotone fun x =>
    let v := a[i];
    do
    let v ← f x v
    pure (a.set i v h✝)

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

Proof state:
case isTrue
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
a : Array α
i : Nat
f : γ → α → m α
hmono : monotone f
h✝ : i < a.size
⊢ monotone fun x =>
    let v := a[i];
    do
    let v ← f x v
    pure (a.set i v h✝)

Tactic:
apply monotone_bind

Result:
case isTrue.hmono₁
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
a : Array α
i : Nat
f : γ → α → m α
hmono : monotone f
h✝ : i < a.size
⊢ monotone fun x => f x a[i]

case isTrue.hmono₂
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
a : Array α
i : Nat
f : γ → α → m α
hmono : monotone f
h✝ : i < a.size
⊢ monotone fun x v => pure (a.set i v h✝)

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

Tactic:
apply monotone_const

Result:
no goals

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

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 γ
a : Array α
i : Nat
f : γ → α → m α
hmono : monotone f
⊢ monotone fun x => a.modifyM i (f x)

Tactic:
unfold Array.modifyM

Result:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
a : Array α
i : Nat
f : γ → α → m α
hmono : monotone f
⊢ monotone fun x =>
    if h : i < a.size then
      let v := a[i];
      do
      let v ← f x v
      pure (a.set i v h)
    else pure a

Proof state:
case isTrue.hmono₁
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
a : Array α
i : Nat
f : γ → α → m α
hmono : monotone f
h✝ : i < a.size
⊢ monotone fun x => f x a[i]

Tactic:
apply monotone_apply

Result:
case isTrue.hmono₁.h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α : Type u
γ : Type w
inst✝ : PartialOrder γ
a : Array α
i : Nat
f : γ → α → m α
hmono : monotone f
h✝ : i < a.size
⊢ monotone f