Theorem: gradual (lean/solutions/09_tactics.lean)

State before:
p q : Prop
⊢ p ∧ q ↔ q ∧ p
Tactic:
step_1
State after:
case red
p q : Prop
⊢ p ∧ q → q ∧ p

case blue
p q : Prop
⊢ q ∧ p → p ∧ q

State before:
case red
p q : Prop
⊢ p ∧ q → q ∧ p

case blue
p q : Prop
⊢ q ∧ p → p ∧ q
Tactic:
step_2
State after:
case red
p q : Prop
hA : p ∧ q
⊢ q ∧ p

State before:
case red
p q : Prop
hA : p ∧ q
⊢ q ∧ p
Tactic:
step_3
State after:
case red1
p q : Prop
hA : p ∧ q
⊢ q

case red2
p q : Prop
hA : p ∧ q
⊢ p

State before:
case red1
p q : Prop
hA : p ∧ q
⊢ q

case red2
p q : Prop
hA : p ∧ q
⊢ p
Tactic:
step_4
State after:
no goals