## 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?

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):

(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.