-- 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 : 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
⊢ i = j

Tactic:
omega

Result:
no goals

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
⊢ motive as.size ∧ ∃ h_1, ∀ (i : Nat) (h_2 : i < as.size), p i bs[i] h_2

Tactic:
have := (Nat.zero_add _).symm.trans h

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

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 : 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
⊢ i < as.size

Tactic:
omega

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

Tactic:
simp only [size_push] at h'

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 β
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

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

Tactic:
apply h₂

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)
⊢ motive as.size ∧ ∃ h, ∀ (i : Nat) (h_1 : i < as.size), p i (mapFinIdxM.map as f as.size 0 ⋯ #[]).run[i] h_1

Tactic:
exact go rfl nofun h0

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)
⊢ motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p i (as.mapFinIdx f)[i] h

Tactic:
simp [mapFinIdx, mapFinIdxM]

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)
⊢ motive as.size ∧ ∃ h, ∀ (i : Nat) (h_1 : i < as.size), p i (mapFinIdxM.map as f as.size 0 ⋯ #[]).run[i] h_1