Theorem: ProjectivePlane.intersectionPoint_uniq (ProjectivePlane.lean)

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
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

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
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

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
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

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
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

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
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

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

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

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

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

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