mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
⊢ (parallelFamily fun j ↦ F.map (line j)).obj zero = F.obj zero

pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
⊢ (parallelFamily fun j ↦ F.map (line j)).obj one = F.obj one

Tactic:
<;>

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
⊢ (parallelFamily fun j ↦ F.map (line j)).obj zero = F.obj zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
⊢ (parallelFamily fun j ↦ F.map (line j)).obj one = F.obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id j) ≫ t.π.app j ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map (Hom.id j)

pp: case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
a✝ : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝) ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map (line a✝)

Tactic:
<;>

Goal state after:
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id j) ≫ t.π.app j ≫ eqToHom ⋯ =
    (t.π.app j ≫ eqToHom ⋯) ≫ F.map (Hom.id j)

case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
a✝ : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝) ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ F.map (line a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one

Tactic:
<;>

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ F.map (Hom.id j) ≫ eqToHom ⋯ ≫ t.ι.app j =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id j)

pp: case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
a✝ : J
⊢ F.map (line a✝) ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝)

Tactic:
<;>

Goal state after:
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ F.map (Hom.id j) ≫ eqToHom ⋯ ≫ t.ι.app j =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id j)

case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
a✝ : J
⊢ F.map (line a✝) ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one

Tactic:
<;>

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
X✝ : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id X✝) ≫ t.π.app X✝ ≫ eqToHom ⋯ =
    (t.π.app X✝ ≫ eqToHom ⋯) ≫ (parallelFamily fun j ↦ F.map (line j)).map (Hom.id X✝)

pp: case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
a✝ : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝) ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelFamily fun j ↦ F.map (line j)).map (line a✝)

Tactic:
<;>

Goal state after:
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
X✝ : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id X✝) ≫ t.π.app X✝ ≫ eqToHom ⋯ =
    (t.π.app X✝ ≫ eqToHom ⋯) ≫ (parallelFamily fun j ↦ F.map (line j)).map (Hom.id X✝)

case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
a✝ : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝) ≫ t.π.app one ≫ eqToHom ⋯ =
    (t.π.app zero ≫ eqToHom ⋯) ≫ (parallelFamily fun j ↦ F.map (line j)).map (line a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j ↦ F.map (line j)).obj zero = F.obj zero

pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j ↦ F.map (line j)).obj one = F.obj one

Tactic:
<;>

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j ↦ F.map (line j)).obj zero = F.obj zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j ↦ F.map (line j)).obj one = F.obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
X✝ : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).map (Hom.id X✝) ≫ eqToHom ⋯ ≫ t.ι.app X✝ =
    (eqToHom ⋯ ≫ t.ι.app X✝) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id X✝)

pp: case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
a✝ : J
⊢ (parallelFamily fun j ↦ F.map (line j)).map (line a✝) ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝)

Tactic:
<;>

Goal state after:
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
X✝ : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).map (Hom.id X✝) ≫ eqToHom ⋯ ≫ t.ι.app X✝ =
    (eqToHom ⋯ ≫ t.ι.app X✝) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (Hom.id X✝)

case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
a✝ : J
⊢ (parallelFamily fun j ↦ F.map (line j)).map (line a✝) ≫ eqToHom ⋯ ≫ t.ι.app one =
    (eqToHom ⋯ ≫ t.ι.app zero) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map (line a✝)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case e'_2.mpr.left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ G = WalkingPair.rec G H WalkingPair.left ∨ H = WalkingPair.rec G H WalkingPair.left

pp: case e'_2.mpr.right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ G = WalkingPair.rec G H WalkingPair.right ∨ H = WalkingPair.rec G H WalkingPair.right

Tactic:
<;>

Goal state after:
case e'_2.mpr.left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ G = WalkingPair.rec G H WalkingPair.left ∨ H = WalkingPair.rec G H WalkingPair.left

case e'_2.mpr.right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ G = WalkingPair.rec G H WalkingPair.right ∨ H = WalkingPair.rec G H WalkingPair.right
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case e'_2.mpr.left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ G = WalkingPair.rec G H WalkingPair.left ∨ H = WalkingPair.rec G H WalkingPair.left

pp: case e'_2.mpr.right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ G = WalkingPair.rec G H WalkingPair.right ∨ H = WalkingPair.rec G H WalkingPair.right

Tactic:
<;>

Goal state after:
case e'_2.mpr.left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ G = WalkingPair.rec G H WalkingPair.left ∨ H = WalkingPair.rec G H WalkingPair.left

case e'_2.mpr.right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ G = WalkingPair.rec G H WalkingPair.right ∨ H = WalkingPair.rec G H WalkingPair.right
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case pos
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
x : c.pt
h✝ : ∃ y, (ConcreteCategory.hom c.inl) y = x
⊢ (ConcreteCategory.hom m) x =
    (ConcreteCategory.hom m)
      ((ConcreteCategory.hom c.inl) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, ⋯⟩))

pp: case neg
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
x : c.pt
h✝ : ¬∃ y, (ConcreteCategory.hom c.inl) y = x
⊢ (ConcreteCategory.hom m) x =
    (ConcreteCategory.hom m)
      ((ConcreteCategory.hom c.inr) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩))

Tactic:
<;>

Goal state after:
case pos
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
x : c.pt
h✝ : ∃ y, (ConcreteCategory.hom c.inl) y = x
⊢ (ConcreteCategory.hom m) x =
    (ConcreteCategory.hom m)
      ((ConcreteCategory.hom c.inl) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, ⋯⟩))

case neg
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
this :
  ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)
T : Type u
m : c.pt ⟶ T
x : c.pt
h✝ : ¬∃ y, (ConcreteCategory.hom c.inl) y = x
⊢ (ConcreteCategory.hom m) x =
    (ConcreteCategory.hom m)
      ((ConcreteCategory.hom c.inr) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩))
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case inl
n : ℤ
h : |n| = n
⊢ |n|.negOnePow = n.negOnePow

pp: case inr
n : ℤ
h : |n| = -n
⊢ |n|.negOnePow = n.negOnePow

Tactic:
<;>

Goal state after:
case inl
n : ℤ
h : |n| = n
⊢ |n|.negOnePow = n.negOnePow

case inr
n : ℤ
h : |n| = -n
⊢ |n|.negOnePow = n.negOnePow
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Ring R
k : ℕ
⊢ ↑↑(↑(2 * k)).negOnePow = (-1) ^ (2 * k)

pp: case inr
R : Type u_1
inst✝ : Ring R
k : ℕ
⊢ ↑↑(↑(2 * k + 1)).negOnePow = (-1) ^ (2 * k + 1)

Tactic:
<;>

Goal state after:
case inl
R : Type u_1
inst✝ : Ring R
k : ℕ
⊢ ↑↑(↑(2 * k)).negOnePow = (-1) ^ (2 * k)

case inr
R : Type u_1
inst✝ : Ring R
k : ℕ
⊢ ↑↑(↑(2 * k + 1)).negOnePow = (-1) ^ (2 * k + 1)
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inl
α : 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

pp: case inl.inr.inl
α : 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

pp: case inl.inr.inr
α : 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

pp: case inr.inl.inl
α : 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

pp: case inr.inl.inr.inl
α : 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

pp: case inr.inl.inr.inr
α : 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

pp: case inr.inr.inl
α : 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

pp: case inr.inr.inr.inl
α : 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

pp: case inr.inr.inr.inr
α : 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:
<;>

Goal state after:
case inl.inl
α : 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

case inl.inr.inl
α : 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

case inl.inr.inr
α : 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

case inr.inl.inl
α : 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

case inr.inl.inr.inl
α : 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

case inr.inl.inr.inr
α : 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

case inr.inr.inl
α : 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

case inr.inr.inr.inl
α : 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

case inr.inr.inr.inr
α : 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
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d

pp: case inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ d < c

Tactic:
<;>

Goal state after:
case inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ a < d

case inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hbd : b < d
hdc : d < c
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d

pp: case inl.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ d < c

Tactic:
<;>

Goal state after:
case inl.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ a < d

case inl.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hdc : d < c
hcb : c < b
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d

pp: case inl.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ d < c

Tactic:
<;>

Goal state after:
case inl.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ a < d

case inl.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hab : a < b
hbc : b < c
hcb : c < b
hbd : b < d
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ a < d

pp: case inr.inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c

Tactic:
<;>

Goal state after:
case inr.inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ a < d

case inr.inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c

pp: case inr.inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ c < a

Tactic:
<;>

Goal state after:
case inr.inl.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ d < c

case inr.inl.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hbd : b < d
hdc : d < c
⊢ c < a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ a < d

pp: case inr.inl.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ d < c

Tactic:
<;>

Goal state after:
case inr.inl.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ a < d

case inr.inl.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hdc : d < c
hcb : c < b
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inl.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ a < d

pp: case inr.inl.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ d < c

Tactic:
<;>

Goal state after:
case inr.inl.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ a < d

case inr.inl.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hbc : b < c
hca : c < a
hcb : c < b
hbd : b < d
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ a < d

pp: case inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ d < c

Tactic:
<;>

Goal state after:
case inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ a < d

case inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hbd : b < d
hdc : d < c
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ a < d

pp: case inr.inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c

Tactic:
<;>

Goal state after:
case inr.inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ a < d

case inr.inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c

pp: case inr.inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ c < a

Tactic:
<;>

Goal state after:
case inr.inr.inr.inl.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ d < c

case inr.inr.inr.inl.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hdc : d < c
hcb : c < b
⊢ c < a
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d

pp: case inr.inr.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ d < c

Tactic:
<;>

Goal state after:
case inr.inr.inr.inr.left
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d

case inr.inr.inr.inr.right
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ d < c