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 t 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
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
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
⊢ ∀ (x : line P), (p ⊔ q) ⊓ (r ⊔ s) ∈ x → q ∈ x → ¬r ∈ x
Tactic:
intro l htl hql hrl
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
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
⊢ 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
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
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
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
l_is_a : l = a
⊢ 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
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
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
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ a
l_is_a : l = a
⊢ 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
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
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
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
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
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
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_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]
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
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
⊢ l = q ⊔ t
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
l : line P
htl : (p ⊔ q) ⊓ (r ⊔ s) ∈ l
hql : q ∈ l
hrl : r ∈ l
⊢ l = q ⊔ t
Tactic:
apply connectingLine_uniq <;> 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
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]
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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_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]
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 (t ⊔ q) b (r ⊔ t)
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 (t ⊔ q) b (r ⊔ t)
Tactic:
apply dual_triangle
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
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
⊢ ¬collinear t q r
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
c_is_r_t : c = r ⊔ t
triangle_tqr : ¬collinear t q r
⊢ ¬collinear t q r
Tactic:
assumption
Proof state after:
no goals
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ isQuadrangle p q r s → isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
intro ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
Proof state after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
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
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
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
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬collinear p r s
triangle_qrs : ¬collinear q r s
a : line P := p ⊔ q
b : line P := q ⊔ r
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
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
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
let d := s ⊔ p
Proof state after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
have triangle_abc : ¬ collinear a b c := by
  apply dual_quadrangle_part
  exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
Proof state after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
have triangle_abd : ¬ collinear a b d := by
  apply triangle_rotate
  apply dual_quadrangle_part
  apply quadrangle_rotate
  apply quadrangle_rotate
  apply quadrangle_rotate
  exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
Proof state after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
have triangle_acd : ¬ collinear a c d := by
  apply triangle_rotate
  apply triangle_rotate
  apply dual_quadrangle_part
  apply quadrangle_rotate
  apply quadrangle_rotate
  exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
Proof state after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
have triangle_bcd : ¬ collinear b c d := by
  apply dual_quadrangle_part
  apply quadrangle_rotate
  exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
Proof state after:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
triangle_bcd : ¬collinear b c d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
triangle_abd : ¬collinear a b d
triangle_acd : ¬collinear a c d
triangle_bcd : ¬collinear b c d
⊢ isQuadrangle (p ⊔ q) (q ⊔ r) (r ⊔ s) (s ⊔ p)
Tactic:
exact ⟨triangle_abc, triangle_abd, triangle_acd, triangle_bcd⟩
Proof state after:
no goals
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
⊢ ¬collinear a b c
Tactic:
apply dual_quadrangle_part
Proof state after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
⊢ isQuadrangle p q r s
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
⊢ isQuadrangle p q r s
Tactic:
exact ⟨triangle_pqr, triangle_pqs, triangle_prs, triangle_qrs⟩
Proof state after:
no goals
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ ¬collinear a b d
Tactic:
apply triangle_rotate
Proof state after:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ ¬collinear d a b
Theorem: ProjectivePlane.dual_quadrangle
Proof state before:
case a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ ¬collinear d a b
Tactic:
apply dual_quadrangle_part
Proof state after:
case a.a
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
triangle_pqr : ¬collinear p q r
triangle_pqs : ¬collinear p q s
triangle_prs : ¬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
d : line P := s ⊔ p
triangle_abc : ¬collinear a b c
⊢ isQuadrangle s p q r