Split into two case

Stream: new members

[abdullah uyu]

I have the following setup. I want to proceed with splitting the goal into two cases where $b = c$ and $b \neq c$. How can I do that?

import Mathlib.Logic.Basic

variable (Point : Type)
variable (collinear : Point -> Point -> Point -> Prop)

#check Point
#check collinear

axiom l1 (a b : Point) : collinear a b a
axiom l2 (a b p q : Point) : collinear a p q → collinear b p q → p ≠ q → collinear a b p
axiom l3 (a b c d p: Point) : collinear p a b → collinear p c d →
∃ q: Point , collinear q a c ∧ collinear q b d

theorem switch_two_three (a b c: Point) : collinear a b c → collinear a c b := by
intro

[Ruben Van de Velde]

by_cases h: b = c

[abdullah uyu]

Thank you very much.

[Yaël Dillies]

Even better: obtain rfl | hbc := eq_or_ne b c

[abdullah uyu]

Well, that worked quite nice:

theorem switch_two_three (a b c: Point) : collinear a b c → collinear a c b := by
intro col
obtain rfl | hbc := eq_or_ne b c
exact col
apply l2 Point collinear a c b c
exact col
apply l1 Point collinear c b
exact hbc

With that, I have proved my first theorem! This feels good :) I have another question though, why did I have to apply l2 that way? I would have expected something like l2 a c b c.

[Patrick Massot]

Because you used parenthesis in your variables so they are explicit variables.

[Patrick Massot]

Try with curly braces instead.

[abdullah uyu]

Brilliant! Thank you :)