-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_eq_iff {f : α → β} {l : Vector α n} {l' : Vector β n} :
    map f l = l' ↔ ∀ i (h : i < n), l'[i] = f l[i]

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β
l : Vector α n
l' : Vector β n
⊢ map f l = l' ↔ ∀ (i : Nat) (h : i < n), l'[i] = f l[i]

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Vector β l.size
⊢ map f { toArray := l, size_toArray := ⋯ } = l' ↔
    ∀ (i : Nat) (h : i < l.size), l'[i] = f { toArray := l, size_toArray := ⋯ }[i]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
w : ∀ (i : Nat) (h : i < l.size), l'[i] = f l[i]
i : Nat
h : ¬i < l.size
⊢ l'[i]? = Option.map f l[i]?

Tactic:
rw [getElem?_neg, getElem?_neg, Option.map_none'] <;> omega

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
⊢ (∀ (i : Nat), l'[i]? = Option.map f l[i]?) ↔ ∀ (i : Nat) (h : i < l.size), l'[i] = f l[i]

Tactic:
constructor

Result:
case mk.mk.mp
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
⊢ (∀ (i : Nat), l'[i]? = Option.map f l[i]?) → ∀ (i : Nat) (h : i < l.size), l'[i] = f l[i]

case mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
⊢ (∀ (i : Nat) (h : i < l.size), l'[i] = f l[i]) → ∀ (i : Nat), l'[i]? = Option.map f l[i]?

Proof state:
case mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
w : ∀ (i : Nat) (h : i < l.size), l'[i] = f l[i]
i : Nat
⊢ l'[i]? = Option.map f l[i]?

Tactic:
if h : i < l.size then
  simpa [h, h'] using w i h
else
  rw [getElem?_neg, getElem?_neg, Option.map_none'] <;> omega

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
⊢ map f { toArray := l, size_toArray := ⋯ } = { toArray := l', size_toArray := h' } ↔
    ∀ (i : Nat) (h : i < l.size), { toArray := l', size_toArray := h' }[i] = f { toArray := l, size_toArray := ⋯ }[i]

Tactic:
simp only [map_mk, eq_mk, Array.map_eq_iff, getElem_mk]

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
⊢ (∀ (i : Nat), l'[i]? = Option.map f l[i]?) ↔ ∀ (i : Nat) (h : i < l.size), l'[i] = f l[i]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
w : ∀ (i : Nat) (h : i < l.size), l'[i] = f l[i]
i : Nat
h : i < l.size
⊢ l'[i]? = Option.map f l[i]?

Tactic:
simpa [h, h'] using w i h

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Vector β l.size
⊢ map f { toArray := l, size_toArray := ⋯ } = l' ↔
    ∀ (i : Nat) (h : i < l.size), l'[i] = f { toArray := l, size_toArray := ⋯ }[i]

Tactic:
rcases l' with ⟨l', h'⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
⊢ map f { toArray := l, size_toArray := ⋯ } = { toArray := l', size_toArray := h' } ↔
    ∀ (i : Nat) (h : i < l.size), { toArray := l', size_toArray := h' }[i] = f { toArray := l, size_toArray := ⋯ }[i]

Proof state:
case mk.mk.mp
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
w : ∀ (i : Nat), l'[i]? = Option.map f l[i]?
i : Nat
h : i < l.size
⊢ l'[i] = f l[i]

Tactic:
simpa [h, h'] using w i

Result:
no goals

Proof state:
case mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
⊢ (∀ (i : Nat) (h : i < l.size), l'[i] = f l[i]) → ∀ (i : Nat), l'[i]? = Option.map f l[i]?

Tactic:
intro w i

Result:
case mk.mk.mpr
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
w : ∀ (i : Nat) (h : i < l.size), l'[i] = f l[i]
i : Nat
⊢ l'[i]? = Option.map f l[i]?

Proof state:
case mk.mk.mp
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
⊢ (∀ (i : Nat), l'[i]? = Option.map f l[i]?) → ∀ (i : Nat) (h : i < l.size), l'[i] = f l[i]

Tactic:
intro w i h

Result:
case mk.mk.mp
α : Type u_1
β : Type u_2
f : α → β
l : Array α
l' : Array β
h' : l'.size = l.size
w : ∀ (i : Nat), l'[i]? = Option.map f l[i]?
i : Nat
h : i < l.size
⊢ l'[i] = f l[i]