awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatSupCat
e : α.X ≃o β.X
a : α.X
⊢ Eq (α := α.X)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X) SemilatSupCat.X
            _ _ α α
            (CategoryStruct.comp (Y := β) { toFun := (⇑e : (a : α.X) → β.X), map_sup' := ⋯, map_bot' := ⋯ }
              { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := ⋯, map_bot' := ⋯ }) :
          (a : α.X) → α.X)
        a :
      α.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X) (CC := SemilatSupCat.X) (𝟙 α) :
          (a : α.X) → α.X)
        a :
      α.X)

Tactic:
e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatSupCat
e : α.X ≃o β.X
a : α.X
⊢ Eq (α := α.X)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X) SemilatSupCat.X
            _ _ α α
            (CategoryStruct.comp (Y := β) { toFun := (⇑e : (a : α.X) → β.X), map_sup' := ⋯, map_bot' := ⋯ }
              { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := ⋯, map_bot' := ⋯ }) :
          (a : α.X) → α.X)
        a :
      α.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X) (CC := SemilatSupCat.X) (𝟙 α) :
          (a : α.X) → α.X)
        a :
      α.X)

Tactic:
exact e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatSupCat
e : α.X ≃o β.X
h :
  ∀ (a : β.X),
    Eq (α := β.X)
      ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X)
              SemilatSupCat.X _ _ β β
              (CategoryStruct.comp (Y := α) { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := ⋯, map_bot' := ⋯ }
                { toFun := (⇑e : (a : α.X) → β.X), map_sup' := ⋯, map_bot' := ⋯ }) :
            (a : β.X) → β.X)
          a :
        β.X)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X) (CC := SemilatSupCat.X)
              (𝟙 β) :
            (a : β.X) → β.X)
          a :
        β.X)
⊢ CategoryStruct.comp (Y := α) { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := ⋯, map_bot' := ⋯ }
      { toFun := (⇑e : (a : α.X) → β.X), map_sup' := ⋯, map_bot' := ⋯ } =
    𝟙 β

Tactic:
ext
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatSupCat
e : α.X ≃o β.X
a : β.X
⊢ Eq (α := β.X)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X) SemilatSupCat.X
            _ _ β β
            (CategoryStruct.comp (Y := α) { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := ⋯, map_bot' := ⋯ }
              { toFun := (⇑e : (a : α.X) → β.X), map_sup' := ⋯, map_bot' := ⋯ }) :
          (a : β.X) → β.X)
        a :
      β.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X) (CC := SemilatSupCat.X) (𝟙 β) :
          (a : β.X) → β.X)
        a :
      β.X)

Tactic:
e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatSupCat
e : α.X ≃o β.X
a : β.X
⊢ Eq (α := β.X)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X) SemilatSupCat.X
            _ _ β β
            (CategoryStruct.comp (Y := α) { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := ⋯, map_bot' := ⋯ }
              { toFun := (⇑e : (a : α.X) → β.X), map_sup' := ⋯, map_bot' := ⋯ }) :
          (a : β.X) → β.X)
        a :
      β.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatSupCat.{u}) ↦ SupBotHom x1.X x2.X) (CC := SemilatSupCat.X) (𝟙 β) :
          (a : β.X) → β.X)
        a :
      β.X)

Tactic:
exact e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatInfCat
e : α.X ≃o β.X
h :
  ∀ (a : α.X),
    Eq (α := α.X)
      ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X)
              SemilatInfCat.X _ _ α α
              (CategoryStruct.comp (Y := β) { toFun := (⇑e : (a : α.X) → β.X), map_inf' := ⋯, map_top' := ⋯ }
                { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := ⋯, map_top' := ⋯ }) :
            (a : α.X) → α.X)
          a :
        α.X)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X) (CC := SemilatInfCat.X)
              (𝟙 α) :
            (a : α.X) → α.X)
          a :
        α.X)
⊢ CategoryStruct.comp (Y := β) { toFun := (⇑e : (a : α.X) → β.X), map_inf' := ⋯, map_top' := ⋯ }
      { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := ⋯, map_top' := ⋯ } =
    𝟙 α

Tactic:
ext
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatInfCat
e : α.X ≃o β.X
a : α.X
⊢ Eq (α := α.X)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X) SemilatInfCat.X
            _ _ α α
            (CategoryStruct.comp (Y := β) { toFun := (⇑e : (a : α.X) → β.X), map_inf' := ⋯, map_top' := ⋯ }
              { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := ⋯, map_top' := ⋯ }) :
          (a : α.X) → α.X)
        a :
      α.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X) (CC := SemilatInfCat.X) (𝟙 α) :
          (a : α.X) → α.X)
        a :
      α.X)

Tactic:
e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatInfCat
e : α.X ≃o β.X
a : α.X
⊢ Eq (α := α.X)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X) SemilatInfCat.X
            _ _ α α
            (CategoryStruct.comp (Y := β) { toFun := (⇑e : (a : α.X) → β.X), map_inf' := ⋯, map_top' := ⋯ }
              { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := ⋯, map_top' := ⋯ }) :
          (a : α.X) → α.X)
        a :
      α.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X) (CC := SemilatInfCat.X) (𝟙 α) :
          (a : α.X) → α.X)
        a :
      α.X)

Tactic:
exact e.symm_apply_apply _

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatInfCat
e : α.X ≃o β.X
h :
  ∀ (a : β.X),
    Eq (α := β.X)
      ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X)
              SemilatInfCat.X _ _ β β
              (CategoryStruct.comp (Y := α) { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := ⋯, map_top' := ⋯ }
                { toFun := (⇑e : (a : α.X) → β.X), map_inf' := ⋯, map_top' := ⋯ }) :
            (a : β.X) → β.X)
          a :
        β.X)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X) (CC := SemilatInfCat.X)
              (𝟙 β) :
            (a : β.X) → β.X)
          a :
        β.X)
⊢ CategoryStruct.comp (Y := α) { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := ⋯, map_top' := ⋯ }
      { toFun := (⇑e : (a : α.X) → β.X), map_inf' := ⋯, map_top' := ⋯ } =
    𝟙 β

Tactic:
ext
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatInfCat
e : α.X ≃o β.X
a : β.X
⊢ Eq (α := β.X)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X) SemilatInfCat.X
            _ _ β β
            (CategoryStruct.comp (Y := α) { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := ⋯, map_top' := ⋯ }
              { toFun := (⇑e : (a : α.X) → β.X), map_inf' := ⋯, map_top' := ⋯ }) :
          (a : β.X) → β.X)
        a :
      β.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X) (CC := SemilatInfCat.X) (𝟙 β) :
          (a : β.X) → β.X)
        a :
      β.X)

Tactic:
e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.Semilat
Goal:
α β : SemilatInfCat
e : α.X ≃o β.X
a : β.X
⊢ Eq (α := β.X)
    ((@ConcreteCategory.hom _ instLargeCategory (fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X) SemilatInfCat.X
            _ _ β β
            (CategoryStruct.comp (Y := α) { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := ⋯, map_top' := ⋯ }
              { toFun := (⇑e : (a : α.X) → β.X), map_inf' := ⋯, map_top' := ⋯ }) :
          (a : β.X) → β.X)
        a :
      β.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : SemilatInfCat.{u}) ↦ InfTopHom x1.X x2.X) (CC := SemilatInfCat.X) (𝟙 β) :
          (a : β.X) → β.X)
        a :
      β.X)

Tactic:
exact e.apply_symm_apply _

Premises used: OrderIso.apply_symm_apply
-- Module: Mathlib.Order.Category.Semilat
Goal:
⊢ SemilatSupCat.dual ⋙
      forget₂ SemilatInfCat (FC := fun (x1 x2 : SemilatInfCat.{u_1}) ↦ InfTopHom x1.X x2.X) (CC := SemilatInfCat.X)
        PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier) =
    forget₂ SemilatSupCat (FC := fun (x1 x2 : SemilatSupCat.{u_1}) ↦ SupBotHom x1.X x2.X) (CC := SemilatSupCat.X)
        PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier) ⋙
      PartOrd.dual

Tactic:
rfl

Premises used: SemilatSupCat.dual, CategoryTheory.Functor.comp, OrderDual, rfl
-- Module: Mathlib.Order.Category.Semilat
Goal:
⊢ SemilatInfCat.dual ⋙
      forget₂ SemilatSupCat (FC := fun (x1 x2 : SemilatSupCat.{u_1}) ↦ SupBotHom x1.X x2.X) (CC := SemilatSupCat.X)
        PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier) =
    forget₂ SemilatInfCat (FC := fun (x1 x2 : SemilatInfCat.{u_1}) ↦ InfTopHom x1.X x2.X) (CC := SemilatInfCat.X)
        PartOrd (FD := fun (x1 x2 : PartOrd.{u_1}) ↦ (↑x1 : Type u_1) →o (↑x2 : Type u_1)) (CD := PartOrd.carrier) ⋙
      PartOrd.dual

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, SemilatInfCat.dual, OrderDual, rfl
-- Module: Mathlib.Order.Circular.ZMod
Goal:
a b c : ℤ
⊢ btw a b c ↔ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Circular.ZMod
Goal:
a b c : ℤ
⊢ sbtw a b c ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Circular.ZMod
Goal:
n : ℕ
a b c : Fin n
⊢ btw a b c ↔ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Circular.ZMod
Goal:
n : ℕ
a b c : Fin n
⊢ sbtw a b c ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a : α
⊢ btw a a a

Tactic:
btw_refl _

Premises used: CircularPreorder.btw_refl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
h : btw a b c
⊢ btw b c a

Tactic:
btw_cyclic_left h

Premises used: CircularPreorder.btw_cyclic_left
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
h : btw a b c
⊢ btw c a b

Tactic:
h.cyclic_left.cyclic_left

Premises used: Btw.btw.cyclic_left
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
⊢ btw a b c ↔ btw c a b

Tactic:
⟨btw_cyclic_right, btw_cyclic_left⟩

Premises used: btw_cyclic_right, CircularPreorder.btw_cyclic_left, Iff.intro
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
⊢ sbtw a b c ↔ btw a b c ∧ ¬btw c b a

Tactic:
CircularPreorder.sbtw_iff_btw_not_btw

Premises used: CircularPreorder.sbtw_iff_btw_not_btw
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
h : sbtw a b c
⊢ btw a b c

Tactic:
(sbtw_iff_btw_not_btw.1 h).1

Premises used: sbtw_iff_btw_not_btw, And.left, Iff.mp
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
h : sbtw a b c
⊢ ¬btw c b a

Tactic:
(sbtw_iff_btw_not_btw.1 h).2

Premises used: sbtw_iff_btw_not_btw, And.right, Iff.mp
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
h : btw a b c
⊢ ¬sbtw c b a

Tactic:
fun h' => h'.not_btw h

Premises used: Not, SBtw.sbtw.not_btw
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
habc : btw a b c
hcba : ¬btw c b a
⊢ sbtw a b c

Tactic:
sbtw_iff_btw_not_btw.2 ⟨habc, hcba⟩

Premises used: Iff.mpr, sbtw_iff_btw_not_btw, And.intro
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
h : sbtw a b c
⊢ sbtw b c a

Tactic:
h.btw.cyclic_left.sbtw_of_not_btw fun h' => h.not_btw h'.cyclic_left

Premises used: Btw.btw.cyclic_left, Btw.btw.sbtw_of_not_btw, SBtw.sbtw.btw, SBtw.sbtw.not_btw
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
h : sbtw a b c
⊢ sbtw c a b

Tactic:
h.cyclic_left.cyclic_left

Premises used: SBtw.sbtw.cyclic_left
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
⊢ sbtw a b c ↔ sbtw c a b

Tactic:
⟨sbtw_cyclic_right, sbtw_cyclic_left⟩

Premises used: sbtw_cyclic_left, sbtw_cyclic_right, Iff.intro
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c d : α
h : sbtw a b c
⊢ sbtw b d c → sbtw a d c

Tactic:
sbtw_trans_left h

Premises used: CircularPreorder.sbtw_trans_left
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c d : α
hbc : sbtw a b c
hcd : sbtw a c d
⊢ sbtw a b d

Tactic:
(hbc.cyclic_left.trans_left hcd.cyclic_left).cyclic_right

Premises used: SBtw.sbtw.cyclic_left, SBtw.sbtw.cyclic_right, SBtw.sbtw.trans_left
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b c : α
h : sbtw a b c
⊢ ¬sbtw c b a

Tactic:
h.btw.not_sbtw

Premises used: Btw.btw.not_sbtw, SBtw.sbtw.btw
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b : α
⊢ ¬sbtw a b a

Tactic:
fun h => h.not_btw h.btw

Premises used: Not, SBtw.sbtw.btw, SBtw.sbtw.not_btw
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b : α
⊢ ¬sbtw a a b

Tactic:
fun h => sbtw_irrefl_left_right h.cyclic_left

Premises used: SBtw.sbtw.cyclic_left, sbtw_irrefl_left_right, Not
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b : α
⊢ ¬sbtw a b b

Tactic:
fun h => sbtw_irrefl_left_right h.cyclic_right

Premises used: sbtw_irrefl_left_right, SBtw.sbtw.cyclic_right, Not
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a : α
⊢ ¬sbtw a a a

Tactic:
sbtw_irrefl_left_right

Premises used: sbtw_irrefl_left_right
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPartialOrder α
a b c : α
h : btw a b c
⊢ btw c b a → a = b ∨ b = c ∨ c = a

Tactic:
btw_antisymm h

Premises used: CircularPartialOrder.btw_antisymm
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
⊢ btw a b a

Tactic:
or_self_iff.1 (btw_total a b a)

Premises used: or_self_iff, CircularOrder.btw_total, Iff.mp
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
⊢ btw a b a

Tactic:
btw_refl_left_right _ _

Premises used: btw_refl_left_right
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
⊢ btw a a b

Tactic:
btw_rfl_left_right.cyclic_right

Premises used: Btw.btw.cyclic_right, btw_rfl_left_right
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
⊢ btw a a b

Tactic:
btw_refl_left _ _

Premises used: btw_refl_left
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
⊢ btw a b b

Tactic:
btw_rfl_left_right.cyclic_left

Premises used: Btw.btw.cyclic_left, btw_rfl_left_right
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
⊢ btw a b b

Tactic:
btw_refl_right _ _

Premises used: btw_refl_right
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b c : α
rw : btw a b c ∧ ¬btw c b a ↔ ¬btw c b a
⊢ sbtw a b c ↔ ¬btw c b a

Tactic:
rw [sbtw_iff_btw_not_btw]

Premises used: sbtw_iff_btw_not_btw
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b c : α
⊢ btw a b c ∧ ¬btw c b a ↔ ¬btw c b a

Tactic:
and_iff_right_of_imp (btw_total _ _ _).resolve_left

Premises used: Or.resolve_left, CircularOrder.btw_total, and_iff_right_of_imp
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b c : α
⊢ btw a b c ∧ ¬btw c b a ↔ ¬btw c b a

Tactic:
exact and_iff_right_of_imp (btw_total _ _ _).resolve_left

Premises used: Or.resolve_left, CircularOrder.btw_total, and_iff_right_of_imp
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b c : α
⊢ btw a b c ↔ ¬sbtw c b a

Tactic:
iff_not_comm.1 sbtw_iff_not_btw

Premises used: iff_not_comm, Iff.mp, sbtw_iff_not_btw
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b x : α
⊢ x ∈ cIcc a b ↔ btw a x b

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.cIcc
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularPreorder α
a b x : α
⊢ x ∈ cIoo a b ↔ sbtw a x b

Tactic:
Iff.rfl

Premises used: Set.Mem, Set.cIoo, Iff.rfl, setOf
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
⊢ a ∈ cIcc a b

Tactic:
btw_rfl_left

Premises used: Set.Mem, setOf, btw_rfl_left, Set.cIcc
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
⊢ b ∈ cIcc a b

Tactic:
btw_rfl_right

Premises used: Set.Mem, setOf, btw_rfl_right, Set.cIcc
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
h : ∀ (x : α), x ∈ (cIcc a b)ᶜ ↔ x ∈ cIoo b a
⊢ (cIcc a b)ᶜ = cIoo b a

Tactic:
ext
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b x : α
h : x ∈ (cIcc a b)ᶜ ↔ sbtw b x a
h₁ : x ∈ (cIcc a b)ᶜ ↔ ¬btw a x b
h₂ : Membership.mem (γ := Set α) {x : α | btw a x b}ᶜ x ↔ ¬btw a x b
h₃ : ¬Membership.mem (γ := Set α) {x : α | btw a x b} x ↔ ¬btw a x b
h₄ h₅ : ¬btw a x b ↔ ¬btw a x b
⊢ x ∈ (cIcc a b)ᶜ ↔ x ∈ cIoo b a

Tactic:
rw [Set.mem_cIoo, sbtw_iff_not_btw, cIcc, mem_compl_iff, mem_setOf]

Premises used: Set.mem_setOf, Set.mem_cIoo, Set.cIcc, sbtw_iff_not_btw, Set.mem_compl_iff
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
h : ∀ (x : α), x ∈ (cIoo a b)ᶜ ↔ x ∈ cIcc b a
⊢ (cIoo a b)ᶜ = cIcc b a

Tactic:
ext
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : CircularOrder α
a b x : α
h : x ∈ (cIoo a b)ᶜ ↔ btw b x a
h₁ : x ∈ (cIoo a b)ᶜ ↔ ¬sbtw a x b
h₂ : Membership.mem (γ := Set α) {x : α | sbtw a x b}ᶜ x ↔ ¬sbtw a x b
h₃ : ¬Membership.mem (γ := Set α) {x : α | sbtw a x b} x ↔ ¬sbtw a x b
h₄ h₅ : ¬sbtw a x b ↔ ¬sbtw a x b
⊢ x ∈ (cIoo a b)ᶜ ↔ x ∈ cIcc b a

Tactic:
rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_setOf]

Premises used: Set.mem_cIcc, Set.cIoo, Set.mem_setOf, btw_iff_not_sbtw, Set.mem_compl_iff
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
a b c : α
inst : LE α
⊢ btw a b c ↔ a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
a b c : α
inst : LT α
⊢ sbtw a b c ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c : α
simp_rw :
  (a ≤ b ∧ ¬b ≤ a) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ a ≤ b ∧ ¬b ≤ a ↔
    (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)
⊢ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b ↔
    (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)

Tactic:
simp_rw [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c : α
⊢ (a ≤ b ∧ ¬b ≤ a) ∧ b ≤ c ∧ ¬c ≤ b ∨ (b ≤ c ∧ ¬c ≤ b) ∧ c ≤ a ∧ ¬a ≤ c ∨ (c ≤ a ∧ ¬a ≤ c) ∧ a ≤ b ∧ ¬b ≤ a ↔
    (a ≤ b ∧ b ≤ c ∨ b ≤ c ∧ c ≤ a ∨ c ≤ a ∧ a ≤ b) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)

Tactic:
grind
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
.inl ?_

Premises used: Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
inl : a < d ∧ d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
refine .inl ?_
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
inl : a < d
inl₁ : d < c
⊢ a < d ∧ d < c

Tactic:
constructor
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
inl inl₁ inl₂ inl₃ inl₄ inl₅ inl₆ inl₇ inl₈ inl₉ inl₁₀ inl₁₁ : ¬a < d → False
⊢ a < d

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
inl inl₁ inl₂ inl₃ inl₄ inl₅ inl₆ inl₇ inl₈ inl₉ inl₁₀ inl₁₁ : ¬d < c → False
⊢ d < c

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
inl inl₁ : a < d ∧ d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
.inl ?_

Premises used: Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
inl : a < d ∧ d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
refine .inl ?_
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
inl : a < d
inl₁ : d < c
⊢ a < d ∧ d < c

Tactic:
constructor
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
inl inl₁ inl₂ inl₃ inl₄ inl₅ inl₆ inl₇ inl₈ inl₉ inl₁₀ inl₁₁ : ¬a < d → False
⊢ a < d

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
inl inl₁ inl₂ inl₃ inl₄ inl₅ inl₆ inl₇ inl₈ inl₉ inl₁₀ inl₁₁ : ¬d < c → False
⊢ d < c

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
inl inl₁ : a < d ∧ d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
.inl ?_

Premises used: Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
inl : a < d ∧ d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
refine .inl ?_
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
inl : a < d
inl₁ : d < c
⊢ a < d ∧ d < c

Tactic:
constructor
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
inl inl₁ inl₂ inl₃ inl₄ inl₅ inl₆ inl₇ inl₈ inl₉ inl₁₀ inl₁₁ : ¬a < d → False
⊢ a < d

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
inl inl₁ inl₂ inl₃ inl₄ inl₅ inl₆ inl₇ inl₈ inl₉ inl₁₀ inl₁₁ : ¬d < c → False
⊢ d < c

Tactic:
order