Theorem: ProjectivePlane.dual_quadrangle_part (ProjectivePlane.lean)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ isQuadrangle p q r s → ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
intro ⟨triangle_pqr, _, _, triangle_qrs⟩
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬collinear p r s
triangle_qrs : ¬collinear q r s
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬collinear p r s
triangle_qrs : ¬collinear q r s
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
let a := p ⊔ q
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
let b := q ⊔ r
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)

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

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
let t := a ⊓ c
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
have t_is_not_q : q ≠ t := by
    intro h
    have : collinear q r s := by
      simp[collinear]
      rw[h]
      exists c
      apply And.intro
      . simp
      . apply And.intro
        . simp
        . simp
    contradiction
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
have t_is_not_r : r ≠ t := by
  intro h
  have : collinear p q r := by
   simp[collinear]
   rw[h]
   exists a
   apply And.intro
   . simp
   . apply And.intro
     . simp
     . simp
  contradiction
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
have a_is_q_t : a = q ⊔ t := by
    apply connectingLine_uniq
    . assumption
    . simp
    . simp
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
have c_is_r_t : c = r ⊔ t := by
  apply connectingLine_uniq
  . assumption
  . simp
  . simp
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
have triangle_tqr :  ¬ collinear t q r := by
  simp[collinear]
  intro l htl hql hrl
  have l_is_a : l = a := by
    rw[a_is_q_t]
    apply connectingLine_uniq <;> assumption
  rw[l_is_a] at hrl
  have : collinear p q r := by
    simp[collinear]
    exists a
    apply And.intro
    . simp
    . apply And.intro
      . simp
      . assumption
  contradiction
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
have : ¬ collinear a b c := by
  rw[a_is_q_t, c_is_r_t, connectingLine_comm]
  apply dual_triangle
  assumption
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
this : ¬collinear a b c
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
this : ¬collinear a b c
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ s)
Tactic:
assumption
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
⊢ q ≠ t
Tactic:
intro h
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ False

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ False
Tactic:
have : collinear q r s := by
  simp[collinear]
  rw[h]
  exists c
  apply And.intro
  . simp
  . apply And.intro
    . simp
    . simp
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
this : collinear q r s
⊢ False

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
this : collinear q r s
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ collinear q r s
Tactic:
simp[collinear]
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ ∃ l, q ∈ l ∧ r ∈ l ∧ s ∈ l

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ ∃ l, q ∈ l ∧ r ∈ l ∧ s ∈ l
Tactic:
rw[h]
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ ∃ l, t ∈ l ∧ r ∈ l ∧ s ∈ l

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ ∃ l, t ∈ l ∧ r ∈ l ∧ s ∈ l
Tactic:
exists c
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ t ∈ c ∧ r ∈ c ∧ s ∈ c

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ t ∈ c ∧ r ∈ c ∧ s ∈ c
Tactic:
apply And.intro
State after:
case left
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ t ∈ c

case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ r ∈ c ∧ s ∈ c

State before:
case left
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ t ∈ c

case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ r ∈ c ∧ s ∈ c
Tactic:
. simp
State after:
case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ r ∈ c ∧ s ∈ c

State before:
case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
h : q = t
⊢ r ∈ c ∧ s ∈ c
Tactic:
. apply And.intro
  . simp
  . simp
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
⊢ r ≠ t
Tactic:
intro h
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ False

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ False
Tactic:
have : collinear p q r := by
 simp[collinear]
 rw[h]
 exists a
 apply And.intro
 . simp
 . apply And.intro
   . simp
   . simp
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
this : collinear p q r
⊢ False

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
this : collinear p q r
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ collinear p q r
Tactic:
simp[collinear]
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ ∃ l, p ∈ l ∧ q ∈ l ∧ r ∈ l

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ ∃ l, p ∈ l ∧ q ∈ l ∧ r ∈ l
Tactic:
rw[h]
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ ∃ l, p ∈ l ∧ q ∈ l ∧ t ∈ l

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ ∃ l, p ∈ l ∧ q ∈ l ∧ t ∈ l
Tactic:
exists a
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ p ∈ a ∧ q ∈ a ∧ t ∈ a

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ p ∈ a ∧ q ∈ a ∧ t ∈ a
Tactic:
apply And.intro
State after:
case left
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ p ∈ a

case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ q ∈ a ∧ t ∈ a

State before:
case left
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ p ∈ a

case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ q ∈ a ∧ t ∈ a
Tactic:
. simp
State after:
case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ q ∈ a ∧ t ∈ a

State before:
case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
h : r = t
⊢ q ∈ a ∧ t ∈ a
Tactic:
. apply And.intro
  . simp
  . simp
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ a = q ⊔ t
Tactic:
apply connectingLine_uniq
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ q ≠ t

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ q ∈ a

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ t ∈ a

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ q ≠ t

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ q ∈ a

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ t ∈ a
Tactic:
. assumption
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ q ∈ a

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ t ∈ a

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ q ∈ a

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ t ∈ a
Tactic:
. simp
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ t ∈ a

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
⊢ t ∈ a
Tactic:
. simp
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ c = r ⊔ t
Tactic:
apply connectingLine_uniq
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ r ≠ t

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ r ∈ c

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ t ∈ c

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ r ≠ t

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ r ∈ c

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ t ∈ c
Tactic:
. assumption
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ r ∈ c

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ t ∈ c

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ r ∈ c

case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ t ∈ c
Tactic:
. simp
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ t ∈ c

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
⊢ t ∈ c
Tactic:
. simp
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
⊢ ¬collinear t q r
Tactic:
simp[collinear]
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
⊢ ∀ (x : line P), (p ⊔ q) ⊓ (r ⊔ s) ∈ x → q ∈ x → ¬r ∈ x

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
⊢ ∀ (x : line P), (p ⊔ q) ⊓ (r ⊔ s) ∈ x → q ∈ x → ¬r ∈ x
Tactic:
intro l htl hql hrl
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
⊢ False

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
⊢ False
Tactic:
have l_is_a : l = a := by
  rw[a_is_q_t]
  apply connectingLine_uniq <;> assumption
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
l_is_a : l = a
⊢ False

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
l_is_a : l = a
⊢ False
Tactic:
rw[l_is_a] at hrl
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ False

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ False
Tactic:
have : collinear p q r := by
  simp[collinear]
  exists a
  apply And.intro
  . simp
  . apply And.intro
    . simp
    . assumption
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
this : collinear p q r
⊢ False

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
this : collinear p q r
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
⊢ l = a
Tactic:
rw[a_is_q_t]
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
⊢ l = q ⊔ t

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
⊢ l = q ⊔ t
Tactic:
apply connectingLine_uniq <;> assumption
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ collinear p q r
Tactic:
simp[collinear]
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ ∃ l, p ∈ l ∧ q ∈ l ∧ r ∈ l

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ ∃ l, p ∈ l ∧ q ∈ l ∧ r ∈ l
Tactic:
exists a
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ p ∈ a ∧ q ∈ a ∧ r ∈ a

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ p ∈ a ∧ q ∈ a ∧ r ∈ a
Tactic:
apply And.intro
State after:
case left
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ p ∈ a

case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ q ∈ a ∧ r ∈ a

State before:
case left
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ p ∈ a

case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ q ∈ a ∧ r ∈ a
Tactic:
. simp
State after:
case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ q ∈ a ∧ r ∈ a

State before:
case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ q ∈ a ∧ r ∈ a
Tactic:
. apply And.intro
  . simp
  . assumption
State after:
no goals

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
⊢ ¬collinear a b c
Tactic:
rw[a_is_q_t, c_is_r_t, connectingLine_comm]
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
⊢ ¬collinear (t ⊔ q) b (r ⊔ t)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
⊢ ¬collinear (t ⊔ q) b (r ⊔ t)
Tactic:
apply dual_triangle
State after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
⊢ ¬collinear t q r

State before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
left✝¹ : ¬collinear p q s
left✝ : ¬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
t : P := a ⊓ c
t_is_not_q : q ≠ t
t_is_not_r : r ≠ t
a_is_q_t : a = q ⊔ t
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
⊢ ¬collinear t q r
Tactic:
assumption
State after:
no goals