Access functions on rationals and reals

Stream: general

[Philipp Weisang]

As and exercise, I want to show that the rationals and reals are fields.
The field class looks like this:

class field (α : Type) where
  add : α → α → α
  zero : α
  inv1 : α → α
  add_assoc : ∀ x y z : α, add (add x y) z = add x (add y z)
  add_comm : ∀ x y : α, add x y = add y x
  zero_add : ∀ x : α, add zero x = x
  add_zero : ∀ x : α, add x zero = x
  inv_add : ∀ x : α, add (inv1 x) x = zero
  add_inv : ∀ x : α, add x (inv1 x) = zero

  mul : α → α → α
  one : α
  inv2 : α -> α
  mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
  mul_comm  : ∀ x y : α, mul x y = mul y x
  one_mul : ∀ x : α, mul one x = x
  mul_one : ∀ x : α, mul x one = x
  inv_mul : ∀ x : α,  x ≠ zero -> mul (inv2 x) x = one

  dist : ∀ x y z : α, mul x (add y z) = add (mul x y) (mul x z)

I want to prove instance : field ℚ where ...

I have tried to access addition functions on the rationals in the following ways (as suggested by Claude and ChatGpt):
  add := Rat.add
add := fun a b => a + b
add := (· + ·)

If anyone knows how to do this I'd appreciate some help.

[Etienne Marion]

Can you provide a #mwe? Also please use #backticks to display code (those blue texts are links that you can follow for explanations).

[Philipp Weisang]

For mwe, I am not quite sure because i don't know how the imports behave between different folders.
The code is in a folder in a mathlib project without any other imports.

[Vlad Tsyrklevich]

Hover your mouse over the code above in Zulip, you will see a two boxes pop up in the top-right. One will take you to Lean playground where you can test it (This is why #backticks / #mwe are nice, they allow people to quickly test and help you rather than slowly reconstructing your environment.)

[Philipp Weisang]

Understood, thanks.
Is there anything else you need to know for mwe?
I think there should not be any relevant import, open, universe, and variable things.
Just a plain mathlib project.
But i did import a couple of things in another folder in case that is relevant.

[Eric Wieser]

For a mwe we need code that runs in the Lean playground, which Vlad explains how to access above

[Philipp Weisang]

import Mathlib
class field (α : Type) where
add : α → α → α
zero : α
inv1 : α → α
add_assoc : ∀ x y z : α, add (add x y) z = add x (add y z)
add_comm : ∀ x y : α, add x y = add y x
zero_add : ∀ x : α, add zero x = x
add_zero : ∀ x : α, add x zero = x
inv_add : ∀ x : α, add (inv1 x) x = zero
add_inv : ∀ x : α, add x (inv1 x) = zero

mul : α → α → α
one : α
inv2 : α -> α
mul_assoc : ∀ x y z : α, mul (mul x y) z = mul x (mul y z)
mul_comm : ∀ x y : α, mul x y = mul y x
one_mul : ∀ x : α, mul one x = x
mul_one : ∀ x : α, mul x one = x
inv_mul : ∀ x : α, x ≠ zero -> mul (inv2 x) x = one

dist : ∀ x y z : α, mul x (add y z) = add (mul x y) (mul x z)

This seems to run in the playground (had to adjust spacing for some reason).

[Edward van de Meent]

it runs, yes... but there are at least two typos (which lean happily misinterprets as intentional)

[Philipp Weisang]

Fixed those

[Eric Wieser]

This isn't a mwe, because your question is about providing an instance, but your mwe does not include that question

[Eric Wieser]

It's ok if there are errors in the lines you're asking about

[Philipp Weisang]

I don't quite know what you mean.
I want to prove

instance : field \Q

given my definition of the field class.
Should I have included that line in the code I shared?

[Yan Yablonovskiy 🇺🇦]

If you just want a solution

instance: field ℚ := by
  apply field.mk (add := (. + .)) (zero := (0 : ℚ)) (mul := (. * .)) (one := (1 : ℚ))
    (inv1 := fun x ↦ -x) (inv2 := fun x ↦ x⁻¹) (add_assoc := Rat.add_assoc) (inv_mul := by grind)
  <;> simp [Rat.add_comm,Rat.mul_comm,Rat.mul_add]; grind

[Philipp Weisang]

Thank you. That works at least in the playground.
For some reason it is still not working in the project but I'll figure that out some other time.