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

State before:
α : Type u_1
n : ℕ
w : Fin n → α
v : Fin n → Option α
⊢ toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
Tactic:
induction' n with n ih
State after:
case zero
α : Type u_1
w : Fin 0 → α
v : Fin 0 → Option α
⊢ toOptionVec v = some w ↔ ∀ (i : Fin 0), v i = some (w i)

case succ
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
⊢ toOptionVec v = some w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)

State before:
case zero
α : Type u_1
w : Fin 0 → α
v : Fin 0 → Option α
⊢ toOptionVec v = some w ↔ ∀ (i : Fin 0), v i = some (w i)
Tactic:
simp[Matrix.empty_eq]
State after:
no goals

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
⊢ toOptionVec v = some w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)
Tactic:
simp[toOptionVec]
State after:
case succ
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
⊢ ((toOptionVec (v ∘ succ)).bind fun vs => Option.map (fun z => z :> vs) (v 0)) = some w ↔
    ∀ (i : Fin (n + 1)), v i = some (w i)

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
⊢ ((toOptionVec (v ∘ succ)).bind fun vs => Option.map (fun z => z :> vs) (v 0)) = some w ↔
    ∀ (i : Fin (n + 1)), v i = some (w i)
Tactic:
rcases hz : v 0 with (_ | a) <;> simp
State after:
case succ.none
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
hz : v 0 = none
⊢ ∃ x, ¬v x = some (w x)

case succ.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
⊢ ((toOptionVec (v ∘ succ)).bind fun a_1 => some (a :> a_1)) = some w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)

State before:
case succ.none
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
hz : v 0 = none
⊢ ∃ x, ¬v x = some (w x)

case succ.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
⊢ ((toOptionVec (v ∘ succ)).bind fun a_1 => some (a :> a_1)) = some w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)
Tactic:
{ exact ⟨0, by simp[hz]⟩ }
State after:
case succ.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
⊢ ((toOptionVec (v ∘ succ)).bind fun a_1 => some (a :> a_1)) = some w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)

State before:
case succ.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
⊢ ((toOptionVec (v ∘ succ)).bind fun a_1 => some (a :> a_1)) = some w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)
Tactic:
{ rcases hs : toOptionVec (v ∘ Fin.succ) with (_ | z) <;> simp
  { have : ∃ i : Fin n, v i.succ = none := by simpa using hs
    rcases this with ⟨i, hi⟩
    exact ⟨i.succ, by simp[hi]⟩ }
  { have : ∀ i, v i.succ = some (z i) := ih.mp hs
    have : v = some a :> (fun i => some (z i)) :=
      by funext i; cases i using Fin.cases <;> simp[hz, this]
    simp[this, ←comp_vecCons', Iff.symm Function.funext_iff ] } }
State after:
no goals

State before:
case succ.none
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
hz : v 0 = none
⊢ ∃ x, ¬v x = some (w x)
Tactic:
exact ⟨0, by simp[hz]⟩
State after:
no goals

State before:
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
hz : v 0 = none
⊢ ¬v 0 = some (w 0)
Tactic:
simp[hz]
State after:
no goals

State before:
case succ.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
⊢ ((toOptionVec (v ∘ succ)).bind fun a_1 => some (a :> a_1)) = some w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)
Tactic:
rcases hs : toOptionVec (v ∘ Fin.succ) with (_ | z) <;> simp
State after:
case succ.some.none
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
hs : toOptionVec (v ∘ succ) = none
⊢ ∃ x, ¬v x = some (w x)

case succ.some.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)

State before:
case succ.some.none
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
hs : toOptionVec (v ∘ succ) = none
⊢ ∃ x, ¬v x = some (w x)

case succ.some.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)
Tactic:
{ have : ∃ i : Fin n, v i.succ = none := by simpa using hs
  rcases this with ⟨i, hi⟩
  exact ⟨i.succ, by simp[hi]⟩ }
State after:
case succ.some.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)

State before:
case succ.some.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)
Tactic:
{ have : ∀ i, v i.succ = some (z i) := ih.mp hs
  have : v = some a :> (fun i => some (z i)) :=
    by funext i; cases i using Fin.cases <;> simp[hz, this]
  simp[this, ←comp_vecCons', Iff.symm Function.funext_iff ] }
State after:
no goals

State before:
case succ.some.none
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
hs : toOptionVec (v ∘ succ) = none
⊢ ∃ x, ¬v x = some (w x)
Tactic:
have : ∃ i : Fin n, v i.succ = none := by simpa using hs
State after:
case succ.some.none
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
hs : toOptionVec (v ∘ succ) = none
this : ∃ i, v i.succ = none
⊢ ∃ x, ¬v x = some (w x)

State before:
case succ.some.none
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
hs : toOptionVec (v ∘ succ) = none
this : ∃ i, v i.succ = none
⊢ ∃ x, ¬v x = some (w x)
Tactic:
rcases this with ⟨i, hi⟩
State after:
case succ.some.none.intro
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
hs : toOptionVec (v ∘ succ) = none
i : Fin n
hi : v i.succ = none
⊢ ∃ x, ¬v x = some (w x)

State before:
case succ.some.none.intro
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
hs : toOptionVec (v ∘ succ) = none
i : Fin n
hi : v i.succ = none
⊢ ∃ x, ¬v x = some (w x)
Tactic:
exact ⟨i.succ, by simp[hi]⟩
State after:
no goals

State before:
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
hs : toOptionVec (v ∘ succ) = none
⊢ ∃ i, v i.succ = none
Tactic:
simpa using hs
State after:
no goals

State before:
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
hs : toOptionVec (v ∘ succ) = none
i : Fin n
hi : v i.succ = none
⊢ ¬v i.succ = some (w i.succ)
Tactic:
simp[hi]
State after:
no goals

State before:
case succ.some.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)
Tactic:
have : ∀ i, v i.succ = some (z i) := ih.mp hs
State after:
case succ.some.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this : ∀ (i : Fin n), v i.succ = some (z i)
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)

State before:
case succ.some.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this : ∀ (i : Fin n), v i.succ = some (z i)
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)
Tactic:
have : v = some a :> (fun i => some (z i)) :=
  by funext i; cases i using Fin.cases <;> simp[hz, this]
State after:
case succ.some.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this✝ : ∀ (i : Fin n), v i.succ = some (z i)
this : v = some a :> fun i => some (z i)
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)

State before:
case succ.some.some
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this✝ : ∀ (i : Fin n), v i.succ = some (z i)
this : v = some a :> fun i => some (z i)
⊢ a :> z = w ↔ ∀ (i : Fin (n + 1)), v i = some (w i)
Tactic:
simp[this, ←comp_vecCons', Iff.symm Function.funext_iff ]
State after:
no goals

State before:
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this : ∀ (i : Fin n), v i.succ = some (z i)
⊢ v = some a :> fun i => some (z i)
Tactic:
funext i
State after:
case h
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this : ∀ (i : Fin n), v i.succ = some (z i)
i : Fin (n + 1)
⊢ v i = (some a :> fun i => some (z i)) i

State before:
case h
α : Type u_1
n : ℕ
ih : ∀ {w : Fin n → α} {v : Fin n → Option α}, toOptionVec v = some w ↔ ∀ (i : Fin n), v i = some (w i)
w : Fin (n + 1) → α
v : Fin (n + 1) → Option α
a : α
hz : v 0 = some a
z : Fin n → α
hs : toOptionVec (v ∘ succ) = some z
this : ∀ (i : Fin n), v i.succ = some (z i)
i : Fin (n + 1)
⊢ v i = (some a :> fun i => some (z i)) i
Tactic:
cases i using Fin.cases <;> simp[hz, this]
State after:
no goals