awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
⊢ (∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update (β := α) b i x
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
⊢ a ⋖ b ↔ ∃ (i : ι) (x : α i), x ⋖ b i ∧ a = Function.update (β := α) b i x
have 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
Tactic: rw [covBy_iff]
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst_1 : DecidableEq ι
⊢ (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), x ⋖ b i ∧ a = Function.update (β := α) b i x
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
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
⊢ (∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j) ↔
    ∃ (i : ι) (x : α i), x ⋖ b i ∧ a = Function.update (β := α) b i x
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithTop α
⊢ a ⋖ ⊤ ↔ ∃ (b : α), IsMax b ∧ a = (↑b : WithTop α)
have coe : ∀ (a : α), (↑a : WithTop α) ⋖ ⊤ ↔ ∃ (b : α), IsMax b ∧ (↑a : WithTop α) = (↑b : WithTop α)
Tactic: cases a with
  | coe a => simp [CovBy, WithTop.forall, isMax_iff_forall_not_lt]
  | top => simp [CovBy]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Cover (goal)
Goal:
α : Type u_1
inst : Preorder α
a : WithTop α
coe : ∀ (a : α), (↑a : WithTop α) ⋖ ⊤ ↔ ∃ (b : α), IsMax b ∧ (↑a : WithTop α) = (↑b : WithTop α)
⊢ a ⋖ ⊤ ↔ ∃ (b : α), IsMax b ∧ a = (↑b : WithTop α)
have top : CovBy.{u_1} (α := WithTop α) ⊤ ⊤ ↔ ∃ (b : α), IsMax b ∧ ⊤ = (↑b : WithTop α)
Tactic: cases a with
  | coe a => simp [CovBy, WithTop.forall, isMax_iff_forall_not_lt]
  | top => simp [CovBy]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Cover (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
wf : WellFoundedLT α
a : α
h : ¬IsMax a
⊢ ∃ (a' : α), a ⋖ a'
have h₁ : ∃ (b : α), a < b
Tactic: rw [not_isMax_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
⊢ motive (min a b)
have rw : motive (if a ≤ b then a else b)
Tactic: rw [min_def]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
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
⊢ motive (if a ≤ b then a else b)
have neg : ∀ (h : ¬a ≤ b), motive b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb : a ≤ b → motive b
⊢ motive (max a b)
have rw : motive (if a ≤ b then b else a)
Tactic: rw [max_def]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
motive : α → Prop
ha : b ≤ a → motive a
hb pos : ∀ (h : a ≤ b), motive b
⊢ motive (if a ≤ b then b else a)
have neg : ∀ (h : ¬a ≤ b), motive a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ min a b = if b ≤ a then b else a
have inl : ∀ (h : a < b), min a b = if b ≤ a then b else a
Tactic: obtain h | h | h := lt_trichotomy a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : ∀ (h : a < b), min a b = if b ≤ a then b else a
⊢ min a b = if b ≤ a then b else a
have inr : ∀ (h : a = b), min a b = if b ≤ a then b else a
Tactic: obtain h | h | h := lt_trichotomy a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
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
⊢ min a b = if b ≤ a then b else a
have inr₁ : ∀ (h : b < a), min a b = if b ≤ a then b else a
Tactic: obtain h | h | h := lt_trichotomy a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ max a b = if b ≤ a then a else b
have inl : ∀ (h : a < b), max a b = if b ≤ a then a else b
Tactic: obtain h | h | h := lt_trichotomy a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : ∀ (h : a < b), max a b = if b ≤ a then a else b
⊢ max a b = if b ≤ a then a else b
have inr : ∀ (h : a = b), max a b = if b ≤ a then a else b
Tactic: obtain h | h | h := lt_trichotomy a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
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
⊢ max a b = if b ≤ a then a else b
have inr₁ : ∀ (h : b < a), max a b = if b ≤ a then a else b
Tactic: obtain h | h | h := lt_trichotomy a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ min a b ≤ a
have rw : (if a ≤ b then a else b) ≤ a
Tactic: rw [min_def]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) ≤ a
have pos : ∀ (h : a ≤ b), a ≤ a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
pos : ∀ (h : a ≤ b), a ≤ a
⊢ (if a ≤ b then a else b) ≤ a
have neg : ∀ (h : ¬a ≤ b), b ≤ a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ min a b ≤ b
have rw : (if a ≤ b then a else b) ≤ b
Tactic: rw [min_def]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) ≤ b
have pos : ∀ (h : a ≤ b), a ≤ b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
pos : ∀ (h : a ≤ b), a ≤ b
⊢ (if a ≤ b then a else b) ≤ b
have neg : ∀ (h : ¬a ≤ b), b ≤ b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ min a b
have rw : c ≤ if a ≤ b then a else b
Tactic: rw [min_def]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
⊢ c ≤ if a ≤ b then a else b
have pos : a ≤ b → c ≤ a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : c ≤ a
h₂ : c ≤ b
pos : a ≤ b → c ≤ a
⊢ c ≤ if a ≤ b then a else b
have neg : ¬a ≤ b → c ≤ b
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ min a (min b c) = min b (min a c)
have rw : min (min a b) c = min b (min a c)
Tactic: rw [← min_assoc, min_comm a, min_assoc]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
rw : min (min a b) c = min b (min a c)
⊢ min a (min b c) = min b (min a c)
have rw₁ : min (min b a) c = min b (min a c)
Tactic: rw [← min_assoc, min_comm a, min_assoc]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
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)
⊢ min a (min b c) = min b (min a c)
have rw₂ : min b (min a c) = min b (min a c)
Tactic: rw [← min_assoc, min_comm a, min_assoc]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ min a a = a
have rw : (if a ≤ a then a else a) = a
Tactic: rw [min_def, ite_id]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a : α
rw : (if a ≤ a then a else a) = a
⊢ min a a = a
have rw₁ : a = a
Tactic: rw [min_def, ite_id]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
⊢ a < min b c
have inl : b ≤ c → a < min b c
Tactic: cases le_total b c
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
inl : b ≤ c → a < min b c
⊢ a < min b c
have inr : c ≤ b → a < min b c
Tactic: cases le_total b c
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ a < b
have rw : compareOfLessAndEq a b = Ordering.lt ↔ a < b
Tactic: rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq_eq_lt]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : compareOfLessAndEq a b = Ordering.lt ↔ a < b
⊢ compare a b = Ordering.lt ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq_eq_lt]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.eq ↔ a = b
have rw : compareOfLessAndEq a b = Ordering.eq ↔ a = b
Tactic: rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq_eq_eq le_refl not_le]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : compareOfLessAndEq a b = Ordering.eq ↔ a = b
⊢ compare a b = Ordering.eq ↔ a = b
have rw₁ : a = b ↔ a = b
Tactic: rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq_eq_eq le_refl not_le]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ b < a
have rw : compareOfLessAndEq a b = Ordering.gt ↔ b < a
Tactic: rw [LinearOrder.compare_eq_compareOfLessAndEq,
    compareOfLessAndEq_eq_gt le_antisymm le_total not_le]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : compareOfLessAndEq a b = Ordering.gt ↔ b < a
⊢ compare a b = Ordering.gt ↔ b < a
have rw₁ : b < a ↔ b < a
Tactic: rw [LinearOrder.compare_eq_compareOfLessAndEq,
    compareOfLessAndEq_eq_gt le_antisymm le_total not_le]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b
have lt : ∀ (h : compare a b = Ordering.lt), Ordering.lt ≠ Ordering.gt ↔ a ≤ b
Tactic: cases h : compare a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
lt : ∀ (h : compare a b = Ordering.lt), Ordering.lt ≠ Ordering.gt ↔ a ≤ b
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b
have eq : ∀ (h : compare a b = Ordering.eq), Ordering.eq ≠ Ordering.gt ↔ a ≤ b
Tactic: cases h : compare a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
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
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b
have gt : ∀ (h : compare a b = Ordering.gt), Ordering.gt ≠ Ordering.gt ↔ a ≤ b
Tactic: cases h : compare a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.lt ↔ b ≤ a
have lt : ∀ (h : compare a b = Ordering.lt), Ordering.lt ≠ Ordering.lt ↔ b ≤ a
Tactic: cases h : compare a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
lt : ∀ (h : compare a b = Ordering.lt), Ordering.lt ≠ Ordering.lt ↔ b ≤ a
⊢ compare a b ≠ Ordering.lt ↔ b ≤ a
have eq : ∀ (h : compare a b = Ordering.eq), Ordering.eq ≠ Ordering.lt ↔ b ≤ a
Tactic: cases h : compare a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
lt : ∀ (h : compare a b = Ordering.lt), Ordering.lt ≠ Ordering.lt ↔ b ≤ a
eq : ∀ (h : compare a b = Ordering.eq), Ordering.eq ≠ Ordering.lt ↔ b ≤ a
⊢ compare a b ≠ Ordering.lt ↔ b ≤ a
have gt : ∀ (h : compare a b = Ordering.gt), Ordering.gt ≠ Ordering.lt ↔ b ≤ a
Tactic: cases h : compare a b
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
o : Ordering
⊢ compare a b = o ↔ o.Compares a b
have lt : compare a b = Ordering.lt ↔ Ordering.lt.Compares a b
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
o : Ordering
lt : compare a b = Ordering.lt ↔ Ordering.lt.Compares a b
⊢ compare a b = o ↔ o.Compares a b
have eq : compare a b = Ordering.eq ↔ Ordering.eq.Compares a b
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
o : Ordering
lt : compare a b = Ordering.lt ↔ Ordering.lt.Compares a b
eq : compare a b = Ordering.eq ↔ Ordering.eq.Compares a b
⊢ compare a b = o ↔ o.Compares a b
have gt : compare a b = Ordering.gt ↔ Ordering.gt.Compares a b
Tactic: cases o
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.lt ↔ Ordering.lt.Compares a b
have lt : compare a b = Ordering.lt ↔ a < b
Tactic: simp only [Ordering.Compares]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ compare a b = Ordering.gt ↔ Ordering.gt.Compares a b
have gt : compare a b = Ordering.gt ↔ a > b
Tactic: simp only [Ordering.Compares]
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ cmp a b = compare a b
have refine : (cmp a b).Compares a b
Tactic: refine ((compare_iff ..).2 ?_).symm
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then Ordering.lt
      else if (fun (x1 x2 : α) ↦ x1 < x2) b a then Ordering.gt else Ordering.eq).Compares
    a b
have pos : ∀ (h1 : (fun (x1 x2 : α) ↦ x1 < x2) a b), Ordering.lt.Compares a b
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
pos : ∀ (h1 : (fun (x1 x2 : α) ↦ x1 < x2) a b), Ordering.lt.Compares a b
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then Ordering.lt
      else if (fun (x1 x2 : α) ↦ x1 < x2) b a then Ordering.gt else Ordering.eq).Compares
    a b
have pos₁ : ∀ (h1 : ¬(fun (x1 x2 : α) ↦ x1 < x2) a b) (h2 : (fun (x1 x2 : α) ↦ x1 < x2) b a), Ordering.gt.Compares a b
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
pos : ∀ (h1 : (fun (x1 x2 : α) ↦ x1 < x2) a b), Ordering.lt.Compares a b
pos₁ : ∀ (h1 : ¬(fun (x1 x2 : α) ↦ x1 < x2) a b) (h2 : (fun (x1 x2 : α) ↦ x1 < x2) b a), Ordering.gt.Compares a b
⊢ (if (fun (x1 x2 : α) ↦ x1 < x2) a b then Ordering.lt
      else if (fun (x1 x2 : α) ↦ x1 < x2) b a then Ordering.gt else Ordering.eq).Compares
    a b
have neg : ∀ (h1 : ¬(fun (x1 x2 : α) ↦ x1 < x2) a b) (h2 : ¬(fun (x1 x2 : α) ↦ x1 < x2) b a), Ordering.eq.Compares a b
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b_1 c a b : α
⊢ compare a b = (compare b a).swap
have lt : compare b a = Ordering.lt → compare a b = Ordering.lt.swap
Tactic: cases _ : compare b a
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b_1 c a b : α
lt : compare b a = Ordering.lt → compare a b = Ordering.lt.swap
⊢ compare a b = (compare b a).swap
have eq : compare b a = Ordering.eq → compare a b = Ordering.eq.swap
Tactic: cases _ : compare b a
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b_1 c a b : α
lt : compare b a = Ordering.lt → compare a b = Ordering.lt.swap
eq : compare b a = Ordering.eq → compare a b = Ordering.eq.swap
⊢ compare a b = (compare b a).swap
have gt : compare b a = Ordering.gt → compare a b = Ordering.gt.swap
Tactic: cases _ : compare b a
-- Lean 4 proof step from Mathlib.Order.Defs.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c a_1 b_1 c_1 : α
h₁ : (compare a_1 b_1).isLE = true
h₂ : (compare b_1 c_1).isLE = true
⊢ (compare a_1 c_1).isLE = true
have simp : ∀ (h₁ : a_1 ≤ b_1) (h₂ : b_1 ≤ c_1), a_1 ≤ c_1
Tactic: simp only [← Ordering.ne_gt_iff_isLE, compare_le_iff_le] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Defs.PartialOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
hab : a = b
⊢ a ≤ b
have rw : b ≤ b
Tactic: rw [hab]
-- Lean 4 proof step from Mathlib.Order.Defs.Unbundled (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Symm r
inst_1 : IsTrans α r
a b c d : α
h₁ : r a b
h₂ : r c d
⊢ r a c ↔ r b d
have rw : r b c ↔ r b d
Tactic: rw [rel_congr_left h₁, rel_congr_right h₂]
-- Lean 4 proof step from Mathlib.Order.Defs.Unbundled (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : Std.Symm r
inst_1 : IsTrans α r
a b c d : α
h₁ : r a b
h₂ : r c d
rw : r b c ↔ r b d
⊢ r a c ↔ r b d
have rw₁ : r b d ↔ r b d
Tactic: rw [rel_congr_left h₁, rel_congr_right h₂]
-- Lean 4 proof step from Mathlib.Order.Defs.Unbundled (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
⊢ r a c
have inl : ∀ (h₃ : r a b), r a c
Tactic: rcases trichotomous_of r a b with (h₃ | rfl | h₃)
-- Lean 4 proof step from Mathlib.Order.Defs.Unbundled (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
inl : ∀ (h₃ : r a b), r a c
⊢ r a c
have inr : ∀ (h₁ : ¬r a a) (h₂ : r a c), r a c
Tactic: rcases trichotomous_of r a b with (h₃ | rfl | h₃)
Cleared hypotheses: b, h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Defs.Unbundled (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : ¬r b a
h₂ : r b c
inl : ∀ (h₃ : r a b), r a c
inr : ∀ (h₁ : ¬r a a) (h₂ : r a c), r a c
⊢ r a c
have inr₁ : ∀ (h₃ : r b a), r a c
Tactic: rcases trichotomous_of r a b with (h₃ | rfl | h₃)
-- Lean 4 proof step from Mathlib.Order.Defs.Unbundled (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
⊢ r a c
have inl : ∀ (h₃ : r b c), r a c
Tactic: rcases trichotomous_of r b c with (h₃ | rfl | h₃)
-- Lean 4 proof step from Mathlib.Order.Defs.Unbundled (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
inl : ∀ (h₃ : r b c), r a c
⊢ r a c
have inr : ∀ (h₂ : ¬r b b), r a b
Tactic: rcases trichotomous_of r b c with (h₃ | rfl | h₃)
Cleared hypotheses: c, h₂
-- Lean 4 proof step from Mathlib.Order.Defs.Unbundled (goal)
Goal:
α : Sort u_1
r : α → α → Prop
inst : IsTrans α r
inst_1 : Std.Trichotomous r
a b c : α
h₁ : r a b
h₂ : ¬r c b
inl : ∀ (h₃ : r b c), r a c
inr : ∀ (h₂ : ¬r b b), r a b
⊢ r a c
have inr₁ : ∀ (h₃ : r c b), r a c
Tactic: rcases trichotomous_of r b c with (h₃ | rfl | h₃)
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
⊢ DirSupClosedOn D sᶜ ↔ DirSupInaccOn D s
have simp_rw : (∀ ⦃d : Set α⦄,
    d ∈ D → d ⊆ sᶜ → d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ sᶜ) ↔
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ¬Disjoint d s
Tactic: simp_rw [DirSupClosedOn, DirSupInaccOn, ← not_disjoint_iff_nonempty_inter]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
⊢ DirSupClosed sᶜ ↔ DirSupInacc s
have rw : DirSupClosedOn univ sᶜ ↔ DirSupInacc s
Tactic: rw [← dirSupClosedOn_univ, dirSupClosedOn_compl, dirSupInaccOn_univ]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
rw : DirSupClosedOn univ sᶜ ↔ DirSupInacc s
⊢ DirSupClosed sᶜ ↔ DirSupInacc s
have rw₁ : DirSupInaccOn univ s ↔ DirSupInacc s
Tactic: rw [← dirSupClosedOn_univ, dirSupClosedOn_compl, dirSupInaccOn_univ]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
rw : DirSupClosedOn univ sᶜ ↔ DirSupInacc s
rw₁ : DirSupInaccOn univ s ↔ DirSupInacc s
⊢ DirSupClosed sᶜ ↔ DirSupInacc s
have rw₂ : DirSupInacc s ↔ DirSupInacc s
Tactic: rw [← dirSupClosedOn_univ, dirSupClosedOn_compl, dirSupInaccOn_univ]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
⊢ DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s
have rw : DirSupClosedOn D sᶜᶜ ↔ DirSupClosedOn D s
Tactic: rw [← dirSupClosedOn_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
D : Set (Set α)
inst : Preorder α
rw : DirSupClosedOn D sᶜᶜ ↔ DirSupClosedOn D s
⊢ DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s
have rw₁ : DirSupClosedOn D s ↔ DirSupClosedOn D s
Tactic: rw [← dirSupClosedOn_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
⊢ DirSupInacc sᶜ ↔ DirSupClosed s
have rw : DirSupClosed sᶜᶜ ↔ DirSupClosed s
Tactic: rw [← dirSupClosed_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
rw : DirSupClosed sᶜᶜ ↔ DirSupClosed s
⊢ DirSupInacc sᶜ ↔ DirSupClosed s
have rw₁ : DirSupClosed s ↔ DirSupClosed s
Tactic: rw [← dirSupClosed_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
⊢ DirSupInaccOn D (⋃₀ s)
have rw : DirSupClosedOn D (⋂₀ (Compl.compl '' s))
Tactic: rw [← dirSupClosedOn_compl, Set.compl_sUnion]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
D : Set (Set α)
inst : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
⊢ DirSupClosedOn D (⋂₀ (Compl.compl '' s))
have hs₁ : ∀ x ∈ Compl.compl '' s, DirSupClosedOn D x
Tactic: apply DirSupClosedOn.sInter
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (s ∩ t)
have rw : DirSupClosedOn D (⋂₀ {s, t})
Tactic: rw [← sInter_pair]
-- Lean 4 proof step from Mathlib.Order.DirSupClosed (goal)
Goal:
α : Type u_1
s t : Set α
D : Set (Set α)
inst : Preorder α
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (⋂₀ {s, t})
have refine : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) {s, t} x → DirSupClosedOn D x
Tactic: refine .sInter ?_