Theorem: Part.mem_vector_mOfFn (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u_1
x✝¹ : Vector α 0
x✝ : Fin 0 →. α
⊢ x✝¹ ∈ Vector.mOfFn x✝ ↔ ∀ (i : Fin 0), x✝¹.get i ∈ x✝ i
Tactic:
simp[Vector.mOfFn, Vector.eq_nil]
State after:
no goals

State before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ w ∈ Vector.mOfFn v ↔ ∀ (i : Fin (n + 1)), w.get i ∈ v i
Tactic:
simp[Vector.mOfFn, @mem_vector_mOfFn _ n]
State after:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ (∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1) ↔ ∀ (i : Fin (n + 1)), w.get i ∈ v i

State before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ (∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1) ↔ ∀ (i : Fin (n + 1)), w.get i ∈ v i
Tactic:
exact ⟨by rintro ⟨a, ha, v, hv, rfl⟩ i; cases i using Fin.cases <;> simp[ha, hv],
  by intro h; exact ⟨w.head, by simpa using h 0, w.tail, fun i => by simpa using h i.succ, by simp⟩⟩
State after:
no goals

State before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ (∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1) → ∀ (i : Fin (n + 1)), w.get i ∈ v i
Tactic:
rintro ⟨a, ha, v, hv, rfl⟩ i
State after:
case intro.intro.intro.intro
α : Type u_1
n : ℕ
v✝ : Fin (n + 1) →. α
a : α
ha : a ∈ v✝ 0
v : Vector α n
hv : ∀ (i : Fin n), v.get i ∈ v✝ i.succ
i : Fin (n + 1)
⊢ (a ::ᵥ v).get i ∈ v✝ i

State before:
case intro.intro.intro.intro
α : Type u_1
n : ℕ
v✝ : Fin (n + 1) →. α
a : α
ha : a ∈ v✝ 0
v : Vector α n
hv : ∀ (i : Fin n), v.get i ∈ v✝ i.succ
i : Fin (n + 1)
⊢ (a ::ᵥ v).get i ∈ v✝ i
Tactic:
cases i using Fin.cases <;> simp[ha, hv]
State after:
no goals

State before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ (∀ (i : Fin (n + 1)), w.get i ∈ v i) → ∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1
Tactic:
intro h
State after:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
⊢ ∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1

State before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
⊢ ∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1
Tactic:
exact ⟨w.head, by simpa using h 0, w.tail, fun i => by simpa using h i.succ, by simp⟩
State after:
no goals

State before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
⊢ w.head ∈ v 0
Tactic:
simpa using h 0
State after:
no goals

State before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
i : Fin n
⊢ w.tail.get i ∈ v i.succ
Tactic:
simpa using h i.succ
State after:
no goals

State before:
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
⊢ w = w.head ::ᵥ w.tail
Tactic:
simp
State after:
no goals