Theorem: R5'_false (meetings/ex6.lean)

State before:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
⊢ R5' p [] ↔ False
Tactic:
simp
State after:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
⊢ ¬R5' p []

State before:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
⊢ ¬R5' p []
Tactic:
intro hr
State after:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ False

State before:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ False
Tactic:
rw [R5'] at hr
State after:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
⊢ False

case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ p = [] → False

case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ p = [] → False

State before:
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
⊢ False
Tactic:
exact hr
State after:
no goals

State before:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ p = [] → False
Tactic:
intro heq
State after:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
heq : p = []
⊢ False

State before:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
heq : p = []
⊢ False
Tactic:
rw [heq] at hr
State after:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' [] []
heq : p = []
⊢ False

State before:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' [] []
heq : p = []
⊢ False
Tactic:
rw [R5'] at hr
State after:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
heq : p = []
⊢ False

State before:
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
heq : p = []
⊢ False
Tactic:
exact hr
State after:
no goals

State before:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ p = [] → False
Tactic:
intro heq
State after:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
heq : p = []
⊢ False

State before:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
heq : p = []
⊢ False
Tactic:
rw [heq] at hr
State after:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' [] []
heq : p = []
⊢ False

State before:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' [] []
heq : p = []
⊢ False
Tactic:
rw [R5'] at hr
State after:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
heq : p = []
⊢ False

State before:
case x_2
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : False
heq : p = []
⊢ False
Tactic:
exact hr
State after:
no goals