Theorem: List.mem_fins (LeanSAT/Upstream/ToStd.lean)

State before:
n : Nat
x : Fin n
⊢ x ∈ fins n
Tactic:
rw [mem_iff_get]
State after:
n : Nat
x : Fin n
⊢ ∃ n_1, get (fins n) n_1 = x

State before:
n : Nat
x : Fin n
⊢ ∃ n_1, get (fins n) n_1 = x
Tactic:
refine ⟨⟨x,?_⟩,?_⟩
State after:
case refine_1
n : Nat
x : Fin n
⊢ ↑x < length (fins n)

case refine_2
n : Nat
x : Fin n
⊢ get (fins n) { val := ↑x, isLt := ?refine_1 } = x

State before:
case refine_1
n : Nat
x : Fin n
⊢ ↑x < length (fins n)
Tactic:
simp
State after:
no goals

State before:
case refine_2
n : Nat
x : Fin n
⊢ get (fins n) { val := ↑x, isLt := ⋯ } = x
Tactic:
simp
State after:
no goals