awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Basic
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_min 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_min_def : ∀ (a b : α), B_min a b = if A_le a b then a else b
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
a b : α
⊢ A_min a b = B_min a b

Tactic:
(A_min_def _ _).trans (B_min_def _ _).symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Order.Basic
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_min 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_min_def : ∀ (a b : α), B_min a b = if A_le a b then a else b
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
a b : α
⊢ A_min a b = B_min a b

Tactic:
exact (A_min_def _ _).trans (B_min_def _ _).symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Order.Basic
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_min 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_min_def : ∀ (a b : α), B_min a b = if A_le a b then a else b
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
⊢ A_min = B_min

Tactic:
have : A_min = B_min := by
      funext a b
      exact (A_min_def _ _).trans (B_min_def _ _).symm
-- Module: Mathlib.Order.Basic
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_min 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_min_def : ∀ (a b : α), B_min a b = if A_le a b then a else b
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
this : A_min = B_min
refl :
  ∀ (B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else 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 :
        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 }
⊢ { 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 := B_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 }

Tactic:
cases this
-- Module: Mathlib.Order.Basic
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
h : ∀ (a b : α), A_max a b = B_max a b
⊢ A_max = B_max

Tactic:
funext a b
-- Module: Mathlib.Order.Basic
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
a b : α
⊢ A_max a b = B_max a b

Tactic:
(A_max_def _ _).trans (B_max_def _ _).symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Order.Basic
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
a b : α
⊢ A_max a b = B_max a b

Tactic:
exact (A_max_def _ _).trans (B_max_def _ _).symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Order.Basic
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
⊢ A_max = B_max

Tactic:
have : A_max = B_max := by
      funext a b
      exact (A_max_def _ _).trans (B_max_def _ _).symm
-- Module: Mathlib.Order.Basic
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
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 }
⊢ { 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 }

Tactic:
cases this
-- Module: Mathlib.Order.Basic
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_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_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
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
h : ∀ (a b : α), A_compare a b = B_compare a b
⊢ A_compare = B_compare

Tactic:
funext a b
-- Module: Mathlib.Order.Basic
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_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_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
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
a b : α
⊢ A_compare a b = B_compare a b

Tactic:
(A_compare_canonical _ _).trans (B_compare_canonical _ _).symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Order.Basic
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_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_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
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
a b : α
⊢ A_compare a b = B_compare a b

Tactic:
exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Order.Basic
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_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_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
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
⊢ A_compare = B_compare

Tactic:
have : A_compare = B_compare := by
      funext a b
      exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm
-- Module: Mathlib.Order.Basic
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_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_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
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
this : A_compare = B_compare
⊢ { 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:
congr
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
A B : Preorder α
H a : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
ext x y
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
H x y
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
A B : Preorder α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y : α
⊢ x ≤ y ↔ x ≤ y

Tactic:
exact H x y
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
A B : PartialOrder α
H a : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
ext x y