-- 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:
k k' : BuildKey
⊢ (match k with
      | moduleFacet m f =>
        match k' with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match k' 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 k' 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 k' with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    k = k'

Tactic:
cases k with
| moduleFacet m f =>
  cases k'
  case moduleFacet m' f' =>
    dsimp only; split
    next m_eq => intro f_eq; rw [eq_of_cmp m_eq, eq_of_cmp f_eq]
    next => intro; contradiction
  all_goals (intro; contradiction)
| packageFacet p f =>
  cases k'
  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
  all_goals (intro; contradiction)
| targetFacet p t f =>
  cases k'
  case targetFacet p' t' f' =>
    dsimp only; split
    next p_eq =>
      split
      next t_eq =>
        intro f_eq
        rw [eq_of_cmp p_eq, eq_of_cmp t_eq, eq_of_cmp f_eq]
      next => intro; contradiction
    next => intro; contradiction
  all_goals (intro; contradiction)
| customTarget p t =>
  cases k'
  case customTarget p' t' =>
    dsimp only; split
    next p_eq => intro t_eq; rw [eq_of_cmp p_eq, eq_of_cmp t_eq]
    next => intro; contradiction
  all_goals (intro; contradiction)

Result:
no goals

Proof state:
p f p' f' : Name
x✝ : Ordering
p_eq : p.quickCmp p' = Ordering.eq
⊢ f.quickCmp f' = Ordering.eq → packageFacet p f = packageFacet p' f'

Tactic:
intro f_eq

Result:
p f p' f' : Name
x✝ : Ordering
p_eq : p.quickCmp p' = Ordering.eq
f_eq : f.quickCmp f' = Ordering.eq
⊢ packageFacet p f = packageFacet p' f'

Proof state:
p t f p' t' f' : Name
x✝¹ : Ordering
p_eq : p.quickCmp p' = Ordering.eq
x✝ : Ordering
t_eq : t.quickCmp t' = Ordering.eq
f_eq : f.quickCmp f' = Ordering.eq
⊢ targetFacet p t f = targetFacet p' t' f'

Tactic:
rw [eq_of_cmp p_eq, eq_of_cmp t_eq, eq_of_cmp f_eq]

Result:
no goals

Proof state:
p t f p' t' f' : Name
x✝² : Ordering
p_eq : p.quickCmp p' = Ordering.eq
x✝¹ : Ordering
x✝ : t.quickCmp t' = Ordering.eq → False
⊢ t.quickCmp t' = Ordering.eq → targetFacet p t f = targetFacet p' t' f'

Tactic:
intro

Result:
p t f p' t' f' : Name
x✝² : Ordering
p_eq : p.quickCmp p' = Ordering.eq
x✝¹ : Ordering
x✝ : t.quickCmp t' = Ordering.eq → False
a✝ : t.quickCmp t' = Ordering.eq
⊢ targetFacet p t f = targetFacet p' t' f'

Proof state:
m f m' f' : Name
x✝¹ : Ordering
x✝ : m.quickCmp m' = Ordering.eq → False
⊢ m.quickCmp m' = Ordering.eq → moduleFacet m f = moduleFacet m' f'

Tactic:
intro

Result:
m f m' f' : Name
x✝¹ : Ordering
x✝ : m.quickCmp m' = Ordering.eq → False
a✝ : m.quickCmp m' = Ordering.eq
⊢ moduleFacet m f = moduleFacet m' f'

Proof state:
p t f p' t' f' : Name
⊢ (match p.quickCmp p' with
      | Ordering.eq =>
        match t.quickCmp t' with
        | Ordering.eq => f.quickCmp f'
        | ord => ord
      | ord => ord) =
      Ordering.eq →
    targetFacet p t f = targetFacet p' t' f'

Tactic:
split

Result:
case h_1
p t f p' t' f' : Name
x✝ : Ordering
heq✝ : p.quickCmp p' = Ordering.eq
⊢ (match t.quickCmp t' with
      | Ordering.eq => f.quickCmp f'
      | ord => ord) =
      Ordering.eq →
    targetFacet p t f = targetFacet p' t' f'

case h_2
p t f p' t' f' : Name
x✝¹ : Ordering
x✝ : p.quickCmp p' = Ordering.eq → False
⊢ p.quickCmp p' = Ordering.eq → targetFacet p t f = targetFacet p' t' f'

Proof state:
case h_2
p t p' t' : Name
x✝¹ : Ordering
x✝ : p.quickCmp p' = Ordering.eq → False
⊢ p.quickCmp p' = Ordering.eq → customTarget p t = customTarget p' t'

Tactic:
next => intro; contradiction

Result:
no goals

Proof state:
case packageFacet.customTarget
p f package✝ target✝ : Name
a✝ :
  (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:
contradiction

Result:
no goals

Proof state:
case h_2
p t f p' t' f' : Name
x✝¹ : Ordering
x✝ : p.quickCmp p' = Ordering.eq → False
⊢ p.quickCmp p' = Ordering.eq → targetFacet p t f = targetFacet p' t' f'

Tactic:
next => intro; contradiction

Result:
no goals

Proof state:
m f m' f' : Name
⊢ (match moduleFacet m f with
      | moduleFacet m f =>
        match moduleFacet m' f' with
        | moduleFacet m' f' =>
          match m.quickCmp m' with
          | Ordering.eq => f.quickCmp f'
          | ord => ord
        | x => Ordering.lt
      | packageFacet p f =>
        match moduleFacet m' f' 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 m' f' 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 m' f' with
        | customTarget p' t' =>
          match p.quickCmp p' with
          | Ordering.eq => t.quickCmp t'
          | ord => ord
        | x => Ordering.gt) =
      Ordering.eq →
    moduleFacet m f = moduleFacet m' f'

Tactic:
dsimp only

Result:
m f m' f' : Name
⊢ (match m.quickCmp m' with
      | Ordering.eq => f.quickCmp f'
      | ord => ord) =
      Ordering.eq →
    moduleFacet m f = moduleFacet m' f'