internlm/Lean-Github huggingface dataset:
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 α),
    (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
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 #[]
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 α
⊢ (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)]
Proof state after:
case refine_1
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc✝ : Array α
hlt : i < n
acc : Array α
⊢ acc = acc ++ #[]
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 α
⊢ acc = acc ++ #[]
Tactic:
rfl
Proof state after:
no goals
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
Proof 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 #[]
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 →
      (∀ (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
Proof 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 #[]
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
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
Proof 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 #[]
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
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]
Proof 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 }))
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
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 _)]
Proof 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) #[])
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
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]
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:
unfold Array.ofFn.go
Proof 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 #[]
Theorem: Array.ofFn_go_eq
Proof 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]
Proof state after:
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hnlt : ¬i < n
⊢ acc = acc ++ #[]
Theorem: Array.ofFn_go_eq
Proof state before:
α✝ α : Type u
n : Nat
f : Fin n → α
i : Nat
acc : Array α
hnlt : ¬i < n
⊢ acc = acc ++ #[]
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.ofFn_go_succ'
Proof 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
Proof 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
Theorem: Array.ofFn_go_succ'
Proof 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]
Proof state after:
no goals
Theorem: Array.ofFn_go_succ'
Proof 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
Proof state after:
no goals
Theorem: Array.ofFn_go_succ'
Proof 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
Proof 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
Theorem: Array.ofFn_go_succ'
Proof 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
Proof 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
Theorem: Array.ofFn_go_succ'
Proof 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]
Proof state after:
no goals
Theorem: Array.ofFn_go_succ'
Proof 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
Proof 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
Theorem: Array.ofFn_go_succ'
Proof 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)]
Proof 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
Theorem: Array.ofFn_go_succ'
Proof 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
Proof state after:
no goals
Theorem: Array.ofFn_go_succ'
Proof 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
Proof 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
Theorem: Array.ofFn_go_succ'
Proof 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
Proof 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
Theorem: Array.ofFn_go_succ'
Proof 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)]
Proof state after:
no goals
Theorem: Array.ofFn_go_succ'
Proof 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
Proof 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
Theorem: Array.ofFn_go_succ'
Proof 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
Proof 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
Theorem: Array.ofFn_go_succ'
Proof 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]
Proof 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 }))
Theorem: Array.ofFn_go_succ'
Proof 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]
Proof 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 }))
Theorem: Array.ofFn_go_succ'
Proof 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
Proof state after:
no goals
Theorem: Array.ofFn_succ'
Proof state before:
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
⊢ (ofFn f).data = f { val := 0, isLt := (_ : 0 < Nat.succ n) } :: (ofFn (f ∘ Fin.succ)).data
Tactic:
conv =>
  lhs; unfold Array.ofFn; unfold Array.ofFn.go
  rw [dif_pos n.zero_lt_succ]
  rw [Array.ofFn_go_succ', Array.ofFn_go_eq]
  rw [Array.append_data']
Proof state after:
no goals
Theorem: Array.foldl_ofFn_eq
Proof state before:
α✝ α : Type u
β : Type v
init : β
g : β → α → β
n : Nat
f : Fin n → α
⊢ foldl g init (ofFn f) 0 (size (ofFn f)) = Fin.foldAll (flip g ∘ f) init
Tactic:
rw [Array.foldl_eq_foldl_data']
Proof state after:
α✝ α : Type u
β : Type v
init : β
g : β → α → β
n : Nat
f : Fin n → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Theorem: Array.foldl_ofFn_eq
Proof state before:
α✝ α : Type u
β : Type v
init : β
g : β → α → β
n : Nat
f : Fin n → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Tactic:
induction n generalizing init
Proof state after:
case zero
α✝ α : Type u
β : Type v
g : β → α → β
init : β
f : Fin Nat.zero → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init

case succ
α✝ α : Type u
β : Type v
g : β → α → β
n✝ : Nat
n_ih✝ : ∀ {init : β} {f : Fin n✝ → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n✝) → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Theorem: Array.foldl_ofFn_eq
Proof state before:
α✝ α : Type u
β : Type v
g : β → α → β
init : β
f : Fin Nat.zero → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Tactic:
case zero => rfl
Proof state after:
no goals
Theorem: Array.foldl_ofFn_eq
Proof state before:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Tactic:
case succ n h_ind =>
  rw [ofFn_succ']; dsimp [List.foldl]; rw [h_ind, Fin.foldAll_succ]; rfl
Proof state after:
no goals
Theorem: Array.foldl_ofFn_eq
Proof state before:
α✝ α : Type u
β : Type v
g : β → α → β
init : β
f : Fin Nat.zero → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.foldl_ofFn_eq
Proof state before:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Tactic:
rw [ofFn_succ']
Proof state after:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g init (f { val := 0, isLt := (_ : 0 < Nat.succ n) } :: (ofFn (f ∘ Fin.succ)).data) =
    Fin.foldAll (flip g ∘ f) init
Theorem: Array.foldl_ofFn_eq
Proof state before:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g init (f { val := 0, isLt := (_ : 0 < Nat.succ n) } :: (ofFn (f ∘ Fin.succ)).data) =
    Fin.foldAll (flip g ∘ f) init
Tactic:
dsimp [List.foldl]
Proof state after:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g (g init (f 0)) (ofFn (f ∘ Fin.succ)).data = Fin.foldAll (flip g ∘ f) init
Theorem: Array.foldl_ofFn_eq
Proof state before:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g (g init (f 0)) (ofFn (f ∘ Fin.succ)).data = Fin.foldAll (flip g ∘ f) init
Tactic:
rw [h_ind, Fin.foldAll_succ]
Proof state after:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ Fin.foldAll (flip g ∘ f ∘ Fin.succ) (g init (f 0)) = Fin.foldAll ((flip g ∘ f) ∘ Fin.succ) ((flip g ∘ f) 0 init)
Theorem: Array.foldl_ofFn_eq
Proof state before:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ Fin.foldAll (flip g ∘ f ∘ Fin.succ) (g init (f 0)) = Fin.foldAll ((flip g ∘ f) ∘ Fin.succ) ((flip g ∘ f) 0 init)
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.nodup_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
x : Array α
a : α
⊢ Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
Tactic:
induction x using cons_induction with
| empty =>
  simp only [nodup_empty, not_mem_empty, not_false_eq_true, and_self, iff_true]
  exact nodup_singleton a
| cons b x IH =>
  simp only [push_cons_eq_cons_push, nodup_cons, mem_push, mem_cons, IH]
  simp only [not_or, and_assoc]
  apply and_congr_right'
  simp only [← and_assoc]; rewrite[and_comm (a:=x.Nodup)]
  apply and_congr_left'; apply and_congr_left'
  exact ⟨Ne.symm, Ne.symm⟩
Proof state after:
no goals
Theorem: Array.nodup_push
Proof state before:
case empty
α : Type u
inst✝ : DecidableEq α
a : α
⊢ Nodup (push #[] a) ↔ Nodup #[] ∧ ¬a ∈ #[]
Tactic:
simp only [nodup_empty, not_mem_empty, not_false_eq_true, and_self, iff_true]
Proof state after:
case empty
α : Type u
inst✝ : DecidableEq α
a : α
⊢ Nodup (push #[] a)
Theorem: Array.nodup_push
Proof state before:
case empty
α : Type u
inst✝ : DecidableEq α
a : α
⊢ Nodup (push #[] a)
Tactic:
exact nodup_singleton a
Proof state after:
no goals
Theorem: Array.nodup_push
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ Nodup (push (cons b x) a) ↔ Nodup (cons b x) ∧ ¬a ∈ cons b x
Tactic:
simp only [push_cons_eq_cons_push, nodup_cons, mem_push, mem_cons, IH]
Proof state after:
case cons
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
IH : Nodup (push x a) ↔ Nodup x ∧ ¬a ∈ x
⊢ ¬(b ∈ x ∨ b = a) ∧ Nodup x ∧ ¬a ∈ x ↔ (¬b ∈ x ∧ Nodup x) ∧ ¬(a = b ∨ a ∈ x)