internlm/Lean-Github huggingface dataset:
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
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
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
triangle_tqr : ¬collinear t 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
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
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
triangle_tqr : ¬collinear t q r
this : ¬collinear a b 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
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
Proof state after:
no goals
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
⊢ q ≠ t
Tactic:
intro h
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
h : q = t
⊢ False
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
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
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
h : q = t
this : collinear q r s
⊢ False
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
h : q = t
this : collinear q r s
⊢ False
Tactic:
contradiction
Proof state after:
no goals
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
h : q = t
⊢ collinear q r s
Tactic:
simp[collinear]
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
h : q = t
⊢ ∃ l, q ∈ l ∧ r ∈ l ∧ s ∈ l
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
h : q = t
⊢ ∃ l, q ∈ l ∧ r ∈ l ∧ s ∈ l
Tactic:
rw[h]
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
h : q = t
⊢ ∃ l, t ∈ l ∧ r ∈ l ∧ s ∈ l
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
h : q = t
⊢ ∃ l, t ∈ l ∧ r ∈ l ∧ s ∈ l
Tactic:
exists 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
h : q = t
⊢ t ∈ c ∧ r ∈ c ∧ s ∈ c
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
h : q = t
⊢ t ∈ c ∧ r ∈ c ∧ s ∈ c
Tactic:
apply And.intro
Proof 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
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof state after:
no goals
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
⊢ r ≠ t
Tactic:
intro h
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
h : r = t
⊢ False
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
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
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
h : r = t
this : collinear p q r
⊢ False
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
h : r = t
this : collinear p q r
⊢ False
Tactic:
contradiction
Proof state after:
no goals
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
h : r = t
⊢ collinear p q r
Tactic:
simp[collinear]
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
h : r = t
⊢ ∃ l, p ∈ l ∧ q ∈ l ∧ r ∈ l
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
h : r = t
⊢ ∃ l, p ∈ l ∧ q ∈ l ∧ r ∈ l
Tactic:
rw[h]
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
h : r = t
⊢ ∃ l, p ∈ l ∧ q ∈ l ∧ t ∈ l
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
h : r = t
⊢ ∃ l, p ∈ l ∧ q ∈ l ∧ t ∈ l
Tactic:
exists a
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
h : r = t
⊢ p ∈ a ∧ q ∈ a ∧ t ∈ a
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
h : r = t
⊢ p ∈ a ∧ q ∈ a ∧ t ∈ a
Tactic:
apply And.intro
Proof 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
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof state after:
no goals
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 = q ⊔ t
Tactic:
apply connectingLine_uniq
Proof 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
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof state after:
no goals
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
⊢ c = r ⊔ t
Tactic:
apply connectingLine_uniq
Proof 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
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof 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
Theorem: ProjectivePlane.dual_quadrangle_part
Proof 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
Proof state after:
no goals