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

State before:
α : Type u_1
n : ℕ
v : Fin n → Option α
⊢ toOptionVec v = none ↔ ∃ i, v i = none
Tactic:
induction' n with n ih
State after:
case zero
α : Type u_1
v : Fin 0 → Option α
⊢ toOptionVec v = none ↔ ∃ i, v i = none

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

State before:
case zero
α : Type u_1
v : Fin 0 → Option α
⊢ toOptionVec v = none ↔ ∃ i, v i = none
Tactic:
simp
State after:
no goals

State before:
case succ
α : Type u_1
n : ℕ
ih : ∀ {v : Fin n → Option α}, toOptionVec v = none ↔ ∃ i, v i = none
v : Fin (n + 1) → Option α
⊢ toOptionVec v = none ↔ ∃ i, v i = none
Tactic:
simp[toOptionVec]
State after:
case succ
α : Type u_1
n : ℕ
ih : ∀ {v : Fin n → Option α}, toOptionVec v = none ↔ ∃ i, v i = none
v : Fin (n + 1) → Option α
⊢ (∀ (a : Fin n → α), toOptionVec (v ∘ succ) = some a → v 0 = none) ↔ ∃ i, v i = none

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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