Theorem: r3_not_strict_order (meetings/ex6.lean)

State before:
⊢ ¬StrictOrder R3
Tactic:
intro hso
State after:
hso : StrictOrder R3
⊢ False

State before:
hso : StrictOrder R3
⊢ False
Tactic:
rw [StrictOrder] at hso
State after:
hso : ∀ (a b c : ℕplus), (R3 a b → R3 b c → R3 a c) ∧ Trichotomy (R3 a b) (R3 b a) (a = b)
⊢ False

State before:
hso : ∀ (a b c : ℕplus), (R3 a b → R3 b c → R3 a c) ∧ Trichotomy (R3 a b) (R3 b a) (a = b)
⊢ False
Tactic:
specialize hso 2 3 1
State after:
hso : (R3 2 3 → R3 3 1 → R3 2 1) ∧ Trichotomy (R3 2 3) (R3 3 2) (2 = 3)
⊢ False

State before:
hso : (R3 2 3 → R3 3 1 → R3 2 1) ∧ Trichotomy (R3 2 3) (R3 3 2) (2 = 3)
⊢ False
Tactic:
rcases hso with ⟨_, (⟨_, _, heq⟩ | ⟨_, hdvd3, _⟩ | ⟨hdvd2, _, _⟩)⟩
State after:
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : 2 = 3
⊢ False

case intro.inr.inl.intro.intro
left✝¹ : R3 2 3 → R3 3 1 → R3 2 1
left✝ : ¬R3 2 3
hdvd3 : R3 3 2
right✝ : ¬2 = 3
⊢ False

case intro.inr.inr.intro.intro
left✝¹ : R3 2 3 → R3 3 1 → R3 2 1
hdvd2 : R3 2 3
left✝ : ¬R3 3 2
right✝ : ¬2 = 3
⊢ False

State before:
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : 2 = 3
⊢ False
Tactic:
rw [←Subtype.coe_inj] at heq
State after:
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : ↑2 = ↑3
⊢ False

State before:
case intro.inl.intro.intro
left✝² : R3 2 3 → R3 3 1 → R3 2 1
left✝¹ : ¬R3 2 3
left✝ : ¬R3 3 2
heq : ↑2 = ↑3
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case intro.inr.inl.intro.intro
left✝¹ : R3 2 3 → R3 3 1 → R3 2 1
left✝ : ¬R3 2 3
hdvd3 : R3 3 2
right✝ : ¬2 = 3
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case intro.inr.inr.intro.intro
left✝¹ : R3 2 3 → R3 3 1 → R3 2 1
hdvd2 : R3 2 3
left✝ : ¬R3 3 2
right✝ : ¬2 = 3
⊢ False
Tactic:
contradiction
State after:
no goals