Theorem: List.mem_ofFn (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ ∃ i, f i = a
Tactic:
rewrite [List.mem_iff_get]
State after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, get (ofFn f) n_1 = a) ↔ ∃ i, f i = a

State before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, get (ofFn f) n_1 = a) ↔ ∃ i, f i = a
Tactic:
simp only [get_ofFn]
State after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) ↔ ∃ i, f i = a

State before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) ↔ ∃ i, f i = a
Tactic:
constructor
State after:
case mp
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) → ∃ i, f i = a

case mpr
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a

State before:
case mp
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) → ∃ i, f i = a

case mpr
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Tactic:
. rintro ⟨⟨i,hi⟩,ha⟩
  simp only [length_ofFn] at hi
  exact ⟨⟨i,hi⟩, ha⟩
State after:
case mpr
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a

State before:
case mpr
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Tactic:
. rintro ⟨⟨i,hi⟩,ha⟩
  exists ⟨i, by rewrite [length_ofFn]; exact hi⟩
State after:
no goals

State before:
case mp
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) → ∃ i, f i = a
Tactic:
rintro ⟨⟨i,hi⟩,ha⟩
State after:
case mp.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < length (ofFn f)
ha : f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi }) = a
⊢ ∃ i, f i = a

State before:
case mp.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < length (ofFn f)
ha : f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi }) = a
⊢ ∃ i, f i = a
Tactic:
simp only [length_ofFn] at hi
State after:
case mp.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi✝ : i < length (ofFn f)
ha : f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi✝ }) = a
hi : i < n
⊢ ∃ i, f i = a

State before:
case mp.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi✝ : i < length (ofFn f)
ha : f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi✝ }) = a
hi : i < n
⊢ ∃ i, f i = a
Tactic:
exact ⟨⟨i,hi⟩, ha⟩
State after:
no goals

State before:
case mpr
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ i, f i = a) → ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Tactic:
rintro ⟨⟨i,hi⟩,ha⟩
State after:
case mpr.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a

State before:
case mpr.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
Tactic:
exists ⟨i, by rewrite [length_ofFn]; exact hi⟩
State after:
no goals

State before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ i < length (ofFn f)
Tactic:
rewrite [length_ofFn]
State after:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ i < n

State before:
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ i < n
Tactic:
exact hi
State after:
no goals