Theorem: IMOSL.IMO2009C1.and_and_or_not_iff (IMOSLLean4/IMO2009/C1/C1.lean)

State before:
P Q R : Prop
⊢ (P ∧ Q) ∧ (R ∨ ¬Q) ↔ (P ∧ R) ∧ Q
Tactic:
rw [and_assoc, and_or_left, and_not_self_iff,
  or_false_iff, and_assoc, and_comm (b := Q)]
State after:
no goals