Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), A_le a a
le_trans✝¹ : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge✝¹ : ∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a
le_antisymm✝¹ : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_le B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), B_le a a
le_trans✝ : ∀ (a b c : α), B_le a b → B_le b c → B_le a c
lt_iff_le_not_ge✝ : ∀ (a b : α), B_lt a b ↔ B_le a b ∧ ¬B_le b a
le_antisymm✝ : ∀ (a b : α), B_le a b → B_le b a → a = b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_total✝ : ∀ (a b : α), B_le a b ∨ B_le b a
B_decidableLE : DecidableLE α
B_decidableEq : DecidableEq α
B_decidableLT : DecidableLT α
B_min_def : ∀ (a b : α), B_min a b = if B_le a b then a else b
B_max_def : ∀ (a b : α), B_max a b = if B_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
⊢ { le := A_le, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := lt_iff_le_not_ge✝¹,
          le_antisymm := le_antisymm✝¹, min := A_min, max := A_max, compare := A_compare, le_total := le_total✝¹,
          toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
          min_def := A_min_def, max_def := A_max_def,
          compare_eq_compareOfLessAndEq := A_compare_canonical }.toPartialOrder =
      { le := B_le, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := lt_iff_le_not_ge✝,
          le_antisymm := le_antisymm✝, min := B_min, max := B_max, compare := B_compare, le_total := le_total✝,
          toDecidableLE := B_decidableLE, toDecidableEq := B_decidableEq, toDecidableLT := B_decidableLT,
          min_def := B_min_def, max_def := B_max_def,
          compare_eq_compareOfLessAndEq := B_compare_canonical }.toPartialOrder →
    { le := A_le, lt := A_lt, le_refl := le_refl✝¹, le_trans := le_trans✝¹, lt_iff_le_not_ge := lt_iff_le_not_ge✝¹,
        le_antisymm := le_antisymm✝¹, min := A_min, max := A_max, compare := A_compare, le_total := le_total✝¹,
        toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
        min_def := A_min_def, max_def := A_max_def, compare_eq_compareOfLessAndEq := A_compare_canonical } =
      { le := B_le, lt := B_lt, le_refl := le_refl✝, le_trans := le_trans✝, lt_iff_le_not_ge := lt_iff_le_not_ge✝,
        le_antisymm := le_antisymm✝, min := B_min, max := B_max, compare := B_compare, le_total := le_total✝,
        toDecidableLE := B_decidableLE, toDecidableEq := B_decidableEq, toDecidableLT := B_decidableLT,
        min_def := B_min_def, max_def := B_max_def, compare_eq_compareOfLessAndEq := B_compare_canonical }

Tactic:
by
    rintro ⟨⟩
    obtain rfl : A_decidableLE = B_decidableLE := Subsingleton.elim _ _
    obtain rfl : A_decidableEq = B_decidableEq := Subsingleton.elim _ _
    obtain rfl : A_decidableLT = B_decidableLT := Subsingleton.elim _ _
    have : A_min = B_min := by
      funext a b
      exact (A_min_def _ _).trans (B_min_def _ _).symm
    cases this
    have : A_max = B_max := by
      funext a b
      exact (A_max_def _ _).trans (B_max_def _ _).symm
    cases this
    have : A_compare = B_compare := by
      funext a b
      exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm
    congr

Goal state after: