-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_induction (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β)
    (motive : Nat → Prop) (h0 : motive 0)
    (p : (i : Nat) → β → (h : i < as.size) → Prop)
    (hs : ∀ i h, motive i → p i (f i as[i] h) h ∧ motive (i + 1)) :
    motive as.size ∧ ∃ eq : (Array.mapFinIdx as f).size = as.size,
      ∀ i h, p i ((Array.mapFinIdx as f)[i]) h

Proof state:
case succ
α : Type u_1
β : Type u_2
as : Array α
f : (i : Nat) → α → i < as.size → β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → p i (f i as[i] h) h ∧ motive (i + 1)
i : Nat
ih :
  ∀ {bs : Array β} {j : Nat} {h : i + j = as.size},
    j = bs.size →
      (∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h) →
        motive j →
          let arr := mapFinIdxM.map as f i j h bs;
          motive as.size ∧ ∃ eq, ∀ (i_1 : Nat) (h : i_1 < as.size), p i_1 arr[i_1] h
bs : Array β
j : Nat
h : i + 1 + j = as.size
h₁ : j = bs.size
h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h
hm : motive j
⊢ motive as.size ∧
    ∃ h_1, ∀ (i_1 : Nat) (h_2 : i_1 < as.size), p i_1 (mapFinIdxM.map as f i (j + 1) ⋯ (bs.push (f j as[j] ⋯)))[i_1] h_2

Tactic:
apply @ih (bs.push (f j as[j] (by omega))) (j + 1) (by omega) (by simp; omega)

Result:
case succ.h₂
α : Type u_1
β : Type u_2
as : Array α
f : (i : Nat) → α → i < as.size → β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → p i (f i as[i] h) h ∧ motive (i + 1)
i : Nat
ih :
  ∀ {bs : Array β} {j : Nat} {h : i + j = as.size},
    j = bs.size →
      (∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h) →
        motive j →
          let arr := mapFinIdxM.map as f i j h bs;
          motive as.size ∧ ∃ eq, ∀ (i_1 : Nat) (h : i_1 < as.size), p i_1 arr[i_1] h
bs : Array β
j : Nat
h : i + 1 + j = as.size
h₁ : j = bs.size
h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h
hm : motive j
⊢ ∀ (i_1 : Nat) (h_1 : i_1 < as.size) (h' : i_1 < (bs.push (f j as[j] ⋯)).size), p i_1 (bs.push (f j as[j] ⋯))[i_1] h_1

case succ.hm
α : Type u_1
β : Type u_2
as : Array α
f : (i : Nat) → α → i < as.size → β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → p i (f i as[i] h) h ∧ motive (i + 1)
i : Nat
ih :
  ∀ {bs : Array β} {j : Nat} {h : i + j = as.size},
    j = bs.size →
      (∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h) →
        motive j →
          let arr := mapFinIdxM.map as f i j h bs;
          motive as.size ∧ ∃ eq, ∀ (i_1 : Nat) (h : i_1 < as.size), p i_1 arr[i_1] h
bs : Array β
j : Nat
h : i + 1 + j = as.size
h₁ : j = bs.size
h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h
hm : motive j
⊢ motive (j + 1)

Proof state:
case succ.h₂.isFalse
α : Type u_1
β : Type u_2
as : Array α
f : (i : Nat) → α → i < as.size → β
motive : Nat → Prop
h0 : motive 0
p : (i : Nat) → β → i < as.size → Prop
hs : ∀ (i : Nat) (h : i < as.size), motive i → p i (f i as[i] h) h ∧ motive (i + 1)
i✝ : Nat
ih :
  ∀ {bs : Array β} {j : Nat} {h : i✝ + j = as.size},
    j = bs.size →
      (∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h) →
        motive j →
          let arr := mapFinIdxM.map as f i✝ j h bs;
          motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p i arr[i] h
bs : Array β
h₂ : ∀ (i : Nat) (h : i < as.size) (h' : i < bs.size), p i bs[i] h
i : Nat
i_lt : i < as.size
h✝ : ¬i < bs.size
h' : i < bs.size + 1
h : i✝ + 1 + i = as.size
h₁ : i = bs.size
hm : motive i
⊢ p i (f i as[i] ⋯) i_lt

Tactic:
apply (hs i (by omega) hm).1

Result:
no goals