-- Mathlib/.lake/packages/lean4/src/lean/Lean/Data/RArray.lean
theorem RArray.size_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) :
    (ofFn f h).size = n :=
  go 0 n h (Nat.le_refl _)
where
  go lb ub h1 h2 : (ofFn.go f lb ub h1 h2).size = ub - lb

Proof state:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
ih1 : Nat := (lb✝ + ub✝) / 2
ih2 : (ofFn.go f lb✝ ih1 ⋯ ⋯).size = ih1 - lb✝
hiu : (ofFn.go f ih1 ub✝ ⋯ h2✝).size = ub✝ - ih1
⊢ (if h : lb✝ + 1 = ub✝ then leaf (f ⟨lb✝, ⋯⟩)
      else
        let mid := (lb✝ + ub✝) / 2;
        branch mid (ofFn.go f lb✝ mid ⋯ ⋯) (ofFn.go f mid ub✝ ⋯ h2✝)).size =
    ub✝ - lb✝

Tactic:
simp +zetaDelta [size, *]

Result:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
ih1 : Nat := (lb✝ + ub✝) / 2
ih2 : (ofFn.go f lb✝ ih1 ⋯ ⋯).size = ih1 - lb✝
hiu : (ofFn.go f ih1 ub✝ ⋯ h2✝).size = ub✝ - ih1
⊢ (lb✝ + ub✝) / 2 - lb✝ + (ub✝ - (lb✝ + ub✝) / 2) = ub✝ - lb✝

Proof state:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
ih1 : Nat := (lb✝ + ub✝) / 2
ih2 : (ofFn.go f lb✝ ih1 ⋯ ⋯).size = ih1 - lb✝
hiu : (ofFn.go f ih1 ub✝ ⋯ h2✝).size = ub✝ - ih1
⊢ (lb✝ + ub✝) / 2 - lb✝ + (ub✝ - (lb✝ + ub✝) / 2) = ub✝ - lb✝

Tactic:
omega

Result:
no goals

Proof state:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ : Nat
h1✝ : lb✝ < lb✝ + 1
h2✝ : lb✝ + 1 ≤ n
⊢ (ofFn.go f lb✝ (lb✝ + 1) h1✝ h2✝).size = lb✝ + 1 - lb✝

Tactic:
simp [ofFn.go, size]

Result:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ : Nat
h1✝ : lb✝ < lb✝ + 1
h2✝ : lb✝ + 1 ≤ n
⊢ 1 = lb✝ + 1 - lb✝

Proof state:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
ih1 : Nat := (lb✝ + ub✝) / 2
ih2 : (ofFn.go f lb✝ ih1 ⋯ ⋯).size = ih1 - lb✝
hiu : (ofFn.go f ih1 ub✝ ⋯ h2✝).size = ub✝ - ih1
⊢ (ofFn.go f lb✝ ub✝ h1✝ h2✝).size = ub✝ - lb✝

Tactic:
rw [ofFn.go]

Result:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
ih1 : Nat := (lb✝ + ub✝) / 2
ih2 : (ofFn.go f lb✝ ih1 ⋯ ⋯).size = ih1 - lb✝
hiu : (ofFn.go f ih1 ub✝ ⋯ h2✝).size = ub✝ - ih1
⊢ (if h : lb✝ + 1 = ub✝ then leaf (f ⟨lb✝, ⋯⟩)
      else
        let mid := (lb✝ + ub✝) / 2;
        branch mid (ofFn.go f lb✝ mid ⋯ ⋯) (ofFn.go f mid ub✝ ⋯ h2✝)).size =
    ub✝ - lb✝

Proof state:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ : Nat
h1✝ : lb✝ < lb✝ + 1
h2✝ : lb✝ + 1 ≤ n
⊢ 1 = lb✝ + 1 - lb✝

Tactic:
omega

Result:
no goals

Proof state:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub : Nat
h1 : lb < ub
h2 : ub ≤ n
⊢ (ofFn.go f lb ub h1 h2).size = ub - lb

Tactic:
induction lb, ub, h1, h2 using RArray.ofFn.go.induct (n := n)

Result:
case case1
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ : Nat
h1✝ : lb✝ < lb✝ + 1
h2✝ : lb✝ + 1 ≤ n
⊢ (ofFn.go f lb✝ (lb✝ + 1) h1✝ h2✝).size = lb✝ + 1 - lb✝

case case2
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
ih2✝ : (ofFn.go f lb✝ mid✝ ⋯ ⋯).size = mid✝ - lb✝
ih1✝ : (ofFn.go f mid✝ ub✝ ⋯ h2✝).size = ub✝ - mid✝
⊢ (ofFn.go f lb✝ ub✝ h1✝ h2✝).size = ub✝ - lb✝

Proof state:
case case2
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
ih2✝ : (ofFn.go f lb✝ mid✝ ⋯ ⋯).size = mid✝ - lb✝
ih1✝ : (ofFn.go f mid✝ ub✝ ⋯ h2✝).size = ub✝ - mid✝
⊢ (ofFn.go f lb✝ ub✝ h1✝ h2✝).size = ub✝ - lb✝

Tactic:
case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega

Result:
no goals

Proof state:
case case1
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ : Nat
h1✝ : lb✝ < lb✝ + 1
h2✝ : lb✝ + 1 ≤ n
⊢ (ofFn.go f lb✝ (lb✝ + 1) h1✝ h2✝).size = lb✝ + 1 - lb✝

case case2
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
ih2✝ : (ofFn.go f lb✝ mid✝ ⋯ ⋯).size = mid✝ - lb✝
ih1✝ : (ofFn.go f mid✝ ub✝ ⋯ h2✝).size = ub✝ - mid✝
⊢ (ofFn.go f lb✝ ub✝ h1✝ h2✝).size = ub✝ - lb✝

Tactic:
case case1 => simp [ofFn.go, size]; omega

Result:
case case2
α : Type
n : Nat
f : Fin n → α
h : 0 < n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
ih2✝ : (ofFn.go f lb✝ mid✝ ⋯ ⋯).size = mid✝ - lb✝
ih1✝ : (ofFn.go f mid✝ ub✝ ⋯ h2✝).size = ub✝ - mid✝
⊢ (ofFn.go f lb✝ ub✝ h1✝ h2✝).size = ub✝ - lb✝