case mk.zero
n✝ m n : ℕ
h : zero < n + 1
⊢ { val := zero, isLt := h } = 0 ∨ ∃ j, { val := zero, isLt := h } = succ j

case mk.succ
n✝ m n j : ℕ
h : Nat.succ j < n + 1
⊢ { val := Nat.succ j, isLt := h } = 0 ∨ ∃ j_1, { val := Nat.succ j, isLt := h } = succ j_1
n✝ m n : ℕ
i : Fin (n + 1)
⊢ i = 0 ∨ ∃ j, i = succ j
rcases i with ⟨_ | j, h⟩
case mk.zero.h
n✝ m n : ℕ
h : zero < n + 1
⊢ { val := zero, isLt := h } = 0
case mk.zero
n✝ m n : ℕ
h : zero < n + 1
⊢ { val := zero, isLt := h } = 0 ∨ ∃ j, { val := zero, isLt := h } = succ j
left
no goals
case mk.zero.h
n✝ m n : ℕ
h : zero < n + 1
⊢ { val := zero, isLt := h } = 0
rfl
case mk.succ.h
n✝ m n j : ℕ
h : Nat.succ j < n + 1
⊢ ∃ j_1, { val := Nat.succ j, isLt := h } = succ j_1
case mk.succ
n✝ m n j : ℕ
h : Nat.succ j < n + 1
⊢ { val := Nat.succ j, isLt := h } = 0 ∨ ∃ j_1, { val := Nat.succ j, isLt := h } = succ j_1
right
no goals
case mk.succ.h
n✝ m n j : ℕ
h : Nat.succ j < n + 1
⊢ ∃ j_1, { val := Nat.succ j, isLt := h } = succ j_1
exact ⟨⟨j, Nat.lt_of_succ_lt_succ h⟩, rfl⟩