Theorem: ProjectivePlane.connectingLine_uniq (ProjectivePlane.lean)

State before:
P L : Type
p q r s : P
inst✝ : ProjectivePlane P
⊢ ∀ {p q : P} {l : line P}, p ≠ q → p ∈ l → q ∈ l → l = p ⊔ q
Tactic:
intro p q l hpq hpl hql
State after:
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
⊢ l = p ⊔ q

State before:
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
⊢ l = p ⊔ q
Tactic:
let m := p ⊔ q
State after:
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
⊢ l = p ⊔ q

State before:
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
⊢ l = p ⊔ q
Tactic:
have hpm : p ∈ m := by simp
State after:
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
⊢ l = p ⊔ q

State before:
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
⊢ l = p ⊔ q
Tactic:
have hqm : q ∈ m := by simp
State after:
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
⊢ l = p ⊔ q

State before:
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
⊢ l = p ⊔ q
Tactic:
have h : p = q ∨ l = m := point_line_uniq hpl hql hpm hqm
State after:
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 : p = q ∨ l = m
⊢ l = p ⊔ q

State before:
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 : p = q ∨ l = m
⊢ l = p ⊔ q
Tactic:
cases h with
| inl hpq' => contradiction
| inr h' => assumption
State after:
no goals

State before:
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
⊢ p ∈ m
Tactic:
simp
State after:
no goals

State before:
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
⊢ q ∈ m
Tactic:
simp
State after:
no goals

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
State after:
no goals

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
State after:
no goals