-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_eq_iff {l : Vector α n} :
    mapIdx f l = l' ↔ ∀ (i : Nat) (h : i < n), f i l[i] = l'[i]

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

Tactic:
simp only [mapIdx_mk, eq_mk, Array.mapIdx_eq_iff, getElem_mk]

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

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

Tactic:
constructor

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

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

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

Tactic:
rintro h' i h

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

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

Tactic:
simp_all [Array.getElem?_eq_none_iff.mpr w]

Result:
no goals

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

Tactic:
simp only [Nat.not_lt] at w

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

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

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

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

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

Tactic:
specialize h' i

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

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

Tactic:
simp_all

Result:
no goals

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

Tactic:
by_cases w : i < l.size

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

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

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

Tactic:
intro h' i

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

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

Tactic:
specialize h' w

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

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

Tactic:
simp_all

Result:
no goals

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

Tactic:
specialize h' i

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

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

Tactic:
rcases l with ⟨l, rfl⟩

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