-- 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))
jb : β ia
h :
  Eq (α := γ ia ib)
    (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 ib) :
      γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
        ((mk (β := fun (a : α) ↦ β a) ia ib).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 ib)
⊢ 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)
have h₁ : ∀ (hb : ib ≠ jb),
  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)
Tactic: obtain rfl | hb := eq_or_ne ib jb