awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (goal)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
j : J
x y : (↑(F.1 j) : Type u)
k : J
x' y' : (↑(F.obj k) : Type u)
hx :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) x' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) x : c.pt)
hy :
  Eq (α := c.pt) ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app k) : (a : ToType (F.obj k)) → c.pt) y' : c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) : (a : ToType (F.obj j)) → c.pt) y : c.pt)
h : x' ≤ y'
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₁))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₁) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₁) : Type u))
        x' :
      (↑(F.obj l₁) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₁) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₁) : Type u))
        x :
      (↑(F.obj l₁) : Type u))
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ :
  Eq (α := ToType (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier) (F.obj l₂))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map a₂) :
          (a : (↑(F.obj k) : Type u)) → (↑(F.obj l₂) : Type u))
        y' :
      (↑(F.obj l₂) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
            (F.map b₂) :
          (a : (↑(F.obj j) : Type u)) → (↑(F.obj l₂) : Type u))
        y :
      (↑(F.obj l₂) : Type u))
m : J
d : l₁ ⟶ m
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
⊢ x ≤ y
have rw : ∀
  (h :
    LE.le (α := (↑(F.obj m) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
              (F.map (a₁ ≫ d)) :
            (a : (↑(F.obj k) : Type u)) → (↑(F.obj m) : Type u))
          x' :
        (↑(F.obj m) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)
              (F.map (a₁ ≫ d)) :
            (a : (↑(F.obj k) : Type u)) → (↑(F.obj m) : Type u))
          y' :
        (↑(F.obj m) : Type u)))
  (d' : l₂ ⟶ m) (h₁ : a₁ ≫ d = a₂ ≫ d') (h₂ : b₁ ≫ d = b₂ ≫ d'), x ≤ y
Tactic: rw [← (F.map (a₁ ≫ d)).le_iff_le] at h
Cleared hypotheses: h, d', h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (goal)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
j : J
⊢ (cocone hc).ι.app j ≫ ofHom (CoconePt.desc hc s) = s.ι.app j
have hf : ∀ (x : (↑(F.obj j) : Type u)),
  Eq (α := (↑s.pt : Type u))
    ((Hom.hom ((cocone hc).ι.app j ≫ ofHom (CoconePt.desc hc s)) : (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u)) x :
      (↑s.pt : Type u))
    ((Hom.hom (s.ι.app j) : (a : (↑(F.obj j) : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (goal)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
m : (cocone hc).pt ⟶ s.pt
hm : ∀ (j : J), (cocone hc).ι.app j ≫ m = s.ι.app j
⊢ m = ofHom (CoconePt.desc hc s)
have hf : ∀ (x : (↑(cocone hc).pt : Type u)),
  Eq (α := (↑s.pt : Type u)) ((Hom.hom m : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
    ((Hom.hom (ofHom (CoconePt.desc hc s)) : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Category.PartOrdEmb (goal)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ PartOrdEmb
c :
  Cocone (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier))
hc : IsColimit c
s : Cocone F
m : (cocone hc).pt ⟶ s.pt
hm : ∀ (j : J), (cocone hc).ι.app j ≫ m = s.ι.app j
x : (↑(cocone hc).pt : Type u)
⊢ Eq (α := (↑s.pt : Type u)) ((Hom.hom m : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
    ((Hom.hom (ofHom (CoconePt.desc hc s)) : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u)) x : (↑s.pt : Type u))
have hf : ∀ (j : J)
  (x :
    (F ⋙ forget PartOrdEmb (FC := fun (x1 x2 : PartOrdEmb.{u}) ↦ (↑x1 : Type u) ↪o (↑x2 : Type u)) (CC := carrier)).obj
      j),
  Eq (α := (↑s.pt : Type u))
    ((Hom.hom m : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
      (↑s.pt : Type u))
    ((Hom.hom (ofHom (CoconePt.desc hc s)) : (a : (↑(cocone hc).pt : Type u)) → (↑s.pt : Type u))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget PartOrdEmb).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) j)) :
      (↑s.pt : Type u))
Tactic: obtain ⟨j, x, rfl⟩ := Types.jointly_surjective_of_isColimit hc x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Category.Preord (goal)
Goal:
X Y : Preord
a₁ a₂ : X ⟶ Y
h : preordToCat.map a₁ = preordToCat.map a₂
⊢ a₁ = a₂
have hf : ∀ (x : (↑X : Type u)),
  Eq (α := (↑Y : Type u)) ((Preord.Hom.hom a₁ : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
    ((Preord.Hom.hom a₂ : (a : (↑X : Type u)) → (↑Y : Type u)) x : (↑Y : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Category.Semilat (goal)
Goal:
α β : SemilatSupCat
e : α.X ≃o β.X
⊢ CategoryStruct.comp (Y := β) { toFun := (⇑e : (a : α.X) → β.X), map_sup' := ⋯, map_bot' := ⋯ }
      { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := ⋯, map_bot' := ⋯ } =
    𝟙 α
have 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 : (a : α.X) → β.X), map_sup' := sorry, map_bot' := sorry }
              { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := sorry, map_bot' := sorry }) :
          (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: ext
-- Lean 4 proof step from Mathlib.Order.Category.Semilat (goal)
Goal:
α β : SemilatSupCat
e : α.X ≃o β.X
⊢ CategoryStruct.comp (Y := α) { toFun := (⇑e.symm : (a : β.X) → α.X), map_sup' := ⋯, map_bot' := ⋯ }
      { toFun := (⇑e : (a : α.X) → β.X), map_sup' := ⋯, map_bot' := ⋯ } =
    𝟙 β
have 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' := sorry, map_bot' := sorry }
              { toFun := (⇑e : (a : α.X) → β.X), map_sup' := sorry, map_bot' := sorry }) :
          (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: ext
-- Lean 4 proof step from Mathlib.Order.Category.Semilat (goal)
Goal:
α β : SemilatInfCat
e : α.X ≃o β.X
⊢ CategoryStruct.comp (Y := β) { toFun := (⇑e : (a : α.X) → β.X), map_inf' := ⋯, map_top' := ⋯ }
      { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := ⋯, map_top' := ⋯ } =
    𝟙 α
have 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' := sorry, map_top' := sorry }
              { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := sorry, map_top' := sorry }) :
          (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: ext
-- Lean 4 proof step from Mathlib.Order.Category.Semilat (goal)
Goal:
α β : SemilatInfCat
e : α.X ≃o β.X
⊢ CategoryStruct.comp (Y := α) { toFun := (⇑e.symm : (a : β.X) → α.X), map_inf' := ⋯, map_top' := ⋯ }
      { toFun := (⇑e : (a : α.X) → β.X), map_inf' := ⋯, map_top' := ⋯ } =
    𝟙 β
have 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' := sorry, map_top' := sorry }
              { toFun := (⇑e : (a : α.X) → β.X), map_inf' := sorry, map_top' := sorry }) :
          (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: ext
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : CircularOrder α
a b c : α
⊢ sbtw a b c ↔ ¬btw c b a
have rw : btw a b c ∧ ¬btw c b a ↔ ¬btw c b a
Tactic: rw [sbtw_iff_btw_not_btw]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
⊢ (cIcc a b)ᶜ = cIoo b a
have h : ∀ (x : α), x ∈ (cIcc a b)ᶜ ↔ x ∈ cIoo b a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : CircularOrder α
a b x : α
⊢ x ∈ (cIcc a b)ᶜ ↔ x ∈ cIoo b a
have h : x ∈ (cIcc a b)ᶜ ↔ sbtw b x a
Tactic: rw [Set.mem_cIoo, sbtw_iff_not_btw, cIcc, mem_compl_iff, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : CircularOrder α
a b x : α
h : x ∈ (cIcc a b)ᶜ ↔ sbtw b x a
⊢ x ∈ (cIcc a b)ᶜ ↔ x ∈ cIoo b a
have h₁ : x ∈ (cIcc a b)ᶜ ↔ ¬btw a x b
Tactic: rw [Set.mem_cIoo, sbtw_iff_not_btw, cIcc, mem_compl_iff, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
⊢ x ∈ (cIcc a b)ᶜ ↔ x ∈ cIoo b a
have h₂ : Membership.mem (γ := Set α) {x : α | btw a x b}ᶜ x ↔ ¬btw a x b
Tactic: rw [Set.mem_cIoo, sbtw_iff_not_btw, cIcc, mem_compl_iff, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
⊢ x ∈ (cIcc a b)ᶜ ↔ x ∈ cIoo b a
have h₃ : ¬Membership.mem (γ := Set α) {x : α | btw a x b} x ↔ ¬btw a x b
Tactic: rw [Set.mem_cIoo, sbtw_iff_not_btw, cIcc, mem_compl_iff, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
⊢ x ∈ (cIcc a b)ᶜ ↔ x ∈ cIoo b a
have h₄ : ¬btw a x b ↔ ¬btw a x b
Tactic: rw [Set.mem_cIoo, sbtw_iff_not_btw, cIcc, mem_compl_iff, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : CircularOrder α
a b : α
⊢ (cIoo a b)ᶜ = cIcc b a
have h : ∀ (x : α), x ∈ (cIoo a b)ᶜ ↔ x ∈ cIcc b a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : CircularOrder α
a b x : α
⊢ x ∈ (cIoo a b)ᶜ ↔ x ∈ cIcc b a
have h : x ∈ (cIoo a b)ᶜ ↔ btw b x a
Tactic: rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : CircularOrder α
a b x : α
h : x ∈ (cIoo a b)ᶜ ↔ btw b x a
⊢ x ∈ (cIoo a b)ᶜ ↔ x ∈ cIcc b a
have h₁ : x ∈ (cIoo a b)ᶜ ↔ ¬sbtw a x b
Tactic: rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
⊢ x ∈ (cIoo a b)ᶜ ↔ x ∈ cIcc b a
have h₂ : Membership.mem (γ := Set α) {x : α | sbtw a x b}ᶜ x ↔ ¬sbtw a x b
Tactic: rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
⊢ x ∈ (cIoo a b)ᶜ ↔ x ∈ cIcc b a
have h₃ : ¬Membership.mem (γ := Set α) {x : α | sbtw a x b} x ↔ ¬sbtw a x b
Tactic: rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
⊢ x ∈ (cIoo a b)ᶜ ↔ x ∈ cIcc b a
have h₄ : ¬sbtw a x b ↔ ¬sbtw a x b
Tactic: rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_setOf]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c : α
⊢ 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)
have 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)
Tactic: simp_rw [lt_iff_le_not_ge]
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inl : a < d ∧ d < c
Tactic: refine .inl ?_
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inl : a < d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d
have inl : ¬a < d → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ d < c
have inl : ¬d < c → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inl : a < d ∧ d < c
Tactic: first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inl : a < d ∧ d < c
Tactic: refine .inl ?_
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inl : a < d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d
have inl : ¬a < d → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ d < c
have inl : ¬d < c → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inl : a < d ∧ d < c
Tactic: first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inl : a < d ∧ d < c
Tactic: refine .inl ?_
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inl : a < d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
⊢ a < d ∧ d < c
have inl₁ : d < c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d
have inl : ¬a < d → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ d < c
have inl : ¬d < c → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inl : a < d ∧ d < c
Tactic: first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : d < c ∧ c < a
Tactic: refine .inr <| .inl ?_
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c
have inr : ¬d < c → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ c < a
have inr : ¬c < a → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : a < d ∧ d < c
Tactic: refine .inl ?_
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : a < d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ a < d
have inr : ¬a < d → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ d < c
have inr : ¬d < c → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : a < d ∧ d < c
Tactic: first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : a < d ∧ d < c
Tactic: refine .inl ?_
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : a < d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
⊢ a < d ∧ d < c
have inr₁ : d < c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ a < d
have inr : ¬a < d → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ d < c
have inr : ¬d < c → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : a < d ∧ d < c
Tactic: first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : a < d ∧ d < c
Tactic: refine .inl ?_
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : a < d
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ a < d
have inr : ¬a < d → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ d < c
have inr : ¬d < c → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : a < d ∧ d < c
Tactic: first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : d < c ∧ c < a
Tactic: refine .inr <| .inl ?_
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c
have inr : ¬d < c → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
Goal:
α : Type u_1
inst : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ c < a
have inr : ¬c < a → False
Tactic: order
-- Lean 4 proof step from Mathlib.Order.Circular (goal)
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
have inr : c < a ∧ a < d
Tactic: refine .inr <| .inr ?_