Defining Subgroups (Problems with "set")

Stream: lean4

[Hannah Santos]

I've been trying to write and prove some things about Groups and whatnot, but I'm on a standstill with a little problem that showed up on the Subgroup definition. I'm studying through a Report I found that shows some definitions and how to write them on Lean4, so I'm confused why it's not working.

------------------------------------------------
-- Group Definition :
------------------------------------------------

class has_Op (α : Type u) where op : α × α → α
notation:65 a:65 " ⋆ " b:66 => has_Op.op ⟨a, b⟩
open has_Op

class Semigroup (α : Type u) extends has_Op α where
  Op_Ass : ∀ (a b c : α), a ⋆ b ⋆ c = a ⋆ (b ⋆ c)
open Semigroup

class has_Id (α : Type u) where e : α
open has_Id

class Monoid (α : Type u) extends Semigroup α, has_Id α where
  Id_Op : ∀ (a : α), e ⋆ a = a
  Op_Id : ∀ (a : α), a ⋆ e = a
open Monoid

class has_Inv (α : Type u) where inv : α → α
postfix:max "⁻¹"  => has_Inv.inv
open has_Inv

class Group (α : Type u) extends Monoid α, has_Inv α where
  Op_Inv_L : ∀ (a : α), a⁻¹ ⋆ a = e
  Op_Inv_R : ∀ (a : α), a ⋆ a⁻¹ = e
open Group

def invG [Group G] (x a : G): Prop :=
  x ⋆ a = e ∧ a ⋆ x = e
notation:65 a:65 " é o inverso de " b:66 => invG a b

def idG [Group G] (x a : G) : Prop :=
  a ⋆ x = a ∧ x ⋆ a = a
notation:65 x:65 " é a identidade no " a:66 => idG x a

------------------------------------------------
-- Subgroups :
------------------------------------------------

class Subgroup [Group G] (S : set G) : Prop :=
  Op_in : ∀ (a b : G), a ∈ S ∧ b ∈ S → (a ⋆ b) ∈ S
  Id_in : (e : G) ∈ S
  Inv_in : ∀ (a : G), a ∈ S → (a⁻¹) ∈ S


/-
Group.lean:284:35
Expected type
G : Type ?u.89434
inst✝ : Group G
⊢ Type ?u.89434
Messages (1)
Group.lean:284:30
type expected, got
  (set G : ?m.89440 PUnit)
All Messages (1)
-/

[Martin Dvořák]

Just to be on the same page, you want to define everything independently of Mathlib?

[Hannah Santos]

Yep.

[Martin Dvořák]

Do you also want to define docs#Set yourself? Note that the Mathlib one is spelled with capital 'S'.

[Hannah Santos]

I also thought it was with a capital S, but it looks like set is also a thing?

[Hannah Santos]

Not sure myself.

[Martin Dvořák]

I'm pretty sure that set (all lowercase) is a verb.

[Hannah Santos]

So.... this is a problem?
Report I read

[Martin Dvořák]

This looks like Lean 3.

[Martin Dvořák]

Just add import Mathlib.Init.Set on your first line and change set to Set in your code.

[Hannah Santos]

Oh!

[Hannah Santos]

It was working so well that I thought it was Lean4.

[Hannah Santos]

Thank you.

[Kevin Buzzard]

I would recommend that you set_option autoImplicit false because if you have this set to true and you start using stuff like set believing that it's a thing in Lean 4, then Lean 4 will happily make it a thing, which is probably not what you want.