Theorem: Matrix.mem_toList_iff (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u_1
n : ℕ
v : Fin n → α
a : α
⊢ a ∈ toList v ↔ ∃ i, v i = a
Tactic:
induction n <;> simp[*]
State after:
case succ
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (a = v 0 ∨ ∃ i, v i.succ = a) ↔ ∃ i, v i = a

State before:
case succ
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (a = v 0 ∨ ∃ i, v i.succ = a) ↔ ∃ i, v i = a
Tactic:
constructor
State after:
case succ.mp
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (a = v 0 ∨ ∃ i, v i.succ = a) → ∃ i, v i = a

case succ.mpr
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (∃ i, v i = a) → a = v 0 ∨ ∃ i, v i.succ = a

State before:
case succ.mp
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (a = v 0 ∨ ∃ i, v i.succ = a) → ∃ i, v i = a

case succ.mpr
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (∃ i, v i = a) → a = v 0 ∨ ∃ i, v i.succ = a
Tactic:
{ rintro (rfl | ⟨i, rfl⟩) <;> simp }
State after:
case succ.mpr
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (∃ i, v i = a) → a = v 0 ∨ ∃ i, v i.succ = a

State before:
case succ.mpr
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (∃ i, v i = a) → a = v 0 ∨ ∃ i, v i.succ = a
Tactic:
{ rintro ⟨i, rfl⟩; cases i using Fin.cases <;> simp }
State after:
no goals

State before:
case succ.mp
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (a = v 0 ∨ ∃ i, v i.succ = a) → ∃ i, v i = a
Tactic:
rintro (rfl | ⟨i, rfl⟩) <;> simp
State after:
no goals

State before:
case succ.mpr
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (∃ i, v i = a) → a = v 0 ∨ ∃ i, v i.succ = a
Tactic:
rintro ⟨i, rfl⟩
State after:
case succ.mpr.intro
α : Type u_1
n✝ : ℕ
v : Fin (n✝ + 1) → α
i : Fin (n✝ + 1)
a✝ : ∀ {v_1 : Fin n✝ → α}, v i ∈ toList v_1 ↔ ∃ i_1, v_1 i_1 = v i
⊢ v i = v 0 ∨ ∃ i_1, v i_1.succ = v i

State before:
case succ.mpr.intro
α : Type u_1
n✝ : ℕ
v : Fin (n✝ + 1) → α
i : Fin (n✝ + 1)
a✝ : ∀ {v_1 : Fin n✝ → α}, v i ∈ toList v_1 ↔ ∃ i_1, v_1 i_1 = v i
⊢ v i = v 0 ∨ ∃ i_1, v i_1.succ = v i
Tactic:
cases i using Fin.cases <;> simp
State after:
no goals