Theorem: Fin.eq_of_ge (Regex/Data/SparseSet/Bijection.lean)

State before:
n : Nat
i : Fin (n + 1)
h : ↑i ≥ n
⊢ i = ⟨n, ⋯⟩
Tactic:
apply Fin.eq_of_val_eq
State after:
case a
n : Nat
i : Fin (n + 1)
h : ↑i ≥ n
⊢ ↑i = ↑⟨n, ⋯⟩

State before:
case a
n : Nat
i : Fin (n + 1)
h : ↑i ≥ n
⊢ ↑i = ↑⟨n, ⋯⟩
Tactic:
exact Nat.le_antisymm (Nat.le_of_succ_le_succ i.isLt) h
State after:
no goals