Theorem: ProjectivePlane.dual_quadrangle (ProjectivePlane.lean)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ isQuadrangle p q r s → isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
intro ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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 (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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 (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
let a := p ⊔ q
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
let b := q ⊔ r
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
let c := r ⊔ s
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
let d := s ⊔ p
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
have triangle_abc : ¬ collinear a b c := by
  apply dual_quadrangle_part
  exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
have triangle_abd : ¬ collinear a b d := by
  apply triangle_rotate
  apply dual_quadrangle_part
  apply quadrangle_rotate
  apply quadrangle_rotate
  apply quadrangle_rotate
  exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
have triangle_acd : ¬ collinear a c d := by
  apply triangle_rotate
  apply triangle_rotate
  apply dual_quadrangle_part
  apply quadrangle_rotate
  apply quadrangle_rotate
  exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
have triangle_bcd : ¬ collinear b c d := by
  apply dual_quadrangle_part
  apply quadrangle_rotate
  exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
triangle_bcd : ¬collinear b c d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
triangle_bcd : ¬collinear b c d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
exact ⟨triangle_abc, triangle_abd, triangle_acd, triangle_bcd⟩
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
⊢ ¬collinear a b c
Tactic:
apply dual_quadrangle_part
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
⊢ isQuadrangle p q r s

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
⊢ isQuadrangle p q r s
Tactic:
exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ ¬collinear a b d
Tactic:
apply triangle_rotate
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ ¬collinear d a b

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ ¬collinear d a b
Tactic:
apply dual_quadrangle_part
State after:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle s p q r

State before:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle s p q r
Tactic:
apply quadrangle_rotate
State after:
case a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle r s p q

State before:
case a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle r s p q
Tactic:
apply quadrangle_rotate
State after:
case a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle q r s p

State before:
case a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle q r s p
Tactic:
apply quadrangle_rotate
State after:
case a.a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle p q r s

State before:
case a.a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle p q r s
Tactic:
exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ ¬collinear a c d
Tactic:
apply triangle_rotate
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ ¬collinear d a c

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ ¬collinear d a c
Tactic:
apply triangle_rotate
State after:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ ¬collinear c d a

State before:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ ¬collinear c d a
Tactic:
apply dual_quadrangle_part
State after:
case a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle r s p q

State before:
case a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle r s p q
Tactic:
apply quadrangle_rotate
State after:
case a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle q r s p

State before:
case a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle q r s p
Tactic:
apply quadrangle_rotate
State after:
case a.a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle p q r s

State before:
case a.a.a.a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle p q r s
Tactic:
exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ ¬collinear b c d
Tactic:
apply dual_quadrangle_part
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle q r s p

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle q r s p
Tactic:
apply quadrangle_rotate
State after:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle p q r s

State before:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane 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
a : line P := p ⊔ q
b : line P := q ⊔ r
c : line P := r ⊔ s
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle p q r s
Tactic:
exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
State after:
no goals