Theorem: ProjectivePlane.intersectionPoint_comm (ProjectivePlane.lean)

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

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

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

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

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