Theorem: Geometry.triangle_rotate (ProjectivePlane.lean)

State before:
P L : Type
p q r s : P
inst✝ : Geometry P
⊢ ¬collinear p q r → ¬collinear q r p
Tactic:
simp[collinear]
State after:
P L : Type
p q r s : P
inst✝ : Geometry P
⊢ (∀ (x : line P), p ∈ x → q ∈ x → ¬r ∈ x) → ∀ (x : line P), q ∈ x → r ∈ x → ¬p ∈ x

State before:
P L : Type
p q r s : P
inst✝ : Geometry P
⊢ (∀ (x : line P), p ∈ x → q ∈ x → ¬r ∈ x) → ∀ (x : line P), q ∈ x → r ∈ x → ¬p ∈ x
Tactic:
intro triangle_pqr l hq hr hp
State after:
P L : Type
p q r s : P
inst✝ : Geometry P
triangle_pqr : ∀ (x : line P), p ∈ x → q ∈ x → ¬r ∈ x
l : line P
hq : q ∈ l
hr : r ∈ l
hp : p ∈ l
⊢ False

State before:
P L : Type
p q r s : P
inst✝ : Geometry P
triangle_pqr : ∀ (x : line P), p ∈ x → q ∈ x → ¬r ∈ x
l : line P
hq : q ∈ l
hr : r ∈ l
hp : p ∈ l
⊢ False
Tactic:
apply triangle_pqr <;> assumption
State after:
no goals