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

Proof state:
case refine_2.refine_3
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
i : Fin as.size
b : Array β
m : motive ↑i
eq : b.size = ↑i
w : ∀ (i : Fin as.size) (h2 : ↑i < b.size), p i b[↑i]
j : Fin as.size
h : ↑j < ((fun r a => r.push (f a)) b as[i]).size
⊢ p j ((fun r a => r.push (f a)) b as[i])[↑j]

Tactic:
simp at h ⊢

Result:
case refine_2.refine_3
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
i : Fin as.size
b : Array β
m : motive ↑i
eq : b.size = ↑i
w : ∀ (i : Fin as.size) (h2 : ↑i < b.size), p i b[↑i]
j : Fin as.size
h✝ : ↑j < ((fun r a => r.push (f a)) b as[i]).size
h : ↑j < b.size + 1
⊢ p j (b.push (f as[↑i]))[↑j]

Proof state:
case refine_3.intro.intro
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
m : motive as.size
eq : (foldl (fun r a => r.push (f a)) #[] as).size = as.size
i : Nat
h : i < as.size
w : ∀ (i : Fin as.size) (h2 : ↑i < as.size), p i (foldl (fun r a => r.push (f a)) #[] as)[↑i]
⊢ p ⟨i, h⟩ (map f as)[i]

Tactic:
specialize w ⟨i, h⟩ h

Result:
case refine_3.intro.intro
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
m : motive as.size
eq : (foldl (fun r a => r.push (f a)) #[] as).size = as.size
i : Nat
h : i < as.size
w : p ⟨i, h⟩ (foldl (fun r a => r.push (f a)) #[] as)[↑⟨i, h⟩]
⊢ p ⟨i, h⟩ (map f as)[i]

Proof state:
case refine_3
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
t :
  motive as.size ∧
    (foldl (fun r a => r.push (f a)) #[] as).size = as.size ∧
      ∀ (i : Fin as.size) (h2 : ↑i < (foldl (fun r a => r.push (f a)) #[] as).size),
        p i (foldl (fun r a => r.push (f a)) #[] as)[↑i]
⊢ motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (map f as)[i]

case refine_1
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
⊢ (fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) 0 #[]

case refine_2
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
⊢ ∀ (i : Fin as.size) (b : Array β),
    (fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) (↑i) b →
      (fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) (↑i + 1)
        ((fun r a => r.push (f a)) b as[i])

Tactic:
obtain ⟨m, eq, w⟩ := t

Result:
case refine_3.intro.intro
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
m : motive as.size
eq : (foldl (fun r a => r.push (f a)) #[] as).size = as.size
w :
  ∀ (i : Fin as.size) (h2 : ↑i < (foldl (fun r a => r.push (f a)) #[] as).size),
    p i (foldl (fun r a => r.push (f a)) #[] as)[↑i]
⊢ motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (map f as)[i]

case refine_1
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
⊢ (fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) 0 #[]

case refine_2
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
⊢ ∀ (i : Fin as.size) (b : Array β),
    (fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) (↑i) b →
      (fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) (↑i + 1)
        ((fun r a => r.push (f a)) b as[i])

Proof state:
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
i : Fin as.size
b : Array β
m : motive ↑i
eq : b.size = ↑i
w : ∀ (i : Fin as.size) (h2 : ↑i < b.size), p i b[↑i]
j : Fin as.size
h✝ : ↑j < ((fun r a => r.push (f a)) b as[i]).size
h : ↑j < b.size + 1
h' : ¬↑j < b.size
⊢ j = i

Tactic:
omega

Result:
no goals

Proof state:
case refine_3.intro.intro
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
m : motive as.size
eq : (foldl (fun r a => r.push (f a)) #[] as).size = as.size
w :
  ∀ (i : Fin as.size) (h2 : ↑i < (foldl (fun r a => r.push (f a)) #[] as).size),
    p i (foldl (fun r a => r.push (f a)) #[] as)[↑i]
i : Nat
h : i < as.size
⊢ p ⟨i, h⟩ (map f as)[i]

Tactic:
simp only [eq] at w

Result:
case refine_3.intro.intro
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
m : motive as.size
eq : (foldl (fun r a => r.push (f a)) #[] as).size = as.size
i : Nat
h : i < as.size
w : ∀ (i : Fin as.size) (h2 : ↑i < as.size), p i (foldl (fun r a => r.push (f a)) #[] as)[↑i]
⊢ p ⟨i, h⟩ (map f as)[i]

Proof state:
case refine_2.refine_1
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
i : Fin as.size
b : Array β
m : motive ↑i
eq : b.size = ↑i
w : ∀ (i : Fin as.size) (h2 : ↑i < b.size), p i b[↑i]
⊢ motive (↑i + 1)

Tactic:
exact (hs _ m).2

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
as : Array α
f : α → β
motive : Nat → Prop
h0 : motive 0
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)
i : Fin as.size
b : Array β
m : motive ↑i
eq : b.size = ↑i
w : ∀ (i : Fin as.size) (h2 : ↑i < b.size), p i b[↑i]
j : Fin as.size
h✝ : ↑j < ((fun r a => r.push (f a)) b as[i]).size
h : ↑j < b.size + 1
h' : ↑j < b.size
⊢ p j (if h : ↑j < b.size then b[↑j] else f as[↑i])

Tactic:
simp_all

Result:
no goals