Theorem: SizedArrayLike.get_ofFn_go (Algdata/Classes/ArrayLike.lean)

State before:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
⊢ (i ≥ j → (ofFn.go cont f j x)[i] = f { val := i, isLt := hi }) ∧ (i < j → (ofFn.go cont f j x)[i] = x[i])
Tactic:
unfold ofFn.go
State after:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
⊢ (i ≥ j →
      (if h : j < len then ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := h }) h) else x)[i] =
        f { val := i, isLt := hi }) ∧
    (i < j →
      (if h : j < len then ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := h }) h) else x)[i] = x[i])

State before:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
⊢ (i ≥ j →
      (if h : j < len then ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := h }) h) else x)[i] =
        f { val := i, isLt := hi }) ∧
    (i < j →
      (if h : j < len then ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := h }) h) else x)[i] = x[i])
Tactic:
if hj : j < len then
  simp only [dif_pos hj]
  have IH := get_ofFn_go f i (j+1) hi
  apply And.intro
  . show i ≥ j → _
    intro hij
    cases Nat.eq_or_lt_of_le hij with
    | inl heq =>
      cases heq
      apply Eq.trans ((IH _).2 i.lt_succ_self)
      exact ArrayLike.get_set_eq x i (f ⟨i,hi⟩)
    | inr hgt => exact Eq.trans ((IH _).1 hgt) rfl
  . show i < j → _
    intro hij
    apply Eq.trans ((IH _).2 (Nat.lt_succ_of_lt hij))
    exact ArrayLike.get_set_ne x (Nat.ne_of_gt hij) (f ⟨j,hj⟩) hi
else
  simp only [dif_neg hj]
  refine And.intro ?_ (fun _ => True.intro)
  intro hij
  have : len ≤ i := trans (r:=LE.le) (s:=LE.le) (Nat.ge_of_not_lt hj) hij
  exact False.elim <| Nat.le_lt_antisymm this hi
State after:
no goals

State before:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
⊢ (i ≥ j →
      (if h : j < len then ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := h }) h) else x)[i] =
        f { val := i, isLt := hi }) ∧
    (i < j →
      (if h : j < len then ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := h }) h) else x)[i] = x[i])
Tactic:
simp only [dif_pos hj]
State after:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
⊢ (i ≥ j →
      (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }) ∧
    (i < j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i])

State before:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
⊢ (i ≥ j →
      (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }) ∧
    (i < j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i])
Tactic:
have IH := get_ofFn_go f i (j+1) hi
State after:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
⊢ (i ≥ j →
      (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }) ∧
    (i < j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i])

State before:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
⊢ (i ≥ j →
      (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }) ∧
    (i < j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i])
Tactic:
apply And.intro
State after:
case left
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
⊢ i ≥ j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }

case right
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
⊢ i < j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i]

State before:
case left
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
⊢ i ≥ j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }

case right
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
⊢ i < j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i]
Tactic:
. show i ≥ j → _
  intro hij
  cases Nat.eq_or_lt_of_le hij with
  | inl heq =>
    cases heq
    apply Eq.trans ((IH _).2 i.lt_succ_self)
    exact ArrayLike.get_set_eq x i (f ⟨i,hi⟩)
  | inr hgt => exact Eq.trans ((IH _).1 hgt) rfl
State after:
case right
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
⊢ i < j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i]

State before:
case right
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
⊢ i < j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i]
Tactic:
. show i < j → _
  intro hij
  apply Eq.trans ((IH _).2 (Nat.lt_succ_of_lt hij))
  exact ArrayLike.get_set_ne x (Nat.ne_of_gt hij) (f ⟨j,hj⟩) hi
State after:
no goals

State before:
case left
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
⊢ i ≥ j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }
Tactic:
intro hij
State after:
case left
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
hij : i ≥ j
⊢ (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }

State before:
case left
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
hij : i ≥ j
⊢ (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }
Tactic:
cases Nat.eq_or_lt_of_le hij with
| inl heq =>
  cases heq
  apply Eq.trans ((IH _).2 i.lt_succ_self)
  exact ArrayLike.get_set_eq x i (f ⟨i,hi⟩)
| inr hgt => exact Eq.trans ((IH _).1 hgt) rfl
State after:
no goals

State before:
case left.inl
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
hij : i ≥ j
heq : j = i
⊢ (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }
Tactic:
cases heq
State after:
case left.inl.refl
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i : Nat
hi : i < len
x : cont
hj : i < len
IH :
  ∀ (x : cont),
    (i ≥ i + 1 → (ofFn.go cont f (i + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < i + 1 → (ofFn.go cont f (i + 1) x)[i] = x[i])
hij : i ≥ i
⊢ (ofFn.go cont f (i + 1) (SetElem.setElem x i (f { val := i, isLt := hj }) hj))[i] = f { val := i, isLt := hi }

State before:
case left.inl.refl
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i : Nat
hi : i < len
x : cont
hj : i < len
IH :
  ∀ (x : cont),
    (i ≥ i + 1 → (ofFn.go cont f (i + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < i + 1 → (ofFn.go cont f (i + 1) x)[i] = x[i])
hij : i ≥ i
⊢ (ofFn.go cont f (i + 1) (SetElem.setElem x i (f { val := i, isLt := hj }) hj))[i] = f { val := i, isLt := hi }
Tactic:
apply Eq.trans ((IH _).2 i.lt_succ_self)
State after:
case left.inl.refl
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i : Nat
hi : i < len
x : cont
hj : i < len
IH :
  ∀ (x : cont),
    (i ≥ i + 1 → (ofFn.go cont f (i + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < i + 1 → (ofFn.go cont f (i + 1) x)[i] = x[i])
hij : i ≥ i
⊢ (SetElem.setElem x i (f { val := i, isLt := hj }) hj)[i] = f { val := i, isLt := hi }

State before:
case left.inl.refl
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i : Nat
hi : i < len
x : cont
hj : i < len
IH :
  ∀ (x : cont),
    (i ≥ i + 1 → (ofFn.go cont f (i + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < i + 1 → (ofFn.go cont f (i + 1) x)[i] = x[i])
hij : i ≥ i
⊢ (SetElem.setElem x i (f { val := i, isLt := hj }) hj)[i] = f { val := i, isLt := hi }
Tactic:
exact ArrayLike.get_set_eq x i (f ⟨i,hi⟩)
State after:
no goals

State before:
case left.inr
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
hij : i ≥ j
hgt : j < i
⊢ (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = f { val := i, isLt := hi }
Tactic:
exact Eq.trans ((IH _).1 hgt) rfl
State after:
no goals

State before:
case right
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
⊢ i < j → (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i]
Tactic:
intro hij
State after:
case right
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
hij : i < j
⊢ (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i]

State before:
case right
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
hij : i < j
⊢ (ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := hj }) hj))[i] = x[i]
Tactic:
apply Eq.trans ((IH _).2 (Nat.lt_succ_of_lt hij))
State after:
case right
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
hij : i < j
⊢ (SetElem.setElem x j (f { val := j, isLt := hj }) hj)[i] = x[i]

State before:
case right
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : j < len
IH :
  ∀ (x : cont),
    (i ≥ j + 1 → (ofFn.go cont f (j + 1) x)[i] = f { val := i, isLt := hi }) ∧
      (i < j + 1 → (ofFn.go cont f (j + 1) x)[i] = x[i])
hij : i < j
⊢ (SetElem.setElem x j (f { val := j, isLt := hj }) hj)[i] = x[i]
Tactic:
exact ArrayLike.get_set_ne x (Nat.ne_of_gt hij) (f ⟨j,hj⟩) hi
State after:
no goals

State before:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : ¬j < len
⊢ (i ≥ j →
      (if h : j < len then ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := h }) h) else x)[i] =
        f { val := i, isLt := hi }) ∧
    (i < j →
      (if h : j < len then ofFn.go cont f (j + 1) (SetElem.setElem x j (f { val := j, isLt := h }) h) else x)[i] = x[i])
Tactic:
simp only [dif_neg hj]
State after:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : ¬j < len
⊢ (i ≥ j → x[i] = f { val := i, isLt := hi }) ∧ (i < j → True)

State before:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : ¬j < len
⊢ (i ≥ j → x[i] = f { val := i, isLt := hi }) ∧ (i < j → True)
Tactic:
refine And.intro ?_ (fun _ => True.intro)
State after:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : ¬j < len
⊢ i ≥ j → x[i] = f { val := i, isLt := hi }

State before:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : ¬j < len
⊢ i ≥ j → x[i] = f { val := i, isLt := hi }
Tactic:
intro hij
State after:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : ¬j < len
hij : i ≥ j
⊢ x[i] = f { val := i, isLt := hi }

State before:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : ¬j < len
hij : i ≥ j
⊢ x[i] = f { val := i, isLt := hi }
Tactic:
have : len ≤ i := trans (r:=LE.le) (s:=LE.le) (Nat.ge_of_not_lt hj) hij
State after:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : ¬j < len
hij : i ≥ j
this : len ≤ i
⊢ x[i] = f { val := i, isLt := hi }

State before:
cont : Type u
elem : Type w
len : Nat
inst✝ : SizedArrayLike cont Nat elem (fun x => x < len) fun i x => i < len
f : Fin len → elem
i j : Nat
hi : i < len
x : cont
hj : ¬j < len
hij : i ≥ j
this : len ≤ i
⊢ x[i] = f { val := i, isLt := hi }
Tactic:
exact False.elim <| Nat.le_lt_antisymm this hi
State after:
no goals