case zero
α : Type u
m n : ℕ
f✝ : Fin (m * n) → α
f : Fin (zero * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < zero * n) })

case succ
α : Type u
m✝ n : ℕ
f✝ : Fin (m✝ * n) → α
m : ℕ
IH :
  ∀ (f : Fin (m * n) → α),
    ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
f : Fin (succ m * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
induction' m with m IH
no goals
case zero
α : Type u
m n : ℕ
f✝ : Fin (m * n) → α
f : Fin (zero * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < zero * n) })
simp [ofFn_zero, zero_mul, ofFn_zero, join]
case succ
α : Type u
m✝ n : ℕ
f✝ : Fin (m✝ * n) → α
m : ℕ
IH :
  ∀ (f : Fin (m * n) → α),
    ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
f : Fin (succ m * n) → α
⊢ (join
        (ofFn fun i =>
          ofFn fun j =>
            f
              (↑(Fin.cast (_ : m * n + n = succ m * n))
                (↑(Fin.castAdd n) { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) }))) ++
      ofFn fun j => f (↑(Fin.cast (_ : m * n + n = succ m * n)) (↑(Fin.natAdd (m * n)) j))) =
    join
        (ofFn fun i =>
          ofFn fun j =>
            f { val := ↑(↑Fin.castSucc i) * n + ↑j, isLt := (_ : ↑(↑Fin.castSucc i) * n + ↑j < succ m * n) }) ++
      ofFn fun j => f { val := ↑(Fin.last m) * n + ↑j, isLt := (_ : ↑(Fin.last m) * n + ↑j < succ m * n) }
case succ
α : Type u
m✝ n : ℕ
f✝ : Fin (m✝ * n) → α
m : ℕ
IH :
  ∀ (f : Fin (m * n) → α),
    ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
f : Fin (succ m * n) → α
⊢ ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < succ m * n) })
simp_rw [ofFn_succ', succ_mul, join_concat, ofFn_add, IH]
no goals
case succ
α : Type u
m✝ n : ℕ
f✝ : Fin (m✝ * n) → α
m : ℕ
IH :
  ∀ (f : Fin (m * n) → α),
    ofFn f = join (ofFn fun i => ofFn fun j => f { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) })
f : Fin (succ m * n) → α
⊢ (join
        (ofFn fun i =>
          ofFn fun j =>
            f
              (↑(Fin.cast (_ : m * n + n = succ m * n))
                (↑(Fin.castAdd n) { val := ↑i * n + ↑j, isLt := (_ : ↑i * n + ↑j < m * n) }))) ++
      ofFn fun j => f (↑(Fin.cast (_ : m * n + n = succ m * n)) (↑(Fin.natAdd (m * n)) j))) =
    join
        (ofFn fun i =>
          ofFn fun j =>
            f { val := ↑(↑Fin.castSucc i) * n + ↑j, isLt := (_ : ↑(↑Fin.castSucc i) * n + ↑j < succ m * n) }) ++
      ofFn fun j => f { val := ↑(Fin.last m) * n + ↑j, isLt := (_ : ↑(Fin.last m) * n + ↑j < succ m * n) }
rfl