awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ : 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 : α
hbc : b < c
hca : c < a
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 : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
.inr <| .inl ?_

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

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

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

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

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hbc : b < c
hca : c < a
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 : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
inr : 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 : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
inr : a < d
inr₁ : d < c
⊢ a < d ∧ d < c

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

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

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
inr inr₁ : 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 : α
hbc : b < c
hca : c < a
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 : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
inr : 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 : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
inr : a < d
inr₁ : d < c
⊢ a < d ∧ d < c

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

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

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
inr inr₁ : 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 : α
hca : c < a
hab : a < b
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 : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
inr : 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 : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
inr : a < d
inr₁ : d < c
⊢ a < d ∧ d < c

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

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

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
inr inr₁ : 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 : α
hca : c < a
hab : a < b
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 : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
.inr <| .inl ?_

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

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

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

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

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hca : c < a
hab : a < b
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 : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
.inr <| .inl ?_

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

Tactic:
.inr <| .inr ?_

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

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

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

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

Tactic:
order
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

Tactic:
Or.inl (hab.antisymm hba)

Premises used: LE.le.antisymm, Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

Tactic:
exact Or.inl (hab.antisymm hba)

Premises used: LE.le.antisymm, Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

Tactic:
Or.inl (hab.antisymm hba)

Premises used: LE.le.antisymm, Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

Tactic:
exact Or.inl (hab.antisymm hba)

Premises used: LE.le.antisymm, Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

Tactic:
Or.inr (Or.inl <| hbc.antisymm hcb)

Premises used: LE.le.antisymm, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

Tactic:
exact Or.inr (Or.inl <| hbc.antisymm hcb)

Premises used: LE.le.antisymm, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

Tactic:
Or.inr (Or.inl <| hbc.antisymm hcb)

Premises used: LE.le.antisymm, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

Tactic:
exact Or.inr (Or.inl <| hbc.antisymm hcb)

Premises used: LE.le.antisymm, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

Tactic:
Or.inr (Or.inr <| hca.antisymm hac)

Premises used: LE.le.antisymm, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

Tactic:
exact Or.inr (Or.inr <| hca.antisymm hac)

Premises used: LE.le.antisymm, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

Tactic:
Or.inr (Or.inl <| hbc.antisymm hcb)

Premises used: LE.le.antisymm, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

Tactic:
exact Or.inr (Or.inl <| hbc.antisymm hcb)

Premises used: LE.le.antisymm, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

Tactic:
Or.inl (hab.antisymm hba)

Premises used: LE.le.antisymm, Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

Tactic:
exact Or.inl (hab.antisymm hba)

Premises used: LE.le.antisymm, Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

Tactic:
Or.inl (hab.antisymm hba)

Premises used: LE.le.antisymm, Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

Tactic:
exact Or.inl (hab.antisymm hba)

Premises used: LE.le.antisymm, Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

Tactic:
Or.inr (Or.inr <| hca.antisymm hac)

Premises used: LE.le.antisymm, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

Tactic:
exact Or.inr (Or.inr <| hca.antisymm hac)

Premises used: LE.le.antisymm, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inl : ∀ (hab : a ≤ b), btw a b c ∨ btw c b a
inr : ∀ (hba : b ≤ a), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a

Tactic:
rcases le_total a b with hab | hba

Premises used: le_total
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
inl : ∀ (hbc : b ≤ c), btw a b c ∨ btw c b a
inl₁ : ∀ (hcb : c ≤ b), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a

Tactic:
rcases le_total b c with hbc | hcb

Premises used: le_total
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
inr : ∀ (hbc : b ≤ c), btw a b c ∨ btw c b a
inr₁ : ∀ (hcb : c ≤ b), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a

Tactic:
rcases le_total b c with hbc | hcb

Premises used: le_total
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
inl : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
inl₁ : ∀ (hac : a ≤ c), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a

Tactic:
rcases le_total c a with hca | hac

Premises used: le_total
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
inl : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
inl₁ : ∀ (hac : a ≤ c), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a

Tactic:
rcases le_total c a with hca | hac

Premises used: le_total
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
inr : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
inr₁ : ∀ (hac : a ≤ c), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a

Tactic:
rcases le_total c a with hca | hac

Premises used: le_total
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
inr : ∀ (hca : c ≤ a), btw a b c ∨ btw c b a
inr₁ : ∀ (hac : a ≤ c), btw a b c ∨ btw c b a
⊢ btw a b c ∨ btw c b a

Tactic:
rcases le_total c a with hca | hac

Premises used: le_total
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
Or.inl (Or.inl ⟨hab, hbc⟩)

Premises used: And.intro, Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inl (Or.inl ⟨hab, hbc⟩)

Premises used: Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
Or.inl (Or.inl ⟨hab, hbc⟩)

Premises used: And.intro, Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inl (Or.inl ⟨hab, hbc⟩)

Premises used: Or.inl
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
Or.inl (Or.inr <| Or.inr ⟨hca, hab⟩)

Premises used: And.intro, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inl (Or.inr <| Or.inr ⟨hca, hab⟩)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
Or.inr (Or.inr <| Or.inr ⟨hac, hcb⟩)

Premises used: And.intro, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inr (Or.inr <| Or.inr ⟨hac, hcb⟩)

Premises used: Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
Or.inl (Or.inr <| Or.inl ⟨hbc, hca⟩)

Premises used: And.intro, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inl (Or.inr <| Or.inl ⟨hbc, hca⟩)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)

Premises used: And.intro, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hbc : b ≤ c
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
Or.inr (Or.inl ⟨hcb, hba⟩)

Premises used: And.intro, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inr (Or.inl ⟨hcb, hba⟩)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)

Premises used: And.intro, Or.inl, Or.inr
-- Module: Mathlib.Order.Circular
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
hba : b ≤ a
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inr (Or.inr <| Or.inl ⟨hba, hac⟩)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : Preorder α
toOrderHom : α →o α
le_closure' : ∀ (x : α), x ≤ toOrderHom.toFun x
idempotent' : ∀ (x : α), toOrderHom.toFun (toOrderHom.toFun x) = toOrderHom.toFun x
IsClosed : (x : α) → Prop
isClosed_iff : ∀ {x : α}, IsClosed x ↔ toOrderHom.toFun x = x
IsClosed_1 : (x : α) → Prop
le_closure'_1 :
  ∀ (x : α),
    x ≤
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
        x
idempotent'_1 :
  ∀ (x : α),
    { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
        ({ toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
          x) =
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
        x
isClosed_iff_1 :
  ∀ {x : α},
    IsClosed_1 x ↔
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
          x =
        x
h :
  Eq.{u_1 + 1} (α := (a : α) → α)
    ((fun (c : ClosureOperator α) ↦ ((⇑c.toOrderHom : (a : α) → α) : (a : α) → α))
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
        isClosed_iff := @isClosed_iff })
    ((fun (c : ClosureOperator α) ↦ ((⇑c.toOrderHom : (a : α) → α) : (a : α) → α))
      {
        toOrderHom :=
          { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff }.toOrderHom,
        le_closure' := le_closure'_1, idempotent' := idempotent'_1, IsClosed := IsClosed_1,
        isClosed_iff := @isClosed_iff_1 })
e_IsClosed : ∀ (x : α), IsClosed x ↔ IsClosed_1 x
⊢ { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
      isClosed_iff := @isClosed_iff : ClosureOperator α } =
    {
      toOrderHom :=
        { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff }.toOrderHom,
      le_closure' := le_closure'_1, idempotent' := idempotent'_1, IsClosed := IsClosed_1,
      isClosed_iff := @isClosed_iff_1 }

Tactic:
congr with x
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : Preorder α
toOrderHom : α →o α
le_closure' : ∀ (x : α), x ≤ toOrderHom.toFun x
idempotent' : ∀ (x : α), toOrderHom.toFun (toOrderHom.toFun x) = toOrderHom.toFun x
IsClosed : (x : α) → Prop
isClosed_iff : ∀ {x : α}, IsClosed x ↔ toOrderHom.toFun x = x
IsClosed_1 : (x : α) → Prop
le_closure'_1 :
  ∀ (x : α),
    x ≤
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
        x
idempotent'_1 :
  ∀ (x : α),
    { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
        ({ toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
          x) =
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
            isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
        x
isClosed_iff_1 :
  ∀ {x : α},
    IsClosed_1 x ↔
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff : ClosureOperator α }.toFun
          x =
        x
h :
  Eq.{u_1 + 1} (α := (a : α) → α)
    ((fun (c : ClosureOperator α) ↦ ((⇑c.toOrderHom : (a : α) → α) : (a : α) → α))
      { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
        isClosed_iff := @isClosed_iff })
    ((fun (c : ClosureOperator α) ↦ ((⇑c.toOrderHom : (a : α) → α) : (a : α) → α))
      {
        toOrderHom :=
          { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
              isClosed_iff := @isClosed_iff }.toOrderHom,
        le_closure' := le_closure'_1, idempotent' := idempotent'_1, IsClosed := IsClosed_1,
        isClosed_iff := @isClosed_iff_1 })
x : α
⊢ IsClosed x ↔ IsClosed_1 x

Tactic:
simp_all
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_4
inst : Preorder α
c : ClosureOperator α
⊢ c.conjBy (OrderIso.refl α) = c

Tactic:
rfl

Premises used: ClosureOperator.conjBy, rfl
-- Module: Mathlib.Order.Closure
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
e₁ : α ≃o β
e₂ : β ≃o γ
c : ClosureOperator α
⊢ c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂

Tactic:
rfl

Premises used: OrderHomClass.toOrderHom, RelIso.trans, ClosureOperator.conjBy, rfl, OrderIso.trans