awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
⊢ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
have mpr : a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a → ¬b ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a → ¬b ≤ a
mp₁ mp₂ : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
⊢ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
have mp₃ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬a ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a → ¬b ≤ a
mp₁ mp₂ : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mp₃ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬a ≤ b
⊢ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
have mp₄ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬b ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a → ¬b ≤ a
mp₁ mp₂ : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mp₃ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬a ≤ b
mp₄ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬b ≤ a
⊢ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
have mpr₁ : a ≤ b → ¬b ≤ a → ¬b ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a → ¬b ≤ a
mp₁ mp₂ : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mp₃ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬a ≤ b
mp₄ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬b ≤ a
mpr₁ : a ≤ b → ¬b ≤ a → ¬b ≤ a
⊢ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
have mpr₂ : ¬a ≤ b → ¬b ≤ a → ¬b ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a → ¬b ≤ a
mp₁ mp₂ : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mp₃ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬a ≤ b
mp₄ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬b ≤ a
mpr₁ : a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₂ : ¬a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₃ : a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₄ : ¬a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₅ : a ≤ b → ¬b ≤ a → b ≤ a → False
mpr₆ : ¬a ≤ b → ¬b ≤ a → b ≤ a → False
⊢ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
have mp₅ : ¬b ≤ a → a ≤ b → ¬a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a → ¬b ≤ a
mp₁ mp₂ : ¬b ≤ a → a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
mp₃ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬a ≤ b
mp₄ : ¬b ≤ a → ¬(a ≤ b ∧ ¬b ≤ a) → ¬b ≤ a
mpr₁ : a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₂ : ¬a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₃ : a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₄ : ¬a ≤ b → ¬b ≤ a → ¬b ≤ a
mpr₅ : a ≤ b → ¬b ≤ a → b ≤ a → False
mpr₆ : ¬a ≤ b → ¬b ≤ a → b ≤ a → False
mp₅ : ¬b ≤ a → a ≤ b → ¬a ≤ b → False
⊢ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a ∨ ¬a ≤ b ∧ ¬b ≤ a
have mp₆ : ¬b ≤ a → a ≤ b → ¬¬b ≤ a → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ a < b ∨ AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b < a ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have simp_rw : a ≤ b ∧ ¬b ≤ a ∨
  AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: simp_rw [lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have tauto : ¬(a ≤ b ∧ ¬b ≤ a) →
  AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inl₂ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inr₂ : ¬¬b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₂ :
  ¬¬b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₃ inl₄ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inl₅ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₂ :
  ¬¬b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₃ inl₄ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₅ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inr₃ : b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₂ :
  ¬¬b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₃ inl₄ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₅ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₃ inr₄ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inr₅ : b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₂ :
  ¬¬b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₃ inl₄ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₅ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₃ inr₄ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₅ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inl₆ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₂ :
  ¬¬b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₃ inl₄ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₅ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₃ inr₄ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₅ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₆ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inl₇ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬¬a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₂ :
  ¬¬b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₃ inl₄ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₅ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₃ inr₄ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₅ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₆ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₇ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬¬a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₈ inl₉ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inr₆ : b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₂ :
  ¬¬b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₃ inl₄ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₅ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₃ inr₄ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₅ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₆ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₇ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬¬a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₈ inl₉ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₆ : b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inr₇ : b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬¬a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Comparable (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
tauto :
  ¬(a ≤ b ∧ ¬b ≤ a) →
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr : ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁ : ¬a ≤ b → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₁ :
  ¬¬b ≤ a → AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₂ :
  ¬¬b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₃ inl₄ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₅ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₃ inr₄ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₅ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬(b ≤ a ∧ ¬a ≤ b) → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₆ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₇ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬¬a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₈ inl₉ : ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₆ : b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inr₇ inr₈ inr₉ :
  b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬¬a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
inl₁₀ inl₁₁ inl₁₂ :
  ¬a ≤ b → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → ¬b ≤ a → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
⊢ a ≤ b ∧ ¬b ≤ a ∨
    AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b ∨ b ≤ a ∧ ¬a ≤ b ∨ IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have inr₁₀ : b ≤ a → ¬AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b → a ≤ b → IncompRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
⊢ (cmpLE x y).swap = cmpLE y x
have pos : ∀ (xy : x ≤ y), (cmpLE x y).swap = cmpLE y x
Tactic: by_cases xy : x ≤ y
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
pos : ∀ (xy : x ≤ y), (cmpLE x y).swap = cmpLE y x
⊢ (cmpLE x y).swap = cmpLE y x
have neg : ∀ (xy : ¬x ≤ y), (cmpLE x y).swap = cmpLE y x
Tactic: by_cases xy : x ≤ y
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : x ≤ y
⊢ (cmpLE x y).swap = cmpLE y x
have pos : ∀ (yx : y ≤ x), (cmpLE x y).swap = cmpLE y x
Tactic: by_cases yx : y ≤ x
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : x ≤ y
pos : ∀ (yx : y ≤ x), (cmpLE x y).swap = cmpLE y x
⊢ (cmpLE x y).swap = cmpLE y x
have neg : ∀ (yx : ¬y ≤ x), (cmpLE x y).swap = cmpLE y x
Tactic: by_cases yx : y ≤ x
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : ¬x ≤ y
⊢ (cmpLE x y).swap = cmpLE y x
have pos : ∀ (yx : y ≤ x), (cmpLE x y).swap = cmpLE y x
Tactic: by_cases yx : y ≤ x
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : ¬x ≤ y
pos : ∀ (yx : y ≤ x), (cmpLE x y).swap = cmpLE y x
⊢ (cmpLE x y).swap = cmpLE y x
have neg : ∀ (yx : ¬y ≤ x), (cmpLE x y).swap = cmpLE y x
Tactic: by_cases yx : y ≤ x
-- Lean 4 proof step from Mathlib.Order.Compare (goal)
Goal:
α : Type u_3
inst : LE α
inst_1 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
inst_2 : DecidableLE α
x y : α
xy : ¬x ≤ y
yx : ¬y ≤ x
⊢ (cmpLE x y).swap = cmpLE y x
have neg : False
Tactic: simp [cmpLE, *, Ordering.swap]