internlm/Lean-Github huggingface dataset:
Theorem: r5_strict_order
Proof 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
Proof 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)
Theorem: r5_strict_order
Proof 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]
Proof 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)
Theorem: r5_strict_order
Proof 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
Proof 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)
Theorem: r5_strict_order
Proof 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
Proof 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)
Theorem: r5_strict_order
Proof 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)]
Proof 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)
Theorem: r5_strict_order
Proof 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)]
Proof 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)
Theorem: r5_strict_order
Proof 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
Proof 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)
Theorem: r5_strict_order
Proof 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
Proof 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)
Theorem: r5_strict_order
Proof 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
Proof 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)