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

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
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 #[]

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

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

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

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

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

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
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 #[]

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
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 #[]

State before:
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 #[]
Tactic:
intro acc
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 #[]

State before:
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 #[]
Tactic:
rw [dif_neg (Nat.lt_irrefl n), dif_neg (Nat.lt_irrefl n)]
State after:
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc✝ : Array α
hlt : i < n
acc : Array α
⊢ acc = acc ++ #[]

State before:
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc✝ : Array α
hlt : i < n
acc : Array α
⊢ acc = acc ++ #[]
Tactic:
rfl
State after:
no goals

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
State after:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (∀ (acc : Array α), ofFn.go f (Nat.succ k) acc = acc ++ ofFn.go f (Nat.succ k) #[]) →
        ∀ (acc : Array α), ofFn.go f k acc = acc ++ ofFn.go f k #[]

State before:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (∀ (acc : Array α), ofFn.go f (Nat.succ k) acc = acc ++ ofFn.go f (Nat.succ k) #[]) →
        ∀ (acc : Array α), ofFn.go f k acc = acc ++ ofFn.go f k #[]
Tactic:
intro i hi h_ind acc
State after:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i✝ : Nat
acc✝ : Array α
hlt : i✝ < n
i : Nat
hi : i < n
h_ind : ∀ (acc : Array α), ofFn.go f (Nat.succ i) acc = acc ++ ofFn.go f (Nat.succ i) #[]
acc : Array α
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]

State before:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i✝ : Nat
acc✝ : Array α
hlt : i✝ < n
i : Nat
hi : i < n
h_ind : ∀ (acc : Array α), ofFn.go f (Nat.succ i) acc = acc ++ ofFn.go f (Nat.succ i) #[]
acc : Array α
⊢ ofFn.go f i acc = acc ++ ofFn.go f i #[]
Tactic:
unfold Array.ofFn.go
State after:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i✝ : Nat
acc✝ : Array α
hlt : i✝ < n
i : Nat
hi : i < n
h_ind : ∀ (acc : Array α), ofFn.go f (Nat.succ i) acc = acc ++ ofFn.go f (Nat.succ i) #[]
acc : Array α
⊢ (if h : i < n then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) =
    acc ++ if h : i < n then ofFn.go f (i + 1) (push #[] (f { val := i, isLt := h })) else #[]

State before:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i✝ : Nat
acc✝ : Array α
hlt : i✝ < n
i : Nat
hi : i < n
h_ind : ∀ (acc : Array α), ofFn.go f (Nat.succ i) acc = acc ++ ofFn.go f (Nat.succ i) #[]
acc : Array α
⊢ (if h : i < n then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) =
    acc ++ if h : i < n then ofFn.go f (i + 1) (push #[] (f { val := i, isLt := h })) else #[]
Tactic:
rw [dif_pos hi, dif_pos hi]
State after:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i✝ : Nat
acc✝ : Array α
hlt : i✝ < n
i : Nat
hi : i < n
h_ind : ∀ (acc : Array α), ofFn.go f (Nat.succ i) acc = acc ++ ofFn.go f (Nat.succ i) #[]
acc : Array α
⊢ ofFn.go f (i + 1) (push acc (f { val := i, isLt := hi })) =
    acc ++ ofFn.go f (i + 1) (push #[] (f { val := i, isLt := hi }))

State before:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i✝ : Nat
acc✝ : Array α
hlt : i✝ < n
i : Nat
hi : i < n
h_ind : ∀ (acc : Array α), ofFn.go f (Nat.succ i) acc = acc ++ ofFn.go f (Nat.succ i) #[]
acc : Array α
⊢ ofFn.go f (i + 1) (push acc (f { val := i, isLt := hi })) =
    acc ++ ofFn.go f (i + 1) (push #[] (f { val := i, isLt := hi }))
Tactic:
rw [h_ind (acc.push _), h_ind (#[].push _)]
State after:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i✝ : Nat
acc✝ : Array α
hlt : i✝ < n
i : Nat
hi : i < n
h_ind : ∀ (acc : Array α), ofFn.go f (Nat.succ i) acc = acc ++ ofFn.go f (Nat.succ i) #[]
acc : Array α
⊢ push acc (f { val := i, isLt := hi }) ++ ofFn.go f (Nat.succ i) #[] =
    acc ++ (push #[] (f { val := i, isLt := hi }) ++ ofFn.go f (Nat.succ i) #[])

State before:
case refine_2
α✝ α : Type u
n : Nat
f : Fin n → α
i✝ : Nat
acc✝ : Array α
hlt : i✝ < n
i : Nat
hi : i < n
h_ind : ∀ (acc : Array α), ofFn.go f (Nat.succ i) acc = acc ++ ofFn.go f (Nat.succ i) #[]
acc : Array α
⊢ push acc (f { val := i, isLt := hi }) ++ ofFn.go f (Nat.succ i) #[] =
    acc ++ (push #[] (f { val := i, isLt := hi }) ++ ofFn.go f (Nat.succ i) #[])
Tactic:
conv =>
  rhs; rw [←Array.append_assoc]
State after:
no goals

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:
unfold Array.ofFn.go
State after:
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hnlt : ¬i < n
⊢ (if h : i < n then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) =
    acc ++ if h : i < n then ofFn.go f (i + 1) (push #[] (f { val := i, isLt := h })) else #[]

State before:
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hnlt : ¬i < n
⊢ (if h : i < n then ofFn.go f (i + 1) (push acc (f { val := i, isLt := h })) else acc) =
    acc ++ if h : i < n then ofFn.go f (i + 1) (push #[] (f { val := i, isLt := h })) else #[]
Tactic:
rw [dif_neg hnlt, dif_neg hnlt]
State after:
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hnlt : ¬i < n
⊢ acc = acc ++ #[]

State before:
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hnlt : ¬i < n
⊢ acc = acc ++ #[]
Tactic:
rfl
State after:
no goals