Theorem: ProjectivePlane.dual_triangle (ProjectivePlane.lean)

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

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

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
⊢ ¬collinear p q r → ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ p)
Tactic:
intro hnc
State after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
⊢ ¬collinear (p ⊔ q) (q ⊔ r) (r ⊔ p)

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

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
⊢ ∀ (x : line (line P)), p ⊔ q ∈ x → q ⊔ r ∈ x → ¬r ⊔ p ∈ x
Tactic:
intro s hpq hqr hrp
State after:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
⊢ False

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
⊢ False
Tactic:
have hsq : s = q := by
  have diff_lines : a ≠ b := (triangle_lines_unequal hnc).left
  have hsq': s = q ∨ a = b := by
    apply point_line_uniq <;> (simp ; try assumption)
  cases hsq' with
  | inl it => exact it
  | inr not_it => contradiction
State after:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
hsq : s = q
⊢ False

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
hsq : s = q
⊢ False
Tactic:
have c : collinear p q r := by
 exists (r ⊔ p)
 rw[hsq] at hrp
 simp
 assumption
State after:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
hsq : s = q
c : collinear p q r
⊢ False

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
hsq : s = q
c : collinear p q r
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
⊢ s = q
Tactic:
have diff_lines : a ≠ b := (triangle_lines_unequal hnc).left
State after:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
diff_lines : a ≠ b
⊢ s = q

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
diff_lines : a ≠ b
⊢ s = q
Tactic:
have hsq': s = q ∨ a = b := by
  apply point_line_uniq <;> (simp ; try assumption)
State after:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
diff_lines : a ≠ b
hsq' : s = q ∨ a = b
⊢ s = q

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
diff_lines : a ≠ b
hsq' : s = q ∨ a = b
⊢ s = q
Tactic:
cases hsq' with
| inl it => exact it
| inr not_it => contradiction
State after:
no goals

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
diff_lines : a ≠ b
⊢ s = q ∨ a = b
Tactic:
apply point_line_uniq <;> (simp ; try assumption)
State after:
no goals

State before:
case a
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
diff_lines : a ≠ b
⊢ q ∈ b
Tactic:
simp
State after:
no goals

State before:
case a
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
diff_lines : a ≠ b
⊢ s ∈ q ⊔ r
Tactic:
try assumption
State after:
no goals

State before:
case a
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
diff_lines : a ≠ b
⊢ s ∈ q ⊔ r
Tactic:
assumption
State after:
no goals

State before:
case inl
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
diff_lines : a ≠ b
it : s = q
⊢ s = q
Tactic:
exact it
State after:
no goals

State before:
case inr
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
diff_lines : a ≠ b
not_it : a = b
⊢ s = q
Tactic:
contradiction
State after:
no goals

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
hsq : s = q
⊢ collinear p q r
Tactic:
exists (r ⊔ p)
State after:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
hsq : s = q
⊢ p ∈ r ⊔ p ∧ q ∈ r ⊔ p ∧ r ∈ r ⊔ p

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ s
hsq : s = q
⊢ p ∈ r ⊔ p ∧ q ∈ r ⊔ p ∧ r ∈ r ⊔ p
Tactic:
rw[hsq] at hrp
State after:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ q
hsq : s = q
⊢ p ∈ r ⊔ p ∧ q ∈ r ⊔ p ∧ r ∈ r ⊔ p

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ q
hsq : s = q
⊢ p ∈ r ⊔ p ∧ q ∈ r ⊔ p ∧ r ∈ r ⊔ p
Tactic:
simp
State after:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ q
hsq : s = q
⊢ q ∈ r ⊔ p

State before:
P L : Type
p q r s✝ : P
inst✝ : ProjectivePlane P
a : line P := p ⊔ q
b : line P := q ⊔ r
hnc : ¬collinear p q r
s : line (line P)
hpq : p ⊔ q ∈ s
hqr : q ⊔ r ∈ s
hrp : r ⊔ p ∈ q
hsq : s = q
⊢ q ∈ r ⊔ p
Tactic:
assumption
State after:
no goals