prove 2 points collinear using `collinear_pair`

Stream: mathlib4

[max]

hello i am quite new to mathlib and lean. i have this code that I have been trying to make work but cant.

I found the theorem collinear_pair and I would like to just copy the proposition and then use collinear_pair to prove it. I don't know why this doesn't work, since I copied all the state that is shown in mathlib\Mathlib\LinearAlgebra\AffineSpace\FiniteDimensional.lean

It seems so hard to just reuse an existing theorem, trying to provide the other info like k, V and P to collinear_pair doesn't seem to work either. The goal state just remains as **⊢** Collinear k {a, b}

variable (k : Type*) {V : Type*} {P : Type*}
variable {ι : Type*}

open AffineSubspace Module

variable [DivisionRing k] [AddCommGroup V] [Module k V] [AffineSpace V P]

variable (a b : P)
-- theorem collinear_pair (p₁ p₂ : P) : Collinear k ({p₁, p₂} : Set P) := by
theorem ab_collinear (a b : P) : Collinear k ({a, b} : Set P) := by
  rw [collinear_pair a b]

[Yaël Dillies]

rw is for rewriting with equalities. Here collinear_pair does not state an equality.

[max]

when i try theorem ab_collinear (a b : P) : Collinear k ({a, b} : Set P) := collinear_pair k a b my VSCode still shows the goal state as

k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
a b : P
⊢ P

[Yaël Dillies]

Where is your cursor? Is it on b by any chance? and does it say "Expected type" in the infoview?

[Yaël Dillies]

If so, that's just Lean telling you that the variable you are hovering is of type P

[max]

image.png
my cursor is at the end of the line

[max]

oh, i was expecting no goals. so that means that I successfully reused collinear_pair

[Etienne Marion]

The no goals only appear if you are in tactic mode, i.e. you started with by

[Yaël Dillies]

Yes, it says "Expected type" above what you called the goal state in your previous message

[max]

how do I know im done then? just the lack of error message?

[Yaël Dillies]

Yes. If the underline is too weak of a signal for you, I suggest you install the VSCode extension called "Error Lens". It is life-changing.

[max]

okay thank you! i remember a while ago there was like a :tada:

[Yaël Dillies]

Yes, that was in Lean 3. Sadly, doing maths in Lean 4 provides you with much less dopamine

[Andrew Yang]

Yaël Dillies said:

Yes. If the underline is too weak of a signal for you, I suggest you install the VSCode extension called "Error Lens". It is life-changing.

I just installed it and it changed my life.

[Patrick Massot]

Note: the tada emoji is still there in lean.nvim, so you can have a huge win by dropping VSCode in favor of neovim and get back your dopamine.

[Kevin Buzzard]

It's certainly possible to put it back in VS Code, but wasn't the issue that it was being displayed when the goals weren't accomplished? Is that also the case in nvim?

[Julian Berman]

Yeah, we don't do anything special there to "fix" that possibility, we just act optimistic I suppose that in preferring the frequent dopamine vs. occasional disappointment. (Actually I just said "let's leave it as is and see if anyone complains", and no one did so far.)

[Kevin Buzzard]

Yeah the argument for removing the tada was that it was confusing beginners (who might think "I see a tada therefore I must be done, even though there are errors everywhere"), but it's unlikely that someone completely clueless will be using nvim!