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

State before:
p q r s : Prop
⊢ p ∧ q ∧ r → p ∧ r
Tactic:
intro hpqr
State after:
p q r s : Prop
hpqr : p ∧ q ∧ r
⊢ p ∧ r

State before:
p q r s : Prop
hpqr : p ∧ q ∧ r
⊢ p ∧ r
Tactic:
eliminate hpqr with hp hqr
State after:
case intro
p q r s : Prop
hp : p
hqr : q ∧ r
⊢ p ∧ r

State before:
case intro
p q r s : Prop
hp : p
hqr : q ∧ r
⊢ p ∧ r
Tactic:
eliminate hqr with hq hr
State after:
case intro.intro
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p ∧ r

State before:
case intro.intro
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p ∧ r
Tactic:
split_goal
State after:
case intro.intro.left
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p

case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r

State before:
case intro.intro.left
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p

case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r
Tactic:
{ assumption }
State after:
case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r

State before:
case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r
Tactic:
{ assumption }
State after:
no goals

State before:
case intro.intro.left
p q r s : Prop
hp : p
hq : q
hr : r
⊢ p
Tactic:
assumption
State after:
no goals

State before:
case intro.intro.right
p q r s : Prop
hp : p
hq : q
hr : r
⊢ r
Tactic:
assumption
State after:
no goals