awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a b : α
rw : ¬(a ≤ b ∧ ¬b ≤ a) ↔ ¬a ≤ b ∨ b ≤ a
rw₁ : ¬a ≤ b ∨ ¬¬b ≤ a ↔ ¬a ≤ b ∨ b ≤ a
rw₂ rw₃ : ¬a ≤ b ∨ b ≤ a ↔ ¬a ≤ b ∨ b ≤ a
⊢ ¬a < b ↔ ¬a ≤ b ∨ b ≤ a

Tactic:
rw [lt_iff_le_not_ge, Classical.not_and_iff_not_or_not, Classical.not_not]

Premises used: Classical.not_not, lt_iff_le_not_ge, Classical.not_and_iff_not_or_not
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a b : α
⊢ ¬a < b ↔ a ≤ b → b ≤ a

Tactic:
simp [not_lt_iff_not_le_or_ge, or_iff_not_imp_left]

Premises used: not_lt_iff_not_le_or_ge, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
x : α
⊢ x < x ↔ False

Tactic:
⟨lt_irrefl x, False.elim⟩

Premises used: lt_irrefl, False.elim, Iff.intro
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a : α
⊢ a < a → False

Tactic:
lt_irrefl a

Premises used: lt_irrefl, Not
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a b : α
hab : a = b
⊢ ¬a < b

Tactic:
fun h' ↦ h'.ne hab

Premises used: Not, LT.lt.ne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a b : α
h : ¬a ≤ b
⊢ a ≠ b

Tactic:
fun hab ↦ h (le_of_eq hab)

Premises used: le_of_eq, Not
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a b : α
inst_1 : Subsingleton α
⊢ a ≤ b

Tactic:
(Subsingleton.elim a b).le

Premises used: Eq.le, Subsingleton.elim
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a b : α
inst_1 : Subsingleton α
⊢ ¬a < b

Tactic:
(Subsingleton.elim a b).not_lt

Premises used: Eq.not_lt, Subsingleton.elim
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a b : α
H : ∀ (c : α), c ≤ a → c ≤ b
⊢ a ≤ b

Tactic:
H _ le_rfl

Premises used: le_rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a b : α
⊢ (∀ ⦃c : α⦄, c ≤ a → c ≤ b) ↔ a ≤ b

Tactic:
⟨le_of_forall_le, fun h _ hca ↦ le_trans hca h⟩

Premises used: le_of_forall_le, Iff.intro, le_trans
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a b c d : α
h₁ : c ≤ a
h₂ : b ≤ d
⊢ a ≤ b → c ≤ d

Tactic:
fun hab ↦ (h₁.trans hab).trans h₂

Premises used: LE.le.trans
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : Preorder α
a b c d : α
h₁ : c ≤ a
h₂ : b ≤ d
⊢ a < b → c < d

Tactic:
fun hab ↦ (h₁.trans_lt hab).trans_le h₂

Premises used: LT.lt.trans_le, LE.le.trans_lt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
⊢ a ≠ b → a ≤ b → a < b

Tactic:
flip lt_of_le_of_ne

Premises used: flip, lt_of_le_of_ne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ a < b ↔ a ≠ b

Tactic:
⟨ne_of_lt, h.lt_of_ne⟩

Premises used: LE.le.lt_of_ne, Iff.intro, ne_of_lt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ ¬a < b ↔ a = b

Tactic:
h.lt_iff_ne.not_left

Premises used: Iff.not_left, LE.le.lt_iff_ne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ b ≤ a ↔ a = b

Tactic:
⟨h.antisymm, Eq.ge⟩

Premises used: Eq.ge, LE.le.antisymm, Iff.intro
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
inst_1 : DecidableLE α
⊢ a ≤ b ↔ a = b ∨ a < b

Tactic:
Decidable.le_iff_lt_or_eq.trans or_comm

Premises used: Iff.trans, Decidable.le_iff_lt_or_eq, or_comm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
⊢ a ≤ b ↔ a = b ∨ a < b

Tactic:
le_iff_lt_or_eq.trans or_comm

Premises used: le_iff_lt_or_eq, Iff.trans, or_comm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
⊢ a < b ↔ a ≤ b ∧ a ≠ b

Tactic:
⟨fun h ↦ ⟨le_of_lt h, ne_of_lt h⟩, fun ⟨h1, h2⟩ ↦ h1.lt_of_ne h2⟩

Premises used: le_of_lt, _private.0.lt_iff_le_and_ne.match_1, LE.le.lt_of_ne, And.intro, LT.lt, Iff.intro, ne_of_lt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
inst_1 : DecidableLE α
⊢ a = b ↔ a ≤ b ∧ ¬a < b

Tactic:
⟨fun h ↦ ⟨h.le, h ▸ lt_irrefl _⟩, fun ⟨h₁, h₂⟩ ↦
    h₁.antisymm <| Decidable.byContradiction fun h₃ ↦ h₂ (h₁.lt_of_not_ge h₃)⟩

Premises used: LE.le.lt_of_not_ge, lt_irrefl, LE.le.antisymm, Eq.rec, Eq.le, And.intro, Iff.intro, Decidable.byContradiction, _private.0.Decidable.eq_iff_le_not_lt.match_1, Eq
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
⊢ a = b ↔ a ≤ b ∧ ¬a < b

Tactic:
open scoped Classical in
  Decidable.eq_iff_le_not_lt

Premises used: Decidable.eq_iff_le_not_lt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
inst_1 : DecidableLE α
h : a ≤ b
⊢ a = b ∨ a < b

Tactic:
(Decidable.lt_or_eq_of_le h).symm

Premises used: Decidable.lt_or_eq_of_le, Or.symm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ a = b ∨ a < b

Tactic:
(lt_or_eq_of_le h).symm

Premises used: lt_or_eq_of_le, Or.symm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬a < b
⊢ a = b

Tactic:
h₁.eq_or_lt.resolve_right h₂

Premises used: LE.le.eq_or_lt, Or.resolve_right
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
h : a ≠ b
⊢ a ≤ b ↔ a < b

Tactic:
⟨fun h' ↦ lt_of_le_of_ne h' h, fun h ↦ h.le⟩

Premises used: LT.lt.le, Iff.intro, lt_of_le_of_ne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
h : a ≠ b
⊢ ¬a ≤ b ∨ ¬b ≤ a

Tactic:
not_and_or.1 <| le_antisymm_iff.not.1 h

Premises used: Iff.not, le_antisymm_iff, not_and_or, Iff.mp
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
inst_1 : DecidableEq α
⊢ (a ≠ b ↔ a < b) ↔ a ≤ b

Tactic:
⟨fun h ↦ Decidable.byCases le_of_eq (le_of_lt ∘ h.mp), fun h ↦ ⟨lt_of_le_of_ne h, ne_of_lt⟩⟩

Premises used: le_of_lt, Function.comp, Iff.intro, Iff.mp, Decidable.byCases, le_of_eq, ne_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
⊢ (a ≠ b ↔ a < b) ↔ a ≤ b

Tactic:
open scoped Classical in
  Decidable.ne_iff_lt_iff_le

Premises used: Decidable.ne_iff_lt_iff_le
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
H : ∀ (c : α), c ≤ a ↔ c ≤ b
⊢ a = b

Tactic:
((H _).1 le_rfl).antisymm ((H _).2 le_rfl)

Premises used: Iff.mpr, le_rfl, LE.le.antisymm, Iff.mp
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
f : β → β → α
comm : ∀ (a b : β), f a b ≤ f b a
⊢ ∀ (a b : β), f a b = f b a

Tactic:
fun _ _ ↦ (comm _ _).antisymm <| comm _ _

Premises used: LE.le.antisymm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
rw : f (f c b) a ≤ f c (f b a)
⊢ f a (f b c) ≤ f (f a b) c

Tactic:
rw [comm.comm, comm.comm b, comm.comm _ c, comm.comm a]

Premises used: Std.Commutative.comm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)

Tactic:
assoc ..
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)

Tactic:
exact assoc ..
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
c : α
⊢ a < c ∨ c ≤ b

Tactic:
(lt_or_ge a c).imp id h.trans'

Premises used: id, lt_or_ge, Or.imp, LE.le.trans'
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
c : α
⊢ a ≤ c ∨ c < b

Tactic:
(le_or_gt a c).imp id h.trans_lt'

Premises used: id, le_or_gt, LE.le.trans_lt', Or.imp
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
c : α
⊢ a ≤ c ∨ c ≤ b

Tactic:
(h.gt_or_le c).imp le_of_lt id

Premises used: le_of_lt, id, LE.le.gt_or_le, Or.imp
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
h : a < b
c : α
⊢ a < c ∨ c < b

Tactic:
(le_or_gt b c).imp h.trans_le id

Premises used: id, le_or_gt, LT.lt.trans_le, Or.imp
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
h : a ≠ b
⊢ a < b ∨ b < a

Tactic:
lt_or_gt_of_ne h

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ a < b ∨ b < a ↔ a ≠ b

Tactic:
ne_iff_lt_or_gt.symm

Premises used: ne_iff_lt_or_gt, Iff.symm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ ¬a < b ↔ a = b ∨ b < a

Tactic:
not_lt.trans <| Decidable.le_iff_eq_or_lt.trans <| or_congr eq_comm Iff.rfl

Premises used: or_congr, Iff.rfl, eq_comm, not_lt, Iff.trans, Decidable.le_iff_eq_or_lt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ ∃ (c : α), a ≤ c ∧ b ≤ c

Tactic:
match le_total a b with
  | Or.inl h => ⟨_, h, le_rfl⟩
  | Or.inr h => ⟨_, le_rfl, h⟩

Premises used: le_rfl, _private.0.exists_ge_of_linear.match_1, Exists, le_total, LE.le, And, And.intro, Exists.intro
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
H : ∀ (c : α), c < a → c < b
⊢ a ≤ b

Tactic:
le_of_not_gt fun h ↦ lt_irrefl _ (H _ h)

Premises used: lt_irrefl, le_of_not_gt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ (∀ ⦃c : α⦄, c < a → c < b) ↔ a ≤ b

Tactic:
⟨le_of_forall_lt, fun h _ hca ↦ lt_of_lt_of_le hca h⟩

Premises used: le_of_forall_lt, Iff.intro, lt_of_lt_of_le
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
H : ∀ (c : α), c < a → c ≠ b
⊢ a ≤ b

Tactic:
le_of_not_gt fun hb ↦ H b hb rfl

Premises used: le_of_not_gt, rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
H : ∀ (c : α), c ≤ a → c ≠ b
⊢ a < b

Tactic:
lt_of_not_ge fun hb ↦ H b hb rfl

Premises used: lt_of_not_ge, rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ (∀ (c : α), c < a → c ≠ b) ↔ a ≤ b

Tactic:
⟨le_of_forall_lt_imp_ne, fun ha _ hc ↦ (hc.trans_le ha).ne⟩

Premises used: le_of_forall_lt_imp_ne, LT.lt.trans_le, Iff.intro, LT.lt.ne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ (∀ (c : α), c ≤ a → c ≠ b) ↔ a < b

Tactic:
⟨lt_of_forall_le_imp_ne, fun ha _ hc ↦ (hc.trans_lt ha).ne⟩

Premises used: lt_of_forall_le_imp_ne, Iff.intro, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
h : ∀ (c : α), c < a ↔ c < b
⊢ a = b

Tactic:
(le_of_forall_lt fun _ ↦ (h _).1).antisymm <| le_of_forall_lt fun _ ↦ (h _).2

Premises used: Iff.mpr, LE.le.antisymm, le_of_forall_lt, Iff.mp
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
x y x' y' : α
ltc : x < y ↔ x' < y'
gtc : y < x ↔ y' < x'
⊢ x = y ↔ x' = y'

Tactic:
grind
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
inl : ∀ (hab : a ≤ b), p (min a b)
inr : ∀ (hba : b ≤ a), p (min a b)
⊢ p (min a b)

Tactic:
obtain hab | hba := le_total a b

Premises used: le_total
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
hab : a ≤ b
⊢ p (min a b)

Tactic:
simp [min_eq_left, min_eq_right, *]

Premises used: min_eq_right, min_eq_left
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
hba : b ≤ a
⊢ p (min a b)

Tactic:
simp [min_eq_left, min_eq_right, *]

Premises used: min_eq_right, min_eq_left
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
p : α → Prop
ha : p a
hb : p b
⊢ p (min a b)

Tactic:
min_rec (fun _ ↦ ha) fun _ ↦ hb

Premises used: min_rec
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
rw : (if ¬b ≤ a then a else b) = if a < b then a else b
⊢ min a b = if a < b then a else b

Tactic:
rw [min_comm, min_def, ← ite_not]

Premises used: min_comm, min_def, ite_not
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then a else b) = if a < b then a else b

Tactic:
simp only [not_le]

Premises used: not_le
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
rw : (if ¬b ≤ a then b else a) = if a < b then b else a
⊢ max a b = if a < b then b else a

Tactic:
rw [max_comm, max_def, ← ite_not]

Premises used: ite_not, max_def, max_comm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then b else a) = if a < b then b else a

Tactic:
simp only [not_le]

Premises used: not_le
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_5
inst : LinearOrder α
inst_1 : Preorder β
a b : α
c d : β
H : a ≤ b → c ≤ d
h : d < c
⊢ b < a

Tactic:
lt_of_not_ge fun h' ↦ (H h').not_gt h

Premises used: lt_of_not_ge, LE.le.not_gt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
a b : α
c d : β
⊢ a ≤ b → c ≤ d ↔ d < c → b < a

Tactic:
⟨lt_imp_lt_of_le_imp_le, le_imp_le_of_lt_imp_lt⟩

Premises used: le_imp_le_of_lt_imp_lt, Iff.intro, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_5
inst : Preorder α
inst_1 : Preorder β
a b : α
c d : β
H : a ≤ b ↔ c ≤ d
H' : b ≤ a ↔ d ≤ c
⊢ b < a ↔ d < c

Tactic:
lt_iff_le_not_ge.trans <| (and_congr H' (not_congr H)).trans lt_iff_le_not_ge.symm

Premises used: lt_iff_le_not_ge, Iff.trans, Iff.symm, not_congr, and_congr
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
a b : α
c d : β
H : a ≤ b ↔ c ≤ d
⊢ b < a ↔ d < c

Tactic:
not_le.symm.trans <| (not_congr H).trans <| not_le

Premises used: not_le, Iff.trans, Iff.symm, not_congr
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_5
inst : LinearOrder α
inst_1 : LinearOrder β
a b : α
c d : β
⊢ (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c)

Tactic:
⟨lt_iff_lt_of_le_iff_le, fun H ↦ not_lt.symm.trans <| (not_congr H).trans <| not_lt⟩

Premises used: not_lt, Iff.intro, Iff.trans, lt_iff_lt_of_le_iff_le, Iff.symm, not_congr
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder β
r : α → α → Prop
inst_1 : Std.Symm r
f : α → β
h : ∀ (a b : α), r a b → f a ≤ f b
a b : α
⊢ r a b → f a = f b

Tactic:
fun hab ↦
  le_antisymm (h a b hab) (h b a <| symm hab)

Premises used: le_antisymm, symm
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
le A_lt : α → α → Prop
le_refl : ∀ (a : α), le a a
le_trans : ∀ (a b c : α), le a b → le b c → le a c
A_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
B_lt : α → α → Prop
le_refl_1 : ∀ (a : α), le a a
le_trans_1 : ∀ (a b c : α), le a b → le b c → le a c
B_iff : ∀ (a b : α), B_lt a b ↔ le a b ∧ ¬le b a
h : ∀ (a b : α), A_lt a b = B_lt a b
⊢ A_lt = B_lt

Tactic:
funext a b
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
le A_lt : α → α → Prop
le_refl : ∀ (a : α), le a a
le_trans : ∀ (a b c : α), le a b → le b c → le a c
A_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
B_lt : α → α → Prop
le_refl_1 : ∀ (a : α), le a a
le_trans_1 : ∀ (a b c : α), le a b → le b c → le a c
B_iff : ∀ (a b : α), B_lt a b ↔ le a b ∧ ¬le b a
a b : α
h : (le a b ∧ ¬le b a) = B_lt a b
h₁ h₂ : (le a b ∧ ¬le b a) = (le a b ∧ ¬le b a)
⊢ A_lt a b = B_lt a b

Tactic:
rw [A_iff, B_iff]
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
le A_lt : α → α → Prop
le_refl : ∀ (a : α), le a a
le_trans : ∀ (a b c : α), le a b → le b c → le a c
A_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
B_lt : α → α → Prop
le_refl_1 : ∀ (a : α), le a a
le_trans_1 : ∀ (a b c : α), le a b → le b c → le a c
B_iff : ∀ (a b : α), B_lt a b ↔ le a b ∧ ¬le b a
⊢ A_lt = B_lt

Tactic:
have : A_lt = B_lt := by
      funext a b
      rw [A_iff, B_iff]
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
le A_lt : α → α → Prop
le_refl : ∀ (a : α), le a a
le_trans : ∀ (a b c : α), le a b → le b c → le a c
A_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
B_lt : α → α → Prop
le_refl_1 : ∀ (a : α), le a a
le_trans_1 : ∀ (a b c : α), le a b → le b c → le a c
B_iff : ∀ (a b : α), B_lt a b ↔ le a b ∧ ¬le b a
this : A_lt = B_lt
refl :
  ∀ (B_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a),
    Eq.{u_2 + 1} (α := Preorder α)
      { le := le, lt := A_lt, le_refl := le_refl, le_trans := le_trans, lt_iff_le_not_ge := A_iff }
      { le := le, lt := A_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := B_iff }
⊢ Eq.{u_2 + 1} (α := Preorder α)
    { le := le, lt := A_lt, le_refl := le_refl, le_trans := le_trans, lt_iff_le_not_ge := A_iff }
    { le := le, lt := B_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := B_iff }

Tactic:
cases this
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
le A_lt : α → α → Prop
le_refl : ∀ (a : α), le a a
le_trans : ∀ (a b c : α), le a b → le b c → le a c
A_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
le_refl_1 : ∀ (a : α), le a a
le_trans_1 : ∀ (a b c : α), le a b → le b c → le a c
B_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
⊢ Eq.{u_2 + 1} (α := Preorder α)
    { le := le, lt := A_lt, le_refl := le_refl, le_trans := le_trans, lt_iff_le_not_ge := A_iff }
    { le := le, lt := A_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := B_iff }

Tactic:
congr
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
toPreorder : Preorder α
le_antisymm le_antisymm_1 : ∀ (a b : α), a ≤ b → b ≤ a → a = b
⊢ { toPreorder := toPreorder, le_antisymm := le_antisymm : PartialOrder α } =
    { toPreorder := toPreorder, le_antisymm := le_antisymm_1 }

Tactic:
congr
-- 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
B_decidableEq : DecidableEq α
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
B_decidableLE : DecidableLE α
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_decidableLT : DecidableLT α
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
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
⊢ A_decidableLE = B_decidableLE

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
B_decidableEq : DecidableEq α
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
B_decidableLT : DecidableLT α
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
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
⊢ A_decidableEq = B_decidableEq

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
B_decidableLT : DecidableLT α
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_decidableLT = B_decidableLT

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- 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
h : ∀ (a b : α), A_min a b = B_min a b
⊢ A_min = B_min

Tactic:
funext a b