internlm/Lean-Github huggingface dataset:
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof 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])
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof state after:
no goals
Theorem: SizedArrayLike.get_ofFn_go
Proof 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]
Proof 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])
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof 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])
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof 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]
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof 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]
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof state after:
no goals
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof 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 }
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof state after:
no goals
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof 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 }
Theorem: SizedArrayLike.get_ofFn_go
Proof 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)
Proof 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 }
Theorem: SizedArrayLike.get_ofFn_go
Proof 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⟩)
Proof state after:
no goals
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof state after:
no goals
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof 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]
Theorem: SizedArrayLike.get_ofFn_go
Proof 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))
Proof 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]
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof state after:
no goals
Theorem: SizedArrayLike.get_ofFn_go
Proof 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]
Proof 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)
Theorem: SizedArrayLike.get_ofFn_go
Proof 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)
Proof 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 }
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof 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 }
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof 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 }
Theorem: SizedArrayLike.get_ofFn_go
Proof 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
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.leaf
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
⊢ IsHeap lt x i
Tactic:
if hi : i < x.size then
  have hr : 2*i+2 ≥ x.size := .step hl
  refine .node' i hi ?_ ?_ (.out_of_range _ hl) (.out_of_range _ hr)
  . intro hl'; exact absurd hl' (Nat.not_lt_of_le hl)
  . intro hr'; exact absurd hr' (Nat.not_lt_of_le hr)
else
  exact .out_of_range i (Nat.ge_of_not_lt hi)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.leaf
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
⊢ IsHeap lt x i
Tactic:
have hr : 2*i+2 ≥ x.size := .step hl
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ IsHeap lt x i
Theorem: Algdata.BinaryHeap.IsHeap.leaf
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ IsHeap lt x i
Tactic:
refine .node' i hi ?_ ?_ (.out_of_range _ hl) (.out_of_range _ hr)
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.leaf
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Tactic:
. intro hl'; exact absurd hl' (Nat.not_lt_of_le hl)
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.leaf
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Tactic:
. intro hr'; exact absurd hr' (Nat.not_lt_of_le hr)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.leaf
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
Tactic:
intro hl'
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hl' : 2 * i + 1 < Subarray.size x
⊢ lt x[i] x[2 * i + 1] = false
Theorem: Algdata.BinaryHeap.IsHeap.leaf
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hl' : 2 * i + 1 < Subarray.size x
⊢ lt x[i] x[2 * i + 1] = false
Tactic:
exact absurd hl' (Nat.not_lt_of_le hl)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.leaf
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Tactic:
intro hr'
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hr' : 2 * i + 2 < Subarray.size x
⊢ lt x[i] x[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.leaf
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : i < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hr' : 2 * i + 2 < Subarray.size x
⊢ lt x[i] x[2 * i + 2] = false
Tactic:
exact absurd hr' (Nat.not_lt_of_le hr)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.leaf
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
hi : ¬i < Subarray.size x
⊢ IsHeap lt x i
Tactic:
exact .out_of_range i (Nat.ge_of_not_lt hi)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.node_odd
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ IsHeap lt x i
Tactic:
have hleft : IsHeap lt x (2*i+1) := by
  refine .leaf lt x _ (Nat.le_trans hr ?_)
  conv =>
    rhs
    rewrite [Nat.two_mul (2*i+1), Nat.add_assoc _ _ 1, Nat.add_comm (2*i+1) 1, ←Nat.add_assoc _ 1 _]
    change 2*i+2+(2*i+1)
  exact Nat.le_add_right (2*i+2) (2*i+1)
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
⊢ IsHeap lt x i