Error in VSCode

Stream: lean4

[Valéry Croizier]

Hi, VSCode marks "h.left a b" line 22 a an error and it looks like a a bug because highlighting is messed up after that. My code may be wrong too.

class Preorder (α : Type u) extends LE α where
  le_refl  (a : α) : a ≤ a
  le_trans {a b c : α} : a ≤ b → b ≤ c → a ≤ c

def Monotone [Preorder α] [Preorder β] (f : α → β) :=
  ∀ {a b}, a ≤ b → f a ≤ f b

def Connection [Preorder α] [Preorder β] (f : α → β) (g : β → α) :=
  ∀ {a b}, f a ≤ b ↔ a ≤ g b

def MonotoneLoop [Preorder α] [Preorder β] (f : α → β) (g : β → α) :=
  ∀ {a b}, a ≤ g (f a) ∧ f (g b) ≤ b

theorem t_1_107' [Preorder α] [Preorder β]
(f : α → β) (g : β → α) (m_f : Monotone f) (m_g : Monotone g) :
Connection f g ↔ MonotoneLoop f g :=
Iff.intro
  (fun h a b => And.intro
    (h.mp (Preorder.le_refl (f a)))
    (h.mpr (Preorder.le_refl (g b))))
  (fun h a b => Iff.intro
    (fun (k : f a ≤ b) => Preorder.le_trans (h.left a b) (m_g k)
    (fun (k : a ≤ g b) => Preorder.le_trans (m_f k) (h.right a b))))

[Marc Huisinga]

The highlighting is messed up because you're missing a bracket on the second to last line and the error occurs because a and b are implicit in MonotoneLoop. Making them explicit fixes it:

class Preorder (α : Type u) extends LE α where
  le_refl  (a : α) : a ≤ a
  le_trans {a b c : α} : a ≤ b → b ≤ c → a ≤ c

def Monotone [Preorder α] [Preorder β] (f : α → β) :=
  ∀ {a b}, a ≤ b → f a ≤ f b

def Connection [Preorder α] [Preorder β] (f : α → β) (g : β → α) :=
  ∀ {a b}, f a ≤ b ↔ a ≤ g b

def MonotoneLoop [Preorder α] [Preorder β] (f : α → β) (g : β → α) :=
  ∀ a b, a ≤ g (f a) ∧ f (g b) ≤ b

theorem t_1_107' [Preorder α] [Preorder β]
(f : α → β) (g : β → α) (m_f : Monotone f) (m_g : Monotone g) :
Connection f g ↔ MonotoneLoop f g :=
Iff.intro
  (fun h a b => And.intro
    (h.mp (Preorder.le_refl (f a)))
    (h.mpr (Preorder.le_refl (g b))))
  (fun h a b => Iff.intro
    (fun (k : f a ≤ b) => Preorder.le_trans ((h a b).left) (m_g k))
    (fun (k : a ≤ g b) => Preorder.le_trans (m_f k) ((h a b).right)))

[Valéry Croizier]

Thanks, that works. Is there a solution with implicit variables?

[Marc Huisinga]

Valéry Croizier said:

Thanks, that works. Is there a solution with implicit variables?

Lean won't know how to infer one of them (because either a or b does not occur in the goal when you use either .left or .right) but you can make them explicit in the place where you use the function too:

theorem t_1_107' [Preorder α] [Preorder β]
(f : α → β) (g : β → α) (m_f : Monotone f) (m_g : Monotone g) :
Connection f g ↔ MonotoneLoop f g :=
Iff.intro
  (fun h a b => And.intro
    (h.mp (Preorder.le_refl (f a)))
    (h.mpr (Preorder.le_refl (g b))))
  (fun h a b => Iff.intro
    (fun (k : f a ≤ b) => Preorder.le_trans ((@h a b).left) (m_g k))
    (fun (k : a ≤ g b) => Preorder.le_trans (m_f k) ((@h a b).right)))

or with named arguments:

theorem t_1_107' [Preorder α] [Preorder β]
(f : α → β) (g : β → α) (m_f : Monotone f) (m_g : Monotone g) :
Connection f g ↔ MonotoneLoop f g :=
Iff.intro
  (fun h a b => And.intro
    (h.mp (Preorder.le_refl (f a)))
    (h.mpr (Preorder.le_refl (g b))))
  (fun h a b => Iff.intro
    (fun (k : f a ≤ b) => Preorder.le_trans ((h (b := b)).left) (m_g k))
    (fun (k : a ≤ g b) => Preorder.le_trans (m_f k) ((h (a := a)).right)))