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

State before:
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
⊢ ofFn.go f (Nat.succ i) acc = ofFn.go (f ∘ Fin.succ) i acc
Tactic:
by_cases i < n
State after:
case pos
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
h✝ : i < n
⊢ ofFn.go f (Nat.succ i) acc = ofFn.go (f ∘ Fin.succ) i acc

case neg
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
h✝ : ¬i < n
⊢ ofFn.go f (Nat.succ i) acc = ofFn.go (f ∘ Fin.succ) i acc

State before:
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hnlt : ¬i < n
⊢ ofFn.go f (Nat.succ i) acc = ofFn.go (f ∘ Fin.succ) i acc
Tactic:
case neg hnlt =>
  have : ¬ i.succ < n.succ := λ h => absurd (Nat.lt_of_succ_lt_succ h) hnlt
  unfold Array.ofFn.go
  rw [dif_neg this, dif_neg hnlt]
State after:
no goals

State before:
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hlt : i < n
⊢ ofFn.go f (Nat.succ i) acc = ofFn.go (f ∘ Fin.succ) i acc
Tactic:
case pos hlt =>
  refine Nat.recAscend (motive:=λ i =>∀ acc, Array.ofFn.go f i.succ acc = Array.ofFn.go (f ∘ Fin.succ) i acc) ?_ ?_ i (Nat.le_of_lt hlt) acc
    <;> dsimp
  . intro acc
    unfold Array.ofFn.go
    rw [dif_neg (Nat.lt_irrefl n.succ), dif_neg (Nat.lt_irrefl n)]
  . intro i hi h_ind acc
    unfold Array.ofFn.go
    rw [dif_pos (Nat.succ_lt_succ hi), dif_pos hi]
    rw [h_ind]
    rfl
State after:
no goals

State before:
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hnlt : ¬i < n
⊢ ofFn.go f (Nat.succ i) acc = ofFn.go (f ∘ Fin.succ) i acc
Tactic:
have : ¬ i.succ < n.succ := λ h => absurd (Nat.lt_of_succ_lt_succ h) hnlt
State after:
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hnlt : ¬i < n
this : ¬Nat.succ i < Nat.succ n
⊢ ofFn.go f (Nat.succ i) acc = ofFn.go (f ∘ Fin.succ) i acc

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

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

State before:
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hlt : i < n
⊢ ofFn.go f (Nat.succ i) acc = ofFn.go (f ∘ Fin.succ) i acc
Tactic:
refine Nat.recAscend (motive:=λ i =>∀ acc, Array.ofFn.go f i.succ acc = Array.ofFn.go (f ∘ Fin.succ) i acc) ?_ ?_ i (Nat.le_of_lt hlt) acc
  <;> dsimp
State after:
case refine_1
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (acc : Array α), ofFn.go f (Nat.succ n) acc = ofFn.go (f ∘ Fin.succ) n acc

case refine_2
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (∀ (acc : Array α), ofFn.go f (Nat.succ (Nat.succ k)) acc = ofFn.go (f ∘ Fin.succ) (Nat.succ k) acc) →
        ∀ (acc : Array α), ofFn.go f (Nat.succ k) acc = ofFn.go (f ∘ Fin.succ) k acc

State before:
case refine_1
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (acc : Array α), ofFn.go f (Nat.succ n) acc = ofFn.go (f ∘ Fin.succ) n acc

case refine_2
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (∀ (acc : Array α), ofFn.go f (Nat.succ (Nat.succ k)) acc = ofFn.go (f ∘ Fin.succ) (Nat.succ k) acc) →
        ∀ (acc : Array α), ofFn.go f (Nat.succ k) acc = ofFn.go (f ∘ Fin.succ) k acc
Tactic:
. intro acc
  unfold Array.ofFn.go
  rw [dif_neg (Nat.lt_irrefl n.succ), dif_neg (Nat.lt_irrefl n)]
State after:
case refine_2
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (∀ (acc : Array α), ofFn.go f (Nat.succ (Nat.succ k)) acc = ofFn.go (f ∘ Fin.succ) (Nat.succ k) acc) →
        ∀ (acc : Array α), ofFn.go f (Nat.succ k) acc = ofFn.go (f ∘ Fin.succ) k acc

State before:
case refine_2
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (k : Nat),
    k < n →
      (∀ (acc : Array α), ofFn.go f (Nat.succ (Nat.succ k)) acc = ofFn.go (f ∘ Fin.succ) (Nat.succ k) acc) →
        ∀ (acc : Array α), ofFn.go f (Nat.succ k) acc = ofFn.go (f ∘ Fin.succ) k acc
Tactic:
. intro i hi h_ind acc
  unfold Array.ofFn.go
  rw [dif_pos (Nat.succ_lt_succ hi), dif_pos hi]
  rw [h_ind]
  rfl
State after:
no goals

State before:
case refine_1
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc : Array α
hlt : i < n
⊢ ∀ (acc : Array α), ofFn.go f (Nat.succ n) acc = ofFn.go (f ∘ Fin.succ) n acc
Tactic:
intro acc
State after:
case refine_1
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc✝ : Array α
hlt : i < n
acc : Array α
⊢ ofFn.go f (Nat.succ n) acc = ofFn.go (f ∘ Fin.succ) n acc

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

State before:
case refine_1
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc✝ : Array α
hlt : i < n
acc : Array α
⊢ (if h : Nat.succ n < Nat.succ n then ofFn.go f (Nat.succ n + 1) (push acc (f { val := Nat.succ n, isLt := h }))
    else acc) =
    if h : n < n then ofFn.go (f ∘ Fin.succ) (n + 1) (push acc ((f ∘ Fin.succ) { val := n, isLt := h })) else acc
Tactic:
rw [dif_neg (Nat.lt_irrefl n.succ), dif_neg (Nat.lt_irrefl n)]
State after:
no goals

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

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

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

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

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