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

State before:
n : Nat
i : Fin (length (fins n))
⊢ ↑i < n
Tactic:
cases i
State after:
case mk
n val✝ : Nat
isLt✝ : val✝ < length (fins n)
⊢ ↑{ val := val✝, isLt := isLt✝ } < n

State before:
case mk
n val✝ : Nat
isLt✝ : val✝ < length (fins n)
⊢ ↑{ val := val✝, isLt := isLt✝ } < n
Tactic:
simp
State after:
case mk
n val✝ : Nat
isLt✝ : val✝ < length (fins n)
⊢ val✝ < n

State before:
case mk
n val✝ : Nat
isLt✝ : val✝ < length (fins n)
⊢ val✝ < n
Tactic:
simp_all
State after:
no goals

State before:
n : Nat
i : Fin (length (fins n))
⊢ get (fins n) i = { val := ↑i, isLt := ⋯ }
Tactic:
rcases i with ⟨j,hj⟩
State after:
case mk
n j : Nat
hj : j < length (fins n)
⊢ get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }

State before:
case mk
n j : Nat
hj : j < length (fins n)
⊢ get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }
Tactic:
revert hj
State after:
case mk
n j : Nat
⊢ ∀ (hj : j < length (fins n)), get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }

State before:
case mk
n j : Nat
⊢ ∀ (hj : j < length (fins n)), get (fins n) { val := j, isLt := hj } = { val := ↑{ val := j, isLt := hj }, isLt := ⋯ }
Tactic:
simp
State after:
case mk
n j : Nat
⊢ ∀ (hj : j < n), get (fins n) { val := j, isLt := ⋯ } = { val := j, isLt := ⋯ }

State before:
case mk
n j : Nat
⊢ ∀ (hj : j < n), get (fins n) { val := j, isLt := ⋯ } = { val := j, isLt := ⋯ }
Tactic:
intro hj
State after:
case mk
n j : Nat
hj : j < n
⊢ get (fins n) { val := j, isLt := ⋯ } = { val := j, isLt := ⋯ }

State before:
case mk
n j : Nat
hj : j < n
⊢ get (fins n) { val := j, isLt := ⋯ } = { val := j, isLt := ⋯ }
Tactic:
apply Option.some_inj.mp
State after:
case mk
n j : Nat
hj : j < n
⊢ some (get (fins n) { val := j, isLt := ⋯ }) = some { val := j, isLt := ⋯ }

State before:
case mk
n j : Nat
hj : j < n
⊢ some (get (fins n) { val := j, isLt := ⋯ }) = some { val := j, isLt := ⋯ }
Tactic:
rw [← get?_eq_get]
State after:
case mk
n j : Nat
hj : j < n
⊢ get? (fins n) j = some { val := j, isLt := ⋯ }

State before:
case mk
n j : Nat
hj : j < n
⊢ get? (fins n) j = some { val := j, isLt := ⋯ }
Tactic:
induction n
State after:
case mk.zero
j : Nat
hj : j < Nat.zero
⊢ get? (fins Nat.zero) j = some { val := j, isLt := ⋯ }

case mk.succ
j n✝ : Nat
n_ih✝ : ∀ (hj : j < n✝), get? (fins n✝) j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n✝
⊢ get? (fins (Nat.succ n✝)) j = some { val := j, isLt := ⋯ }

State before:
case mk.zero
j : Nat
hj : j < Nat.zero
⊢ get? (fins Nat.zero) j = some { val := j, isLt := ⋯ }
Tactic:
contradiction
State after:
no goals

State before:
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
⊢ get? (fins (Nat.succ n')) j = some { val := j, isLt := ⋯ }
Tactic:
conv => lhs; rw [fins_succ]
State after:
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }

State before:
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Tactic:
by_cases h : j = n'
State after:
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }

case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }

State before:
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Tactic:
rw [get?_append_right]
State after:
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ get? [Fin.last n'] (j - length (map Fin.castSucc (fins n'))) = some { val := j, isLt := ⋯ }

case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ length (map Fin.castSucc (fins n')) ≤ j

State before:
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ get? [Fin.last n'] (j - length (map Fin.castSucc (fins n'))) = some { val := j, isLt := ⋯ }
Tactic:
simp [h, Fin.last]
State after:
no goals

State before:
case pos
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : j = n'
⊢ length (map Fin.castSucc (fins n')) ≤ j
Tactic:
simp [h]
State after:
no goals

State before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Tactic:
have : j < n' := Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) h
State after:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this : j < n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }

State before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this : j < n'
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Tactic:
have := ih this
State after:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }

State before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ get? (map Fin.castSucc (fins n') ++ [Fin.last n']) j = some { val := j, isLt := ⋯ }
Tactic:
rw [get?_append, get?_map, this]
State after:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ Option.map Fin.castSucc (some { val := j, isLt := ⋯ }) = some { val := j, isLt := ⋯ }

case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ j < length (map Fin.castSucc (fins n'))

State before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ Option.map Fin.castSucc (some { val := j, isLt := ⋯ }) = some { val := j, isLt := ⋯ }
Tactic:
simp
State after:
no goals

State before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ j < length (map Fin.castSucc (fins n'))
Tactic:
simp
State after:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ j < n'

State before:
case neg
j n' : Nat
ih : ∀ (hj : j < n'), get? (fins n') j = some { val := j, isLt := ⋯ }
hj : j < Nat.succ n'
h : ¬j = n'
this✝ : j < n'
this : get? (fins n') j = some { val := j, isLt := ⋯ }
⊢ j < n'
Tactic:
assumption
State after:
no goals