How to change notation in group

Stream: lean4

[gengenshin]

Now I have to proof this thing as shown

case a
f : LinearFractionalTransformation
⊢ 1.a * f.a + 1.b * f.c = f.a

I have define one in group as id

def id : LinearFractionalTransformation where
  a := 1
  b := 0
  c := 0
  d := 1
  determinant_ne_zero := by simp

and

one := id

I just want to change this 1 notation into id, and it will be trivial.

[Marcus Rossel]

Could you please turn your code snippets into a #mwe? That makes it much easier for people to understand your question.

[gengenshin]

Marcus Rossel said:

Could you please turn your code snippets into a #mwe? That makes it much easier for people to understand your question.

sorry, changed.

[Kevin Buzzard]

Can you click on the #mwe link and then change it into an actual #mwe, using #backticks rather than screenshots?

[gengenshin]

Kevin Buzzard said:

Can you click on the #mwe link and then change it into an actual #mwe, using #backticks rather than screenshots?

sure, and can you share me some insights?

[Kevin Buzzard]

Right now I have no understanding of the question because I don't know the type of any of the terms because you're not asking the question in a way which gives enough information for it to be answered.

You have succeeded in asking a good question when I can just click on the link on your code snippet and it runs without any errors in the lean 4 web editor

[Robert Maxton]

Without more information it's hard to guess, but:

• Presumably you have an instance of One LinearFractionalTransformation somewhere; adding @[simps] to it might let you solve your proof with simp
• Alternatively, unfold_projs might do what you want.