-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Lemmas.lean
theorem monotone_mapFinIdxM (xs : Array α) (f : γ → (i : Nat) → α → i < xs.size → m β)
    (hmono : monotone f) : monotone (fun x => xs.mapFinIdxM (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 γ
xs : Array α
f : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
⊢ monotone fun x => xs.mapFinIdxM (f x)

Tactic:
suffices ∀ i j (h : i + j = xs.size) r, monotone (fun x => Array.mapFinIdxM.map xs (f x) i j h 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 : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
⊢ ∀ (i j : Nat) (h : i + j = xs.size) (r : Array β), monotone fun x => Array.mapFinIdxM.map xs (f x) i j h 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 : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
i j j✝ : Nat
bs✝ : Array β
i✝ : Nat
inv✝¹ : i✝ + 1 + j✝ = xs.size
j_lt✝ : j✝ < xs.size
this✝ : i✝ + (j✝ + 1) = xs.size
inv✝ : i✝.succ + j✝ = xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapFinIdxM.map xs (f x) i✝ (j✝ + 1) this✝ (bs✝.push __do_lift)
⊢ monotone fun x => Array.mapFinIdxM.map xs (f x) i✝.succ j✝ inv✝¹ bs✝

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 : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
i j j✝ : Nat
bs✝ : Array β
i✝ : Nat
inv✝¹ : i✝ + 1 + j✝ = xs.size
j_lt✝ : j✝ < xs.size
this✝ : i✝ + (j✝ + 1) = xs.size
inv✝ : i✝.succ + j✝ = xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapFinIdxM.map xs (f x) i✝ (j✝ + 1) this✝ (bs✝.push __do_lift)
⊢ monotone fun x => f x j✝ xs[j✝] ⋯

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 : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
i j j✝ : Nat
bs✝ : Array β
i✝ : Nat
inv✝¹ : i✝ + 1 + j✝ = xs.size
j_lt✝ : j✝ < xs.size
this✝ : i✝ + (j✝ + 1) = xs.size
inv✝ : i✝.succ + j✝ = xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapFinIdxM.map xs (f x) i✝ (j✝ + 1) this✝ (bs✝.push __do_lift)
⊢ monotone fun x __do_lift => Array.mapFinIdxM.map xs (f x) i✝ (j✝ + 1) ⋯ (bs✝.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 : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
⊢ ∀ (i j : Nat) (h : i + j = xs.size) (r : Array β), monotone fun x => Array.mapFinIdxM.map xs (f x) i j h r

Tactic:
intros i j h 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 : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
i j : Nat
h : i + j = xs.size
r : Array β
⊢ monotone fun x => Array.mapFinIdxM.map xs (f x) i j h r

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

Tactic:
induction i, j, h, r using Array.mapFinIdxM.map.induct xs

Result:
case case1
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 : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
i j j✝ : Nat
bs✝ : Array β
x✝ inv✝ : 0 + j✝ = xs.size
⊢ monotone fun x => Array.mapFinIdxM.map xs (f x) 0 j✝ x✝ bs✝

case case2
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 : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
i j j✝ : Nat
bs✝ : Array β
i✝ : Nat
inv✝¹ : i✝ + 1 + j✝ = xs.size
j_lt✝ : j✝ < xs.size
this✝ : i✝ + (j✝ + 1) = xs.size
inv✝ : i✝.succ + j✝ = xs.size
ih1✝ : ∀ (__do_lift : β), monotone fun x => Array.mapFinIdxM.map xs (f x) i✝ (j✝ + 1) this✝ (bs✝.push __do_lift)
⊢ monotone fun x => Array.mapFinIdxM.map xs (f x) i✝.succ j✝ inv✝¹ bs✝

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 γ
xs : Array α
f : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
i j j✝ : Nat
bs✝ : Array β
i✝ : Nat
inv✝¹ : i✝ + 1 + j✝ = xs.size
j_lt✝ : j✝ < xs.size
this✝ : i✝ + (j✝ + 1) = xs.size
inv✝ : i✝.succ + j✝ = xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapFinIdxM.map xs (f x) i✝ (j✝ + 1) this✝ (bs✝.push __do_lift)
⊢ monotone fun x => f x j✝ xs[j✝]

Tactic:
apply monotone_apply

Result:
case hmono₁.h.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 : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
i j j✝ : Nat
bs✝ : Array β
i✝ : Nat
inv✝¹ : i✝ + 1 + j✝ = xs.size
j_lt✝ : j✝ < xs.size
this✝ : i✝ + (j✝ + 1) = xs.size
inv✝ : i✝.succ + j✝ = xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapFinIdxM.map xs (f x) i✝ (j✝ + 1) this✝ (bs✝.push __do_lift)
⊢ monotone fun x => f x j✝

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 γ
xs : Array α
f : γ → (i : Nat) → α → i < xs.size → m β
hmono : monotone f
i j j✝ : Nat
bs✝ : Array β
i✝ : Nat
inv✝¹ : i✝ + 1 + j✝ = xs.size
j_lt✝ : j✝ < xs.size
this✝ : i✝ + (j✝ + 1) = xs.size
inv✝ : i✝.succ + j✝ = xs.size
ih : ∀ (__do_lift : β), monotone fun x => Array.mapFinIdxM.map xs (f x) i✝ (j✝ + 1) this✝ (bs✝.push __do_lift)
y : γ
⊢ ∀ (y : β), monotone fun x => Array.mapFinIdxM.map xs (f x) i✝ (j✝ + 1) ⋯ (bs✝.push y)

Tactic:
apply ih

Result:
no goals