Theorem: List.get_ofFn_go (LeanSAT/Reflect/BoolExpr/Nat.lean)

State before:
k✝ : Nat
α : Type ?u.1010
f : Fin k✝ → α
i j k : Nat
h : i + j = k✝
hk : k < (ofFn.go f i j h).length
⊢ j + k < k✝
Tactic:
simp[length_ofFn_go] at hk
State after:
k✝ : Nat
α : Type ?u.1010
f : Fin k✝ → α
i j k : Nat
h : i + j = k✝
hk : k < i
⊢ j + k < k✝

State before:
k✝ : Nat
α : Type ?u.1010
f : Fin k✝ → α
i j k : Nat
h : i + j = k✝
hk : k < i
⊢ j + k < k✝
Tactic:
omega
State after:
no goals

State before:
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i j k : Nat
h : i + j = k✝
hk : k < (ofFn.go f i j h).length
⊢ (ofFn.go f i j h).get ⟨k, hk⟩ = f ⟨j + k, ⋯⟩
Tactic:
let i+1 := i
State after:
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j k i : Nat
h : i + 1 + j = k✝
hk : k < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f (i + 1) j h).get ⟨k, hk⟩ = f ⟨j + k, ⋯⟩

State before:
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j k i : Nat
h : i + 1 + j = k✝
hk : k < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f (i + 1) j h).get ⟨k, hk⟩ = f ⟨j + k, ⋯⟩
Tactic:
cases k with
| zero => dsimp [ofFn.go]
| succ k =>
  dsimp [ofFn.go]
  rw [get_ofFn_go]
  congr 2
  simp_arith
State after:
no goals

State before:
case zero
k : Nat
α : Type u_1
f : Fin k → α
i✝ j i : Nat
h : i + 1 + j = k
hk : 0 < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f (i + 1) j h).get ⟨0, hk⟩ = f ⟨j + 0, ⋯⟩
Tactic:
dsimp [ofFn.go]
State after:
no goals

State before:
case succ
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f (i + 1) j h).get ⟨k + 1, hk⟩ = f ⟨j + (k + 1), ⋯⟩
Tactic:
dsimp [ofFn.go]
State after:
case succ
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f i (j + 1) ⋯).get ⟨k, ⋯⟩ = f ⟨j + (k + 1), ⋯⟩

State before:
case succ
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ (ofFn.go f i (j + 1) ⋯).get ⟨k, ⋯⟩ = f ⟨j + (k + 1), ⋯⟩
Tactic:
rw [get_ofFn_go]
State after:
case succ
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ f ⟨j + 1 + k, ⋯⟩ = f ⟨j + (k + 1), ⋯⟩

State before:
case succ
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ f ⟨j + 1 + k, ⋯⟩ = f ⟨j + (k + 1), ⋯⟩
Tactic:
congr 2
State after:
case succ.e_a.e_val
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ j + 1 + k = j + (k + 1)

State before:
case succ.e_a.e_val
k✝ : Nat
α : Type u_1
f : Fin k✝ → α
i✝ j i : Nat
h : i + 1 + j = k✝
k : Nat
hk : k + 1 < (ofFn.go f (i + 1) j h).length
⊢ j + 1 + k = j + (k + 1)
Tactic:
simp_arith
State after:
no goals