internlm/Lean-Github huggingface dataset:
Theorem: ProjectivePlane.connectingLine_uniq
Proof state before:
case inl
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
hpm : p ∈ m
hqm : q ∈ m
hpq' : p = q
⊢ l = p ⊔ q
Tactic:
contradiction
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_uniq
Proof state before:
case inr
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
l : line P
hpq : p ≠ q
hpl : p ∈ l
hql : q ∈ l
m : line P := p ⊔ q
hpm : p ∈ m
hqm : q ∈ m
h' : l = m
⊢ l = p ⊔ q
Tactic:
assumption
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_comm
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
h : q = p
⊢ p ⊔ q = q ⊔ p
Tactic:
rw[h]
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_comm
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
hpq : q ≠ p
⊢ p ⊔ q = q ⊔ p
Tactic:
apply connectingLine_uniq <;> (simp ; try assumption)
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_comm
Proof state before:
case a
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
hpq : q ≠ p
⊢ p ∈ p ⊔ q
Tactic:
simp
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_comm
Proof state before:
case a
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
hpq : q ≠ p
⊢ ¬q = p
Tactic:
try assumption
Proof state after:
no goals
Theorem: ProjectivePlane.connectingLine_comm
Proof state before:
case a
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
hpq : q ≠ p
⊢ ¬q = p
Tactic:
assumption
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_left
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ ∀ (l m : line P), l ⊓ m ∈ l
Tactic:
intro l m
Proof state after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
l m : line P
⊢ l ⊓ m ∈ l
Theorem: ProjectivePlane.intersectionPoint_left
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
l m : line P
⊢ l ⊓ m ∈ l
Tactic:
exact (Exists.choose_spec (exists_intersection_point l m)).left
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_right
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ ∀ (l m : line P), l ⊓ m ∈ m
Tactic:
intro l m
Proof state after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
l m : line P
⊢ l ⊓ m ∈ m
Theorem: ProjectivePlane.intersectionPoint_right
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
l m : line P
⊢ l ⊓ m ∈ m
Tactic:
exact (Exists.choose_spec (exists_intersection_point l m)).right
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_uniq
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ ∀ {l m : line P} {p : P}, l ≠ m → p ∈ l → p ∈ m → p = l ⊓ m
Tactic:
intro l m p hlm hpl hpm
Proof state after:
P L : Type
p✝ q r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
⊢ p = l ⊓ m
Theorem: ProjectivePlane.intersectionPoint_uniq
Proof state before:
P L : Type
p✝ q r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
⊢ p = l ⊓ m
Tactic:
let q :=  l ⊓ m
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
⊢ p = l ⊓ m
Theorem: ProjectivePlane.intersectionPoint_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
⊢ p = l ⊓ m
Tactic:
have hql : q ∈ l := by simp
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
hql : q ∈ l
⊢ p = l ⊓ m
Theorem: ProjectivePlane.intersectionPoint_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
hql : q ∈ l
⊢ p = l ⊓ m
Tactic:
have hqm : q ∈ m := by simp
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
hql : q ∈ l
hqm : q ∈ m
⊢ p = l ⊓ m
Theorem: ProjectivePlane.intersectionPoint_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
hql : q ∈ l
hqm : q ∈ m
⊢ p = l ⊓ m
Tactic:
have h : p = q ∨ l = m := point_line_uniq hpl hql hpm hqm
Proof state after:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
hql : q ∈ l
hqm : q ∈ m
h : p = q ∨ l = m
⊢ p = l ⊓ m
Theorem: ProjectivePlane.intersectionPoint_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
hql : q ∈ l
hqm : q ∈ m
h : p = q ∨ l = m
⊢ p = l ⊓ m
Tactic:
cases h with
| inl h' => exact h'
| inr hlm' => contradiction
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
⊢ q ∈ l
Tactic:
simp
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_uniq
Proof state before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
hql : q ∈ l
⊢ q ∈ m
Tactic:
simp
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_uniq
Proof state before:
case inl
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
hql : q ∈ l
hqm : q ∈ m
h' : p = q
⊢ p = l ⊓ m
Tactic:
exact h'
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_uniq
Proof state before:
case inr
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
l m : line P
p : P
hlm : l ≠ m
hpl : p ∈ l
hpm : p ∈ m
q : P := l ⊓ m
hql : q ∈ l
hqm : q ∈ m
hlm' : l = m
⊢ p = l ⊓ m
Tactic:
contradiction
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_comm
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
l m : line P
h : m = l
⊢ l ⊓ m = m ⊓ l
Tactic:
rw[h]
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_comm
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
l m : line P
hpq : m ≠ l
⊢ l ⊓ m = m ⊓ l
Tactic:
apply intersectionPoint_uniq <;> (simp ; try assumption)
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_comm
Proof state before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
l m : line P
hpq : m ≠ l
⊢ l ⊓ m ∈ l
Tactic:
simp
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_comm
Proof state before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
l m : line P
hpq : m ≠ l
⊢ ¬m = l
Tactic:
try assumption
Proof state after:
no goals
Theorem: ProjectivePlane.intersectionPoint_comm
Proof state before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
l m : line P
hpq : m ≠ l
⊢ ¬m = l
Tactic:
assumption
Proof state after:
no goals
Theorem: ProjectivePlane.triangle_lines_unequal
Proof 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
Proof 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
Theorem: ProjectivePlane.triangle_lines_unequal
Proof 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
Proof 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
Theorem: ProjectivePlane.triangle_lines_unequal
Proof 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]
Proof 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
Theorem: ProjectivePlane.triangle_lines_unequal
Proof 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]
Proof state after:
no goals
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof 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)
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof 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)
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof 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)
Theorem: ProjectivePlane.dual_triangle
Proof 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]
Proof 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
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof state after:
no goals
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_triangle
Proof 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)
Proof 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
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof state after:
no goals
Theorem: ProjectivePlane.dual_triangle
Proof 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)
Proof state after:
no goals
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof state after:
no goals
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof state after:
no goals
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof state after:
no goals
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof state after:
no goals
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof state after:
no goals
Theorem: ProjectivePlane.dual_triangle
Proof 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)
Proof 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
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_triangle
Proof 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
Proof state after:
no goals
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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⟩
Proof 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)
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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)
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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)
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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)
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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)
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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)
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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)
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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)
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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)