-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
ia : α
ib : β ia
x :
  γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))
ja : α
jb : β ja
h :
  ∀ (jb : β ia),
    Eq (α := γ ia jb)
      (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
          (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ia jb) :
        γ ((mk (β := fun (a : α) ↦ β a) ia jb).fst (β := fun (a : α) ↦ β a))
          ((mk (β := fun (a : α) ↦ β a) ia jb).snd (β := fun (a : α) ↦ β a)))
      (update (β := fun (a : α) ↦ (y : β a) → γ a y)
        (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
        ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
        (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
          (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
            f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
          ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
        ia jb)
⊢ Eq (α := γ ja jb)
    (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ja jb) :
      γ ((mk (β := fun (a : α) ↦ β a) ja jb).fst (β := fun (a : α) ↦ β a))
        ((mk (β := fun (a : α) ↦ β a) ja jb).snd (β := fun (a : α) ↦ β a)))
    (update (β := fun (a : α) ↦ (y : β a) → γ a y)
      (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
          f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
      ja jb)
have h₁ : ∀ (ha : ia ≠ ja),
  Eq (α := γ ja jb)
    (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ja jb) :
      γ ((mk (β := fun (a : α) ↦ β a) ja jb).fst (β := fun (a : α) ↦ β a))
        ((mk (β := fun (a : α) ↦ β a) ja jb).snd (β := fun (a : α) ↦ β a)))
    (update (β := fun (a : α) ↦ (y : β a) → γ a y)
      (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
          f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
      ja jb)
Tactic: obtain rfl | ha := eq_or_ne ia ja