case zero
n m : ℕ
k : Fin (zero + 1)
⊢ k + 1 ≤ k ↔ k = last zero

case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
⊢ k + 1 ≤ k ↔ k = last (Nat.succ n✝)
n✝ m n : ℕ
k : Fin (n + 1)
⊢ k + 1 ≤ k ↔ k = last n
cases n
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
⊢ ¬k + 1 ≤ k ↔ k + 1 ≠ k → ¬k + 1 ≤ k
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
⊢ k + 1 ≤ k ↔ k = last (Nat.succ n✝)
rw [← not_iff_not, ← add_one_lt_iff, lt_iff_le_and_ne, not_and']
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
h : k + 1 ≠ k → ¬k + 1 ≤ k
⊢ k + 1 ≠ k
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
⊢ ¬k + 1 ≤ k ↔ k + 1 ≠ k → ¬k + 1 ≤ k
refine' ⟨fun h _ => h, fun h => h _⟩
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
h : k + 1 ≠ k → ¬k + 1 ≤ k
⊢ ¬(if k = last (n✝ + 1) then 0 else ↑k + 1) = ↑k
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
h : k + 1 ≠ k → ¬k + 1 ≤ k
⊢ k + 1 ≠ k
rw [Ne.def, ext_iff, val_add_one]
no goals
case succ
n m n✝ : ℕ
k : Fin (Nat.succ n✝ + 1)
h : k + 1 ≠ k → ¬k + 1 ≤ k
⊢ ¬(if k = last (n✝ + 1) then 0 else ↑k + 1) = ↑k
split_ifs with hk <;> simp [hk, @eq_comm ℕ 0]
case zero
n m : ℕ
k : Fin (zero + 1)
this : Subsingleton (Fin (0 + 1))
⊢ k + 1 ≤ k ↔ k = last zero
case zero
n m : ℕ
k : Fin (zero + 1)
⊢ k + 1 ≤ k ↔ k = last zero
haveI : Subsingleton (Fin (0 + 1)) := by
  convert_to Subsingleton (Fin 1)
  infer_instance
no goals
case zero
n m : ℕ
k : Fin (zero + 1)
this : Subsingleton (Fin (0 + 1))
⊢ k + 1 ≤ k ↔ k = last zero
simp [Subsingleton.elim (k + 1) k, Subsingleton.elim (Fin.last _) k]
n m : ℕ
k : Fin (zero + 1)
⊢ Subsingleton (Fin 1)
n m : ℕ
k : Fin (zero + 1)
⊢ Subsingleton (Fin (0 + 1))
convert_to Subsingleton (Fin 1)
no goals
n m : ℕ
k : Fin (zero + 1)
⊢ Subsingleton (Fin 1)
infer_instance