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

State before:
α : Type ?u.27672
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ j < (a.modify i f).size
Tactic:
rw [Array.modify_preserves_size]
State after:
α : Type ?u.27672
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ j < a.size

State before:
α : Type ?u.27672
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ j < a.size
Tactic:
exact j_size
State after:
no goals

State before:
α : Type u_1
a : Array α
i : Nat
i_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ (a.modify i f)[j] = a[j]
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_size : i < a.size
j : Nat
j_size : j < a.size
f : α → α
h : i ≠ j
⊢ (if h : i < a.size then a.set ⟨i, ⋯⟩ (f (a.get ⟨i, ⋯⟩)) else a)[j] = a[j]

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

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

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

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

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

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

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

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

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

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

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

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

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