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

State before:
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
⊢ (s <: a) x = ![a] x
Tactic:
have : 0 = Fin.last 0 := by rfl
State after:
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
this : 0 = last 0
⊢ (s <: a) x = ![a] x

State before:
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
this : 0 = last 0
⊢ (s <: a) x = ![a] x
Tactic:
cases' x using Fin.cases with i <;> simp[this]
State after:
case succ
n : ℕ
α : Type u
s : Fin 0 → α
a : α
this : 0 = last 0
i : Fin 0
⊢ (s <: a) i.succ = a

State before:
case succ
n : ℕ
α : Type u
s : Fin 0 → α
a : α
this : 0 = last 0
i : Fin 0
⊢ (s <: a) i.succ = a
Tactic:
have := i.isLt
State after:
case succ
n : ℕ
α : Type u
s : Fin 0 → α
a : α
this✝ : 0 = last 0
i : Fin 0
this : ↑i < 0
⊢ (s <: a) i.succ = a

State before:
case succ
n : ℕ
α : Type u
s : Fin 0 → α
a : α
this✝ : 0 = last 0
i : Fin 0
this : ↑i < 0
⊢ (s <: a) i.succ = a
Tactic:
contradiction
State after:
no goals

State before:
n : ℕ
α : Type u
s : Fin 0 → α
a : α
x : Fin (Nat.succ 0)
⊢ 0 = last 0
Tactic:
rfl
State after:
no goals