Theorem: Fano.Fano.quadrangle1236 (ProjectivePlane.lean)

State before:
P L : Type
⊢ ¬collinear Points.p1 Points.p2 Points.p3
Tactic:
simp[collinear]
State after:
no goals

State before:
P L : Type
⊢ ¬collinear Points.p1 Points.p2 Points.p6
Tactic:
simp[collinear]
State after:
no goals

State before:
P L : Type
⊢ ¬collinear Points.p1 Points.p3 Points.p6
Tactic:
simp[collinear]
State after:
no goals

State before:
P L : Type
⊢ ¬collinear Points.p2 Points.p3 Points.p6
Tactic:
simp[collinear]
State after:
no goals