Type error stating simple theorem

Stream: general

[Yahya Sohail]

Hi, sorry if general isn't the right place to ask for help, but I couldn't seem to find a more relevant channel. I'm new to Lean and theorem provers with type theory based logics, but am familiar with the ACL2 theorem prover and Haskell. To learn Lean, I'm attempting to formalize some theorems in Linear Algebra, following Sheldon Axler's Linear Algebra Done Right book. I am trying to prove the additive identity in a vector space is unique. I have the following definitions:

import Mathlib.Algebra.Field.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic

class AxlerField (F : Type _) extends Field F

noncomputable instance : AxlerField ℝ := { }
noncomputable instance : AxlerField ℂ := { }

class VectorSpace (F: Type u1) (V: Type u2) [AxlerField F] :=
  vec_add: V → V → V
  vec_add_comm: ∀ a b, vec_add a b = vec_add b a
  vec_add_assoc: ∀ a b c, vec_add (vec_add a b) c = vec_add a (vec_add b c)
  vec_add_ident: ∃ zero : V, ∀ v : V, vec_add v zero = v
  scalar_mult: F → V → V
  mult_ident: ∀ v, scalar_mult 1 v = v
  vec_distrib: ∀ x u v, scalar_mult x (vec_add u v) = vec_add (scalar_mult x u) (scalar_mult x v)

open VectorSpace

variable [AxlerField F] [VectorSpace F V]

theorem unique_vec_zero : ∃! zero : V, ∀ v : V, VectorSpace.vec_add v zero := by
  sorry

I am getting the following type error on the statement of that final theorem, which I don't quite understand:

application type mismatch    @vec_add v  argument    v  has type    V : Type ?u.584  but is expected to have type    Type ?u.599 : Type (?u.599 + 1)

I think this has something to do with the type of the vec_add operation not being correct? Any guidance would be appreciated.

[Ruben Van de Velde]

If you hover over it, you can see the signature is

VectorSpace.vec_add.{u1, u2} (F : Type u1) {V : Type u2} [AxlerField F] [self : VectorSpace F V] : V → V → V

[Ruben Van de Velde]

Notably, the first argument you need to give explicitly is the type F

[Yahya Sohail]

I'm not sure I am parsing that signature correctly. I think I understand why F needs to be passed (because it can't be inferred from the arguments which are all type V). What part of the signature tells me F must be passed explicitly?

[Yahya Sohail]

Passing F explicitly does fix the error. I can state the theorem as:

theorem unique_vec_zero : ∃! zero : V, ∀ v : V, VectorSpace.vec_add F v zero = v := by
  sorry

[Ruben Van de Velde]

() means explicit, {} or [] means implicit

[Yahya Sohail]

I see. Thanks!

[Yahya Sohail]

I managed to prove the theorem, and I have some questions. Here's my proof:

theorem unique_vec_zero : ∃! zero : V, ∀ v : V, VectorSpace.vec_add F v zero = v := by
  have hzero: ∃ zero : V, ∀ v : V, VectorSpace.vec_add F v zero = v := vec_add_ident
  apply Exists.elim hzero
  intros zero hvec_add_zero
  apply ExistsUnique.intro zero
  exact hvec_add_zero

  intros zero' hvec_add_zero'
  specialize hvec_add_zero zero'
  specialize hvec_add_zero' zero
  rw [vec_add_comm] at hvec_add_zero
  rw [Eq.comm] at hvec_add_zero
  apply Eq.trans hvec_add_zero hvec_add_zero'

1. The line have hzero: ∃ zero : V, ∀ v : V, VectorSpace.vec_add F v zero = v := vec_add_ident essentially restates the definition of vec_add_ident. Is there someway to perform the same operation without having to restate this?
2. Before I perform apply Exists.elim hzero, my goal looks like this:

F : Type u_2
V : Type u_1
inst✝¹ : AxlerField F
inst✝ : VectorSpace F V
hzero : ∃ zero, ∀ (v : V), vec_add F v zero = v
⊢ ∃! zero, ∀ (v : V), vec_add F v zero = v

Afterwards, the last line changes and states ∀ (a : V), (∀ (v : V), vec_add F v a = v) → ∃! zero, ∀ (v : V), vec_add F v zero = v. This doesn't seem right to me. I read the antecedent of the implication as for all a of type V, for all v of type V, vec_add F v a = v. This seems like it doesn't follow from hzero, which only says that there exists at least one such a. I think I am reading this wrong, since after doing intro, it behaved how I expected. Am I reading it wrong or am I reading it right and there is some logical justification for this?

[Yury G. Kudryashov]

Note that you still have the vector space assumption you can use to prove uniqueness.