no goals
n m : ℕ
isLt✝ : 0 < n + 1
x✝¹ : Fin (n + 1)
ha : { val := 0, isLt := isLt✝ } ≠ 0
x✝ : x✝¹ ≠ 0
⊢ pred { val := 0, isLt := isLt✝ } ha = pred x✝¹ x✝ ↔ { val := 0, isLt := isLt✝ } = x✝¹
simp only [mk_zero, ne_eq, not_true] at ha
no goals
n m i : ℕ
isLt✝¹ : i + 1 < n + 1
isLt✝ : 0 < n + 1
x✝ : { val := i + 1, isLt := isLt✝¹ } ≠ 0
hb : { val := 0, isLt := isLt✝ } ≠ 0
⊢ pred { val := i + 1, isLt := isLt✝¹ } x✝ = pred { val := 0, isLt := isLt✝ } hb ↔
    { val := i + 1, isLt := isLt✝¹ } = { val := 0, isLt := isLt✝ }
simp only [mk_zero, ne_eq, not_true] at hb
no goals
n m i : ℕ
hi : i + 1 < n + 1
j : ℕ
hj : j + 1 < n + 1
ha : { val := i + 1, isLt := hi } ≠ 0
hb : { val := j + 1, isLt := hj } ≠ 0
⊢ pred { val := i + 1, isLt := hi } ha = pred { val := j + 1, isLt := hj } hb ↔
    { val := i + 1, isLt := hi } = { val := j + 1, isLt := hj }
simp [Fin.eq_iff_veq]