-- 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.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 : Nat) (h : i < as.size), p i arr[i] 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 : Nat
i_lt : i < as.size
h' : i < (bs.push (f j as[j] ⋯)).size
⊢ p i (if h : i < bs.size then bs[i] else f j as[j] ⋯) i_lt

Tactic:
split

Result:
case succ.h₂.isTrue
α : 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 β
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 : Nat
i_lt : i < as.size
h' : i < (bs.push (f j as[j] ⋯)).size
h✝ : i < bs.size
⊢ p i bs[i] i_lt

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 β
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 : Nat
i_lt : i < as.size
h' : i < (bs.push (f j as[j] ⋯)).size
h✝ : ¬i < bs.size
⊢ p i (f j as[j] ⋯) i_lt

Proof state:
α : 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 + (j + 1) = as.size

Tactic:
omega

Result:
no goals

Proof state:
α : 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
⊢ j = bs.size

Tactic:
omega

Result:
no goals

Proof state:
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 : Nat) (h : i < as.size), p i arr[i] 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 : Nat
i_lt : i < as.size
h' : i < (bs.push (f j as[j] ⋯)).size
⊢ p i (bs.push (f j as[j] ⋯))[i] i_lt

Tactic:
rw [getElem_push]

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 : Nat) (h : i < as.size), p i arr[i] 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 : Nat
i_lt : i < as.size
h' : i < (bs.push (f j as[j] ⋯)).size
⊢ p i (if h : i < bs.size then bs[i] else f j as[j] ⋯) i_lt

Proof state:
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

Tactic:
intro i i_lt h'

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 : Nat) (h : i < as.size), p i arr[i] 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 : Nat
i_lt : i < as.size
h' : i < (bs.push (f j as[j] ⋯)).size
⊢ p i (bs.push (f j as[j] ⋯))[i] i_lt