Theorem: List.ofFn_get_eq_map_cast (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
⊢ (ofFn fun i => g (as.get (Fin.cast h i))) = map g as
Tactic:
ext i b
State after:
case a.a
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
⊢ b ∈ (ofFn fun i => g (as.get (Fin.cast h i))).get? i ↔ b ∈ (map g as).get? i

State before:
case a.a
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
⊢ b ∈ (ofFn fun i => g (as.get (Fin.cast h i))).get? i ↔ b ∈ (map g as).get? i
Tactic:
simp
State after:
case a.a
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b

State before:
case a.a
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Tactic:
by_cases hi : i < n
State after:
case pos
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b

case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b

State before:
case pos
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b

case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Tactic:
{ simp[hi, List.ofFnNthVal, List.get?_eq_get (h ▸ hi)] }
State after:
case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b

State before:
case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Tactic:
{ simp[hi, List.ofFnNthVal, List.get?_len_le (le_of_not_lt $ h ▸ hi)] }
State after:
no goals

State before:
case pos
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Tactic:
simp[hi, List.ofFnNthVal, List.get?_eq_get (h ▸ hi)]
State after:
no goals

State before:
case neg
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
g : α → β
as : List α
h : n = as.length
i : ℕ
b : β
hi : ¬i < n
⊢ ofFnNthVal (fun i => g (as.get (Fin.cast h i))) i = some b ↔ ∃ a, as.get? i = some a ∧ g a = b
Tactic:
simp[hi, List.ofFnNthVal, List.get?_len_le (le_of_not_lt $ h ▸ hi)]
State after:
no goals