internlm/Lean-Github huggingface dataset:
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inl

⊢ 6 ∣ 30 ∨ 30 ∣ 6
Tactic:
left
Proof state after:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inl.h

⊢ 6 ∣ 30
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inl.h

⊢ 6 ∣ 30
Tactic:
use 5
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inr

⊢ 6 ∣ 210 ∨ 210 ∣ 6
Tactic:
left
Proof state after:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inr.h

⊢ 6 ∣ 210
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inl.inr.inr.h

⊢ 6 ∣ 210
Tactic:
use 35
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inl

⊢ 30 ∣ 6 ∨ 6 ∣ 30
Tactic:
right
Proof state after:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inl.h

⊢ 6 ∣ 30
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inl.h

⊢ 6 ∣ 30
Tactic:
use 5
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inr

⊢ 210 ∣ 6 ∨ 6 ∣ 210
Tactic:
right
Proof state after:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inr.h

⊢ 6 ∣ 210
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inr.inl.inr.h

⊢ 6 ∣ 210
Tactic:
use 35
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inl.inr

⊢ 30 ∣ 210 ∨ 210 ∣ 30
Tactic:
left
Proof state after:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inl.inr.h

⊢ 30 ∣ 210
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inl.inr.h

⊢ 30 ∣ 210
Tactic:
use 7
Proof state after:
no goals
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inr.inl

⊢ 210 ∣ 30 ∨ 30 ∣ 210
Tactic:
right
Proof state after:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inr.inl.h

⊢ 30 ∣ 210
Theorem: r4_weak_order
Proof state before:
case right.mk.mk.inr.inr.inr.inr.inr.inr.inr.inl.h

⊢ 30 ∣ 210
Tactic:
use 7
Proof state after:
no goals
Theorem: r4_not_strict_order
Proof state before:
⊢ ¬StrictOrder R4
Tactic:
intro hso
Proof state after:
hso : StrictOrder R4
⊢ False
Theorem: r4_not_strict_order
Proof state before:
hso : StrictOrder R4
⊢ False
Tactic:
simp_rw [StrictOrder, VeryDiv] at hso
Proof state after:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
⊢ False
Theorem: r4_not_strict_order
Proof state before:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
⊢ False
Tactic:
have hf := hso ⟨1, by tauto⟩ ⟨1, by tauto⟩ ⟨1, by tauto⟩
Proof state after:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf :
  (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } →
      R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
          { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } →
        R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
          { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }) ∧
    Trichotomy
      (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
      (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
      ({ val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } =
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
⊢ False
Theorem: r4_not_strict_order
Proof state before:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf :
  (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } →
      R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
          { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } →
        R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
          { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }) ∧
    Trichotomy
      (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
      (R4 { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) }
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
      ({ val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) } =
        { val := 1, property := (_ : 1 = 1 ∨ 1 ∈ {2, 6, 30, 210}) })
⊢ False
Tactic:
simp_rw [R4] at hf
Proof state after:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf : (1 ∣ 1 → 1 ∣ 1 → 1 ∣ 1) ∧ Trichotomy (1 ∣ 1) (1 ∣ 1) True
⊢ False
Theorem: r4_not_strict_order
Proof state before:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf : (1 ∣ 1 → 1 ∣ 1 → 1 ∣ 1) ∧ Trichotomy (1 ∣ 1) (1 ∣ 1) True
⊢ False
Tactic:
rw [Trichotomy] at hf
Proof state after:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf : (1 ∣ 1 → 1 ∣ 1 → 1 ∣ 1) ∧ (¬1 ∣ 1 ∧ ¬1 ∣ 1 ∧ True ∨ ¬1 ∣ 1 ∧ 1 ∣ 1 ∧ ¬True ∨ 1 ∣ 1 ∧ ¬1 ∣ 1 ∧ ¬True)
⊢ False
Theorem: r4_not_strict_order
Proof state before:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
hf : (1 ∣ 1 → 1 ∣ 1 → 1 ∣ 1) ∧ (¬1 ∣ 1 ∧ ¬1 ∣ 1 ∧ True ∨ ¬1 ∣ 1 ∧ 1 ∣ 1 ∧ ¬True ∨ 1 ∣ 1 ∧ ¬1 ∣ 1 ∧ ¬True)
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: r4_not_strict_order
Proof state before:
hso : ∀ (a b c : ↑{1, 2, 6, 30, 210}), (R4 a b → R4 b c → R4 a c) ∧ Trichotomy (R4 a b) (R4 b a) (a = b)
⊢ 1 ∈ {1, 2, 6, 30, 210}
Tactic:
tauto
Proof state after:
no goals
Theorem: r5_strict_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 β
⊢ StrictOrder (R5 S T)
Tactic:
intro p q j
Proof 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)
Theorem: r5_strict_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 β
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]
Proof 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)
Theorem: r5_strict_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 β
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
Proof 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)
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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⟩)
Proof 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
Theorem: r5_strict_order
Proof 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⟩)
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof state after:
no goals
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof state after:
no goals
Theorem: r5_strict_order
Proof 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⟩)
Proof 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
Theorem: r5_strict_order
Proof 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]
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof state after:
no goals
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof 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
Theorem: r5_strict_order
Proof 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
Proof state after:
no goals
Theorem: r5_strict_order
Proof 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
Proof state after:
no goals
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✝¹ : 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
Proof 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)
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✝¹ : 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
Proof 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)
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✝¹ : 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 *
Proof 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
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✝¹ : 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
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 β
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