α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this : Function.RightInverse ↑equivSigmaTuple.symm ↑equivSigmaTuple
⊢ ofFnRec h (ofFn f) = h n f
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
⊢ ofFnRec h (ofFn f) = h n f
have := (@equivSigmaTuple α).rightInverse_symm
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
⊢ ofFnRec h (ofFn f) = h n f
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this : Function.RightInverse ↑equivSigmaTuple.symm ↑equivSigmaTuple
⊢ ofFnRec h (ofFn f) = h n f
dsimp [equivSigmaTuple] at this
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this✝ : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
this :
  cast
      (_ :
        C (ofFn { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.snd) =
          C (ofFn { fst := n, snd := f }.snd))
      (h { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.fst
        { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.snd) =
    h { fst := n, snd := f }.fst { fst := n, snd := f }.snd
⊢ ofFnRec h (ofFn f) = h n f
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
⊢ ofFnRec h (ofFn f) = h n f
have := this.cast_eq (fun s => h s.1 s.2) ⟨n, f⟩
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this✝ : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
this :
  cast (_ : C (ofFn { fst := length (ofFn f), snd := get (ofFn f) }.snd) = C (ofFn { fst := n, snd := f }.snd))
      (h (length (ofFn f)) (get (ofFn f))) =
    h n f
⊢ ofFnRec h (ofFn f) = h n f
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this✝ : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
this :
  cast
      (_ :
        C (ofFn { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.snd) =
          C (ofFn { fst := n, snd := f }.snd))
      (h { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.fst
        { fst := length (ofFn { fst := n, snd := f }.snd), snd := get (ofFn { fst := n, snd := f }.snd) }.snd) =
    h { fst := n, snd := f }.fst { fst := n, snd := f }.snd
⊢ ofFnRec h (ofFn f) = h n f
dsimp only at this
no goals
α : Type u
C : List α → Sort u_1
h : (n : ℕ) → (f : Fin n → α) → C (ofFn f)
n : ℕ
f : Fin n → α
this✝ : Function.RightInverse (fun f => ofFn f.snd) fun l => { fst := length l, snd := get l }
this :
  cast (_ : C (ofFn { fst := length (ofFn f), snd := get (ofFn f) }.snd) = C (ofFn { fst := n, snd := f }.snd))
      (h (length (ofFn f)) (get (ofFn f))) =
    h n f
⊢ ofFnRec h (ofFn f) = h n f
rw [ofFnRec, ← this]