-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : 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 : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
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_max : α → α → α
B_compare : α → α → Ordering
le_refl_1 : ∀ (a : α), A_le a a
le_trans_1 : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm_1 : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total_1 : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge_1 : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
this : A_max = B_max
⊢ { 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 :
      LinearOrder α } =
    { le := A_le, lt := A_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := lt_iff_le_not_ge_1,
      le_antisymm := le_antisymm_1, min := A_min, max := B_max, compare := B_compare, le_total := le_total_1,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
      min_def := B_min_def, max_def := B_max_def, compare_eq_compareOfLessAndEq := B_compare_canonical }
have refl : ∀ (B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a),
  { 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 :
      LinearOrder α } =
    { le := A_le, lt := A_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := lt_iff_le_not_ge_1,
      le_antisymm := le_antisymm_1, min := A_min, max := A_max, compare := B_compare, le_total := le_total_1,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
      min_def := B_min_def, max_def := B_max_def, compare_eq_compareOfLessAndEq := B_compare_canonical }
Tactic: cases this
Cleared hypotheses: B_max, B_max_def, this