Theorem: Geometry.quadrangle_rotate (ProjectivePlane.lean)

State before:
P L : Type
p q r s : P
inst✝ : Geometry P
⊢ isQuadrangle p q r s → isQuadrangle q r s p
Tactic:
intro ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
State after:
P L : Type
p q r s : P
inst✝ : Geometry P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
⊢ isQuadrangle q r s p

State before:
P L : Type
p q r s : P
inst✝ : Geometry P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
⊢ isQuadrangle q r s p
Tactic:
exact ⟨triangle_qrs, triangle_rotate triangle_pqr, triangle_rotate triangle_pqs, triangle_rotate triangle_prs⟩
State after:
no goals