Theorem: r5_strict_order (meetings/ex6.lean)

State before:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ StrictOrder (R5 S T)
Tactic:
intro p q j
State after:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ (R5 S T p q → R5 S T q j → R5 S T p j) ∧ Trichotomy (R5 S T p q) (R5 S T q p) (p = q)

State before:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ (R5 S T p q → R5 S T q j → R5 S T p j) ∧ Trichotomy (R5 S T p q) (R5 S T q p) (p = q)
Tactic:
simp_rw [R5]
State after:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2 → S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2 → S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2) ∧
    Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)

State before:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2 → S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2 → S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2) ∧
    Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)
Tactic:
constructor
State after:
case left
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2 → S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2 → S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2

case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)

State before:
case left
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2 → S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2 → S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2
Tactic:
intros h1 h2
State after:
case left
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
h1 : S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2
h2 : S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2

State before:
case left
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
h1 : S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2
h2 : S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2
Tactic:
rcases h1 with (hSp | ⟨heqp, hTp⟩)
State after:
case left.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
h2 : S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2
hSp : S p.1 q.1
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2

case left.inr.intro
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
h2 : S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2
heqp : p.1 = q.1
hTp : T p.2 q.2
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2

State before:
case left.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
h2 : S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2
hSp : S p.1 q.1
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2
Tactic:
rcases h2 with (hSq | ⟨heqq, hTq⟩)
State after:
case left.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hSp : S p.1 q.1
hSq : S q.1 j.1
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2

case left.inl.inr.intro
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hSp : S p.1 q.1
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2

State before:
case left.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hSp : S p.1 q.1
hSq : S q.1 j.1
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2
Tactic:
left
State after:
case left.inl.inl.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hSp : S p.1 q.1
hSq : S q.1 j.1
⊢ S p.1 j.1

State before:
case left.inl.inl.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hSp : S p.1 q.1
hSq : S q.1 j.1
⊢ S p.1 j.1
Tactic:
exact hS.trans hSp hSq
State after:
no goals

State before:
case left.inl.inr.intro
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hSp : S p.1 q.1
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2
Tactic:
rw [heqq] at hSp
State after:
case left.inl.inr.intro
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hSp : S p.1 j.1
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2

State before:
case left.inl.inr.intro
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hSp : S p.1 j.1
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2
Tactic:
left
State after:
case left.inl.inr.intro.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hSp : S p.1 j.1
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ S p.1 j.1

State before:
case left.inl.inr.intro.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hSp : S p.1 j.1
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ S p.1 j.1
Tactic:
exact hSp
State after:
no goals

State before:
case left.inr.intro
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
h2 : S q.1 j.1 ∨ q.1 = j.1 ∧ T q.2 j.2
heqp : p.1 = q.1
hTp : T p.2 q.2
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2
Tactic:
rcases h2 with (hSq | ⟨heqq, hTq⟩)
State after:
case left.inr.intro.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
hSq : S q.1 j.1
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2

case left.inr.intro.inr.intro
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2

State before:
case left.inr.intro.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
hSq : S q.1 j.1
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2
Tactic:
rw [heqp]
State after:
case left.inr.intro.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
hSq : S q.1 j.1
⊢ S q.1 j.1 ∨ q.1 = j.1 ∧ T p.2 j.2

State before:
case left.inr.intro.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
hSq : S q.1 j.1
⊢ S q.1 j.1 ∨ q.1 = j.1 ∧ T p.2 j.2
Tactic:
left
State after:
case left.inr.intro.inl.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
hSq : S q.1 j.1
⊢ S q.1 j.1

State before:
case left.inr.intro.inl.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
hSq : S q.1 j.1
⊢ S q.1 j.1
Tactic:
exact hSq
State after:
no goals

State before:
case left.inr.intro.inr.intro
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ S p.1 j.1 ∨ p.1 = j.1 ∧ T p.2 j.2
Tactic:
right
State after:
case left.inr.intro.inr.intro.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ p.1 = j.1 ∧ T p.2 j.2

State before:
case left.inr.intro.inr.intro.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ p.1 = j.1 ∧ T p.2 j.2
Tactic:
constructor
State after:
case left.inr.intro.inr.intro.h.left
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ p.1 = j.1

case left.inr.intro.inr.intro.h.right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ T p.2 j.2

State before:
case left.inr.intro.inr.intro.h.left
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ p.1 = j.1
Tactic:
rw [←heqp] at heqq
State after:
case left.inr.intro.inr.intro.h.left
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
heqq : p.1 = j.1
hTq : T q.2 j.2
⊢ p.1 = j.1

State before:
case left.inr.intro.inr.intro.h.left
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
heqq : p.1 = j.1
hTq : T q.2 j.2
⊢ p.1 = j.1
Tactic:
exact heqq
State after:
no goals

State before:
case left.inr.intro.inr.intro.h.right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
heqp : p.1 = q.1
hTp : T p.2 q.2
heqq : q.1 = j.1
hTq : T q.2 j.2
⊢ T p.2 j.2
Tactic:
exact hT.trans hTp hTq
State after:
no goals

State before:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
⊢ Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)
Tactic:
have hStrich := hS.trich p.1 q.1
State after:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hStrich : Trichotomy (S p.1 q.1) (S q.1 p.1) (p.1 = q.1)
⊢ Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)

State before:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hStrich : Trichotomy (S p.1 q.1) (S q.1 p.1) (p.1 = q.1)
⊢ Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)
Tactic:
have hTtrich := hT.trich p.2 q.2
State after:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hStrich : Trichotomy (S p.1 q.1) (S q.1 p.1) (p.1 = q.1)
hTtrich : Trichotomy (T p.2 q.2) (T q.2 p.2) (p.2 = q.2)
⊢ Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)

State before:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hStrich : Trichotomy (S p.1 q.1) (S q.1 p.1) (p.1 = q.1)
hTtrich : Trichotomy (T p.2 q.2) (T q.2 p.2) (p.2 = q.2)
⊢ Trichotomy (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) (p = q)
Tactic:
rw [Trichotomy] at *
State after:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hStrich :
  ¬S p.1 q.1 ∧ ¬S q.1 p.1 ∧ p.1 = q.1 ∨ ¬S p.1 q.1 ∧ S q.1 p.1 ∧ ¬p.1 = q.1 ∨ S p.1 q.1 ∧ ¬S q.1 p.1 ∧ ¬p.1 = q.1
hTtrich :
  ¬T p.2 q.2 ∧ ¬T q.2 p.2 ∧ p.2 = q.2 ∨ ¬T p.2 q.2 ∧ T q.2 p.2 ∧ ¬p.2 = q.2 ∨ T p.2 q.2 ∧ ¬T q.2 p.2 ∧ ¬p.2 = q.2
⊢ ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ p = q ∨
    ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q ∨
      (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q

State before:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝³ : DecidableRel S
inst✝² : DecidableRel T
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
p q j : α × β
hStrich :
  ¬S p.1 q.1 ∧ ¬S q.1 p.1 ∧ p.1 = q.1 ∨ ¬S p.1 q.1 ∧ S q.1 p.1 ∧ ¬p.1 = q.1 ∨ S p.1 q.1 ∧ ¬S q.1 p.1 ∧ ¬p.1 = q.1
hTtrich :
  ¬T p.2 q.2 ∧ ¬T q.2 p.2 ∧ p.2 = q.2 ∨ ¬T p.2 q.2 ∧ T q.2 p.2 ∧ ¬p.2 = q.2 ∨ T p.2 q.2 ∧ ¬T q.2 p.2 ∧ ¬p.2 = q.2
⊢ ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ p = q ∨
    ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q ∨
      (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q
Tactic:
rename_i inst inst_1 inst_2
State after:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
p q j : α × β
hStrich :
  ¬S p.1 q.1 ∧ ¬S q.1 p.1 ∧ p.1 = q.1 ∨ ¬S p.1 q.1 ∧ S q.1 p.1 ∧ ¬p.1 = q.1 ∨ S p.1 q.1 ∧ ¬S q.1 p.1 ∧ ¬p.1 = q.1
hTtrich :
  ¬T p.2 q.2 ∧ ¬T q.2 p.2 ∧ p.2 = q.2 ∨ ¬T p.2 q.2 ∧ T q.2 p.2 ∧ ¬p.2 = q.2 ∨ T p.2 q.2 ∧ ¬T q.2 p.2 ∧ ¬p.2 = q.2
⊢ ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ p = q ∨
    ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q ∨
      (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q

State before:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
p q j : α × β
hStrich :
  ¬S p.1 q.1 ∧ ¬S q.1 p.1 ∧ p.1 = q.1 ∨ ¬S p.1 q.1 ∧ S q.1 p.1 ∧ ¬p.1 = q.1 ∨ S p.1 q.1 ∧ ¬S q.1 p.1 ∧ ¬p.1 = q.1
hTtrich :
  ¬T p.2 q.2 ∧ ¬T q.2 p.2 ∧ p.2 = q.2 ∨ ¬T p.2 q.2 ∧ T q.2 p.2 ∧ ¬p.2 = q.2 ∨ T p.2 q.2 ∧ ¬T q.2 p.2 ∧ ¬p.2 = q.2
⊢ ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ p = q ∨
    ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q ∨
      (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q
Tactic:
unhygienic with_reducible aesop_destruct_products
State after:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
hStrich :
  ¬S (fst, snd).1 (fst_1, snd_1).1 ∧ ¬S (fst_1, snd_1).1 (fst, snd).1 ∧ (fst, snd).1 = (fst_1, snd_1).1 ∨
    ¬S (fst, snd).1 (fst_1, snd_1).1 ∧ S (fst_1, snd_1).1 (fst, snd).1 ∧ ¬(fst, snd).1 = (fst_1, snd_1).1 ∨
      S (fst, snd).1 (fst_1, snd_1).1 ∧ ¬S (fst_1, snd_1).1 (fst, snd).1 ∧ ¬(fst, snd).1 = (fst_1, snd_1).1
hTtrich :
  ¬T (fst, snd).2 (fst_1, snd_1).2 ∧ ¬T (fst_1, snd_1).2 (fst, snd).2 ∧ (fst, snd).2 = (fst_1, snd_1).2 ∨
    ¬T (fst, snd).2 (fst_1, snd_1).2 ∧ T (fst_1, snd_1).2 (fst, snd).2 ∧ ¬(fst, snd).2 = (fst_1, snd_1).2 ∨
      T (fst, snd).2 (fst_1, snd_1).2 ∧ ¬T (fst_1, snd_1).2 (fst, snd).2 ∧ ¬(fst, snd).2 = (fst_1, snd_1).2
fst_2 : α
snd_2 : β
⊢ ¬(S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
      ¬(S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
        (fst, snd) = (fst_1, snd_1) ∨
    ¬(S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
        (S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
          ¬(fst, snd) = (fst_1, snd_1) ∨
      (S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
        ¬(S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
          ¬(fst, snd) = (fst_1, snd_1)

State before:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
hStrich :
  ¬S (fst, snd).1 (fst_1, snd_1).1 ∧ ¬S (fst_1, snd_1).1 (fst, snd).1 ∧ (fst, snd).1 = (fst_1, snd_1).1 ∨
    ¬S (fst, snd).1 (fst_1, snd_1).1 ∧ S (fst_1, snd_1).1 (fst, snd).1 ∧ ¬(fst, snd).1 = (fst_1, snd_1).1 ∨
      S (fst, snd).1 (fst_1, snd_1).1 ∧ ¬S (fst_1, snd_1).1 (fst, snd).1 ∧ ¬(fst, snd).1 = (fst_1, snd_1).1
hTtrich :
  ¬T (fst, snd).2 (fst_1, snd_1).2 ∧ ¬T (fst_1, snd_1).2 (fst, snd).2 ∧ (fst, snd).2 = (fst_1, snd_1).2 ∨
    ¬T (fst, snd).2 (fst_1, snd_1).2 ∧ T (fst_1, snd_1).2 (fst, snd).2 ∧ ¬(fst, snd).2 = (fst_1, snd_1).2 ∨
      T (fst, snd).2 (fst_1, snd_1).2 ∧ ¬T (fst_1, snd_1).2 (fst, snd).2 ∧ ¬(fst, snd).2 = (fst_1, snd_1).2
fst_2 : α
snd_2 : β
⊢ ¬(S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
      ¬(S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
        (fst, snd) = (fst_1, snd_1) ∨
    ¬(S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
        (S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
          ¬(fst, snd) = (fst_1, snd_1) ∨
      (S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
        ¬(S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
          ¬(fst, snd) = (fst_1, snd_1)
Tactic:
simp_all only [Prod.mk.injEq, not_and]
State after:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
hStrich :
  ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1 ∨
    ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1 ∨ S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
hTtrich :
  ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1 ∨
    ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
hStrich :
  ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1 ∨
    ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1 ∨ S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
hTtrich :
  ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1 ∨
    ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
unhygienic aesop_cases hStrich <;> [(unhygienic aesop_cases hTtrich <;> [skip; (unhygienic aesop_cases h_1)]);
  (unhygienic aesop_cases hTtrich <;> [(unhygienic aesop_cases h);
      (unhygienic aesop_cases h <;> [(unhygienic aesop_cases h_1); (unhygienic aesop_cases h_1)])])]
State after:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
p q j : α × β
hStrich :
  ¬S p.1 q.1 ∧ ¬S q.1 p.1 ∧ p.1 = q.1 ∨ ¬S p.1 q.1 ∧ S q.1 p.1 ∧ ¬p.1 = q.1 ∨ S p.1 q.1 ∧ ¬S q.1 p.1 ∧ ¬p.1 = q.1
hTtrich :
  ¬T p.2 q.2 ∧ ¬T q.2 p.2 ∧ p.2 = q.2 ∨ ¬T p.2 q.2 ∧ T q.2 p.2 ∧ ¬p.2 = q.2 ∨ T p.2 q.2 ∧ ¬T q.2 p.2 ∧ ¬p.2 = q.2
⊢ ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ p = q ∨
    ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q ∨
      (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q
Tactic:
with_reducible aesop_destruct_products
State after:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
hStrich :
  ¬S (fst, snd).1 (fst_1, snd_1).1 ∧ ¬S (fst_1, snd_1).1 (fst, snd).1 ∧ (fst, snd).1 = (fst_1, snd_1).1 ∨
    ¬S (fst, snd).1 (fst_1, snd_1).1 ∧ S (fst_1, snd_1).1 (fst, snd).1 ∧ ¬(fst, snd).1 = (fst_1, snd_1).1 ∨
      S (fst, snd).1 (fst_1, snd_1).1 ∧ ¬S (fst_1, snd_1).1 (fst, snd).1 ∧ ¬(fst, snd).1 = (fst_1, snd_1).1
hTtrich :
  ¬T (fst, snd).2 (fst_1, snd_1).2 ∧ ¬T (fst_1, snd_1).2 (fst, snd).2 ∧ (fst, snd).2 = (fst_1, snd_1).2 ∨
    ¬T (fst, snd).2 (fst_1, snd_1).2 ∧ T (fst_1, snd_1).2 (fst, snd).2 ∧ ¬(fst, snd).2 = (fst_1, snd_1).2 ∨
      T (fst, snd).2 (fst_1, snd_1).2 ∧ ¬T (fst_1, snd_1).2 (fst, snd).2 ∧ ¬(fst, snd).2 = (fst_1, snd_1).2
fst_2 : α
snd_2 : β
⊢ ¬(S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
      ¬(S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
        (fst, snd) = (fst_1, snd_1) ∨
    ¬(S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
        (S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
          ¬(fst, snd) = (fst_1, snd_1) ∨
      (S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
        ¬(S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
          ¬(fst, snd) = (fst_1, snd_1)

State before:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
p q j : α × β
hStrich :
  ¬S p.1 q.1 ∧ ¬S q.1 p.1 ∧ p.1 = q.1 ∨ ¬S p.1 q.1 ∧ S q.1 p.1 ∧ ¬p.1 = q.1 ∨ S p.1 q.1 ∧ ¬S q.1 p.1 ∧ ¬p.1 = q.1
hTtrich :
  ¬T p.2 q.2 ∧ ¬T q.2 p.2 ∧ p.2 = q.2 ∨ ¬T p.2 q.2 ∧ T q.2 p.2 ∧ ¬p.2 = q.2 ∨ T p.2 q.2 ∧ ¬T q.2 p.2 ∧ ¬p.2 = q.2
⊢ ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ p = q ∨
    ¬(S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ (S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q ∨
      (S p.1 q.1 ∨ p.1 = q.1 ∧ T p.2 q.2) ∧ ¬(S q.1 p.1 ∨ q.1 = p.1 ∧ T q.2 p.2) ∧ ¬p = q
Tactic:
aesop_destruct_products
State after:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
hStrich :
  ¬S (fst, snd).1 (fst_1, snd_1).1 ∧ ¬S (fst_1, snd_1).1 (fst, snd).1 ∧ (fst, snd).1 = (fst_1, snd_1).1 ∨
    ¬S (fst, snd).1 (fst_1, snd_1).1 ∧ S (fst_1, snd_1).1 (fst, snd).1 ∧ ¬(fst, snd).1 = (fst_1, snd_1).1 ∨
      S (fst, snd).1 (fst_1, snd_1).1 ∧ ¬S (fst_1, snd_1).1 (fst, snd).1 ∧ ¬(fst, snd).1 = (fst_1, snd_1).1
hTtrich :
  ¬T (fst, snd).2 (fst_1, snd_1).2 ∧ ¬T (fst_1, snd_1).2 (fst, snd).2 ∧ (fst, snd).2 = (fst_1, snd_1).2 ∨
    ¬T (fst, snd).2 (fst_1, snd_1).2 ∧ T (fst_1, snd_1).2 (fst, snd).2 ∧ ¬(fst, snd).2 = (fst_1, snd_1).2 ∨
      T (fst, snd).2 (fst_1, snd_1).2 ∧ ¬T (fst_1, snd_1).2 (fst, snd).2 ∧ ¬(fst, snd).2 = (fst_1, snd_1).2
fst_2 : α
snd_2 : β
⊢ ¬(S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
      ¬(S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
        (fst, snd) = (fst_1, snd_1) ∨
    ¬(S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
        (S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
          ¬(fst, snd) = (fst_1, snd_1) ∨
      (S (fst, snd).1 (fst_1, snd_1).1 ∨ (fst, snd).1 = (fst_1, snd_1).1 ∧ T (fst, snd).2 (fst_1, snd_1).2) ∧
        ¬(S (fst_1, snd_1).1 (fst, snd).1 ∨ (fst_1, snd_1).1 = (fst, snd).1 ∧ T (fst_1, snd_1).2 (fst, snd).2) ∧
          ¬(fst, snd) = (fst_1, snd_1)

State before:
case right
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
hStrich :
  ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1 ∨
    ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1 ∨ S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
hTtrich :
  ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1 ∨
    ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
aesop_cases hStrich <;> [(unhygienic aesop_cases hTtrich <;> [skip; (unhygienic aesop_cases h_1)]);
(unhygienic aesop_cases hTtrich <;> [(unhygienic aesop_cases h);
(unhygienic aesop_cases h <;> [(unhygienic aesop_cases h_1); (unhygienic aesop_cases h_1)])])]
State after:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
hTtrich :
  ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1 ∨
    ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
unhygienic aesop_cases hTtrich <;> [skip; (unhygienic aesop_cases h_1)]
State after:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
hTtrich :
  ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1 ∨
    ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
aesop_cases hTtrich <;> [skip; (unhygienic aesop_cases h_1)]
State after:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
unhygienic aesop_cases h_1
State after:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
aesop_cases h_1
State after:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
hTtrich :
  ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1 ∨
    ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1 ∨ S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
unhygienic aesop_cases hTtrich <;> [(unhygienic aesop_cases h);
   (unhygienic aesop_cases h <;> [(unhygienic aesop_cases h_1); (unhygienic aesop_cases h_1)])]
State after:
case right.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
hTtrich :
  ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1 ∨
    ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1 ∨ S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
aesop_cases hTtrich <;> [(unhygienic aesop_cases h);
(unhygienic aesop_cases h <;> [(unhygienic aesop_cases h_1); (unhygienic aesop_cases h_1)])]
State after:
case right.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1 ∨ S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
unhygienic aesop_cases h
State after:
case right.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1 ∨ S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
aesop_cases h
State after:
case right.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1 ∨ S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
unhygienic aesop_cases h <;> [(unhygienic aesop_cases h_1); (unhygienic aesop_cases h_1)]
State after:
case right.inr.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1 ∨ S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
aesop_cases h <;> [(unhygienic aesop_cases h_1); (unhygienic aesop_cases h_1)]
State after:
case right.inr.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
unhygienic aesop_cases h_1
State after:
case right.inr.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
aesop_cases h_1
State after:
case right.inr.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
unhygienic aesop_cases h_1
State after:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1 ∨ T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
aesop_cases h_1
State after:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

case right.inr.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)

State before:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
simp_all only [true_and, and_self, and_true, not_true_eq_false, forall_true_left, and_false, or_self, or_false]
State after:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)

State before:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)
Tactic:
unhygienic with_reducible aesop_destruct_products
State after:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : ¬T snd_1 snd
right : snd = snd_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)

State before:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : ¬T snd_1 snd
right : snd = snd_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)
Tactic:
aesop_subst [right, right_2]
State after:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left_1 left_3 : ¬T snd_1 snd_1
left left_2 : ¬S fst_1 fst_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)

State before:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left_1 left_3 : ¬T snd_1 snd_1
left left_2 : ¬S fst_1 fst_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)
Tactic:
simp_all only [not_false_eq_true, or_self]
State after:
no goals

State before:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)
Tactic:
with_reducible aesop_destruct_products
State after:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : ¬T snd_1 snd
right : snd = snd_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)

State before:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)
Tactic:
aesop_destruct_products
State after:
case right.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : ¬T snd_1 snd
right : snd = snd_1
⊢ ¬(S fst_1 fst_1 ∨ T snd_1 snd_1)

State before:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
simp_all only [and_false, or_false, and_self, or_true, not_true_eq_false, not_false_eq_true, forall_true_left,
  and_true, false_or]
State after:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬S fst_1 fst_1

State before:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬S fst_1 fst_1
Tactic:
unhygienic with_reducible aesop_destruct_products
State after:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
⊢ ¬S fst_1 fst_1

State before:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
⊢ ¬S fst_1 fst_1
Tactic:
aesop_subst right_2
State after:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left_1 : ¬T snd snd_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
left left_2 : ¬S fst_1 fst_1
⊢ ¬S fst_1 fst_1

State before:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left_1 : ¬T snd snd_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
left left_2 : ¬S fst_1 fst_1
⊢ ¬S fst_1 fst_1
Tactic:
simp_all only [not_false_eq_true]
State after:
no goals

State before:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬S fst_1 fst_1
Tactic:
with_reducible aesop_destruct_products
State after:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
⊢ ¬S fst_1 fst_1

State before:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬S fst_1 fst_1
Tactic:
aesop_destruct_products
State after:
case right.inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
⊢ ¬S fst_1 fst_1

State before:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
simp_all only [and_self, or_true, not_true_eq_false, and_false, or_false, not_false_eq_true, forall_true_left,
  and_true, false_and, true_and, false_or]
State after:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬S fst_1 fst_1

State before:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬S fst_1 fst_1
Tactic:
unhygienic with_reducible aesop_destruct_products
State after:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : ¬T snd_1 snd
right : ¬snd = snd_1
⊢ ¬S fst_1 fst_1

State before:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : ¬T snd_1 snd
right : ¬snd = snd_1
⊢ ¬S fst_1 fst_1
Tactic:
aesop_subst right_2
State after:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left_1 : T snd snd_1
left_3 : ¬T snd_1 snd
right : ¬snd = snd_1
left left_2 : ¬S fst_1 fst_1
⊢ ¬S fst_1 fst_1

State before:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left_1 : T snd snd_1
left_3 : ¬T snd_1 snd
right : ¬snd = snd_1
left left_2 : ¬S fst_1 fst_1
⊢ ¬S fst_1 fst_1
Tactic:
simp_all only [not_false_eq_true]
State after:
no goals

State before:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬S fst_1 fst_1
Tactic:
with_reducible aesop_destruct_products
State after:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : ¬T snd_1 snd
right : ¬snd = snd_1
⊢ ¬S fst_1 fst_1

State before:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ ¬S fst_1 fst ∧ fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬S fst_1 fst_1
Tactic:
aesop_destruct_products
State after:
case right.inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : ¬S fst fst_1
left_1 : T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : fst = fst_1
left_3 : ¬T snd_1 snd
right : ¬snd = snd_1
⊢ ¬S fst_1 fst_1

State before:
case right.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
simp_all only [false_and, or_self, not_false_eq_true, true_or, not_true_eq_false, and_true, and_self, and_false,
  IsEmpty.forall_iff, or_false, or_true]
State after:
no goals

State before:
case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
simp_all only [false_and, or_false, not_true_eq_false, false_or, not_and, and_true, and_false, and_self,
  IsEmpty.forall_iff, true_and]
State after:
case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ fst_1 = fst → ¬T snd_1 snd_1

State before:
case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
⊢ fst_1 = fst → ¬T snd_1 snd_1
Tactic:
intro a
State after:
case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
a : fst_1 = fst
⊢ ¬T snd_1 snd_1

State before:
case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
a : fst_1 = fst
⊢ ¬T snd_1 snd_1
Tactic:
aesop_subst a
State after:
case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst ∧ ¬S fst fst ∧ ¬fst = fst
⊢ ¬T snd_1 snd_1

State before:
case right.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd snd_1 : β
fst_2 : α
snd_2 : β
h_1 : ¬T snd snd_1 ∧ ¬T snd_1 snd ∧ snd = snd_1
h : S fst fst ∧ ¬S fst fst ∧ ¬fst = fst
⊢ ¬T snd_1 snd_1
Tactic:
simp_all only [not_true_eq_false, and_false]
State after:
no goals

State before:
case right.inr.inr.inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
simp_all only [and_self, or_self, not_false_eq_true, and_true, true_or, not_true_eq_false, and_false,
  IsEmpty.forall_iff, or_false, or_true]
State after:
no goals

State before:
case right.inr.inr.inl.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : ¬S fst fst_1 ∧ S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
simp_all only [and_true, or_self, not_false_eq_true, and_false, or_false, not_true_eq_false, and_self,
  IsEmpty.forall_iff, or_true]
State after:
no goals

State before:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
simp_all only [and_self, or_false, not_true_eq_false, and_true, false_or, and_false, IsEmpty.forall_iff,
  false_and, true_and]
State after:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬fst_1 = fst

State before:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬fst_1 = fst
Tactic:
unhygienic with_reducible aesop_destruct_products
State after:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : ¬fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
⊢ ¬fst_1 = fst

State before:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : ¬fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
⊢ ¬fst_1 = fst
Tactic:
apply Aesop.BuiltinRules.not_intro
State after:
case right.inr.inr.inr.inl.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : ¬fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
⊢ fst_1 = fst → False

State before:
case right.inr.inr.inr.inl.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : ¬fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
⊢ fst_1 = fst → False
Tactic:
intro a
State after:
case right.inr.inr.inr.inl.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : ¬fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
a : fst_1 = fst
⊢ False

State before:
case right.inr.inr.inr.inl.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : ¬fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
a : fst_1 = fst
⊢ False
Tactic:
aesop_subst a
State after:
case right.inr.inr.inr.inl.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd snd_1 : β
fst_2 : α
snd_2 : β
left_1 : ¬T snd snd_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
left : S fst fst
left_2 : ¬S fst fst
right_2 : ¬fst = fst
⊢ False

State before:
case right.inr.inr.inr.inl.h
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd snd_1 : β
fst_2 : α
snd_2 : β
left_1 : ¬T snd snd_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
left : S fst fst
left_2 : ¬S fst fst
right_2 : ¬fst = fst
⊢ False
Tactic:
simp_all only
State after:
no goals

State before:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬fst_1 = fst
Tactic:
with_reducible aesop_destruct_products
State after:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : ¬fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
⊢ ¬fst_1 = fst

State before:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : ¬T snd snd_1 ∧ T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬fst_1 = fst
Tactic:
aesop_destruct_products
State after:
case right.inr.inr.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
left : S fst fst_1
left_1 : ¬T snd snd_1
left_2 : ¬S fst_1 fst
right_2 : ¬fst = fst_1
left_3 : T snd_1 snd
right : ¬snd = snd_1
⊢ ¬fst_1 = fst

State before:
case right.inr.inr.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝ : DecidableRel S
inst : DecidableRel T
inst_1 : DecidableEq α
inst_2 : DecidableEq β
fst : α
snd : β
fst_1 : α
snd_1 : β
fst_2 : α
snd_2 : β
h : S fst fst_1 ∧ ¬S fst_1 fst ∧ ¬fst = fst_1
h_1 : T snd snd_1 ∧ ¬T snd_1 snd ∧ ¬snd = snd_1
⊢ ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧ ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ fst = fst_1 ∧ snd = snd_1 ∨
    ¬(S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        (S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1) ∨
      (S fst fst_1 ∨ fst = fst_1 ∧ T snd snd_1) ∧
        ¬(S fst_1 fst ∨ fst_1 = fst ∧ T snd_1 snd) ∧ (fst = fst_1 → ¬snd = snd_1)
Tactic:
simp_all only [and_true, or_false, not_true_eq_false, and_false, or_self, not_false_eq_true, and_self,
  IsEmpty.forall_iff, or_true]
State after:
no goals