Theorem: r5_not_weak_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 β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ ¬WeakOrder (R5 S T)
Tactic:
intro hwo
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

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
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

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
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

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
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

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
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

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
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

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)
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

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)
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

State before:
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
Tactic:
exact hS2.left hS1
State after:
no goals

State before:
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
Tactic:
exact hS3.left hS1
State after:
no goals

State before:
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
Tactic:
have := hS4.right.right
State after:
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
this : ¬p.1 = p.1
⊢ False

State before:
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
this : ¬p.1 = p.1
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
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
Tactic:
rcases hT.trich p.2 p.2 with (hT2 | hT3 | hT4)
State after:
case 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 : α × β
hT1 : T p.2 p.2
hT2 : ¬T p.2 p.2 ∧ ¬T p.2 p.2 ∧ p.2 = p.2
⊢ False

case inr.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 : α × β
hT1 : T p.2 p.2
hT3 : ¬T p.2 p.2 ∧ T p.2 p.2 ∧ ¬p.2 = p.2
⊢ False

case inr.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 : α × β
hT1 : T p.2 p.2
hT4 : T p.2 p.2 ∧ ¬T p.2 p.2 ∧ ¬p.2 = p.2
⊢ False

State before:
case 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 : α × β
hT1 : T p.2 p.2
hT2 : ¬T p.2 p.2 ∧ ¬T p.2 p.2 ∧ p.2 = p.2
⊢ False
Tactic:
exact hT2.left hT1
State after:
no goals

State before:
case inr.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 : α × β
hT1 : T p.2 p.2
hT3 : ¬T p.2 p.2 ∧ T p.2 p.2 ∧ ¬p.2 = p.2
⊢ False
Tactic:
exact hT3.left hT1
State after:
no goals

State before:
case inr.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 : α × β
hT1 : T p.2 p.2
hT4 : T p.2 p.2 ∧ ¬T p.2 p.2 ∧ ¬p.2 = p.2
⊢ False
Tactic:
have := hT4.right.right
State after:
case inr.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 : α × β
hT1 : T p.2 p.2
hT4 : T p.2 p.2 ∧ ¬T p.2 p.2 ∧ ¬p.2 = p.2
this : ¬p.2 = p.2
⊢ False

State before:
case inr.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 : α × β
hT1 : T p.2 p.2
hT4 : T p.2 p.2 ∧ ¬T p.2 p.2 ∧ ¬p.2 = p.2
this : ¬p.2 = p.2
⊢ False
Tactic:
contradiction
State after:
no goals