case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
⊢ Agrees (Array.set arr i x) f m'
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
n : ℕ
m : Fin n → β
H : Agrees arr f m
i : Fin (Array.size arr)
x : α
m' : Fin n → β
hm₁ : ∀ (j : Fin n), ↑j ≠ ↑i → m' j = m j
hm₂ : ∀ (h : ↑i < n), f x = m' { val := ↑i, isLt := h }
⊢ Agrees (Array.set arr i x) f m'
cases H
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
⊢ f (Array.get (Array.set arr i x) { val := j, isLt := hj₁ }) = m' { val := j, isLt := hj₂ }
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
⊢ Agrees (Array.set arr i x) f m'
refine mk' (by simp) fun j hj₁ hj₂ ↦ ?_
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
⊢ f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
⊢ f (Array.get (Array.set arr i x) { val := j, isLt := hj₁ }) = m' { val := j, isLt := hj₂ }
suffices f (Array.set arr i x)[j] = m' ⟨j, hj₂⟩ by simp_all [Array.get_set]
case pos
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ↑i = j
⊢ f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }

case neg
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }
case mk
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
⊢ f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }
by_cases h : i = j
no goals
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
⊢ Array.size arr = Array.size (Array.set arr i x)
simp
no goals
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
this : f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }
⊢ f (Array.get (Array.set arr i x) { val := j, isLt := hj₁ }) = m' { val := j, isLt := hj₂ }
simp_all [Array.get_set]
case pos
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
hj₁ : ↑i < Array.size (Array.set arr i x)
hj₂ : ↑i < Array.size arr
⊢ f (Array.set arr i x)[↑i] = m' { val := ↑i, isLt := hj₂ }
case pos
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ↑i = j
⊢ f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }
subst h
no goals
case pos
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
hj₁ : ↑i < Array.size (Array.set arr i x)
hj₂ : ↑i < Array.size arr
⊢ f (Array.set arr i x)[↑i] = m' { val := ↑i, isLt := hj₂ }
rw [Array.get_set_eq, ← hm₂]
case neg
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ f arr[j] = (fun i => f (Array.get arr i)) { val := j, isLt := hj₂ }

α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ j < Array.size arr

α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ j < Array.size arr
case neg
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ f (Array.set arr i x)[j] = m' { val := j, isLt := hj₂ }
rw [arr.get_set_ne _ _ _ h, hm₁ ⟨j, _⟩ (Ne.symm h)]
no goals
case neg
α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ f arr[j] = (fun i => f (Array.get arr i)) { val := j, isLt := hj₂ }

α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ j < Array.size arr

α : Type u_1
β : Sort u_2
f : α → β
arr : Array α
i : Fin (Array.size arr)
x : α
m' : Fin (Array.size arr) → β
hm₂ : ∀ (h : ↑i < Array.size arr), f x = m' { val := ↑i, isLt := h }
hm₁ : ∀ (j : Fin (Array.size arr)), ↑j ≠ ↑i → m' j = (fun i => f (Array.get arr i)) j
j : ℕ
hj₁ : j < Array.size (Array.set arr i x)
hj₂ : j < Array.size arr
h : ¬↑i = j
⊢ j < Array.size arr
rfl