-- 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:
α : 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 < 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 + 1 = (bs.push (f j as[j] ⋯)).size

Tactic:
simp

Result:
α : 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

Proof state:
case zero
α : 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)
bs : Array β
j : Nat
h : 0 + 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
this : j = as.size
⊢ motive as.size ∧ ∃ h_1, ∀ (i : Nat) (h_2 : i < as.size), p i bs[i] h_2

Tactic:
exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩

Result:
no goals

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

Tactic:
obtain rfl : i = j := by omega

Result:
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

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

Tactic:
exact (hs j (by omega) hm).2

Result:
no goals