internlm/Lean-Github huggingface dataset:
Theorem: Matrix.mem_toList_iff
Proof 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 }
Proof 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
Theorem: Matrix.mem_toList_iff
Proof 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 }
Proof state after:
no goals
Theorem: Matrix.mem_toList_iff
Proof 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
Proof state after:
no goals
Theorem: Matrix.mem_toList_iff
Proof 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⟩
Proof 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
Theorem: Matrix.mem_toList_iff
Proof 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
Proof state after:
no goals
Theorem: Matrix.toOptionVec_some
Proof state before:
α : Type u_1
n : ℕ
v : Fin n → α
⊢ (toOptionVec fun i => some (v i)) = some v
Tactic:
induction n <;> simp[*, Matrix.empty_eq, toOptionVec, Function.comp]
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_none_iff
Proof state before:
α : Type u_1
n : ℕ
v : Fin n → Option α
⊢ toOptionVec v = none ↔ ∃ i, v i = none
Tactic:
induction' n with n ih
Proof 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
Theorem: Matrix.toOptionVec_eq_none_iff
Proof state before:
case zero
α : Type u_1
v : Fin 0 → Option α
⊢ toOptionVec v = none ↔ ∃ i, v i = none
Tactic:
simp
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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]
Proof 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
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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
Proof 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
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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⟩ }
Proof 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
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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⟩
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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
Proof 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
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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⟩ }
Proof 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
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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⟩
Proof 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
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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⟩
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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
Proof 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
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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
Proof 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
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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]
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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))
Proof 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
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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]) _
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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))
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_none_iff
Proof 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]
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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
Proof 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)
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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]
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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]
Proof 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)
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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
Proof 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)
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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]⟩ }
Proof 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)
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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 ] } }
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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]⟩
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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]
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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
Proof 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)
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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]⟩ }
Proof 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)
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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 ] }
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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
Proof 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)
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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⟩
Proof 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)
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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]⟩
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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]
Proof state after:
no goals
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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
Proof 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)
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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]
Proof 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)
Theorem: Matrix.toOptionVec_eq_some_iff
Proof 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 ]
Proof state after:
no goals