awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
A B : PartialOrder α
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 : PartialOrder α
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 : ∀ (x y : α), x < y ↔ x < y
a : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
ext x y
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
a : x ≤ y ↔ x < y ∨ x = y
a₁ : x < y ∨ x = y ↔ x < y ∨ x = y
a₂ a₃ : x < y ∨ x = y ↔ x < y ∨ x = y
⊢ x ≤ y ↔ x ≤ y

Tactic:
rw [le_iff_lt_or_eq, @le_iff_lt_or_eq _ A, H]

Premises used: le_iff_lt_or_eq
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
A B : LinearOrder α
H a : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B

Tactic:
ext x y
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
A B : LinearOrder α
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 : LinearOrder α
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 : LinearOrder α
H : ∀ (x y : α), x < y ↔ x < y
⊢ A = B

Tactic:
LinearOrder.toPartialOrder_injective (PartialOrder.ext_lt H)

Premises used: PartialOrder.ext_lt, LinearOrder.toPartialOrder_injective
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → Compl (π i)
x : (i : ι) → π i
⊢ xᶜ = fun (i : ι) ↦ (x i)ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → Compl (π i)
x : (i : ι) → π i
i : ι
⊢ xᶜ i = (x i)ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
r : α → α → Prop
inst : Irrefl r
⊢ Refl rᶜ

Tactic:
⟨@irrefl α r _⟩

Premises used: Std.Irrefl.irrefl, Std.Refl.mk
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
r : α → α → Prop
inst : Refl r
⊢ Irrefl rᶜ

Tactic:
⟨fun a ↦ not_not_intro (refl a)⟩

Premises used: Std.Refl.refl, not_not_intro, Std.Irrefl.mk
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
⊢ Eq.{u_2 + 1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ x1 < x2)ᶜ fun (x1 x2 : α) ↦ x1 ≥ x2

Tactic:
simp [compl]

Premises used: Compl.compl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
⊢ Eq.{u_2 + 1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ x1 ≤ x2)ᶜ fun (x1 x2 : α) ↦ x1 > x2

Tactic:
simp [compl]

Premises used: Compl.compl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
⊢ Eq.{u_2 + 1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ x1 > x2)ᶜ fun (x1 x2 : α) ↦ x1 ≤ x2

Tactic:
simp [compl]

Premises used: Compl.compl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LinearOrder α
⊢ Eq.{u_2 + 1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ x1 ≥ x2)ᶜ fun (x1 x2 : α) ↦ x1 < x2

Tactic:
simp [compl]

Premises used: Compl.compl
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
⊢ IsEquiv α fun (x1 x2 : α) ↦ x1 = x2

Tactic:
eq_isEquiv α

Premises used: eq_isEquiv
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
h : ∀ (x x : α), Eq.{u_2 + 1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ x1 ≠ x2)ᶜ Eq
⊢ IsEquiv α (fun (x1 x2 : α) ↦ x1 ≠ x2)ᶜ

Tactic:
convert! eq_isEquiv α

Premises used: eq_isEquiv
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
x x_1 : α
⊢ Eq.{u_2 + 1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ x1 ≠ x2)ᶜ Eq

Tactic:
simp [compl]

Premises used: Compl.compl
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → LE (π i)
x y : (i : ι) → π i
⊢ x ≤ y ↔ ∀ (i : ι), x i ≤ y i

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
⊢ x < y ↔ x ≤ y ∧ ∃ (i : ι), x i < y i

Tactic:
simp +contextual [lt_iff_le_not_ge, Pi.le_def]

Premises used: lt_iff_le_not_ge, Pi.le_def
-- Module: Mathlib.Order.Basic
Goal:
β : Type u_3
α₁ : Type u_5
α₂ : Type u_6
inst : LE β
u₁ v₁ : α₁ → β
u₂ v₂ : α₂ → β
⊢ Sum.elim u₁ u₂ ≤ Sum.elim v₁ v₂ ↔ u₁ ≤ v₁ ∧ u₂ ≤ v₂

Tactic:
Sum.forall

Premises used: Sum.forall, Sum.elim
-- Module: Mathlib.Order.Basic
Goal:
β : Type u_3
α₁ : Type u_5
α₂ : Type u_6
inst : LE β
b : β
v₁ : α₁ → β
v₂ : α₂ → β
⊢ const (α₁ ⊕ α₂) b ≤ Sum.elim v₁ v₂ ↔ const α₁ b ≤ v₁ ∧ const α₂ b ≤ v₂

Tactic:
elim_const_const b ▸ elim_le_elim_iff ..

Premises used: Eq.rec, Sum.elim_const_const, Sum.elim_le_elim_iff
-- Module: Mathlib.Order.Basic
Goal:
β : Type u_3
α₁ : Type u_5
α₂ : Type u_6
inst : LE β
b : β
u₁ : α₁ → β
u₂ : α₂ → β
⊢ Sum.elim u₁ u₂ ≤ const (α₁ ⊕ α₂) b ↔ u₁ ≤ const α₁ b ∧ u₂ ≤ const α₂ b

Tactic:
elim_const_const b ▸ elim_le_elim_iff ..

Premises used: Eq.rec, Sum.elim_const_const, Sum.elim_le_elim_iff
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
h : StrongLT (π := π) a b
⊢ a ≤ b

Tactic:
fun _ ↦ (h _).le

Premises used: LT.lt.le
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
inst_1 : Nonempty ι
h : StrongLT (π := π) a b
inhabit : ∀ (inhabited_h : Inhabited ι), a < b
⊢ a < b

Tactic:
inhabit ι
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
inst_1 : Nonempty ι
h : StrongLT (π := π) a b
inhabited_h : Inhabited ι
⊢ a < b

Tactic:
Pi.lt_def.2 ⟨le_of_strongLT h, default, h _⟩

Premises used: Iff.mpr, Inhabited.default, Pi.lt_def, And.intro, le_of_strongLT, Exists.intro
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
inst_1 : Nonempty ι
h : StrongLT (π := π) a b
inhabited_h : Inhabited ι
⊢ a < b

Tactic:
exact Pi.lt_def.2 ⟨le_of_strongLT h, default, h _⟩

Premises used: Iff.mpr, Inhabited.default, Pi.lt_def, And.intro, le_of_strongLT, Exists.intro
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
a b c : (i : ι) → π i
hab : StrongLT (π := π) a b
hbc : b ≤ c
⊢ StrongLT (π := π) a c

Tactic:
fun _ ↦
  (hab _).trans_le <| hbc _

Premises used: LT.lt.trans_le, StrongLT
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a : π i
⊢ x ≤ update (β := π) y i a ↔ x i ≤ a ∧ ∀ (j : ι), j ≠ i → x j ≤ y j

Tactic:
Function.forall_update_iff _ fun j z ↦ x j ≤ z

Premises used: LE.le, Function.forall_update_iff
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
i : ι
a b : π i
⊢ update (β := π) x i a ≤ update (β := π) y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j

Tactic:
simp +contextual [update_le_iff]

Premises used: update_le_iff
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a b : π i
⊢ update (β := π) x i a ≤ update (β := π) x i b ↔ a ≤ b

Tactic:
simp [update_le_update_iff]

Premises used: update_le_update_iff
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a b : π i
⊢ update (β := π) x i a < update (β := π) x i b ↔ a < b

Tactic:
lt_iff_lt_of_le_iff_le' update_le_update_iff' update_le_update_iff'

Premises used: update_le_update_iff', lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a : π i
⊢ x ≤ update (β := π) x i a ↔ x i ≤ a

Tactic:
simp [le_update_iff]

Premises used: le_update_iff
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a : π i
⊢ x < update (β := π) x i a ↔ x i < a

Tactic:
simp [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → SDiff (π i)
x y : (i : ι) → π i
⊢ x \ y = fun (i : ι) ↦ x i \ y i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → SDiff (π i)
x y : (i : ι) → π i
i : ι
⊢ (x \ y) i = x i \ y i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Nonempty β
a b : α
⊢ const β a ≤ const β b ↔ a ≤ b

Tactic:
simp [Pi.le_def]

Premises used: Pi.le_def
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Nonempty β
a b : α
⊢ const β a < const β b ↔ a < b

Tactic:
simpa [Pi.lt_def] using le_of_lt

Premises used: Pi.lt_def, le_of_lt
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder β
inst_1 : LE α
inst_2 : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x x_1 : α
rw : x < x_1 ↔ f x ≤ f x_1 ∧ ¬x_1 ≤ x
rw₁ : x < x_1 ↔ f x ≤ f x_1 ∧ ¬f x_1 ≤ f x
rw₂ : f x < f x_1 ↔ f x ≤ f x_1 ∧ ¬f x_1 ≤ f x
rw₃ rw₄ : f x ≤ f x_1 ∧ ¬f x_1 ≤ f x ↔ f x ≤ f x_1 ∧ ¬f x_1 ≤ f x
⊢ x < x_1 ↔ x ≤ x_1 ∧ ¬x_1 ≤ x

Tactic:
rw [← le, ← le, ← lt, lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
⊢ x ≤ x_1 ∨ x_1 ≤ x

Tactic:
simp only [← le, le_total]

Premises used: le_total
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : f (x ⊓ x_1) = f (if x ≤ x_1 then x else x_1)
simp_rw₁ : f (x ⊓ x_1) = f (if f x ≤ f x_1 then x else x_1)
simp_rw₂ : f (x ⊓ x_1) = if f x ≤ f x_1 then f x else f x_1
simp_rw₃ : f (x ⊓ x_1) = Min.min (f x) (f x_1)
⊢ x ⊓ x_1 = if x ≤ x_1 then x else x_1

Tactic:
simp_rw [← hf.eq_iff, ← le, apply_ite f, ← min_def, min]

Premises used: Function.Injective.eq_iff, apply_ite, min_def
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : f (x ⊔ x_1) = f (if x ≤ x_1 then x_1 else x)
simp_rw₁ : f (x ⊔ x_1) = f (if f x ≤ f x_1 then x_1 else x)
simp_rw₂ : f (x ⊔ x_1) = if f x ≤ f x_1 then f x_1 else f x
simp_rw₃ : f (x ⊔ x_1) = Max.max (f x) (f x_1)
⊢ x ⊔ x_1 = if x ≤ x_1 then x_1 else x

Tactic:
simp_rw [← hf.eq_iff, ← le, apply_ite f, ← max_def, max]

Premises used: Function.Injective.eq_iff, apply_ite, max_def
-- Module: Mathlib.Order.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : Ord.compare (f x) (f x_1) = compareOfLessAndEq x x_1
simp_rw₁ : compareOfLessAndEq (f x) (f x_1) = compareOfLessAndEq x x_1
simp_rw₂ :
  (if f x < f x_1 then Ordering.lt else if f x = f x_1 then Ordering.eq else Ordering.gt) =
    if x < x_1 then Ordering.lt else if x = x_1 then Ordering.eq else Ordering.gt
simp_rw₃ :
  (if f x < f x_1 then Ordering.lt else if f x = f x_1 then Ordering.eq else Ordering.gt) =
    if f x < f x_1 then Ordering.lt else if x = x_1 then Ordering.eq else Ordering.gt
⊢ Ord.compare x x_1 = compareOfLessAndEq x x_1

Tactic:
simp_rw [← compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, ← lt,
      hf.eq_iff]

Premises used: Function.Injective.eq_iff, compareOfLessAndEq, LinearOrder.compare_eq_compareOfLessAndEq
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
⊢ compare (f a) (f b) = compareOfLessAndEq (f a) (f b)

Tactic:
have h := LinearOrder.compare_eq_compareOfLessAndEq (f a) (f b)
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
simp :
  (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
⊢ compare (f a) (f b) = compareOfLessAndEq a b

Tactic:
simp only [h, compareOfLessAndEq]

Premises used: compareOfLessAndEq
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
pos : f a < f b → a < b → Ordering.lt = Ordering.lt
pos₁ : f a < f b → ¬a < b → a = b → False
neg : f a < f b → ¬a < b → ¬a = b → False
pos₂ : ¬f a < f b → f a = f b → a < b → False
pos₃ : ¬f a < f b → f a = f b → ¬a < b → a = b → Ordering.eq = Ordering.eq
neg₁ : ¬f a < f b → f a = f b → ¬a < b → ¬a = b → False
pos₄ : ¬f a < f b → ¬f a = f b → a < b → False
pos₅ : ¬f a < f b → ¬f a = f b → ¬a < b → a = b → False
neg₂ : ¬f a < f b → ¬f a = f b → ¬a < b → ¬a = b → Ordering.gt = Ordering.gt
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt

Tactic:
split_ifs
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : f a < f b
h_2 : a < b
⊢ Ordering.lt = Ordering.lt

Tactic:
rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : f a < f b
h_2 : a < b
⊢ Ordering.lt = Ordering.lt

Tactic:
first | rfl | contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : f a < f b
h_2 : a < b
⊢ Ordering.lt = Ordering.lt

Tactic:
try (first | rfl | contradiction)
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : f a < f b
h_2 : ¬a < b
h_3 : a = b
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : f a < f b
h_2 : ¬a < b
h_3 : a = b
⊢ False

Tactic:
first | rfl | contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : f a < f b
h_2 : ¬a < b
h_3 : a = b
⊢ False

Tactic:
try (first | rfl | contradiction)
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : f a < f b
h_2 : ¬a < b
h_3 : ¬a = b
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : f a < f b
h_2 : ¬a < b
h_3 : ¬a = b
⊢ False

Tactic:
first | rfl | contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : f a < f b
h_2 : ¬a < b
h_3 : ¬a = b
⊢ False

Tactic:
try (first | rfl | contradiction)
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : f a = f b
h_3 : a < b
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : f a = f b
h_3 : a < b
⊢ False

Tactic:
first | rfl | contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : f a = f b
h_3 : a < b
⊢ False

Tactic:
try (first | rfl | contradiction)
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : f a = f b
h_3 : ¬a < b
h_4 : a = b
⊢ Ordering.eq = Ordering.eq

Tactic:
rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : f a = f b
h_3 : ¬a < b
h_4 : a = b
⊢ Ordering.eq = Ordering.eq

Tactic:
first | rfl | contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : f a = f b
h_3 : ¬a < b
h_4 : a = b
⊢ Ordering.eq = Ordering.eq

Tactic:
try (first | rfl | contradiction)
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : ¬f a = f b
h_3 : a < b
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : ¬f a = f b
h_3 : a < b
⊢ False

Tactic:
first | rfl | contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : ¬f a = f b
h_3 : a < b
⊢ False

Tactic:
try (first | rfl | contradiction)
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : ¬f a = f b
h_3 : ¬a < b
h_4 : ¬a = b
⊢ Ordering.gt = Ordering.gt

Tactic:
rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : ¬f a = f b
h_3 : ¬a < b
h_4 : ¬a = b
⊢ Ordering.gt = Ordering.gt

Tactic:
first | rfl | contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : ¬f a = f b
h_3 : ¬a < b
h_4 : ¬a = b
⊢ Ordering.gt = Ordering.gt

Tactic:
try (first | rfl | contradiction)
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h_1 : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_2 : ¬f a < f b
h_3 : f a = f b
h_4 : ¬a < b
h : ¬a = b
⊢ ¬f a = f b

Tactic:
inj.ne h

Premises used: Function.Injective.ne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h_1 : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_2 : ¬f a < f b
h_3 : f a = f b
h_4 : ¬a < b
h : ¬a = b
⊢ ¬f a = f b

Tactic:
exact inj.ne h

Premises used: Function.Injective.ne
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : f a = f b
h_3 : ¬a < b
h_4 : ¬a = b
⊢ ¬f a = f b

Tactic:
have : ¬ f a = f b := by rename_i h; exact inj.ne h
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : f a = f b
h_3 : ¬a < b
h_4 : ¬a = b
this : ¬f a = f b
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : ¬f a = f b
h_3 : ¬a < b
h_4 : a = b
⊢ False

Tactic:
grind
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LE α
p : α → Prop
x y : α
hx : p x
hy : p y
⊢ mk (p := p) x hx ≤ mk (p := p) y hy ↔ x ≤ y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LT α
p : α → Prop
x y : α
hx : p x
hy : p y
⊢ mk (p := p) x hx < mk (p := p) y hy ↔ x < y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LE α
p : α → Prop
x y : Subtype p
⊢ (↑x : α) ≤ (↑y : α) ↔ x ≤ y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LT α
p : α → Prop
x y : Subtype p
⊢ (↑x : α) < (↑y : α) ↔ x < y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
β : Type u_3
inst : LE α
inst_1 : LE β
x y : α × β
⊢ x ≤ y ↔ x.fst ≤ y.fst ∧ x.snd ≤ y.snd

Tactic:
.rfl

Premises used: Iff.rfl