Theorem: Array.ofFn_go_succ (Algdata/Data/Array/Lemmas.lean)

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
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) })

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]
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) })

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)
State after:
no goals

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
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) })

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
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) })

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]
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) })

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
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) })

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]
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) })

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
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) })

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]
State after:
no goals