internlm/Lean-Github huggingface dataset:
Theorem: Array.ofFn_go_succ
Proof state before:
α : Type u
n : Nat
f : Fin (n + 1) → α
i : Nat
acc : Array α
H : i < n + 1
h : i < n
⊢ ofFn.go f i acc =
    push (ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) i acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Tactic:
unfold ofFn.go
Proof state after:
α : Type u
n : Nat
f : Fin (n + 1) → α
i : Nat
acc : Array α
H : i < n + 1
h : i < n
⊢ (if h : i < n + 1 then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) =
    push
      (if h : i < n then
        ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (i + 1)
          (push acc (f { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) }))
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Theorem: Array.ofFn_go_succ
Proof state before:
α : Type u
n : Nat
f : Fin (n + 1) → α
i : Nat
acc : Array α
H : i < n + 1
h : i < n
⊢ (if h : i < n + 1 then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) =
    push
      (if h : i < n then
        ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (i + 1)
          (push acc (f { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) }))
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Tactic:
rw [dif_pos H, dif_pos h]
Proof state after:
α : Type u
n : Nat
f : Fin (n + 1) → α
i : Nat
acc : Array α
H : i < n + 1
h : i < n
⊢ ofFn.go f (i + 1) (push acc (f { val := i, isLt := H })) =
    push
      (ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (i + 1)
        (push acc (f { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) })))
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Theorem: Array.ofFn_go_succ
Proof state before:
α : Type u
n : Nat
f : Fin (n + 1) → α
i : Nat
acc : Array α
H : i < n + 1
h : i < n
⊢ ofFn.go f (i + 1) (push acc (f { val := i, isLt := H })) =
    push
      (ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (i + 1)
        (push acc (f { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < Nat.succ n) })))
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Tactic:
exact ofFn_go_succ f (i+1) _ (Nat.succ_lt_succ h)
Proof state after:
no goals
Theorem: Array.ofFn_go_succ
Proof state before:
α : Type u
n : Nat
f : Fin (n + 1) → α
i : Nat
acc : Array α
H : i < n + 1
h : i = n
⊢ ofFn.go f i acc =
    push (ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) i acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Tactic:
cases h
Proof state after:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ ofFn.go f n acc =
    push (ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) n acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Theorem: Array.ofFn_go_succ
Proof state before:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ ofFn.go f n acc =
    push (ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) n acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Tactic:
unfold ofFn.go
Proof state after:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ (if h : n < n + 1 then ofFn.go f (n + 1) (push acc (f { val := n, isLt := h })) else acc) =
    push
      (if h : n < n then
        ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1)
          (push acc (f { val := ↑{ val := n, isLt := h }, isLt := (_ : ↑{ val := n, isLt := h } < Nat.succ n) }))
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Theorem: Array.ofFn_go_succ
Proof state before:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ (if h : n < n + 1 then ofFn.go f (n + 1) (push acc (f { val := n, isLt := h })) else acc) =
    push
      (if h : n < n then
        ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1)
          (push acc (f { val := ↑{ val := n, isLt := h }, isLt := (_ : ↑{ val := n, isLt := h } < Nat.succ n) }))
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Tactic:
rw [dif_pos n.lt_succ_self]
Proof state after:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ ofFn.go f (n + 1) (push acc (f { val := n, isLt := (_ : n < Nat.succ n) })) =
    push
      (if h : n < n then
        ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1)
          (push acc (f { val := ↑{ val := n, isLt := h }, isLt := (_ : ↑{ val := n, isLt := h } < Nat.succ n) }))
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Theorem: Array.ofFn_go_succ
Proof state before:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ ofFn.go f (n + 1) (push acc (f { val := n, isLt := (_ : n < Nat.succ n) })) =
    push
      (if h : n < n then
        ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1)
          (push acc (f { val := ↑{ val := n, isLt := h }, isLt := (_ : ↑{ val := n, isLt := h } < Nat.succ n) }))
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Tactic:
unfold ofFn.go
Proof state after:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ (if h : n + 1 < n + 1 then
      ofFn.go f (n + 1 + 1)
        (push (push acc (f { val := n, isLt := (_ : n < Nat.succ n) })) (f { val := n + 1, isLt := h }))
    else push acc (f { val := n, isLt := (_ : n < Nat.succ n) })) =
    push
      (if h : n < n then
        if h_1 : n + 1 < n then
          ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1 + 1)
            (push
              (push acc
                (f
                  { val := ↑{ val := n, isLt := (_ : n < n) },
                    isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
              (f { val := ↑{ val := n + 1, isLt := h_1 }, isLt := (_ : ↑{ val := n + 1, isLt := h_1 } < Nat.succ n) }))
        else
          push acc
            (f
              { val := ↑{ val := n, isLt := (_ : n < n) },
                isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) })
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Theorem: Array.ofFn_go_succ
Proof state before:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ (if h : n + 1 < n + 1 then
      ofFn.go f (n + 1 + 1)
        (push (push acc (f { val := n, isLt := (_ : n < Nat.succ n) })) (f { val := n + 1, isLt := h }))
    else push acc (f { val := n, isLt := (_ : n < Nat.succ n) })) =
    push
      (if h : n < n then
        if h_1 : n + 1 < n then
          ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1 + 1)
            (push
              (push acc
                (f
                  { val := ↑{ val := n, isLt := (_ : n < n) },
                    isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
              (f { val := ↑{ val := n + 1, isLt := h_1 }, isLt := (_ : ↑{ val := n + 1, isLt := h_1 } < Nat.succ n) }))
        else
          push acc
            (f
              { val := ↑{ val := n, isLt := (_ : n < n) },
                isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) })
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Tactic:
rw [dif_neg (n+1).lt_irrefl]
Proof state after:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ push acc (f { val := n, isLt := (_ : n < Nat.succ n) }) =
    push
      (if h : n < n then
        if h_1 : n + 1 < n then
          ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1 + 1)
            (push
              (push acc
                (f
                  { val := ↑{ val := n, isLt := (_ : n < n) },
                    isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
              (f { val := ↑{ val := n + 1, isLt := h_1 }, isLt := (_ : ↑{ val := n + 1, isLt := h_1 } < Nat.succ n) }))
        else
          push acc
            (f
              { val := ↑{ val := n, isLt := (_ : n < n) },
                isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) })
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Theorem: Array.ofFn_go_succ
Proof state before:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ push acc (f { val := n, isLt := (_ : n < Nat.succ n) }) =
    push
      (if h : n < n then
        if h_1 : n + 1 < n then
          ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1 + 1)
            (push
              (push acc
                (f
                  { val := ↑{ val := n, isLt := (_ : n < n) },
                    isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
              (f { val := ↑{ val := n + 1, isLt := h_1 }, isLt := (_ : ↑{ val := n + 1, isLt := h_1 } < Nat.succ n) }))
        else
          push acc
            (f
              { val := ↑{ val := n, isLt := (_ : n < n) },
                isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) })
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Tactic:
unfold ofFn.go
Proof state after:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ push acc (f { val := n, isLt := (_ : n < Nat.succ n) }) =
    push
      (if h : n < n then
        if h_1 : n + 1 < n then
          if h_2 : n + 1 + 1 < n then
            ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1 + 1 + 1)
              (push
                (push
                  (push acc
                    (f
                      { val := ↑{ val := n, isLt := (_ : n < n) },
                        isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
                  (f
                    { val := ↑{ val := n + 1, isLt := (_ : n + 1 < n) },
                      isLt := (_ : ↑{ val := n + 1, isLt := (_ : n + 1 < n) } < Nat.succ n) }))
                (f
                  { val := ↑{ val := n + 1 + 1, isLt := h_2 },
                    isLt := (_ : ↑{ val := n + 1 + 1, isLt := h_2 } < Nat.succ n) }))
          else
            push
              (push acc
                (f
                  { val := ↑{ val := n, isLt := (_ : n < n) },
                    isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
              (f
                { val := ↑{ val := n + 1, isLt := (_ : n + 1 < n) },
                  isLt := (_ : ↑{ val := n + 1, isLt := (_ : n + 1 < n) } < Nat.succ n) })
        else
          push acc
            (f
              { val := ↑{ val := n, isLt := (_ : n < n) },
                isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) })
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Theorem: Array.ofFn_go_succ
Proof state before:
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ push acc (f { val := n, isLt := (_ : n < Nat.succ n) }) =
    push
      (if h : n < n then
        if h_1 : n + 1 < n then
          if h_2 : n + 1 + 1 < n then
            ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1 + 1 + 1)
              (push
                (push
                  (push acc
                    (f
                      { val := ↑{ val := n, isLt := (_ : n < n) },
                        isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
                  (f
                    { val := ↑{ val := n + 1, isLt := (_ : n + 1 < n) },
                      isLt := (_ : ↑{ val := n + 1, isLt := (_ : n + 1 < n) } < Nat.succ n) }))
                (f
                  { val := ↑{ val := n + 1 + 1, isLt := h_2 },
                    isLt := (_ : ↑{ val := n + 1 + 1, isLt := h_2 } < Nat.succ n) }))
          else
            push
              (push acc
                (f
                  { val := ↑{ val := n, isLt := (_ : n < n) },
                    isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
              (f
                { val := ↑{ val := n + 1, isLt := (_ : n + 1 < n) },
                  isLt := (_ : ↑{ val := n + 1, isLt := (_ : n + 1 < n) } < Nat.succ n) })
        else
          push acc
            (f
              { val := ↑{ val := n, isLt := (_ : n < n) },
                isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) })
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
Tactic:
rw [dif_neg n.lt_irrefl]
Proof state after:
no goals
Theorem: Array.getElem_ofFn'
Proof state before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
⊢ (ofFn f)[i] = f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
simp only [ofFn_succ f, get_push']
Proof state after:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
⊢ (if h : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) then
      (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i]
    else f { val := n, isLt := (_ : n < Nat.succ n) }) =
    f { val := i, isLt := (_ : i < Nat.succ n) }
Theorem: Array.getElem_ofFn'
Proof state before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
⊢ (if h : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) then
      (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i]
    else f { val := n, isLt := (_ : n < Nat.succ n) }) =
    f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
if h' : i < size (ofFn λ x => f ⟨x.1, Nat.lt_succ_of_lt x.2⟩)
then rw [dif_pos h']; exact IH _ h'
else
  rw [dif_neg h']
  suffices i = n by cases this; rfl
  simp only [size_ofFn] at h h'
  exact Nat.le_antisymm (Nat.le_of_succ_le_succ h) (Nat.ge_of_not_lt h')
Proof state after:
no goals
Theorem: Array.getElem_ofFn'
Proof state before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ (if h : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) then
      (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i]
    else f { val := n, isLt := (_ : n < Nat.succ n) }) =
    f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
rw [dif_pos h']
Proof state after:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i] = f { val := i, isLt := (_ : i < Nat.succ n) }
Theorem: Array.getElem_ofFn'
Proof state before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i] = f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
exact IH _ h'
Proof state after:
no goals
Theorem: Array.getElem_ofFn'
Proof state before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ (if h : i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) then
      (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })[i]
    else f { val := n, isLt := (_ : n < Nat.succ n) }) =
    f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
rw [dif_neg h']
Proof state after:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ f { val := n, isLt := (_ : n < Nat.succ n) } = f { val := i, isLt := (_ : i < Nat.succ n) }
Theorem: Array.getElem_ofFn'
Proof state before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ f { val := n, isLt := (_ : n < Nat.succ n) } = f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
suffices i = n by cases this; rfl
Proof state after:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ i = n
Theorem: Array.getElem_ofFn'
Proof state before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
⊢ i = n
Tactic:
simp only [size_ofFn] at h h'
Proof state after:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < Nat.succ n
h' : ¬i < n
⊢ i = n
Theorem: Array.getElem_ofFn'
Proof state before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < Nat.succ n
h' : ¬i < n
⊢ i = n
Tactic:
exact Nat.le_antisymm (Nat.le_of_succ_le_succ h) (Nat.ge_of_not_lt h')
Proof state after:
no goals
Theorem: Array.getElem_ofFn'
Proof state before:
α : Type u
n✝ : Nat
f✝ : Fin n✝ → α
i n : Nat
IH : ∀ (x : Fin n → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < n) }
f : Fin (Nat.succ n) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) })
this : i = n
⊢ f { val := n, isLt := (_ : n < Nat.succ n) } = f { val := i, isLt := (_ : i < Nat.succ n) }
Tactic:
cases this
Proof state after:
case refl
α : Type u
n : Nat
f✝ : Fin n → α
i : Nat
IH : ∀ (x : Fin i → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < i) }
f : Fin (Nat.succ i) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ i) })
⊢ f { val := i, isLt := (_ : i < Nat.succ i) } = f { val := i, isLt := (_ : i < Nat.succ i) }
Theorem: Array.getElem_ofFn'
Proof state before:
case refl
α : Type u
n : Nat
f✝ : Fin n → α
i : Nat
IH : ∀ (x : Fin i → α) (h : i < size (ofFn x)), (ofFn x)[i] = x { val := i, isLt := (_ : i < i) }
f : Fin (Nat.succ i) → α
h : i < size (ofFn f)
h' : ¬i < size (ofFn fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ i) })
⊢ f { val := i, isLt := (_ : i < Nat.succ i) } = f { val := i, isLt := (_ : i < Nat.succ i) }
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.ofFn_go_eq
Proof state before:
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]
Tactic:
by_cases i < n
Proof state after:
case pos
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
h✝ : i < n
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]

case neg
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
h✝ : ¬i < n
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]
Theorem: Array.ofFn_go_eq
Proof state before:
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]
Tactic:
case pos hlt =>
  refine Nat.recAscend (motive:=λ i => ∀ acc, Array.ofFn.go f i acc = acc ++ Array.ofFn.go f i #[]) (n:=n) ?_ ?_ i (Nat.le_of_lt hlt) acc
  . dsimp; unfold Array.ofFn.go
    intro acc
    rw [dif_neg (Nat.lt_irrefl n), dif_neg (Nat.lt_irrefl n)]
    rfl
  . dsimp
    intro i hi h_ind acc
    unfold Array.ofFn.go
    rw [dif_pos hi, dif_pos hi]
    rw [h_ind (acc.push _), h_ind (#[].push _)]
    conv =>
      rhs; rw [←Array.append_assoc]
Proof state after:
no goals
Theorem: Array.ofFn_go_eq
Proof state before:
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hnlt : ¬i < n
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]
Tactic:
case neg hnlt =>
  unfold Array.ofFn.go
  rw [dif_neg hnlt, dif_neg hnlt]
  rfl
Proof state after:
no goals
Theorem: Array.ofFn_go_eq
Proof state before:
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]
Tactic:
refine Nat.recAscend (motive:=λ i => ∀ acc, Array.ofFn.go f i acc = acc ++ Array.ofFn.go f i #[]) (n:=n) ?_ ?_ i (Nat.le_of_lt hlt) acc
Proof state after:
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) n

case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) (Nat.succ k) →
        (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) k
Theorem: Array.ofFn_go_eq
Proof state before:
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) n

case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) (Nat.succ k) →
        (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) k
Tactic:
. dsimp; unfold Array.ofFn.go
  intro acc
  rw [dif_neg (Nat.lt_irrefl n), dif_neg (Nat.lt_irrefl n)]
  rfl
Proof state after:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) (Nat.succ k) →
        (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) k
Theorem: Array.ofFn_go_eq
Proof state before:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) (Nat.succ k) →
        (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) k
Tactic:
. dsimp
  intro i hi h_ind acc
  unfold Array.ofFn.go
  rw [dif_pos hi, dif_pos hi]
  rw [h_ind (acc.push _), h_ind (#[].push _)]
  conv =>
    rhs; rw [←Array.append_assoc]
Proof state after:
no goals
Theorem: Array.ofFn_go_eq
Proof state before:
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ (fun i => ∀ (acc : Array α), ofFn.go f i acc = acc ++ ofFn.go f i #[]) n
Tactic:
dsimp
Proof state after:
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (acc : Array α), ofFn.go f n acc = acc ++ ofFn.go f n #[]
Theorem: Array.ofFn_go_eq
Proof state before:
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (acc : Array α), ofFn.go f n acc = acc ++ ofFn.go f n #[]
Tactic:
unfold Array.ofFn.go
Proof state after:
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (acc : Array α),
    (if h : n < n then ofFn.go f (n + 1) (push acc (f { val := n, isLt := h })) else acc) =
      acc ++ if h : n < n then ofFn.go f (n + 1) (push #[] (f { val := n, isLt := h })) else #[]