Theorem: ProjectivePlane.triangle_lines_unequal (ProjectivePlane.lean)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ ¬collinear p q r → p ⊔ q ≠ q ⊔ r ∧ p ⊔ q ≠ r ⊔ p ∧ q ⊔ r ≠ r ⊔ p
Tactic:
intro hnc
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
hnc : ¬collinear p q r
⊢ p ⊔ q ≠ q ⊔ r ∧ p ⊔ q ≠ r ⊔ p ∧ q ⊔ r ≠ r ⊔ p

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
hnc : ¬collinear p q r
⊢ p ⊔ q ≠ q ⊔ r ∧ p ⊔ q ≠ r ⊔ p ∧ q ⊔ r ≠ r ⊔ p
Tactic:
apply And.intro
State after:
case left
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
hnc : ¬collinear p q r
⊢ p ⊔ q ≠ q ⊔ r

case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
hnc : ¬collinear p q r
⊢ p ⊔ q ≠ r ⊔ p ∧ q ⊔ r ≠ r ⊔ p

State before:
case left
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
hnc : ¬collinear p q r
⊢ p ⊔ q ≠ q ⊔ r

case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
hnc : ¬collinear p q r
⊢ p ⊔ q ≠ r ⊔ p ∧ q ⊔ r ≠ r ⊔ p
Tactic:
. intro h
  simp[collinear] at hnc
  apply hnc (p ⊔ q)
  . simp
  . simp
  . simp[h]
State after:
case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
hnc : ¬collinear p q r
⊢ p ⊔ q ≠ r ⊔ p ∧ q ⊔ r ≠ r ⊔ p

State before:
case right
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
hnc : ¬collinear p q r
⊢ p ⊔ q ≠ r ⊔ p ∧ q ⊔ r ≠ r ⊔ p
Tactic:
. apply And.intro
  . intro h
    simp[collinear] at hnc
    apply (hnc (p ⊔ q))
    . simp
    . simp
    . simp[h]
  . intro h
    simp[collinear] at hnc
    apply (hnc (q ⊔ r))
    . simp[h]
    . simp
    . simp[h]
State after:
no goals