# Zulip Chat Archive

## Stream: new members

### Topic: Working with fields

#### Leo Shine (Oct 28 2023 at 20:30):

Hello,

I'm trying to write some lean code to work with general fields, and I want to show a goal like

x * b * 2⁻¹ * 2 = x * b

I know that 2 is not equal to zero (as a hypothesis), how do I pass this information into the simplifier or whatever so that it is able to use that fact to prove this seemingly trivial fact?

#### Alex J. Best (Oct 28 2023 at 20:49):

try `field_simp [name_of_hypothesis]`

with the name of the hypothesis that 2 is not zero in your field

#### Leo Shine (Oct 28 2023 at 20:59):

Yes that's great thanks

Is there a way of making it work out things like 4 ≠ 0 based off 2 ≠ 0 automatically?

Also is there a way of getting good error messages when you accidentally write the 2 ≠ 0 hypothesis without saying this is about the particular field you are working over?

This isn't particularly helpful:

type mismatch

hnotorder2

has type

2 ≠ 0 : Prop

but is expected to have type

2 ≠ 0 : Prop

#### Kevin Buzzard (Oct 28 2023 at 21:13):

The best way to ask a question to this community is to give a #mwe . Also note #backticks . From what you say, the issue is that those are different 2s (one is probably a natural) but you can just hover over a 2 or a \ne to see the types of the terms involved.

#### Kevin Buzzard (Oct 28 2023 at 21:15):

As for proving 4!=0 I would rewrite 4 as 2*2 and then use `exact?`

. If you want a more specific answer then please ask the question again but this time in the form "here is some compiling code with a `sorry`

, can you suggest various ways of filling it in?"

#### Leo Shine (Oct 28 2023 at 21:18):

Thanks didnt realise you could get the details of the actual types of the numbers by hovering

I have managed to prove 4!=0, using mul_ne_zero, I guess I don't have a great grasp of which things Lean + tactics can do by default or whether I just have to prove things like 4!=0 given 2!=0 when they come up

#### Kevin Buzzard (Oct 28 2023 at 22:03):

Yeah. Step one is to figure out the difference between a theorem (which you typically `rw`

or `apply`

) and a tactic, and step 1' is to understand that there are only about 50 commonly used tactics and about 10^5 theorems. Step 2 is to get the hang of what the 50 or so tactics do, and this takes time: you just learn by doing, really. The `norm_num`

tactic may or may not prove 4!=0 but that all depends on how you've told it 2!=0 (hence the importance of #mwe s). The `ring`

tactic won't, because of $\Z/4\Z$. You might get somewhere with `nlinarith`

but again it might depend on exactly how you've said that the characteristic isn't 2. etc etc.

#### Miguel Marco (Oct 28 2023 at 22:06):

I have been working precisely on a tactic for this kind of things. This is what I have so far:

```
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Field.Basic
import Mathlib.Algebra.GroupWithZero.Units.Lemmas
import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib
open Lean Meta Elab Tactic Parser Tactic
/-!
# `unify_denoms` tactic
Tactic to clear denominators in algebraic expressions, extends `field_simp` using
rules that require denominators to be nonzero. The corresponding hypotheses are
added as new goals.
-/
/--
The `unify_denoms` tactic tries to unify denominators in expressions, adding the
necessary hypothesis aabout denominators being nonzero as new goals.
--/
syntax (name := unify_denoms) "unify_denoms" (location)? : tactic
macro_rules
| `(tactic | unify_denoms $[at $location]?) => `(tactic |(
field_simp $[at $location]?
repeat (first
| (rw [← one_div] $[at $location]?)
| (rw [div_add_div] $[at $location]?)
| (rw [div_sub_div] $[at $location]?)
| (rw [add_div'] $[at $location]?)
| (rw [div_add'] $[at $location]?)
| (rw [div_sub'] $[at $location]?)
| (rw [sub_div'] $[at $location]?)
| (rw [mul_div_mul_right] $[at $location]?)
| (rw [mul_div_mul_left] $[at $location]?) )))
/--
The `unify_denoms'` tactic extends `unify_denoms` to work also on
(in)equalities.
--/
syntax (name := unify_denoms') "unify_denoms'" (location)?: tactic
macro_rules
| `(tactic | unify_denoms' $[at $location]?) => `(tactic |(
unify_denoms $[at $location]?
repeat (first
| (rw [div_eq_div_iff] $[at $location]?)
| (rw [div_le_div_iff] $[at $location]?)
| (rw [div_lt_div_iff] $[at $location]?)
| (rw [div_eq_iff] $[at $location]?)
| (rw [div_le_iff] $[at $location]?)
| (rw [div_lt_iff] $[at $location]?)
| (rw [eq_div_iff] $[at $location]?)
| (rw [le_div_iff] $[at $location]?)
| (rw [lt_div_iff] $[at $location]?) )))
```

In your example, if you apply it like this:

```
example (X : Type) [Field X] (x b : X) : x * b * 2⁻¹ * 2 = x * b := by
unify_denoms'
```

it will automatically solve the goal, at the price of leaving you with the task of proving a new goal consisting on `2 ≠ 0`

#### Miguel Marco (Oct 28 2023 at 22:11):

To be more precise, what is needed in your example is just the rule `div_eq_iff`

. So this works too:

```
example (X : Type) [Field X] (x b : X) : x * b * 2⁻¹ * 2 = x * b := by
field_simp
rw [div_eq_iff]
```

my tactic just tries a bunch of rules for similar cases.

#### Eric Wieser (Oct 28 2023 at 22:41):

Leo Shine said:

Yes that's great thanks

Is there a way of making it work out things like 4 ≠ 0 based off 2 ≠ 0 automatically?

The `polyrith`

tactic can do this

#### Kevin Buzzard (Oct 28 2023 at 22:46):

Even though it's false for Z/4Z? Does `polyrith`

behave differently with fields?

#### Eric Wieser (Oct 28 2023 at 23:07):

Whoops, I'm thinking of it solving `4 = 0`

from `2 = 0`

#### Miguel Marco (Oct 28 2023 at 23:26):

I guess `cast_eq_zero_iff`

or `charP_iff`

would be the relevant rules.

Last updated: Dec 20 2023 at 11:08 UTC