Theorem: Lecture04.these_are_contradictory (BrownCs22/Demos/Lecture04.lean)

State before:
p q r al_ac betty_beg carl_cac : Prop
h1 : al_ac ∧ (betty_beg ∨ carl_cac)
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
⊢ False
Tactic:
eliminate h1 with h4 h5
State after:
case intro
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h5 : betty_beg ∨ carl_cac
⊢ False

State before:
case intro
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h5 : betty_beg ∨ carl_cac
⊢ False
Tactic:
eliminate h5 with h6 h7
State after:
case intro.inl
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h6 : betty_beg
⊢ False

case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False

State before:
case intro.inl
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h6 : betty_beg
⊢ False

case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False
Tactic:
{ have h8 : ¬ al_ac := h2 h6 contradiction }
State after:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False

State before:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False
Tactic:
{ have h9 : betty_beg := h3 h7 have h10 : ¬ al_ac := h2 h9  contradiction }
State after:
no goals

State before:
case intro.inl
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h6 : betty_beg
⊢ False
Tactic:
have h8 : ¬ al_ac := h2 h6
State after:
case intro.inl
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h6 : betty_beg
h8 : ¬al_ac
⊢ False

State before:
case intro.inl
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h6 : betty_beg
h8 : ¬al_ac
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
⊢ False
Tactic:
have h9 : betty_beg := h3 h7
State after:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
h9 : betty_beg
⊢ False

State before:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
h9 : betty_beg
⊢ False
Tactic:
have h10 : ¬ al_ac := h2 h9
State after:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
h9 : betty_beg
h10 : ¬al_ac
⊢ False

State before:
case intro.inr
p q r al_ac betty_beg carl_cac : Prop
h2 : betty_beg → ¬al_ac
h3 : carl_cac → betty_beg
h4 : al_ac
h7 : carl_cac
h9 : betty_beg
h10 : ¬al_ac
⊢ False
Tactic:
contradiction
State after:
no goals