Theorem: ProjectivePlane.connectingLine_comm (ProjectivePlane.lean)

State before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
h : q = p
⊢ p ⊔ q = q ⊔ p
Tactic:
rw[h]
State after:
no goals

State before:
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
hpq : q ≠ p
⊢ p ⊔ q = q ⊔ p
Tactic:
apply connectingLine_uniq <;> (simp ; try assumption)
State after:
no goals

State before:
case a
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
hpq : q ≠ p
⊢ p ∈ p ⊔ q
Tactic:
simp
State after:
no goals

State before:
case a
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
hpq : q ≠ p
⊢ ¬q = p
Tactic:
try assumption
State after:
no goals

State before:
case a
P L : Type
p✝ q✝ r s : P
inst✝ : ProjectivePlane P
p q : P
hpq : q ≠ p
⊢ ¬q = p
Tactic:
assumption
State after:
no goals