Motive error with two goals printed identically

Stream: lean4

[Chris Henson]

Sorry this mwe is a little long, but not sure how to simplify it any more. At the end of the last proof, I end up in a situation where an attempt to rewrite with the induction hypothesis gives a motive error. After a different rewrite/simp, the goal appears the same (maybe the printing is misleading?), but I no longer get the motive error. Could someone help me understand why and how I would approach debugging in general?

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Closed.Cartesian

open CategoryTheory

inductive Ty (K : Type)
  | Unit : Ty K
  | Basic : K → Ty K
  | Arr : Ty K → Ty K → Ty K
  | Prod : Ty K → Ty K → Ty K
  deriving Repr, DecidableEq

abbrev Context (K : Type) : Type := List (Ty K)

@[simp]
noncomputable def Ty.to_ccc
  {K X: Type}
  [Category X]
  [Limits.HasFiniteProducts X]
  [CartesianClosed X]
  (f : K → X)
  (ty : Ty K)
  : X
  :=
  match ty with
  | Basic k => f k
  | Ty.Prod l r => l.to_ccc f ⨯ r.to_ccc f
  | Ty.Arr l r => l.to_ccc f ⟹  r.to_ccc f
  | Ty.Unit => ⊤_ X

@[simp]
noncomputable def Context.to_ccc
  {K X: Type}
  [Category X]
  [Limits.HasFiniteProducts X]
  [CartesianClosed X]
  (f : K → X)
  (Γ : Context K)
  : X
  :=
  match Γ with
  | [] => ⊤_ X
  | hd :: tl => hd.to_ccc f ⨯ Context.to_ccc f tl

@[simp]
def Context.to_ty {K: Type} (Γ : Context K) : Ty K :=
  match Γ with
  | [] => Ty.Unit
  | hd :: tl => Ty.Prod hd (Context.to_ty tl)

theorem Cat_ccc_to_ty
  {K X: Type}
  [Category X]
  [Limits.HasFiniteProducts X]
  [CartesianClosed X]
  (f : K → X)
  (Γ : Context K)
  : Ty.to_ccc f Γ.to_ty = Context.to_ccc f Γ
  := by
  induction Γ
  case nil => simp
  case cons σ Γ ih =>
    simp
    -- goal is (Ty.to_ccc f σ ⨯ Ty.to_ccc f (Context.to_ty Γ)) = (Ty.to_ccc f σ ⨯ Context.to_ccc f Γ)
    -- if I try `rw [ih]` here, I'll get an error:
    --  "tactic 'rewrite' failed, motive is not type correct"

    -- I guessed at this... not sure how/why it works
    rw [← Limits.prod.functor_obj_obj]
    simp

    -- the goal is the same as above, but this now concludes the proof
    rw [ih]

[Kyle Miller]

It's worth familiarizing yourself with pretty printer options, or be lucky hovering over everything until you spot the difference. If you use set_option pp.all true you can see what changed at least here.

[Kyle Miller]

A tricky thing here is that the ⨯ notation is hiding a proof (docs#CategoryTheory.Limits.prod) that depends on the two explicit arguments, so it's very likely that rewriting one of the two arguments with rw would lead to a type-incorrect term. That's the general sort of meaning of a "motive is not type correct" error.

[Kyle Miller]

In this situation, simp is better at doing such a rewrite, and in fact it closes the goal if you give it ih:

theorem Cat_ccc_to_ty
  {K X: Type}
  [Category X]
  [Limits.HasFiniteProducts X]
  [CartesianClosed X]
  (f : K → X)
  (Γ : Context K)
  : Ty.to_ccc f Γ.to_ty = Context.to_ccc f Γ
  := by
  induction Γ
  case nil => simp
  case cons σ Γ ih =>
    simp [ih]

[Chris Henson]

Okay, I think I roughly understand. Thanks!

[Kyle Miller]

Another tactic to be aware of is congr! (in mathlib), which reduces a goal to showing corresponding parts are equal, while automatically equating things that don't need equating (like proof terms or Decidable/Fintype instances). Core Lean has congr, but congr! has extra features.

If you use it here, it actually closes the goal because it's able to use assumption. If you uncomment the clear line you can see what it reduced the goal to.

theorem Cat_ccc_to_ty
  {K X: Type}
  [Category X]
  [Limits.HasFiniteProducts X]
  [CartesianClosed X]
  (f : K → X)
  (Γ : Context K)
  : Ty.to_ccc f Γ.to_ty = Context.to_ccc f Γ
  := by
  induction Γ
  case nil => simp
  case cons σ Γ ih =>
    simp
    -- clear ih
    congr!