-- 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 neg
α : 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 (f as[↑i])

Tactic:
simp only [show j = i by omega]

Result:
case neg
α : 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 i (f 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)
⊢ motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (map f as)[i]

Tactic:
have t := foldl_induction (as := as) (β := Array β)
  (motive := fun i arr => motive i ∧ arr.size = i ∧ ∀ i h2, p i arr[i.1])
  (init := #[]) (f := fun r a => r.push (f a)) ?_ ?_

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

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
h : ↑j < b.size + 1
⊢ p j (b.push (f as[↑i]))[↑j]

Tactic:
by_cases h' : j < size b

Result:
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 (b.push (f as[↑i]))[↑j]

case neg
α : 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 (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
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:
intro i 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
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]

Proof state:
case neg
α : 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 i (f as[↑i])

Tactic:
exact (hs _ m).1

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 (b.push (f as[↑i]))[↑j]

Tactic:
rw [getElem_push]

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

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 : p ⟨i, h⟩ (foldl (fun r a => r.push (f a)) #[] as)[↑⟨i, h⟩]
⊢ p ⟨i, h⟩ (map f as)[i]

Tactic:
simpa [map_eq_foldl] using w

Result:
no goals