# Zulip Chat Archive

## Stream: maths

### Topic: lift from subring to field

#### Ashvni Narayanan (Jul 09 2020 at 02:12):

```
K: Type u_1
_inst_4: field K
_inst_5: discrete_valuation_field K
S: ideal ↥(val_ring K)
h: ¬S = ⊥
x: ↥(val_ring K)
a: x ∈ S
h: ¬x = 0
h_1: ↑x = 0
⊢ x = 0
```

val_ring K is a subring of K. As far as I understand, I am given that the lift of x to K is 0, and need to prove that x = 0. I don't know how to proceed.

Any help is appreciated, thank you!

#### Mario Carneiro (Jul 09 2020 at 02:14):

Does `exact subtype.eq h_1`

work?

#### Ashvni Narayanan (Jul 09 2020 at 02:15):

Yes, that works!

#### Jalex Stark (Jul 09 2020 at 02:21):

does `assumption_mod_cast`

work?

#### Mario Carneiro (Jul 09 2020 at 02:23):

I don't think `norm_cast`

knows about subtype casts

#### Ashvni Narayanan (Jul 09 2020 at 02:27):

Jalex Stark said:

does

`assumption_mod_cast`

work?

No, it gives the error

```
assumption_mod_cast failed:
exact tactic failed, type mismatch, given expression has type
Type u_1
but is expected to have type
x = 0
```

#### Adam Topaz (Jul 09 2020 at 02:28):

Alternatively, you can rewrite using h_1 (probably after doing a case split on x)

#### Ashvni Narayanan (Jul 09 2020 at 02:39):

I am now having the same problem, with \le :

```
K: Type u_1
_inst_4: field K
_inst_5: discrete_valuation_field K
x: ↥(val_ring K)
⊢ 0 ≤ v ↑x
```

The definition of val_ring K is:

```
def val_ring (K : Type*) [field K] [discrete_valuation_field K] := { x : K | 0 ≤ v x }
```

Any help is appreciated, thank you!

#### Adam Topaz (Jul 09 2020 at 02:40):

Try the same thing -- split x, and see what you get.

#### Adam Topaz (Jul 09 2020 at 02:41):

(I think `exact x.2`

should take care of this in one line.)

#### Ashvni Narayanan (Jul 09 2020 at 02:47):

Ah ok, cases x does it, as does exact x.2 . Thank you!

#### Johan Commelin (Jul 09 2020 at 04:19):

Adam Topaz said:

(I think

`exact x.2`

should take care of this in one line.)

@Ashvni Narayanan This is (strictly speaking) leaking an implementation detail. Hence it is encouraged to prove a lemma `val_ring.zero_le`

as one of the first things after you define `val_ring`

. It is part of the basic API.

#### Ashvni Narayanan (Jul 09 2020 at 14:12):

Ok sure. Thank you!

Last updated: May 06 2021 at 19:30 UTC