-- Mathlib/.lake/packages/lean4/src/lean/lake/Lake/Build/Key.lean
theorem eq_of_quickCmp {k k' : BuildKey}  :
quickCmp k k' = Ordering.eq → k = k'

Proof state:
case packageFacet.moduleFacet
p f module✝ facet✝ : Name
⊢ (match packageFacet p f with
      | moduleFacet m f =>
        match moduleFacet module✝ facet✝ with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match moduleFacet module✝ facet✝ with
        | moduleFacet module facet => Ordering.gt
        | packageFacet p' f' =>
          match p.quickCmp p' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | targetFacet p t f =>
        match moduleFacet module✝ facet✝ with
        | customTarget package target => Ordering.lt
        | targetFacet p' t' f' =>
          match p.quickCmp p' with
          | Ordering.eq =>
            match t.quickCmp t' with
            | Ordering.eq => f.quickCmp f'
            | ord => ord
          | ord => ord
        | x => Ordering.gt
      | customTarget p t =>
        match moduleFacet module✝ facet✝ with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    packageFacet p f = moduleFacet module✝ facet✝

case packageFacet.packageFacet
p f package✝ facet✝ : Name
⊢ (match packageFacet p f with
      | moduleFacet m f =>
        match packageFacet package✝ facet✝ with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match packageFacet package✝ facet✝ with
        | moduleFacet module facet => Ordering.gt
        | packageFacet p' f' =>
          match p.quickCmp p' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | targetFacet p t f =>
        match packageFacet package✝ facet✝ with
        | customTarget package target => Ordering.lt
        | targetFacet p' t' f' =>
          match p.quickCmp p' with
          | Ordering.eq =>
            match t.quickCmp t' with
            | Ordering.eq => f.quickCmp f'
            | ord => ord
          | ord => ord
        | x => Ordering.gt
      | customTarget p t =>
        match packageFacet package✝ facet✝ with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    packageFacet p f = packageFacet package✝ facet✝

case packageFacet.targetFacet
p f package✝ target✝ facet✝ : Name
⊢ (match packageFacet p f with
      | moduleFacet m f =>
        match targetFacet package✝ target✝ facet✝ with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match targetFacet package✝ target✝ facet✝ with
        | moduleFacet module facet => Ordering.gt
        | packageFacet p' f' =>
          match p.quickCmp p' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | targetFacet p t f =>
        match targetFacet package✝ target✝ facet✝ with
        | customTarget package target => Ordering.lt
        | targetFacet p' t' f' =>
          match p.quickCmp p' with
          | Ordering.eq =>
            match t.quickCmp t' with
            | Ordering.eq => f.quickCmp f'
            | ord => ord
          | ord => ord
        | x => Ordering.gt
      | customTarget p t =>
        match targetFacet package✝ target✝ facet✝ with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    packageFacet p f = targetFacet package✝ target✝ facet✝

case packageFacet.customTarget
p f package✝ target✝ : Name
⊢ (match packageFacet p f with
      | moduleFacet m f =>
        match customTarget package✝ target✝ with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match customTarget package✝ target✝ with
        | moduleFacet module facet => Ordering.gt
        | packageFacet p' f' =>
          match p.quickCmp p' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | targetFacet p t f =>
        match customTarget package✝ target✝ with
        | customTarget package target => Ordering.lt
        | targetFacet p' t' f' =>
          match p.quickCmp p' with
          | Ordering.eq =>
            match t.quickCmp t' with
            | Ordering.eq => f.quickCmp f'
            | ord => ord
          | ord => ord
        | x => Ordering.gt
      | customTarget p t =>
        match customTarget package✝ target✝ with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    packageFacet p f = customTarget package✝ target✝

Tactic:
case packageFacet p' f' =>
  dsimp only; split
  next p_eq => intro f_eq; rw [eq_of_cmp p_eq, eq_of_cmp f_eq]
  next => intro; contradiction

Result:
case packageFacet.moduleFacet
p f module✝ facet✝ : Name
⊢ (match packageFacet p f with
      | moduleFacet m f =>
        match moduleFacet module✝ facet✝ with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match moduleFacet module✝ facet✝ with
        | moduleFacet module facet => Ordering.gt
        | packageFacet p' f' =>
          match p.quickCmp p' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | targetFacet p t f =>
        match moduleFacet module✝ facet✝ with
        | customTarget package target => Ordering.lt
        | targetFacet p' t' f' =>
          match p.quickCmp p' with
          | Ordering.eq =>
            match t.quickCmp t' with
            | Ordering.eq => f.quickCmp f'
            | ord => ord
          | ord => ord
        | x => Ordering.gt
      | customTarget p t =>
        match moduleFacet module✝ facet✝ with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    packageFacet p f = moduleFacet module✝ facet✝

case packageFacet.targetFacet
p f package✝ target✝ facet✝ : Name
⊢ (match packageFacet p f with
      | moduleFacet m f =>
        match targetFacet package✝ target✝ facet✝ with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match targetFacet package✝ target✝ facet✝ with
        | moduleFacet module facet => Ordering.gt
        | packageFacet p' f' =>
          match p.quickCmp p' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | targetFacet p t f =>
        match targetFacet package✝ target✝ facet✝ with
        | customTarget package target => Ordering.lt
        | targetFacet p' t' f' =>
          match p.quickCmp p' with
          | Ordering.eq =>
            match t.quickCmp t' with
            | Ordering.eq => f.quickCmp f'
            | ord => ord
          | ord => ord
        | x => Ordering.gt
      | customTarget p t =>
        match targetFacet package✝ target✝ facet✝ with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    packageFacet p f = targetFacet package✝ target✝ facet✝

case packageFacet.customTarget
p f package✝ target✝ : Name
⊢ (match packageFacet p f with
      | moduleFacet m f =>
        match customTarget package✝ target✝ with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match customTarget package✝ target✝ with
        | moduleFacet module facet => Ordering.gt
        | packageFacet p' f' =>
          match p.quickCmp p' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | targetFacet p t f =>
        match customTarget package✝ target✝ with
        | customTarget package target => Ordering.lt
        | targetFacet p' t' f' =>
          match p.quickCmp p' with
          | Ordering.eq =>
            match t.quickCmp t' with
            | Ordering.eq => f.quickCmp f'
            | ord => ord
          | ord => ord
        | x => Ordering.gt
      | customTarget p t =>
        match customTarget package✝ target✝ with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    packageFacet p f = customTarget package✝ target✝