internlm/Lean-Github huggingface dataset:
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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]
Proof state after:
no goals
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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]
Proof state after:
no goals
Theorem: r5_strict_order
Proof 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]
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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]
Proof state after:
no goals
Theorem: r5_strict_order
Proof 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]
Proof state after:
no goals
Theorem: r5_strict_order
Proof 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]
Proof state after:
no goals
Theorem: r5_strict_order
Proof 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]
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof state after:
no goals
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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]
Proof state after:
no goals
Theorem: r5_not_weak_order
Proof state before:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ ¬WeakOrder (R5 S T)
Tactic:
intro hwo
Proof state after:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : WeakOrder (R5 S T)
⊢ False
Theorem: r5_not_weak_order
Proof state before:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : WeakOrder (R5 S T)
⊢ False
Tactic:
rw [WeakOrder] at hwo
Proof state after:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
⊢ False
Theorem: r5_not_weak_order
Proof state before:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
⊢ False
Tactic:
have hf := hwo.2
Proof state after:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
hf : ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
⊢ False
Theorem: r5_not_weak_order
Proof state before:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
hf : ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
⊢ False
Tactic:
have p : α × β := Classical.choice Prod.Nonempty
Proof state after:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
hf : ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
⊢ False
Theorem: r5_not_weak_order
Proof state before:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
hf : ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
⊢ False
Tactic:
specialize hf p p
Proof state after:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hf : R5 S T p p ∨ R5 S T p p
⊢ False
Theorem: r5_not_weak_order
Proof state before:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hf : R5 S T p p ∨ R5 S T p p
⊢ False
Tactic:
simp [R5] at hf
Proof state after:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hf : S p.1 p.1 ∨ T p.2 p.2
⊢ False
Theorem: r5_not_weak_order
Proof state before:
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hf : S p.1 p.1 ∨ T p.2 p.2
⊢ False
Tactic:
rcases hf with (hS1 | hT1)
Proof state after:
case inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hS1 : S p.1 p.1
⊢ False

case inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hT1 : T p.2 p.2
⊢ False
Theorem: r5_not_weak_order
Proof state before:
case inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hS1 : S p.1 p.1
⊢ False
Tactic:
rcases hS.trich p.1 p.1 with (hS2 | hS3 | hS4)
Proof state after:
case inl.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hS1 : S p.1 p.1
hS2 : ¬S p.1 p.1 ∧ ¬S p.1 p.1 ∧ p.1 = p.1
⊢ False

case inl.inr.inl
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hS1 : S p.1 p.1
hS3 : ¬S p.1 p.1 ∧ S p.1 p.1 ∧ ¬p.1 = p.1
⊢ False

case inl.inr.inr
α β : Type
S : α → α → Prop
T : β → β → Prop
hS : CStrictOrder S
hT : CStrictOrder T
inst✝⁵ : DecidableRel S
inst✝⁴ : DecidableRel T
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
hwo : PartialOrder' (R5 S T) ∧ ∀ (a b : α × β), R5 S T a b ∨ R5 S T b a
p : α × β
hS1 : S p.1 p.1
hS4 : S p.1 p.1 ∧ ¬S p.1 p.1 ∧ ¬p.1 = p.1
⊢ False