awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
rw :
  (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x
⊢ a ⋖ b ↔ ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x

Tactic:
rw [covBy_iff]

Premises used: Pi.covBy_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
mp :
  (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) →
    ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x
mpr :
  (∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x) →
    ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
⊢ (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x

Tactic:
constructor
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ b = Function.update (β := α) a i (b i)

Tactic:
simpa [Function.eq_update_iff, eq_comm] using h

Premises used: eq_comm, Function.eq_update_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update (β := α) a i x

Tactic:
exact ⟨i, b i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst_1 : DecidableEq ι
i : ι
x : α i
h : a i ⋖ x
⊢ a i ⋖ Function.update (β := α) a i x i ∧ ∀ (j : ι), j ≠ i → a j = Function.update (β := α) a i x j

Tactic:
simpa +contextual
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a : (i : ι) → α i
inst_1 : DecidableEq ι
i : ι
x : α i
h : a i ⋖ x
⊢ ∃ (i_1 : ι), a i_1 ⋖ Function.update (β := α) a i x i_1 ∧ ∀ (j : ι), j ≠ i_1 → a j = Function.update (β := α) a i x j

Tactic:
exact ⟨i, by simpa +contextual⟩
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
rw :
  (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x
⊢ a ⩿ b ↔ ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x

Tactic:
rw [wcovBy_iff]

Premises used: Pi.wcovBy_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
mp :
  (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) →
    ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x
mpr :
  (∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x) →
    ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
⊢ (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x

Tactic:
constructor
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ a = Function.update (β := α) b i (a i)

Tactic:
simpa [Function.eq_update_iff, eq_comm] using h

Premises used: eq_comm, Function.eq_update_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x

Tactic:
exact ⟨i, a i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
i : ι
x : α i
h : x ⩿ b i
⊢ Function.update (β := α) b i x i ⩿ b i ∧ ∀ (j : ι), j ≠ i → Function.update (β := α) b i x j = b j

Tactic:
simpa +contextual
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst_1 : Nonempty ι
inst_2 : DecidableEq ι
i : ι
x : α i
h : x ⩿ b i
⊢ ∃ (i_1 : ι), Function.update (β := α) b i x i_1 ⩿ b i_1 ∧ ∀ (j : ι), j ≠ i_1 → Function.update (β := α) b i x j = b j

Tactic:
exact ⟨i, by simpa +contextual⟩
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
rw :
  (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), x ⋖ b i ∧ a = Function.update (β := α) b i x
⊢ a ⋖ b ↔ ∃ (i : ι) (x : α i), x ⋖ b i ∧ a = Function.update (β := α) b i x

Tactic:
rw [covBy_iff]

Premises used: Pi.covBy_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
mp :
  (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) →
    ∃ (i : ι) (x : α i), x ⋖ b i ∧ a = Function.update (β := α) b i x
mpr :
  (∃ (i : ι) (x : α i), x ⋖ b i ∧ a = Function.update (β := α) b i x) →
    ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
⊢ (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), x ⋖ b i ∧ a = Function.update (β := α) b i x

Tactic:
constructor
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ a = Function.update (β := α) b i (a i)

Tactic:
simpa [Function.eq_update_iff, eq_comm] using h

Premises used: eq_comm, Function.eq_update_iff
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ ∃ (i : ι) (x : α i), x ⋖ b i ∧ a = Function.update (β := α) b i x

Tactic:
exact ⟨i, a i, hi, by simpa [Function.eq_update_iff, eq_comm] using h⟩
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst_1 : DecidableEq ι
i : ι
x : α i
h : x ⋖ b i
⊢ Function.update (β := α) b i x i ⋖ b i ∧ ∀ (j : ι), j ≠ i → Function.update (β := α) b i x j = b j

Tactic:
simpa +contextual
-- Module: Mathlib.Order.Cover
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
b : (i : ι) → α i
inst_1 : DecidableEq ι
i : ι
x : α i
h : x ⋖ b i
⊢ ∃ (i_1 : ι), Function.update (β := α) b i x i_1 ⋖ b i_1 ∧ ∀ (j : ι), j ≠ i_1 → Function.update (β := α) b i x j = b j

Tactic:
exact ⟨i, by simpa +contextual⟩
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ OrdConnected.{u_1} (α := WithTop α) (range (ι := α) (⇑coeOrderHom : (a : α) → WithTop α))

Tactic:
simp [WithTop.range_coe, ordConnected_Iio]

Premises used: Set.ordConnected_Iio, WithTop.range_coe
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (↑a : WithTop α) ⋖ ⊤ ↔ ∃ (b : α), IsMax b ∧ (↑a : WithTop α) = (↑b : WithTop α)

Tactic:
simp [CovBy, WithTop.forall, isMax_iff_forall_not_lt]

Premises used: CovBy, WithTop.forall, isMax_iff_forall_not_lt
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
⊢ CovBy.{u_1} (α := WithTop α) ⊤ ⊤ ↔ ∃ (b : α), IsMax b ∧ ⊤ = (↑b : WithTop α)

Tactic:
simp [CovBy]

Premises used: CovBy
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a : WithTop α
coe : ∀ (a : α), (↑a : WithTop α) ⋖ ⊤ ↔ ∃ (b : α), IsMax b ∧ (↑a : WithTop α) = (↑b : WithTop α)
top : CovBy.{u_1} (α := WithTop α) ⊤ ⊤ ↔ ∃ (b : α), IsMax b ∧ ⊤ = (↑b : WithTop α)
⊢ a ⋖ ⊤ ↔ ∃ (b : α), IsMax b ∧ a = (↑b : WithTop α)

Tactic:
cases a with
  | coe a => simp [CovBy, WithTop.forall, isMax_iff_forall_not_lt]
  | top => simp [CovBy]

Premises used: CovBy, WithTop.forall, isMax_iff_forall_not_lt, WithTop.top, WithTop.coe
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : WithTop α
⊢ ¬a ⋖ ⊤

Tactic:
simp [covBy_top_iff]

Premises used: WithTop.covBy_top_iff
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (↑a : WithTop α) ⋖ ⊤ ↔ IsMax a

Tactic:
simp [covBy_iff_Ioo_eq, ← image_coe_Ioi]

Premises used: WithTop.image_coe_Ioi, covBy_iff_Ioo_eq
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (↑a : WithTop α) ⩿ ⊤ ↔ IsMax a

Tactic:
simp only [wcovBy_iff_Ioo_eq, ← image_coe_Ioi, le_top, image_eq_empty, true_and, Ioi_eq_empty_iff]

Premises used: wcovBy_iff_Ioo_eq, WithTop.image_coe_Ioi, Set.image_eq_empty, le_top, Set.Ioi_eq_empty_iff, true_and
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
wf : WellFoundedLT α
a : α
h : ¬IsMax a
⊢ ∃ (b : α), a < b

Tactic:
rw [not_isMax_iff] at h

Premises used: not_isMax_iff
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
wf : WellFoundedLT α
a : α
h : ∃ (b : α), a < b
⊢ ∃ (a' : α), a ⋖ a'

Tactic:
⟨_, wellFounded_lt.min_mem (Ioi a) h, fun a' ↦ wf.wf.not_lt_min (Ioi a)⟩

Premises used: WellFounded.min_mem, Set.Ioi, IsWellFounded.wf, wellFounded_lt, And.intro, Exists.intro, WellFounded.not_lt_min
-- Module: Mathlib.Order.Cover
Goal:
α : Type u_1
inst : Preorder α
wf : WellFoundedLT α
a : α
h : ∃ (b : α), a < b
⊢ ∃ (a' : α), a ⋖ a'

Tactic:
exact ⟨_, wellFounded_lt.min_mem (Ioi a) h, fun a' ↦ wf.wf.not_lt_min (Ioi a)⟩
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
⊢ ∀ (a b : α), a ≤ b ∨ b ≤ a

Tactic:
LinearOrder.le_total

Premises used: LinearOrder.le_total
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ ¬a ≤ b → b ≤ a

Tactic:
(le_total a b).resolve_left

Premises used: Or.resolve_left, le_total
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : ¬b ≤ a
⊢ a < b

Tactic:
lt_of_le_not_ge (le_of_not_ge h) h

Premises used: le_of_not_ge, lt_of_le_not_ge
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ a < b ∨ b ≤ a

Tactic:
if hba : b ≤ a then Or.inr hba else Or.inl <| lt_of_not_ge hba

Premises used: lt_of_not_ge, dite, Or.inl, Or.inr
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ a ≤ b ∨ b < a

Tactic:
(lt_or_ge b a).symm

Premises used: Or.symm, lt_or_ge
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ a < b ∨ a = b ∨ b < a

Tactic:
(lt_or_ge a b).imp_right (fun h ↦ (Decidable.lt_or_eq_of_le' h).symm)

Premises used: Decidable.lt_or_eq_of_le', Or.symm, lt_or_ge, Or.imp_right
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : ¬b < a
⊢ a ≤ b

Tactic:
(le_or_gt a b).resolve_right h

Premises used: le_or_gt, Or.resolve_right
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≠ b
⊢ a < b ∨ b < a

Tactic:
(lt_trichotomy a b).imp_right (fun h' ↦ h'.resolve_left h)

Premises used: Or.imp_right, lt_trichotomy
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ a ≠ b ↔ a < b ∨ b < a

Tactic:
⟨lt_or_gt_of_ne, (Or.elim · ne_of_lt ne_of_gt)⟩

Premises used: lt_or_gt_of_ne, ne_of_gt, Iff.intro, Or.elim, ne_of_lt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ a < b ↔ ¬b ≤ a

Tactic:
⟨not_le_of_gt, lt_of_not_ge⟩

Premises used: lt_of_not_ge, Iff.intro, not_le_of_gt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ ¬a < b ↔ b ≤ a

Tactic:
⟨le_of_not_gt, not_lt_of_ge⟩

Premises used: le_of_not_gt, Iff.intro, not_lt_of_ge
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ ¬a ≤ b ↔ b < a

Tactic:
lt_iff_not_ge.symm

Premises used: lt_iff_not_ge, Iff.symm
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : ¬a < b
⊢ a = b ∨ b < a

Tactic:
if h₁ : a = b then Or.inl h₁ else Or.inr (lt_of_not_ge fun hge => h (lt_of_le_of_ne hge h₁))

Premises used: lt_of_not_ge, dite, Or.inl, Or.inr, lt_of_le_of_ne
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LinearOrder β
a b : α
c d : β
H : d < c → b < a
h : a ≤ b
⊢ c ≤ d

Tactic:
le_of_not_gt fun h' => not_le_of_gt (H h') h

Premises used: le_of_not_gt, not_le_of_gt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ min a b = if a ≤ b then a else b

Tactic:
LinearOrder.min_def a b

Premises used: LinearOrder.min_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ max a b = if a ≤ b then b else a

Tactic:
LinearOrder.max_def a b

Premises used: LinearOrder.max_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
rw : motive (if a ≤ b then a else b)
⊢ motive (min a b)

Tactic:
rw [min_def]

Premises used: min_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
pos : ∀ (h : a ≤ b), motive a
neg : ∀ (h : ¬a ≤ b), motive b
⊢ motive (if a ≤ b then a else b)

Tactic:
split_ifs with h
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
h : a ≤ b
⊢ motive a

Tactic:
ha h
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
h : ¬a ≤ b
⊢ motive b

Tactic:
hb (le_of_not_ge h)

Premises used: le_of_not_ge
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
h : a ≤ b
⊢ motive a

Tactic:
exacts [ha h, hb (le_of_not_ge h)]
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
rw : motive (if a ≤ b then b else a)
⊢ motive (max a b)

Tactic:
rw [max_def]

Premises used: max_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb pos : ∀ (h : a ≤ b), motive b
neg : ∀ (h : ¬a ≤ b), motive a
⊢ motive (if a ≤ b then b else a)

Tactic:
split_ifs with h
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
h : a ≤ b
⊢ motive b

Tactic:
hb h
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
h : ¬a ≤ b
⊢ motive a

Tactic:
ha (le_of_not_ge h)

Premises used: le_of_not_ge
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
h : a ≤ b
⊢ motive b

Tactic:
exacts [hb h, ha (le_of_not_ge h)]
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : ∀ (h : a < b), min a b = if b ≤ a then b else a
inr : ∀ (h : a = b), min a b = if b ≤ a then b else a
inr₁ : ∀ (h : b < a), min a b = if b ≤ a then b else a
⊢ min a b = if b ≤ a then b else a

Tactic:
obtain h | h | h := lt_trichotomy a b

Premises used: lt_trichotomy
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ min a b = if b ≤ a then b else a

Tactic:
simp [le_of_lt, not_le_of_gt, h, min_def]

Premises used: le_of_lt, min_def, not_le_of_gt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a = b
⊢ min a b = if b ≤ a then b else a

Tactic:
simp [le_of_lt, not_le_of_gt, h, min_def]

Premises used: le_of_lt, min_def, not_le_of_gt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b < a
⊢ min a b = if b ≤ a then b else a

Tactic:
simp [le_of_lt, not_le_of_gt, h, min_def]

Premises used: le_of_lt, min_def, not_le_of_gt
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : ∀ (h : a < b), max a b = if b ≤ a then a else b
inr : ∀ (h : a = b), max a b = if b ≤ a then a else b
inr₁ : ∀ (h : b < a), max a b = if b ≤ a then a else b
⊢ max a b = if b ≤ a then a else b

Tactic:
obtain h | h | h := lt_trichotomy a b

Premises used: lt_trichotomy
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ max a b = if b ≤ a then a else b

Tactic:
simp [le_of_lt, not_le_of_gt, h, max_def]

Premises used: le_of_lt, not_le_of_gt, max_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a = b
⊢ max a b = if b ≤ a then a else b

Tactic:
simp [le_of_lt, not_le_of_gt, h, max_def]

Premises used: le_of_lt, not_le_of_gt, max_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b < a
⊢ max a b = if b ≤ a then a else b

Tactic:
simp [le_of_lt, not_le_of_gt, h, max_def]

Premises used: le_of_lt, not_le_of_gt, max_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : (if a ≤ b then a else b) ≤ a
⊢ min a b ≤ a

Tactic:
rw [min_def]

Premises used: min_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
pos : ∀ (h : a ≤ b), a ≤ a
neg : ∀ (h : ¬a ≤ b), b ≤ a
⊢ (if a ≤ b then a else b) ≤ a

Tactic:
split_ifs with h
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ a

Tactic:
simp [h, le_of_not_ge]

Premises used: le_of_not_ge
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ a

Tactic:
simp [h, le_of_not_ge]

Premises used: le_of_not_ge
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : (if a ≤ b then a else b) ≤ b
⊢ min a b ≤ b

Tactic:
rw [min_def]

Premises used: min_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
pos : ∀ (h : a ≤ b), a ≤ b
neg : ∀ (h : ¬a ≤ b), b ≤ b
⊢ (if a ≤ b then a else b) ≤ b

Tactic:
split_ifs with h
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ b

Tactic:
simp [h]
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b ≤ b

Tactic:
simp [h]
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
rw : c ≤ if a ≤ b then a else b
⊢ c ≤ min a b

Tactic:
rw [min_def]

Premises used: min_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
pos : a ≤ b → c ≤ a
neg : ¬a ≤ b → c ≤ b
⊢ c ≤ if a ≤ b then a else b

Tactic:
split_ifs
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h : a ≤ b
⊢ c ≤ a

Tactic:
assumption
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h : ¬a ≤ b
⊢ c ≤ b

Tactic:
assumption
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
h₃ : ∀ {d : α}, d ≤ a → d ≤ b → d ≤ c
⊢ c = min a b

Tactic:
le_antisymm (le_min h₁ h₂) (h₃ (min_le_left a b) (min_le_right a b))

Premises used: le_min, min_le_left, le_antisymm, min_le_right
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ min a b = min b a

Tactic:
eq_min (min_le_right a b) (min_le_left a b) fun h₁ h₂ => le_min h₂ h₁

Premises used: le_min, min_le_left, min_le_right, eq_min
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ min (min a b) c = min a (min b c)

Tactic:
eq_min
    (le_trans (min_le_left ..) (min_le_left ..))
    (le_min (le_trans (min_le_left ..) (min_le_right ..)) (min_le_right ..))
    (fun h₁ h₂ ↦
      le_min (le_min h₁ (le_trans h₂ (min_le_left ..))) (le_trans h₂ (min_le_right ..)))

Premises used: le_min, min_le_left, min_le_right, eq_min, le_trans
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
rw : min (min a b) c = min b (min a c)
rw₁ : min (min b a) c = min b (min a c)
rw₂ rw₃ : min b (min a c) = min b (min a c)
⊢ min a (min b c) = min b (min a c)

Tactic:
rw [← min_assoc, min_comm a, min_assoc]

Premises used: min_comm, min_assoc
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a : α
rw : (if a ≤ a then a else a) = a
rw₁ rw₂ : a = a
⊢ min a a = a

Tactic:
rw [min_def, ite_id]

Premises used: ite_id, min_def
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a

Tactic:
(eq_min le_rfl h (fun h _ ↦ h)).symm

Premises used: le_rfl, Eq.symm, eq_min
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b ≤ a
⊢ min a b = b

Tactic:
min_comm b a ▸ min_eq_left h

Premises used: min_comm, Eq.rec, min_eq_left
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ min a b = a

Tactic:
min_eq_left (le_of_lt h)

Premises used: le_of_lt, min_eq_left
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b < a
⊢ min a b = b

Tactic:
min_eq_right (le_of_lt h)

Premises used: le_of_lt, min_eq_right
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
inl : b ≤ c → a < min b c
inr : c ≤ b → a < min b c
⊢ a < min b c

Tactic:
cases le_total b c

Premises used: le_total
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h : b ≤ c
⊢ a < min b c

Tactic:
simp [min_eq_left, min_eq_right, *]

Premises used: min_eq_right, min_eq_left
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
h : c ≤ b
⊢ a < min b c

Tactic:
simp [min_eq_left, min_eq_right, *]

Premises used: min_eq_right, min_eq_left
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : compareOfLessAndEq a b = Ordering.lt ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ compare a b = Ordering.lt ↔ a < b

Tactic:
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq_eq_lt]

Premises used: compareOfLessAndEq_eq_lt, LinearOrder.compare_eq_compareOfLessAndEq
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : compareOfLessAndEq a b = Ordering.eq ↔ a = b
rw₁ rw₂ : a = b ↔ a = b
⊢ compare a b = Ordering.eq ↔ a = b

Tactic:
rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq_eq_eq le_refl not_le]

Premises used: not_le, le_refl, compareOfLessAndEq_eq_eq, LinearOrder.compare_eq_compareOfLessAndEq
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : compareOfLessAndEq a b = Ordering.gt ↔ b < a
rw₁ rw₂ : b < a ↔ b < a
⊢ compare a b = Ordering.gt ↔ b < a

Tactic:
rw [LinearOrder.compare_eq_compareOfLessAndEq,
    compareOfLessAndEq_eq_gt le_antisymm le_total not_le]

Premises used: not_le, compareOfLessAndEq_eq_gt, le_total, le_antisymm, LinearOrder.compare_eq_compareOfLessAndEq
-- Module: Mathlib.Order.Defs.LinearOrder
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
lt : ∀ (h : compare a b = Ordering.lt), Ordering.lt ≠ Ordering.gt ↔ a ≤ b
eq : ∀ (h : compare a b = Ordering.eq), Ordering.eq ≠ Ordering.gt ↔ a ≤ b
gt : ∀ (h : compare a b = Ordering.gt), Ordering.gt ≠ Ordering.gt ↔ a ≤ b
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b

Tactic:
cases h : compare a b

Premises used: Ord.compare