lift from subring to field

Stream: maths

[Ashvni Narayanan]

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]

Does exact subtype.eq h_1 work?

[Ashvni Narayanan]

Yes, that works!

[Jalex Stark]

does assumption_mod_cast work?

[Mario Carneiro]

I don't think norm_cast knows about subtype casts

[Ashvni Narayanan]

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]

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

[Ashvni Narayanan]

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]

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

[Adam Topaz]

(I think exact x.2 should take care of this in one line.)

[Ashvni Narayanan]

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

[Johan Commelin]

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]

Ok sure. Thank you!