Theorem: ArrayLike.get_mapIdx (Algdata/Classes/ArrayLike.lean)

State before:
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : (fun j ys => ∀ (k : Fin n), (↑k < j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ j → ys[↑k] = xs[↑k])) (↑j) ys
k : Fin n
⊢ (↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]) ∧
    (↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k])
Tactic:
dsimp at *
State after:
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ (↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]) ∧
    (↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k])

State before:
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ (↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]) ∧
    (↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k])
Tactic:
constructor
State after:
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]

case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]

State before:
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]

case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Tactic:
. show k.1 < j.1 + 1 → _
  intro hij
  cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hij) with
  | inl heq =>
    cases (Fin.eq_of_val_eq heq)
    simp only [get_set_eq ys]
    exact congrArg _ <| (IH j).2 .refl
  | inr hlt =>
    have : j.1 ≠ k.1 := Ne.symm <| Nat.ne_of_lt hlt
    simp only [get_set_ne ys this]
    exact (IH k).1 hlt
State after:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]

State before:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Tactic:
. show k.1 ≥ j.1 + 1 → _
  intro hij
  simp only [get_set_ne ys (Nat.ne_of_lt hij)]
  exact (IH k).2 (Nat.le_of_succ_le hij)
State after:
no goals

State before:
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k < ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Tactic:
intro hij
State after:
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]

State before:
case left
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Tactic:
cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hij) with
| inl heq =>
  cases (Fin.eq_of_val_eq heq)
  simp only [get_set_eq ys]
  exact congrArg _ <| (IH j).2 .refl
| inr hlt =>
  have : j.1 ≠ k.1 := Ne.symm <| Nat.ne_of_lt hlt
  simp only [get_set_ne ys this]
  exact (IH k).1 hlt
State after:
no goals

State before:
case left.inl
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
heq : ↑k = ↑j
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Tactic:
cases (Fin.eq_of_val_eq heq)
State after:
case left.inl.refl
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
hij : ↑j < ↑j + 1
heq : ↑j = ↑j
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑j] = f j xs[↑j]

State before:
case left.inl.refl
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
hij : ↑j < ↑j + 1
heq : ↑j = ↑j
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑j] = f j xs[↑j]
Tactic:
simp only [get_set_eq ys]
State after:
case left.inl.refl
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
hij : ↑j < ↑j + 1
heq : ↑j = ↑j
⊢ f j ys[↑j] = f j xs[↑j]

State before:
case left.inl.refl
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
hij : ↑j < ↑j + 1
heq : ↑j = ↑j
⊢ f j ys[↑j] = f j xs[↑j]
Tactic:
exact congrArg _ <| (IH j).2 .refl
State after:
no goals

State before:
case left.inr
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
hlt : ↑k < ↑j
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Tactic:
have : j.1 ≠ k.1 := Ne.symm <| Nat.ne_of_lt hlt
State after:
case left.inr
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
hlt : ↑k < ↑j
this : ↑j ≠ ↑k
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]

State before:
case left.inr
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
hlt : ↑k < ↑j
this : ↑j ≠ ↑k
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = f k xs[↑k]
Tactic:
simp only [get_set_ne ys this]
State after:
case left.inr
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
hlt : ↑k < ↑j
this : ↑j ≠ ↑k
⊢ ys[↑k] = f k xs[↑k]

State before:
case left.inr
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k < ↑j + 1
hlt : ↑k < ↑j
this : ↑j ≠ ↑k
⊢ ys[↑k] = f k xs[↑k]
Tactic:
exact (IH k).1 hlt
State after:
no goals

State before:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
⊢ ↑k ≥ ↑j + 1 → (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Tactic:
intro hij
State after:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k ≥ ↑j + 1
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]

State before:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k ≥ ↑j + 1
⊢ (SetElem.setElem ys (↑j) (f j ys[↑j]) (_ : ↑j < n))[↑k] = xs[↑k]
Tactic:
simp only [get_set_ne ys (Nat.ne_of_lt hij)]
State after:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k ≥ ↑j + 1
⊢ ys[↑k] = xs[↑k]

State before:
case right
cont✝ : Type u
idx : Type v
elem✝ : Type w
domGet : cont✝ → idx → Prop
domSet : cont✝ → idx → elem✝ → Prop
inst✝¹ : ArrayLike cont✝ idx elem✝ domGet domSet
cont : Type u
elem : Type w
n : Nat
inst✝ : ArrayLike cont Nat elem (fun x i => i < n) fun x i x => i < n
xs : cont
f : Fin n → elem → elem
i : Nat
hi : i < n
j : Fin n
ys : cont
IH : ∀ (k : Fin n), (↑k < ↑j → ys[↑k] = f k xs[↑k]) ∧ (↑k ≥ ↑j → ys[↑k] = xs[↑k])
k : Fin n
hij : ↑k ≥ ↑j + 1
⊢ ys[↑k] = xs[↑k]
Tactic:
exact (IH k).2 (Nat.le_of_succ_le hij)
State after:
no goals