-- Mathlib/Order/Basic.lean
theorem LinearOrder.toPartialOrder_injective :
    Function.Injective (@LinearOrder.toPartialOrder α) :=
  fun A B h ↦ match A, B with
  | { le := A_le, lt := A_lt,
      decidableLE := A_decidableLE, decidableEq := A_decidableEq, decidableLT := A_decidableLT
      min := A_min, max := A_max, min_def := A_min_def, max_def := A_max_def,
      compare := A_compare, compare_eq_compareOfLessAndEq := A_compare_canonical, .. },
    { le := B_le, lt := B_lt,
      decidableLE := B_decidableLE, decidableEq := B_decidableEq, decidableLT := B_decidableLT
      min := B_min, max := B_max, min_def := B_min_def, max_def := B_max_def,
      compare := B_compare, compare_eq_compareOfLessAndEq := B_compare_canonical, .. } => by
    cases h
    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

Proof state:
case refl.refl
α : Type u_2
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x1 x2 => x1 ≤ x2
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x1 x2 => x1 < x2
A_min_def : ∀ (a b : α), a ⊓ b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), a ⊔ b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), a ⊔ b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), a ⊓ b = if a ≤ b then a else b
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical =
    mk le_total✝ A_decidableLE A_decidableEq A_decidableLT B_min_def B_max_def B_compare_canonical

Tactic:
have : A_max = B_max := by
  funext a b
  exact (A_max_def _ _).trans (B_max_def _ _).symm

Result:
case refl.refl
α : Type u_2
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x1 x2 => x1 ≤ x2
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x1 x2 => x1 < x2
A_min_def : ∀ (a b : α), a ⊓ b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), a ⊔ b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), a ⊔ b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), a ⊓ b = if a ≤ b then a else b
this : A_max = B_max
⊢ mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical =
    mk le_total✝ A_decidableLE A_decidableEq A_decidableLT B_min_def B_max_def B_compare_canonical

Proof state:
α : Type u_2
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x1 x2 => x1 ≤ x2
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x1 x2 => x1 < x2
A_min_def : ∀ (a b : α), a ⊓ b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), a ⊔ b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), a ⊔ b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), a ⊓ b = if a ≤ b then a else b
⊢ A_max = B_max

Tactic:
funext a b

Result:
case h.h
α : Type u_2
A B : LinearOrder α
A_le A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), a ≤ a
le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a
A_decidableLE : DecidableRel fun x1 x2 => x1 ≤ x2
A_decidableEq : DecidableEq α
A_decidableLT : DecidableRel fun x1 x2 => x1 < x2
A_min_def : ∀ (a b : α), a ⊓ b = if a ≤ b then a else b
A_max_def : ∀ (a b : α), a ⊔ b = if a ≤ b then b else a
A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl✝ : ∀ (a : α), a ≤ a
le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a
B_max_def : ∀ (a b : α), a ⊔ b = if a ≤ b then b else a
B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), a ⊓ b = if a ≤ b then a else b
a b : α
⊢ A_max a b = B_max a b