-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_eq_singleton_iff {l : Vector α 1} {f : (i : Nat) → α → (h : i < 1) → β} {b : β} :
    l.mapFinIdx f = #v[b] ↔ ∃ (a : α), l = #v[a] ∧ f 0 a (by omega) = b

Proof state:
case mk.mp
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
b : β
l : Array α
h : l.size = 1
⊢ (∃ a w, f 0 a ⋯ = b) → ∃ a, l = #[a] ∧ f 0 a ⋯ = b

Tactic:
rintro ⟨a, rfl, rfl⟩

Result:
case mk.mp.intro.intro
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
a : α
h : #[a].size = 1
⊢ ∃ a_1, #[a] = #[a_1] ∧ f 0 a_1 ⋯ = f 0 a ⋯

Proof state:
case mk
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
b : β
l : Array α
h : l.size = 1
⊢ (∃ a w, f 0 a ⋯ = b) ↔ ∃ a, l = #[a] ∧ f 0 a ⋯ = b

Tactic:
constructor

Result:
case mk.mp
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
b : β
l : Array α
h : l.size = 1
⊢ (∃ a w, f 0 a ⋯ = b) → ∃ a, l = #[a] ∧ f 0 a ⋯ = b

case mk.mpr
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
b : β
l : Array α
h : l.size = 1
⊢ (∃ a, l = #[a] ∧ f 0 a ⋯ = b) → ∃ a w, f 0 a ⋯ = b

Proof state:
α : Type u_1
β : Type u_2
l : Vector α 1
f : (i : Nat) → α → i < 1 → β
b : β
⊢ l.mapFinIdx f = { toArray := #[b], size_toArray := ⋯ } ↔ ∃ a, l = { toArray := #[a], size_toArray := ⋯ } ∧ f 0 a ⋯ = b

Tactic:
rcases l with ⟨l, h⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
b : β
l : Array α
h : l.size = 1
⊢ { toArray := l, size_toArray := h }.mapFinIdx f = { toArray := #[b], size_toArray := ⋯ } ↔
    ∃ a, { toArray := l, size_toArray := h } = { toArray := #[a], size_toArray := ⋯ } ∧ f 0 a ⋯ = b

Proof state:
α : Type ?u.38717
β : Type ?u.38751
l : Vector α 1
f : (i : Nat) → α → i < 1 → β
b : β
a : α
⊢ 0 < 1

Tactic:
omega

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
b : β
l : Array α
h : l.size = 1
⊢ { toArray := l, size_toArray := h }.mapFinIdx f = { toArray := #[b], size_toArray := ⋯ } ↔
    ∃ a, { toArray := l, size_toArray := h } = { toArray := #[a], size_toArray := ⋯ } ∧ f 0 a ⋯ = b

Tactic:
simp only [mapFinIdx_mk, eq_mk, Array.mapFinIdx_eq_singleton_iff]

Result:
case mk
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
b : β
l : Array α
h : l.size = 1
⊢ (∃ a w, f 0 a ⋯ = b) ↔ ∃ a, l = #[a] ∧ f 0 a ⋯ = b

Proof state:
case mk.mp.intro.intro
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
a : α
h : #[a].size = 1
⊢ ∃ a_1, #[a] = #[a_1] ∧ f 0 a_1 ⋯ = f 0 a ⋯

Tactic:
exact ⟨a, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
a : α
h : #[a].size = 1
⊢ ∃ w, f 0 a ⋯ = f 0 a ⋯

Tactic:
simp

Result:
no goals

Proof state:
case mk.mpr
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
b : β
l : Array α
h : l.size = 1
⊢ (∃ a, l = #[a] ∧ f 0 a ⋯ = b) → ∃ a w, f 0 a ⋯ = b

Tactic:
rintro ⟨a, rfl, rfl⟩

Result:
case mk.mpr.intro.intro
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
a : α
h : #[a].size = 1
⊢ ∃ a_1 w, f 0 a_1 ⋯ = f 0 a ⋯

Proof state:
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
a : α
h : #[a].size = 1
⊢ #[a] = #[a] ∧ f 0 a ⋯ = f 0 a ⋯

Tactic:
simp

Result:
no goals

Proof state:
case mk.mpr.intro.intro
α : Type u_1
β : Type u_2
f : (i : Nat) → α → i < 1 → β
a : α
h : #[a].size = 1
⊢ ∃ a_1 w, f 0 a_1 ⋯ = f 0 a ⋯

Tactic:
exact ⟨a, by simp⟩

Result:
no goals