Theorem: Misc.Array.get_modify_at_idx (LeanSAT/Util/Misc.lean)

State before:
α : Type ?u.26377
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ i < (a.modify i f).size
Tactic:
rw [Array.modify_preserves_size]
State after:
α : Type ?u.26377
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ i < a.size

State before:
α : Type ?u.26377
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ i < a.size
Tactic:
exact i_in_bounds
State after:
no goals

State before:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ (a.modify i f)[i] = f a[i]
Tactic:
simp only [Array.modify, Array.modifyM, Id.bind_eq, Id.pure_eq, Id.run]
State after:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a)[i] = f a[i]

State before:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
⊢ (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a)[i] = f a[i]
Tactic:
split
State after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]

case isFalse
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]

State before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]

case isFalse
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Tactic:
. simp only [getElem]
  have lhs_rw := Array.get_set a ⟨i, i_in_bounds⟩ i i_in_bounds (f (Array.get a ⟨i, i_in_bounds⟩))
  simp only [getElem] at lhs_rw
  rw [lhs_rw]
  simp only [Array.get_eq_getElem, ite_true]
State after:
case isFalse
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]

State before:
case isFalse
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Tactic:
. next i_out_of_bounds =>
  exfalso
  exact i_out_of_bounds i_in_bounds
State after:
no goals

State before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Tactic:
simp only [getElem]
State after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)

State before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)
Tactic:
have lhs_rw := Array.get_set a ⟨i, i_in_bounds⟩ i i_in_bounds (f (Array.get a ⟨i, i_in_bounds⟩))
State after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩)))[i] =
    if ↑⟨i, i_in_bounds⟩ = i then f (a.get ⟨i, i_in_bounds⟩) else a[i]
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)

State before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩)))[i] =
    if ↑⟨i, i_in_bounds⟩ = i then f (a.get ⟨i, i_in_bounds⟩) else a[i]
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)
Tactic:
simp only [getElem] at lhs_rw
State after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩))).get ⟨i, ⋯⟩ =
    if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)

State before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩))).get ⟨i, ⋯⟩ =
    if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩))).get ⟨i, ⋯⟩ = f (a.get ⟨i, i_in_bounds⟩)
Tactic:
rw [lhs_rw]
State after:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩))).get ⟨i, ⋯⟩ =
    if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩
⊢ (if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩) = f (a.get ⟨i, i_in_bounds⟩)

State before:
case isTrue
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : i < a.size
lhs_rw :
  (a.set ⟨i, i_in_bounds⟩ (f (a.get ⟨i, i_in_bounds⟩))).get ⟨i, ⋯⟩ =
    if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩
⊢ (if True then f (a.get ⟨i, i_in_bounds⟩) else a.get ⟨i, i_in_bounds⟩) = f (a.get ⟨i, i_in_bounds⟩)
Tactic:
simp only [Array.get_eq_getElem, ite_true]
State after:
no goals

State before:
case isFalse
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
h✝ : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Tactic:
next i_out_of_bounds =>
exfalso
exact i_out_of_bounds i_in_bounds
State after:
no goals

State before:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
i_out_of_bounds : ¬i < a.size
⊢ (a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)))[i] = f a[i]
Tactic:
exfalso
State after:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
i_out_of_bounds : ¬i < a.size
⊢ False

State before:
α : Type u_1
a : Array α
i : Nat
i_in_bounds : i < a.size
f : α → α
i_out_of_bounds : ¬i < a.size
⊢ False
Tactic:
exact i_out_of_bounds i_in_bounds
State after:
no goals