Theorem: problem_3 (BrownCs22/Homework/Hw1Sols.lean)

State before:
p q r s : Prop
⊢ (p ∨ q) ∧ (p → r) ∧ (q → s) → r ∨ s
Tactic:
intro h_long_and
State after:
p q r s : Prop
h_long_and : (p ∨ q) ∧ (p → r) ∧ (q → s)
⊢ r ∨ s

State before:
p q r s : Prop
h_long_and : (p ∨ q) ∧ (p → r) ∧ (q → s)
⊢ r ∨ s
Tactic:
eliminate h_long_and with hpq h_short_and
State after:
case intro
p q r s : Prop
hpq : p ∨ q
h_short_and : (p → r) ∧ (q → s)
⊢ r ∨ s

State before:
case intro
p q r s : Prop
hpq : p ∨ q
h_short_and : (p → r) ∧ (q → s)
⊢ r ∨ s
Tactic:
eliminate h_short_and with hpr hqs
State after:
case intro.intro
p q r s : Prop
hpq : p ∨ q
hpr : p → r
hqs : q → s
⊢ r ∨ s

State before:
case intro.intro
p q r s : Prop
hpq : p ∨ q
hpr : p → r
hqs : q → s
⊢ r ∨ s
Tactic:
eliminate hpq with hp hq
State after:
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
⊢ r ∨ s

case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s

State before:
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
⊢ r ∨ s

case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s
Tactic:
{ have hr : r := hpr hp 
  left 
  assumption }
State after:
case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s

State before:
case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s
Tactic:
{ have hs : s := hqs hq 
  right 
  assumption }
State after:
no goals

State before:
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
⊢ r ∨ s
Tactic:
have hr : r := hpr hp
State after:
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
hr : r
⊢ r ∨ s

State before:
case intro.intro.inl
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
hr : r
⊢ r ∨ s
Tactic:
left
State after:
case intro.intro.inl.h
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
hr : r
⊢ r

State before:
case intro.intro.inl.h
p q r s : Prop
hpr : p → r
hqs : q → s
hp : p
hr : r
⊢ r
Tactic:
assumption
State after:
no goals

State before:
case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
⊢ r ∨ s
Tactic:
have hs : s := hqs hq
State after:
case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
hs : s
⊢ r ∨ s

State before:
case intro.intro.inr
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
hs : s
⊢ r ∨ s
Tactic:
right
State after:
case intro.intro.inr.h
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
hs : s
⊢ s

State before:
case intro.intro.inr.h
p q r s : Prop
hpr : p → r
hqs : q → s
hq : q
hs : s
⊢ s
Tactic:
assumption
State after:
no goals