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

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
⊢ (ofFn f).getD i d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
simp [List.getD]
State after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
⊢ ((ofFn f).get? i).getD d = if h : i < k then f ⟨i, h⟩ else d

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
⊢ ((ofFn f).get? i).getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
if h : i < (ofFn f).length then
  rw [get?_eq_get h]
  rw [length_ofFn] at h
  rw [dif_pos h]
  simp
else
  rw [get?_eq_none.mpr (by simpa using h)]
  rw [length_ofFn] at h
  rw [dif_neg h]
  rfl
State after:
no goals

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : i < (ofFn f).length
⊢ ((ofFn f).get? i).getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [get?_eq_get h]
State after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : i < (ofFn f).length
⊢ (some ((ofFn f).get ⟨i, h⟩)).getD d = if h : i < k then f ⟨i, h⟩ else d

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : i < (ofFn f).length
⊢ (some ((ofFn f).get ⟨i, h⟩)).getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [length_ofFn] at h
State after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h✝ : i < (ofFn f).length
h : i < k
⊢ (some ((ofFn f).get ⟨i, h✝⟩)).getD d = if h : i < k then f ⟨i, h⟩ else d

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h✝ : i < (ofFn f).length
h : i < k
⊢ (some ((ofFn f).get ⟨i, h✝⟩)).getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [dif_pos h]
State after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h✝ : i < (ofFn f).length
h : i < k
⊢ (some ((ofFn f).get ⟨i, h✝⟩)).getD d = f ⟨i, h⟩

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h✝ : i < (ofFn f).length
h : i < k
⊢ (some ((ofFn f).get ⟨i, h✝⟩)).getD d = f ⟨i, h⟩
Tactic:
simp
State after:
no goals

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < (ofFn f).length
⊢ ((ofFn f).get? i).getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [get?_eq_none.mpr (by simpa using h)]
State after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < (ofFn f).length
⊢ none.getD d = if h : i < k then f ⟨i, h⟩ else d

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < (ofFn f).length
⊢ none.getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [length_ofFn] at h
State after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < k
⊢ none.getD d = if h : i < k then f ⟨i, h⟩ else d

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < k
⊢ none.getD d = if h : i < k then f ⟨i, h⟩ else d
Tactic:
rw [dif_neg h]
State after:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < k
⊢ none.getD d = d

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < k
⊢ none.getD d = d
Tactic:
rfl
State after:
no goals

State before:
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : ¬i < (ofFn f).length
⊢ (ofFn f).length ≤ i
Tactic:
simpa using h
State after:
no goals