-- 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_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]

Tactic:
refine ⟨m, by simpa [map_eq_foldl] using eq, ?_⟩

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 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 β
m : motive ↑i
eq : b.size = ↑i
w : ∀ (i : Fin as.size) (h2 : ↑i < b.size), p i b[↑i]
⊢ motive (↑i + 1) ∧
    ((fun r a => r.push (f a)) b as[i]).size = ↑i + 1 ∧
      ∀ (i_1 : Fin as.size) (h2 : ↑i_1 < ((fun r a => r.push (f a)) b as[i]).size),
        p i_1 ((fun r a => r.push (f a)) b as[i])[↑i_1]

Tactic:
refine ⟨?_, ?_, ?_⟩

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

case refine_2.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 β
m : motive ↑i
eq : b.size = ↑i
w : ∀ (i : Fin as.size) (h2 : ↑i < b.size), p i b[↑i]
⊢ ((fun r a => r.push (f a)) b as[i]).size = ↑i + 1

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]
⊢ ∀ (i_1 : Fin as.size) (h2 : ↑i_1 < ((fun r a => r.push (f a)) b as[i]).size),
    p i_1 ((fun r a => r.push (f a)) b as[i])[↑i_1]

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]
⊢ ∀ (i_1 : Fin as.size) (h2 : ↑i_1 < ((fun r a => r.push (f a)) b as[i]).size),
    p i_1 ((fun r a => r.push (f a)) b as[i])[↑i_1]

Tactic:
intro j 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
⊢ p j ((fun r a => r.push (f a)) b as[i])[↑j]

Proof state:
case refine_2.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 β
m : motive ↑i
eq : b.size = ↑i
w : ∀ (i : Fin as.size) (h2 : ↑i < b.size), p i b[↑i]
⊢ ((fun r a => r.push (f a)) b as[i]).size = ↑i + 1

Tactic:
simp_all

Result:
no goals

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

Tactic:
rw [getElem_push, dif_neg h']

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 j (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)
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]
⊢ (map f as).size = as.size

Tactic:
simpa [map_eq_foldl] using eq

Result:
no goals

Proof state:
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:
intro i b ⟨m, ⟨eq, w⟩⟩

Result:
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 β
m : motive ↑i
eq : b.size = ↑i
w : ∀ (i : Fin as.size) (h2 : ↑i < b.size), p i b[↑i]
⊢ motive (↑i + 1) ∧
    ((fun r a => r.push (f a)) b as[i]).size = ↑i + 1 ∧
      ∀ (i_1 : Fin as.size) (h2 : ↑i_1 < ((fun r a => r.push (f a)) b as[i]).size),
        p i_1 ((fun r a => r.push (f a)) b as[i])[↑i_1]

Proof state:
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 #[]

Tactic:
exact ⟨h0, rfl, nofun⟩

Result:
no goals