-- Mathlib/.lake/packages/lean4/src/lean/Lean/Data/RArray.lean
theorem RArray.get_ofFn {n : Nat} (f : Fin n → α) (h : 0 < n) (i : Fin n) :
    (ofFn f h).get i = f i :=
  go 0 n h (Nat.le_refl _) (Nat.zero_le _) i.2
where
  go lb ub h1 h2 (h3 : lb ≤ i.val) (h3 : i.val < ub) : (ofFn.go f lb ub h1 h2).get i = f i

Proof state:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
hiu : lb✝ ≤ ↑i
h3 : ↑i < ub✝
ih1 : lb✝ ≤ ↑i → ↑i < mid✝ → (ofFn.go f lb✝ mid✝ ⋯ ⋯).getImpl ↑i = f i
ih2 : mid✝ ≤ ↑i → ↑i < ub✝ → (ofFn.go f mid✝ ub✝ ⋯ h2✝).getImpl ↑i = f i
⊢ (if ↑i < (lb✝ + ub✝) / 2 then (ofFn.go f lb✝ ((lb✝ + ub✝) / 2) ⋯ ⋯).getImpl ↑i
    else (ofFn.go f ((lb✝ + ub✝) / 2) ub✝ ⋯ h2✝).getImpl ↑i) =
    f i

Tactic:
split

Result:
case isTrue
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝¹ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
hiu : lb✝ ≤ ↑i
h3 : ↑i < ub✝
ih1 : lb✝ ≤ ↑i → ↑i < mid✝ → (ofFn.go f lb✝ mid✝ ⋯ ⋯).getImpl ↑i = f i
ih2 : mid✝ ≤ ↑i → ↑i < ub✝ → (ofFn.go f mid✝ ub✝ ⋯ h2✝).getImpl ↑i = f i
h✝ : ↑i < (lb✝ + ub✝) / 2
⊢ (ofFn.go f lb✝ ((lb✝ + ub✝) / 2) ⋯ ⋯).getImpl ↑i = f i

case isFalse
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝¹ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
hiu : lb✝ ≤ ↑i
h3 : ↑i < ub✝
ih1 : lb✝ ≤ ↑i → ↑i < mid✝ → (ofFn.go f lb✝ mid✝ ⋯ ⋯).getImpl ↑i = f i
ih2 : mid✝ ≤ ↑i → ↑i < ub✝ → (ofFn.go f mid✝ ub✝ ⋯ h2✝).getImpl ↑i = f i
h✝ : ¬↑i < (lb✝ + ub✝) / 2
⊢ (ofFn.go f ((lb✝ + ub✝) / 2) ub✝ ⋯ h2✝).getImpl ↑i = f i

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

Tactic:
rw [ofFn.go]

Result:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
ih1 : lb✝ ≤ ↑i → ↑i < mid✝ → (ofFn.go f lb✝ mid✝ ⋯ ⋯).get ↑i = f i
ih2 : mid✝ ≤ ↑i → ↑i < ub✝ → (ofFn.go f mid✝ ub✝ ⋯ h2✝).get ↑i = f i
hiu : lb✝ ≤ ↑i
h3 : ↑i < ub✝
⊢ (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✝)).get
      ↑i =
    f i

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

Tactic:
simp [ofFn.go, RArray.get_eq_getImpl, RArray.getImpl]

Result:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ : Nat
h1✝ : lb✝ < lb✝ + 1
h2✝ : lb✝ + 1 ≤ n
h3✝ : lb✝ ≤ ↑i
h3 : ↑i < lb✝ + 1
⊢ f ⟨lb✝, ⋯⟩ = f i

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

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

Tactic:
case case1 =>
  simp [ofFn.go, RArray.get_eq_getImpl, RArray.getImpl]
  congr
  omega

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

Proof state:
case isFalse
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝¹ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
hiu : lb✝ ≤ ↑i
h3 : ↑i < ub✝
ih1 : lb✝ ≤ ↑i → ↑i < mid✝ → (ofFn.go f lb✝ mid✝ ⋯ ⋯).getImpl ↑i = f i
ih2 : mid✝ ≤ ↑i → ↑i < ub✝ → (ofFn.go f mid✝ ub✝ ⋯ h2✝).getImpl ↑i = f i
h✝ : ¬↑i < (lb✝ + ub✝) / 2
⊢ (ofFn.go f ((lb✝ + ub✝) / 2) ub✝ ⋯ h2✝).getImpl ↑i = f i

Tactic:
rw [ih2] <;> omega

Result:
no goals

Proof state:
case isTrue
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝¹ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
hiu : lb✝ ≤ ↑i
h3 : ↑i < ub✝
ih1 : lb✝ ≤ ↑i → ↑i < mid✝ → (ofFn.go f lb✝ mid✝ ⋯ ⋯).getImpl ↑i = f i
ih2 : mid✝ ≤ ↑i → ↑i < ub✝ → (ofFn.go f mid✝ ub✝ ⋯ h2✝).getImpl ↑i = f i
h✝ : ↑i < (lb✝ + ub✝) / 2
⊢ (ofFn.go f lb✝ ((lb✝ + ub✝) / 2) ⋯ ⋯).getImpl ↑i = f i

Tactic:
rw [ih1] <;> omega

Result:
no goals

Proof state:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
ih1 : lb✝ ≤ ↑i → ↑i < mid✝ → (ofFn.go f lb✝ mid✝ ⋯ ⋯).get ↑i = f i
ih2 : mid✝ ≤ ↑i → ↑i < ub✝ → (ofFn.go f mid✝ ub✝ ⋯ h2✝).get ↑i = f i
hiu : lb✝ ≤ ↑i
h3 : ↑i < ub✝
⊢ (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✝)).get
      ↑i =
    f i

Tactic:
simp only [↓reduceDIte, *]

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

Proof state:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub : Nat
h1 : lb < ub
h2 : ub ≤ n
h3✝ : lb ≤ ↑i
h3 : ↑i < ub
⊢ (ofFn.go f lb ub h1 h2).get ↑i = f i

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
i : Fin n
lb ub lb✝ : Nat
h1✝ : lb✝ < lb✝ + 1
h2✝ : lb✝ + 1 ≤ n
h3✝ : lb✝ ≤ ↑i
h3 : ↑i < lb✝ + 1
⊢ (ofFn.go f lb✝ (lb✝ + 1) h1✝ h2✝).get ↑i = f i

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

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

Tactic:
simp [RArray.get_eq_getImpl, RArray.getImpl] at *

Result:
α : Type
n : Nat
f : Fin n → α
h : 0 < n
i : Fin n
lb ub lb✝ ub✝ : Nat
h1✝ : lb✝ < ub✝
h2✝ : ub✝ ≤ n
h✝ : ¬lb✝ + 1 = ub✝
mid✝ : Nat := (lb✝ + ub✝) / 2
hiu : lb✝ ≤ ↑i
h3 : ↑i < ub✝
ih1 : lb✝ ≤ ↑i → ↑i < mid✝ → (ofFn.go f lb✝ mid✝ ⋯ ⋯).getImpl ↑i = f i
ih2 : mid✝ ≤ ↑i → ↑i < ub✝ → (ofFn.go f mid✝ ub✝ ⋯ h2✝).getImpl ↑i = f i
⊢ (if ↑i < (lb✝ + ub✝) / 2 then (ofFn.go f lb✝ ((lb✝ + ub✝) / 2) ⋯ ⋯).getImpl ↑i
    else (ofFn.go f ((lb✝ + ub✝) / 2) ub✝ ⋯ h2✝).getImpl ↑i) =
    f i