-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_elimM (a : γ → m (Option α)) (n : γ → m β) (s : γ → α → m β)
    (hmono₁ : monotone a) (hmono₂ : monotone n) (hmono₃ : monotone s) :
    monotone (fun x => Option.elimM (a x) (n x) (s 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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
y : α
⊢ monotone fun x => (some y).elim (n x) (s x)

Tactic:
dsimp only [Option.elim]

Result:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
y : α
⊢ monotone fun x => s x 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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
⊢ monotone fun x => Option.elimM (a x) (n x) (s 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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
⊢ monotone a

case hmono₂
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
⊢ monotone fun x __do_lift => __do_lift.elim (n x) (s 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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
⊢ monotone fun x => none.elim (n x) (s x)

Tactic:
apply hmono₂

Result:
no goals

Proof state:
case hmono₂.h.none
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
⊢ monotone fun x => none.elim (n x) (s x)

case hmono₂.h.some
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
val✝ : α
⊢ monotone fun x => (some val✝).elim (n x) (s x)

Tactic:
case none => apply hmono₂

Result:
case hmono₂.h.some
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
val✝ : α
⊢ monotone fun x => (some val✝).elim (n x) (s x)

Proof state:
case hmono₂.h.some
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
val✝ : α
⊢ monotone fun x => (some val✝).elim (n x) (s x)

Tactic:
case some y =>
  dsimp only [Option.elim]
  apply monotone_apply
  apply hmono₃

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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
⊢ ∀ (y : Option α), monotone fun x => y.elim (n x) (s x)

Tactic:
intro o

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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
o : Option α
⊢ monotone fun x => o.elim (n x) (s x)

Proof state:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
y : α
⊢ monotone s

Tactic:
apply hmono₃

Result:
no goals

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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
⊢ monotone a

Tactic:
apply hmono₁

Result:
no goals

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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
⊢ monotone fun x __do_lift => __do_lift.elim (n x) (s 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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
⊢ ∀ (y : Option α), monotone fun x => y.elim (n x) (s 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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
y : α
⊢ monotone fun x => s x y

Tactic:
apply monotone_apply

Result:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
y : α
⊢ monotone s

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 γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
o : Option α
⊢ monotone fun x => o.elim (n x) (s x)

Tactic:
cases o

Result:
case hmono₂.h.none
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
⊢ monotone fun x => none.elim (n x) (s x)

case hmono₂.h.some
m : Type u → Type v
inst✝³ : Monad m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
a : γ → m (Option α)
n : γ → m β
s : γ → α → m β
hmono₁ : monotone a
hmono₂ : monotone n
hmono₃ : monotone s
val✝ : α
⊢ monotone fun x => (some val✝).elim (n x) (s x)