CastIndex.lean

opaque f : Nat → Nat
opaque g : Nat → Nat → Nat

inductive T : Nat → Type
  | mk₁ x : T (f x)
  | mk₂ x y : T (g x y)

theorem hcongrArg₂ {α : Sort u} {β : α → Sort v} {γ : ∀ a, β a → Sort w} (f : ∀ a b, γ a b) {a₁ a₂ : α} (ha : a₁ = a₂) {b₁ : β a₁} {b₂ : β a₂} (hb : HEq b₁ b₂) : HEq (f a₁ b₁) (f a₂ b₂) :=
  by cases ha; cases hb; rfl

theorem rec_cast (h : a = b) : @T.rec motive mk₁ mk₂ b (h ▸ t) = cast (h.rec (motive := fun b _ => _ = motive b _) rfl) (@T.rec motive mk₁ mk₂ a t) :=
  eq_of_heq (.trans (hcongrArg₂ _ h.symm (h.rec (.refl _))) (have := h.rec (motive := fun b _ => _ = motive b _) rfl; (this.rec (.refl _) : HEq _ (cast this _))))

example (h : f x = f x') : h ▸ T.mk₁ x = T.mk₁ x' → x = x'
  | h' => cast (rec_cast h) (T.noConfusion h') (·)

example (h : g x y = g x' y') : h ▸ T.mk₂ x y = T.mk₂ x' y' → x = x' ∧ y = y'
  | h' => cast (rec_cast h) (T.noConfusion h') .intro

example (h : f x = g x' y') : h ▸ T.mk₁ x ≠ T.mk₂ x' y'
  | h' => cast (rec_cast h) (T.noConfusion h')