# Zulip Chat Archive

## Stream: new members

### Topic: T

#### Ashvni Narayanan (Jun 23 2020 at 21:10):

I am trying to show that, in with_top \Z , T \neq 0.

```
rw <-with_top.coe_zero,
/-apply with_top.top_ne_zero, does not work out-/
/-apply with_top.none_lt_some, does not work out -/
exfalso,
/-apply with_top.zero_lt_top, dows not work out-/
apply with_top.top_ne_coe,
```

does not work. This code gives me 3 goals,

```
⊢ ⊤ = ↑?m_2
⊢ Type ?
⊢ ?m_1
```

I don't know how to solve this. Any help is appreciated. Thank you!

#### Alex J. Best (Jun 23 2020 at 21:14):

This works:

```
example : (⊤ : with_top ℤ) ≠ 0:=
begin
rintro ⟨⟩, -- you can do intro h, then cases h, or combine this into the line here
end
```

#### Alex J. Best (Jun 23 2020 at 21:16):

The idea is that `with_top \Z`

has two constructors, one from an element of `\Z`

or `\top`

, which are then the two possible (disjoint) cases for what an element of `with_top \Z`

can be. `cases`

splits into the different possibilities for the equality, but in this case there are none, so `intro h, cases h`

does it, using `rintro`

instead is just a fancy lazy (shorter) way of doing the same thing.

#### Ashvni Narayanan (Jun 23 2020 at 21:23):

Is there a way of making cases for a goal?

#### Alex J. Best (Jun 23 2020 at 21:25):

Can you give an example?

#### Anatole Dedecker (Jun 23 2020 at 21:26):

I think what you want is `split`

, but not sure of what you're looking for

#### Ashvni Narayanan (Jun 23 2020 at 21:27):

That does not seem to be working out :(

#### Bryan Gin-ge Chen (Jun 23 2020 at 21:28):

#mwe ?

#### Ashvni Narayanan (Jun 23 2020 at 21:32):

```
import ring_theory.ideals
import ring_theory.principal_ideal_domain
import ring_theory.localization
universe u
noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(val : K -> with_top ℤ )
(mul : ∀ (x y : K), val(x*y) = val(x) + val(y) )
(add : ∀ (x y : K), val(x + y) ≥ min (val(x)) (val(y)) )
(non_zero : ∀ (x : K), val(x) = ⊤ ↔ x = 0 )
namespace discrete_valuation_field
definition discrete_valuation_field.valuation (K : Type*) [field K] [ discrete_valuation_field K ] : K -> with_top ℤ := discrete_valuation_field.val
variables {K : Type*} [field K] [discrete_valuation_field K]
lemma with_top.cases (a : with_top ℤ) : a = ⊤ ∨ ∃ n : ℤ, a = n :=
begin
cases a with n,
{ -- a = ⊤ case
left,
refl, -- true by definition
},
{ -- ℤ case
right,
use n,
refl, -- true by definition
}
end
lemma val_one_is_zero : val(1 : K) = 0 :=
begin
have f : (1 : K) = (1:K)*(1:K),
simp,
have g : val(1 : K) = val((1 : K)*(1 : K)),
rw f,
simp,
have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K),
apply mul,
rw k at g,
rw g,
cases (with_top.cases (val(1:K))) with h1 h2,
rw h1,
rw h1 at g,
rw <-g,
sorry,
sorry,
end
```

#### Alex J. Best (Jun 23 2020 at 21:33):

(deleted)

#### Jalex Stark (Jun 23 2020 at 21:45):

in your example, this line fails for me

```
cases (with_top.cases (val(1:K))) with h1 h2,
```

with error unknown identifier 'with_top.cases'

#### Ashvni Narayanan (Jun 23 2020 at 21:47):

Edited

#### Alex J. Best (Jun 23 2020 at 21:49):

I think you need to use `non_zero`

in the first case.

#### Alex J. Best (Jun 23 2020 at 21:54):

And here is how you could use the built in cases instead of your lemma, its a bit weird though, because it writes `none`

instead of top everywhere, so using the lemma might be nicer.

```
lemma val_one_is_zero : val(1 : K) = 0 :=
begin
have f : (1 : K) = (1:K)*(1:K),
simp,
have g : val(1 : K) = val((1 : K)*(1 : K)),
rw f,
simp,
have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K),
apply mul,
rw k at g,
rw g,
cases t : val(1:K),
rw with_top.none_eq_top at t,
rw non_zero at t,
exfalso,
exact one_ne_zero t,
sorry,
end
```

#### Ashvni Narayanan (Jun 23 2020 at 21:56):

Alex J. Best said:

I think you need to use

`non_zero`

in the first case.

Oh yes, I had tried this. But some error kept coming up.

#### Jalex Stark (Jun 23 2020 at 21:56):

did you read the error?

#### Ashvni Narayanan (Jun 23 2020 at 21:58):

Well, as soon as I proved 1 \neq 0, I think g disappeared, which was no help.

#### Jalex Stark (Jun 23 2020 at 21:58):

you'll have less problems with "disappearing lemmas" if you use focusing braces

#### Jalex Stark (Jun 23 2020 at 21:59):

like this

```
lemma val_one_is_zero : val(1 : K) = 0 :=
begin
have f : (1 : K) = (1:K)*(1:K) := by simp,
have g : val(1 : K) = val((1 : K)*(1 : K)),
{ rw f, simp },
have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K) := by apply mul,
rw k at g, rw g,
cases (with_top.cases (val(1:K))) with h1 h2,
{ contrapose h1,
rw discrete_valuation_field.non_zero, norm_num },
sorry
end
```

#### Ashvni Narayanan (Jun 23 2020 at 22:03):

Oh ok. I will keep that in mind. Thank you!

#### Ashvni Narayanan (Jun 23 2020 at 22:06):

Alex J. Best said:

And here is how you could use the built in cases instead of your lemma, its a bit weird though, because it writes

`none`

instead of top everywhere, so using the lemma might be nicer.`lemma val_one_is_zero : val(1 : K) = 0 := begin have f : (1 : K) = (1:K)*(1:K), simp, have g : val(1 : K) = val((1 : K)*(1 : K)), rw f, simp, have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K), apply mul, rw k at g, rw g, cases t : val(1:K), rw with_top.none_eq_top at t, rw non_zero at t, exfalso, exact one_ne_zero t, sorry, end`

Thank you!

#### Jalex Stark (Jun 23 2020 at 22:15):

here's what I would write. probably the thing of most interest is the use of the `lift`

tactic.

```
import ring_theory.ideals
import ring_theory.principal_ideal_domain
import ring_theory.localization
universe u
noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(val : K -> with_top ℤ )
(mul : ∀ (x y : K), val(x*y) = val(x) + val(y) )
(add : ∀ (x y : K), val(x + y) ≥ min (val(x)) (val(y)) )
(non_zero : ∀ (x : K), val(x) = ⊤ ↔ x = 0 )
namespace discrete_valuation_field
def discrete_valuation_field.valuation (K : Type*) [field K] [ discrete_valuation_field K ] :
K -> with_top ℤ := discrete_valuation_field.val
variables {K : Type*} [field K] [discrete_valuation_field K]
instance (α : Type*) : has_coe α (with_top α) := {coe := some}
instance (α : Type*) : can_lift (with_top α) α :=
begin
refine {coe := coe, cond := λ x, x ≠ ⊤, prf := _},
intros, cases x, { contrapose! a, refl },
use x, refl,
end
lemma val_one_is_zero : val(1 : K) = 0 :=
begin
have f : (1 : K) = (1:K)*(1:K) := by simp,
have g : val(1 : K) = val((1 : K)*(1 : K)),
{ rw f, simp },
have k : val((1 : K)*(1 : K)) = val(1 : K) + val(1 : K) := by apply mul,
rw k at g, rw g,
lift val(1:K) to ℤ with d,
swap, { norm_num [non_zero] },
norm_cast, norm_cast at g, linarith,
end
```

Last updated: May 12 2021 at 23:13 UTC