-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapFinIdx_eq_replicate_iff {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} {b : β} :
    l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = b

Proof state:
case mp
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
w : ∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] x_1 = b_1 → b_1 = b
i : Nat
h : i < l.length
⊢ f i l[i] h = b

Tactic:
exact w (f i l[i] h) i h rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
⊢ (l.length = l.length ∧ ∀ (b_1 : β), b_1 ∈ l.mapFinIdx f → b_1 = b) ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = b

Tactic:
simp only [mem_mapFinIdx, forall_exists_index, true_and]

Result:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
⊢ (∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] x_1 = b_1 → b_1 = b) ↔
    ∀ (i : Nat) (h : i < l.length), f i l[i] h = b

Proof state:
case mp
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
⊢ (∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] x_1 = b_1 → b_1 = b) →
    ∀ (i : Nat) (h : i < l.length), f i l[i] h = b

Tactic:
intro w i h

Result:
case mp
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
w : ∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] x_1 = b_1 → b_1 = b
i : Nat
h : i < l.length
⊢ f i l[i] h = b

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
⊢ l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = b

Tactic:
rw [eq_replicate_iff, length_mapFinIdx]

Result:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
⊢ (l.length = l.length ∧ ∀ (b_1 : β), b_1 ∈ l.mapFinIdx f → b_1 = b) ↔ ∀ (i : Nat) (h : i < l.length), f i l[i] h = b

Proof state:
case mpr
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
w : ∀ (i : Nat) (h : i < l.length), f i l[i] h = b
i : Nat
h : i < l.length
⊢ f i l[i] h = b

Tactic:
exact w i h

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
⊢ (∀ (i : Nat) (h : i < l.length), f i l[i] h = b) →
    ∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] x_1 = b_1 → b_1 = b

Tactic:
rintro w b i h rfl

Result:
case mpr
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
w : ∀ (i : Nat) (h : i < l.length), f i l[i] h = b
i : Nat
h : i < l.length
⊢ f i l[i] h = b

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
⊢ (∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] x_1 = b_1 → b_1 = b) ↔
    ∀ (i : Nat) (h : i < l.length), f i l[i] h = b

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
⊢ (∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] x_1 = b_1 → b_1 = b) →
    ∀ (i : Nat) (h : i < l.length), f i l[i] h = b

case mpr
α : Type u_1
β : Type u_2
l : List α
f : (i : Nat) → α → i < l.length → β
b : β
⊢ (∀ (i : Nat) (h : i < l.length), f i l[i] h = b) →
    ∀ (b_1 : β) (x : Nat) (x_1 : x < l.length), f x l[x] x_1 = b_1 → b_1 = b