# Zulip Chat Archive

## Stream: new members

### Topic: How to multiply an integer times a real

#### Lars Ericson (Jan 05 2021 at 23:42):

The first check works and the second throws an error:

```
import data.real.basic
import analysis.special_functions.pow
variable a : ℤ
#check ((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) -- OK
#check a*((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) -- error
```

The error is

```
foo1.lean:8:16
type mismatch at application
pow 9
term
9
has type
ℝ
but is expected to have type
ℤ
foo1.lean:8:16
failed to synthesize type class instance for
a : ℤ
⊢ has_pow ℤ ℝ
```

I'm trying to figure out how to state this theorem:

```
import data.real.basic
import analysis.special_functions.pow
theorem ex6e_mul_closed (a b c d : ℤ):
(a + b * ((9:ℝ) ^ ((1:ℝ)/(4:ℝ)))) * (c + d * ((9:ℝ) ^ ((1:ℝ)/(4:ℝ))))=
(a * c + b * d * 3) + (a*d + b * c) * ((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) :=
sorry
```

#### Kevin Buzzard (Jan 05 2021 at 23:50):

Lean reads from left to right. Read `a*((9:ℝ) ^ ((1:ℝ)/(4:ℝ)))`

from left to right. First we see `a`

. This is an integer. Then we see `*`

. That is multiplication, which takes two elements of type X and returns an element of type X. Then we solve for X, and it's easy to solve -- a is an integer, so X must be the integers. Then we read on and see real numbers instead of integers. Then we get confused and produce an error.

#### Kevin Buzzard (Jan 05 2021 at 23:51):

The fix is to not let Lean solve for X incorrectly, by not letting it see the integer a, e.g. by writing `(a : ℝ)`

instead of `a`

. Then it will set X = reals and then you should hopefully be fine.

#### Lars Ericson (Jan 06 2021 at 00:51):

The problem is that I have to have `a`

be an integer for this particular theorem. That's why I said `variable a : ℤ`

. I am trying to prove that expressions of form a + b * 9^(1/4) are closed under multiplication, where a and b are integers and 9^(1/4) is a particular irrational number. Writing `a : ℝ`

won't get me there.

#### Bryan Gin-ge Chen (Jan 06 2021 at 00:54):

I think Kevin's suggestion is not to replace the `variable`

statement, but to add the type coercion to the expression you're interested in:

```
import data.real.basic
import analysis.special_functions.pow
variable a : ℤ
#check ((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) -- OK
#check (a : ℝ)*((9:ℝ) ^ ((1:ℝ)/(4:ℝ))) -- also OK
```

#### Lars Ericson (Jan 06 2021 at 01:05):

Thanks @Kevin Buzzard and @Bryan Gin-ge Chen. The following is a bit more awkward but it better represents what I am trying to prove, and doesn't raise an error, I guess because the `subring`

tells Lean something that makes it find a `has_pow`

for this case:

```
import data.real.basic
import analysis.special_functions.pow
theorem ex6e_mul_closed : ∃ s : subring ℝ,
∀ x y z: ℝ,
x ∈ s →
y ∈ s →
z ∈ s →
∀ a b c d: ℤ,
x = a + b * ((9:ℝ) ^ (1/4:ℝ)) →
y = c + d * ((9:ℝ) ^ (1/4:ℝ)) →
z = x * y →
z = (a * c + b * d * 3) + (a * d + b * c) * (9:ℝ) ^ (1/4:ℝ)
:=
sorry
```

#### Eric Wieser (Jan 06 2021 at 01:09):

That's a strange way to state that. Shouldn't the last two lines just be `x * y \in s`

?

#### Eric Wieser (Jan 06 2021 at 01:10):

You seem to be mixing the proof with the theorem statement

#### Bryan Gin-ge Chen (Jan 06 2021 at 01:11):

As Kevin said, Lean reads each expression from left to right, so it has no problem realizing that `a`

in `x = a + b * ((9:ℝ) ^ (1/4:ℝ))`

needs to be coerced to `ℝ`

, since it's already seen `x`

which is of type `ℝ`

.

#### Eric Wieser (Jan 06 2021 at 01:13):

I think your statement can be proved with `use [\top], ...`

which shows your statement is wrong

#### Lars Ericson (Jan 06 2021 at 01:28):

I'm trying to build up pieces of a proof that I have a subring by showing that the form `a+b*I`

is closed under addition and multiplication where `I=(9:ℝ) ^ (1/4:ℝ)`

and `a b: ℤ`

. So this is a lemma about closed under multiplication. Here is an even more awkward statement of it:

```
import data.real.basic
import analysis.special_functions.pow
theorem ex6e_mul_closed : ∃ s : subring ℝ,
∀ x y z: ℝ,
x ∈ s →
y ∈ s →
z ∈ s →
∀ a b c d: ℤ,
x = a + b * ((9:ℝ) ^ (1/4:ℝ)) →
y = c + d * ((9:ℝ) ^ (1/4:ℝ)) →
z = x * y →
∃ e f: ℤ,
e = a * c + b * d * 3 ∧
f = a * d + b * c ∧
z = e + f * (9:ℝ) ^ (1/4:ℝ)
:=
begin
sorry
end
```

I am borrowing the `∃ s : subring ℝ`

from the theorem I want to prove which is

```
theorem ex6e : ∃ s : subring ℝ, ∀ x : ℝ, x ∈ s ↔ ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ) := sorry
```

I'm just putting it up there to get the `has_pow`

problem to go away. It's chicken and egg though because I need to prove closed under multiplication before I have a `subring`

, because it's part of the proof of `subring`

.

I guess I have to rethink this and use `instance`

or look at the structure for `subring`

directly and prove the structure all at one time without lemmas.

Basically I need a framework where I can have a space where I prove the closed under multiplication and a space where I prove the closed under addition. I guess that's an `instance`

.

#### Eric Wieser (Jan 06 2021 at 01:43):

The proof of closure is `s.mul_mem`

for your subring lemma

#### Lars Ericson (Jan 06 2021 at 01:54):

That's the right idea going in the wrong direction. `s.mul_mem`

says that if I have a subring already, then it is closed under multiplication.

I have to go the other way: I am closed under multiplication and addition, and hence I am a subring.

So net net I need to do `instance: subring`

of some sort where what I am focusing on now is the `mul_mem'`

and `add_mem'`

fields of the structure, but I also have to do the other fields. It looks like I can't do these facets as separate lemmas, I have to do everything all at once. They have to be inside the proof of the `instance`

so I can get Lean to give me `has_pow`

between integers and reals while I am in the process of proving my subring, and not after I have proven the subring, which I can't assume because I haven't proven it yet.

Or I guess what you are saying is that Lean is coercing my integers to reals before applying `has_pow`

. Which is OK but it is essential to the nature of what I am proving that my integers are integers "where it counts". I guess "where it counts" is when I establish that the result of addition or multiplication is of form A+B*I where A and B are definitely integers and I is definitely the real 9^(1/4).

#### Yakov Pechersky (Jan 06 2021 at 02:04):

You don't need an `instance`

, you just need a structure. Your proof is the existence of such a structure. You can start your proof of an existence of such a subring (with whatever properties it has) with some statement about `subring.mk'`

if you want.

#### Yakov Pechersky (Jan 06 2021 at 02:04):

Can you post an image or a latex of the actual problem statement you are formalizing?

#### Lars Ericson (Jan 06 2021 at 02:23):

6E:

Screenshot-from-2021-01-05-21-23-27.png

#### Lars Ericson (Jan 06 2021 at 02:26):

`a`

and `b`

have to start life as integers. I can coerce them to real to do the multiplication with the `pow`

, but I have to un-coerce the results of times and plus afterwards back to integer to prove the subring.

#### Yakov Pechersky (Jan 06 2021 at 02:31):

Try this:

```
import data.real.basic
import analysis.special_functions.pow
theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ (1 / 4)) ∈ s :=
begin
refine ⟨subring.mk' _ _ _ _ _, _, _⟩,
end
```

#### Yakov Pechersky (Jan 06 2021 at 02:48):

or use `subring.closure _`

#### Yakov Pechersky (Jan 06 2021 at 03:48):

But I can't make it work:

```
import data.real.basic
import analysis.special_functions.pow
set_option pp.all true
theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
set s : set ℝ := set.insert (9 ^ ((1 : ℝ) / 4)) (set.range (coe : ℤ → ℝ)) with hs,
refine ⟨subring.mk' _ _ _ _ _, _, _⟩,
{ exact s },
{ refine {carrier := s, one_mem' := _, mul_mem' := _},
{ rw [hs],
have := @set.mem_insert_iff ℝ 1 (9 ^ ((1 : ℝ) / 4)) (set.range (coe : ℤ → ℝ)),
rw this, -- failure, they look the same to me though
sorry
},
},
sorry
end
```

#### Yakov Pechersky (Jan 06 2021 at 03:49):

Is there some weird typo I made, or some typeclass issue?

#### Alex J. Best (Jan 06 2021 at 03:54):

If `rw`

fails me I try `erw`

instead

```
import data.real.basic
import analysis.special_functions.pow
--set_option pp.all true
theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
set s : set ℝ := set.insert (9 ^ ((1 : ℝ) / 4)) (set.range (coe : ℤ → ℝ)) with hs,
refine ⟨subring.mk' _ _ _ _ _, _, _⟩,
{ exact s },
{ refine {carrier := s, one_mem' := _, mul_mem' := _},
{ rw [hs],
erw set.mem_insert_iff,
},
},
sorry
end
```

#### Alex J. Best (Jan 06 2021 at 03:54):

In this case it does what you want, https://leanprover-community.github.io/mathlib_docs/tactics.html#erewrite%20/%20erw

#### Alex J. Best (Jan 06 2021 at 04:00):

The root cause of the issue however is that you used `set.insert`

to define `s`

instead of `insert`

, quite confusing indeed.

#### Alex J. Best (Jan 06 2021 at 04:00):

```
import data.real.basic
import analysis.special_functions.pow
--set_option pp.all true
theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
set s : set ℝ := insert (9 ^ ((1 : ℝ) / 4)) (set.range (coe : ℤ → ℝ)) with hs, -- CHANGED set.insert to insert here
refine ⟨subring.mk' _ _ _ _ _, _, _⟩,
{ exact s },
{ refine {carrier := s, one_mem' := _, mul_mem' := _},
{ rw [hs],
rw set.mem_insert_iff,
},
},
sorry
end
```

also works then

#### Alex J. Best (Jan 06 2021 at 04:02):

To see this look at the last line of the error message you get from trying `rw set.mem_insert_iff`

```
rewrite tactic failed, did not find instance of the pattern in the target expression
@has_mem.mem.{?l_1 ?l_1} ?m_2 (set.{?l_1} ?m_2) (@set.has_mem.{?l_1} ?m_2) ?m_3
(@has_insert.insert.{?l_1 ?l_1} ?m_2 (set.{?l_1} ?m_2) (@set.has_insert.{?l_1} ?m_2) ?m_4 ?m_5)
```

its about `has_insert.insert`

, but the goal is

```
@has_mem.mem.{0 0} real (set.{0} real) (@set.has_mem.{0} real)
(@has_one.one.{0} real (@monoid.to_has_one.{0} real (@ring.to_monoid.{0} real real.ring)))
(@set.insert.{0} real ......)
```

which refers to `set.insert`

instead.

#### Alex J. Best (Jan 06 2021 at 04:03):

These things are equal under the hood which is why `erw`

works, but syntactically they don't look the same so `rw`

fails.

#### Alex J. Best (Jan 06 2021 at 04:05):

If you look at src#set.insert you'll see it is a `protected def`

which is maybe a bit of a hint you aren't meant to be calling it directly

#### Lars Ericson (Jan 06 2021 at 05:03):

Thanks for the lift. I guess as long as we know that `a`

and `b`

are integers in `∀ (a b : ℤ)`

it is fine for `a`

to be lifted to ℝ inside the ∀. I would have thought that it was `b`

that needed to be lifted since that is what is multiplied by the power.

I don't understand why technically you need to say `s ≠ ⊤`

. What is `⊤`

, all of the reals? Because all of the reals will not be expressible as a + b * 9^(1/4) for `a b : ℤ`

, so I don't know why the exclusion is necessary.

#### Yakov Pechersky (Jan 06 2021 at 05:06):

I think the formalization might be something like:

```
theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
refine ⟨subring.closure { 9 ^ ((1 : ℝ) / 4), (1 : ℤ) }, _, _⟩,
{ sorry },
{ sorry },
end
```

#### Yakov Pechersky (Jan 06 2021 at 05:06):

but I think there might be some lemmas missing about `subring.closure`

to show this

#### Yakov Pechersky (Jan 06 2021 at 05:07):

The `hs : s ≠ ⊤`

is necessary because like Eric said above, the full `ℝ`

does have the property that `(a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈`

"all of the reals".

#### Yakov Pechersky (Jan 06 2021 at 05:08):

And I think the exercise is to show that a strict subset of the reals is still an integral domain, or in the language here, a subring.

#### Lars Ericson (Jan 06 2021 at 05:18):

But 'a : ℤ', which should be enough information to exclude 's ≠ ⊤'. We know that under 'a : ℤ', the expression '(a : ℝ) + b * (9 ^ ((1 : ℝ) / 4))' is equivalent to '(a : ℤ) + b * (9 ^ ((1 : ℝ) / 4))'. The only thing stopping us from saying the latter is some technicality in Lean about no `has_pow`

for

ℤ and ℝ together. Once you have '(a : ℤ) + b * (9 ^ ((1 : ℝ) / 4))', `⊤`

is not a contender. So it shouldn't be necessary to put it in the theorem statement, because the `a : ℤ`

in the quantifier is enough information already to exclude top.

#### Yakov Pechersky (Jan 06 2021 at 05:26):

When I wrote ` ∀ (a b : ℤ), (a : ℝ)...`

that just indicates that I require `a`

and `b`

to be integers. They're then cast to reals.

#### Lars Ericson (Jan 06 2021 at 05:27):

I've moved it along a little. I should be able to apply `subring.mul_mem`

but it is not matching although it looks exactly like it should:

```
import data.real.basic
import analysis.special_functions.pow
lemma one_in_Z : (1:ℝ) ∈ set.range (coe : ℤ → ℝ) :=
begin
sorry,
end
theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
set s : set ℝ := insert (9 ^ ((1 : ℝ) / 4)) (set.range (coe : ℤ → ℝ)) with hs, -- CHANGED set.insert to insert here
refine ⟨subring.mk' _ _ _ _ _, _, _⟩,
{ exact s },
{ refine {carrier := s, one_mem' := _, mul_mem' := _},
{ rw [hs],
rw set.mem_insert_iff,
right,
exact one_in_Z,
},
intros a b,
intro h1,
intro h2,
have h3 := subring.mul_mem h1 h2,
},
sorry,
sorry,
sorry,
sorry,
sorry,
end
```

where the goal state is

```
Tactic state
widget
filter:
no filter
1 goal
s: set ℝ := insert (9 ^ (1 / 4)) (set.range coe)
hs: s = insert (9 ^ (1 / 4)) (set.range coe)
ab: ℝ
h1: a ∈ s
h2: b ∈ s
⊢ a * b ∈ s
```

and the error is

```
type mismatch at application
subring.mul_mem h1
term
h1
has type
a ∈ s : Prop
but is expected to have type
subring ?m_1 : Type ?
state:
s : set ℝ := insert (9 ^ (1 / 4)) (set.range coe),
hs : s = insert (9 ^ (1 / 4)) (set.range coe),
a b : ℝ,
h1 : a ∈ s,
h2 : b ∈ s
⊢ a * b ∈ s
```

#### Yakov Pechersky (Jan 06 2021 at 05:27):

For sure, for any `(a b : ℤ)`

, `a + b * (9 ^ 1 / 4) ∈ ℝ`

(to use set theory notation.

#### Yakov Pechersky (Jan 06 2021 at 05:29):

I don't think my original approach works because just inserting this 9^x value isn't enough to make that set closed. You won't be able to prove `mul_mem'`

.

#### Lars Ericson (Jan 06 2021 at 05:30):

@Yakov Pechersky they are cast to reals for a technical reason, but the information in the environment, provided by the quantifier, should still include the fact that `a`

and `b`

are integers. You can't, to my mind, prove the subring without using that information. Completely forgetting that `a`

is an integer forces you to say `s ≠ ⊤`

but that is not an insightful statement. All that is saying is "I forget that I just said that `a`

is an integer". There should be a way of retaining that type information about `a`

in the tactic state and then doing the coercion to make `has_pow`

happy. It is not insightful to lose information and than replace it with another tangentially equivalent restriction.

#### Alex J. Best (Jan 06 2021 at 05:30):

The error message is telling you what isn't matching

```
type mismatch at application
subring.mul_mem h1
term
h1
has type
a ∈ s : Prop
but is expected to have type
subring ?m_1 : Type ?
```

the complaint is exactly that the first argument of docs#subring.mul_mem should be a `subring R`

of some ring `R`

, then the second and third arguments are two proofs of membership of that subring

#### Lars Ericson (Jan 06 2021 at 05:31):

Yes subring of R is what we are trying to prove, it is not an assumption.

#### Yakov Pechersky (Jan 06 2021 at 05:32):

It does remember! It'll show `↑1`

for my `(1 : ℤ)`

which is in an expression that expects an ℝ.

#### Alex J. Best (Jan 06 2021 at 05:34):

Lars Ericson said:

Yes subring of R is what we are trying to prove, it is not an assumption.

Right so you can't apply that lemma!

#### Lars Ericson (Jan 06 2021 at 05:35):

I think of `a + b X `

where` X = 9^(1/4)`

as a pair or a vector `<a,b>`

where X is a kind of basis vector. The insight is that it is a ring of 2-element vectors with a slightly funny multiplication operation. The proof has to start with definition of addition and multiplication on such pairs and that such pairs multiplied or added are also pairs. The `has_pow`

takes away from that insight, it is a kind of detour.

#### Lars Ericson (Jan 06 2021 at 05:37):

In other words we are spending a lot of time on coercions and `has_pow`

s and so on because we are losing sight of the idea that we have encoded integer pairs with a trick involving a single irrational real.

#### Lars Ericson (Jan 06 2021 at 05:40):

So `0 = <0, 0>`

, `1 = <1,0>`

, otherwise you have `<a,b>`

where `a,b`

are integers, and `<a,b>+<c,d> = <a+c,b+d>`

and `<a,b>*<c,d> = <a*c+*d*3, a*d+b*c>`

. It's really proving that pairs with that definition of + and * form a ring. The pairs are isomorphic to `a + b *9^(1/4)`

. It seems like it would be easier to prove

- The isomorphism of pairs to that expression
- That the pairs under that * and + are a ring

than to get lost in coercions between integers and reals and complicated libraries of definitions on `pow`

.

#### Yakov Pechersky (Jan 06 2021 at 05:46):

This is what I mean currently:

```
import data.real.basic
import analysis.special_functions.pow
theorem ex6e : ∃ (s : subring ℝ) (hs : s ≠ ⊤),
∀ (a b : ℤ), (a : ℝ) + b * (9 ^ ((1 : ℝ) / 4)) ∈ s :=
begin
use ⊤, -- use the whole ring of reals, the top of the subring lattice
split,
{ sorry }, -- here I am ignoring the fact I have to prove the hs hypothesis
simp
end
```

#### Yakov Pechersky (Jan 06 2021 at 05:46):

It's what Eric remarked on earlier.

#### Alex J. Best (Jan 06 2021 at 05:57):

Here's how I'd structure this exercise (and some of the proofs) if asked to formalise it:

```
import data.real.basic
import analysis.special_functions.pow
lemma important : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := begin sorry end
theorem ex6e : ∃ s : subring ℝ, (∀ x : ℝ, x ∈ s ↔ ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)) ∧ is_integral_domain s :=
begin
rw important, -- 9^1/4 is ugly, use sqrt 3 instead (likely more lemmas in library about sqrt so this will make our life easier)
refine ⟨subring.mk _ _ _ _ _ _ , ⟨_, _⟩⟩, -- separate out all the goals
rotate 6, -- we want our subring to be defined to be the a + b * (9:ℝ) ^ (1/4:ℝ) so switch to that goal first
{ intro x,
refl, }, -- saying to lean this is true by definition forces the subring to have the elements we want, without having to do a set s := ..
rotate 1,
{ use [1,0], norm_num, }, -- 1 and 0 are easy thanks to norm num
{ sorry, }, -- this can hopefully done like the negation below, maybe using the ring, norm_num and linarith tactics.
{ use [0,0], norm_num, },
{ sorry },
{ rintro x ⟨haa, hab, rfl⟩, use [-haa, -hab], rw neg_add, simp, }, -- this is doing the "basis vector" thing lars is referring to using rintro splits our subring element x into components haa hab the rfl part clears all mention of x now we have decomposed it into its components
split,
{ use [0, 1], simp, }, -- maybe library_search does this too...
{ exact mul_comm, }, -- library_search
{ intros x y, exact mul_eq_zero.mp, }, -- library_search
end
```

#### Yakov Pechersky (Jan 06 2021 at 08:25):

Now can you do it using `subring.closure { real.sqrt 3 }`

?

#### Alex J. Best (Jan 06 2021 at 08:27):

Do what, show that above criterion for membership, or show it is an integral domain?

#### Yakov Pechersky (Jan 06 2021 at 08:31):

Ideally, the lemmas about `subring.closure`

should allow you to say:

```
refine ⟨subring.closure { real.sqrt 3 } , _, _⟩,
```

instead

#### Alex J. Best (Jan 06 2021 at 08:35):

Oh for sure, if the goal is to formalise that same object in a easy to work with way I'd set everything up totally differently, I was just trying to match the exercise as closely as possible.

#### Yakov Pechersky (Jan 06 2021 at 08:43):

btw the last line can be expressed as:

```
{ exact @integral_domain.to_is_integral_domain _ (subring.subring.domain _) }
```

#### Yakov Pechersky (Jan 06 2021 at 08:43):

because the parent ring on `ℝ`

is also an integral domain

#### Yakov Pechersky (Jan 06 2021 at 08:44):

But I guess proving that is part of the exercise

#### Alex J. Best (Jan 06 2021 at 08:52):

Yeah my solution is probably cheating via the typeclass mechanism really, at least in a pen and paper proof you would mention subrings of domains being domains explicitly.

#### Eric Wieser (Jan 06 2021 at 09:12):

@Alex J. Best' statement is the only correct one so far

#### Eric Wieser (Jan 06 2021 at 09:13):

The `iff`

is crucial, otherwise it allows larger subrings than the question permits

#### Mario Carneiro (Jan 06 2021 at 09:39):

By the way this ring already exists in mathlib, it's called `zsqrtd 3`

#### Eric Wieser (Jan 06 2021 at 09:45):

Presumably there's some way to interpret docs#zsqrtd as asubring?

#### Eric Wieser (Jan 06 2021 at 09:46):

Sending it through a coercion ring hom would do the trick I assume, although I don't know where the def is for that

#### Eric Wieser (Jan 06 2021 at 09:47):

I'm a little surprised that zqrtd has no coercion to real...

#### Alex J. Best (Jan 06 2021 at 09:50):

Well according to the copyright headers its older than real :grinning:

#### Eric Wieser (Jan 06 2021 at 09:59):

I'll make a pr

#### Eric Wieser (Jan 06 2021 at 11:08):

```
/-- The image of `zsqrtd` in `ℝ`. -/
@[simps]
noncomputable def to_real (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }
```

seems like the def needed, which proves the subring as `to_real.range`

#### Eric Wieser (Jan 06 2021 at 11:10):

I was hoping to be able to also prove

```
lemma to_real_injective (h : 0 ≤ d) (h_not_square : ¬∃ (x : ℤ), x*x = d) :
function.injective (to_real h) :=
(to_real h).injective_iff.mpr $ λ a ha, begin
simp only [to_real_apply] at ha,
have : (↑a.re + ↑a.im * real.sqrt d) * (↑a.re - ↑a.im * real.sqrt d) =
a.re * a.re - (real.sqrt d * real.sqrt d) * (a.im * a.im) := by ring,
replace ha := congr_arg (λ x, x * (↑(a.re) - ↑(a.im) * real.sqrt ↑d)) ha,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)] at ha,
rw sub_eq_zero at ha,
norm_cast at ha,
simp at h_not_square,
sorry,
end
```

but I think I'm missing some knowledge of the lemmas to apply

#### Kevin Buzzard (Jan 06 2021 at 11:51):

A number-theoretic ring like $\mathbb{Z}[\sqrt{d}]$ has two maps to the reals and it's not clear to me that the one you're thinking of is any better than the other one. $\mathbb{Z}[\sqrt{d}]$ should not be thought of as a subring of the reals, it is notation for the abstract ring $\mathbb{Z}[X]/(X^2-d)$ and $X$ is no more positive than it is negative.

#### Eric Wieser (Jan 06 2021 at 12:06):

That's perhaps an argument against it being a coe, but I think the mapping should probably still exist

#### Kevin Buzzard (Jan 06 2021 at 12:06):

Both should ;-)

#### Kevin Buzzard (Jan 06 2021 at 12:07):

This is a great example of an object with a canonical non-trivial automorphism, so everything either is invariant under the automorphism or comes in pairs.

#### Eric Wieser (Jan 06 2021 at 12:09):

#### Eric Wieser (Jan 06 2021 at 12:09):

I only added `to_real`

because we only have `real.sqrt`

#### Eric Wieser (Jan 06 2021 at 12:10):

If you want the other one you can use `conj.to_real`

#### Kevin Buzzard (Jan 06 2021 at 12:10):

That's generally the rule when you only have one of the pair ;-)

#### Alex J. Best (Jan 06 2021 at 12:12):

alternative approach:

```
lemma to_real_injective (h : 0 ≤ d) (h_not_square : ¬∃ (x : ℤ), x*x = d) :
function.injective (to_real h) :=
(to_real h).injective_iff.mpr $ λ a ha, begin
simp only [to_real_apply] at ha,
have := irrational_nrt_of_notint_nrt 2 d (by sorry : (real.sqrt d) ^ 2 =d),
specialize this _ _,
by_cases haim : a.im = 0,
{ sorry },
have := rat_add a.re (rat_mul this (by exact_mod_cast haim : (a.im : ℚ) ≠ 0)),
norm_cast at this,
rw ha at this,
exfalso,
exact rat.not_irrational 0 (by exact_mod_cast this),
sorry,
sorry,
end
```

#### Eric Wieser (Jan 06 2021 at 12:18):

I've solved the lemma in the PR

#### Eric Wieser (Jan 06 2021 at 12:18):

So alternative approaches fine, but the bar is now sorry-free :)

#### Eric Wieser (Jan 06 2021 at 12:20):

@Lars Ericson, with that PR, your problem can now be solved as:

```
-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr
theorem ex6e : ex6 {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
sorry
end
```

where the final goals ought to be fairly easy to close without any knowledge of the reals

#### Lars Ericson (Jan 06 2021 at 14:18):

Thank you all very much. I just did a `leanproject upgrade-mathlib`

which I guess gets me the PR. I will try to fill out the `sorry`

in Eric's final version.

#### Eric Wieser (Jan 06 2021 at 14:18):

It does not get you the PR, because the PR is not merged yet!

#### Eric Wieser (Jan 06 2021 at 14:19):

However, you can still use the `abbreviation ex6`

definition without the PR

#### Lars Ericson (Jan 06 2021 at 14:21):

It still wants `has_pow`

:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr
theorem ex6e : ex6 {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
sorry
end
```

gives error

```
failed to synthesize type class instance for
x : ℝ,
a b : ℤ
⊢ has_pow ℝ ℝ
```

#### Eric Wieser (Jan 06 2021 at 14:21):

Yes, you need `import analysis.special_functions.pow`

#### Lars Ericson (Jan 06 2021 at 14:22):

It wants one more definition, should I add that lemma `to_real_injective`

above?

```
unknown identifier 'zsqrtd.to_real'
state:
⊢ ex6 {x : ℝ | ∃ (a b : ℤ), x = ↑a + ↑b * 9 ^ (1 / 4)}
```

#### Eric Wieser (Jan 06 2021 at 14:23):

You need this one: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20to.20multiply.20an.20integer.20times.20a.20real/near/221755534

#### Eric Wieser (Jan 06 2021 at 14:23):

You don't need the injectivity one, I added that because I thought it might be useful to someone

#### Lars Ericson (Jan 06 2021 at 14:24):

It wants a `d`

.

#### Lars Ericson (Jan 06 2021 at 14:25):

Should I add `variable d: ℕ `

in context?

#### Eric Wieser (Jan 06 2021 at 14:26):

Just add `{d : ℕ}`

after the word `to_real`

#### Lars Ericson (Jan 06 2021 at 14:26):

I can't make it happy. This is my starting point:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
namespace zsqrtd
variable d: ℕ
/-- The image of `zsqrtd` in `ℝ`. -/
@[simps]
noncomputable def to_real (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }
end zsqrtd
-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr
theorem ex6e : ex6 {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
sorry
end
```

it's giving me

```
type mismatch at application
int.cast_nonneg.mpr h
term
h
has type
0 ≤ d
but is expected to have type
0 ≤ ?m_1
state:
d : ℕ,
h : 0 ≤ d,
a b : ℤ√↑d,
this :
(↑(a.re) + ↑(a.im) * real.sqrt ↑d) * (↑(b.re) + ↑(b.im) * real.sqrt ↑d) =
↑(a.re) * ↑(b.re) + (↑(a.re) * ↑(b.im) + ↑(a.im) * ↑(b.re)) * real.sqrt ↑d +
↑(a.im) * ↑(b.im) * (real.sqrt ↑d * real.sqrt ↑d)
⊢ ↑((a * b).re) + ↑((a * b).im) * real.sqrt ↑d =
(↑(a.re) + ↑(a.im) * real.sqrt ↑d) * (↑(b.re) + ↑(b.im) * real.sqrt ↑d)
```

#### Eric Wieser (Jan 06 2021 at 14:27):

d should be a `\Z`

#### Lars Ericson (Jan 06 2021 at 14:27):

Thank you. This is my starting point, it checks:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
/-- The image of `zsqrtd` in `ℝ`. -/
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }
-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr
theorem ex6e : ex6 {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
sorry
end
```

#### Eric Wieser (Jan 06 2021 at 14:28):

Great! You'll want to start by proving `lemma important : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := begin sorry end`

.

#### Lars Ericson (Jan 06 2021 at 14:36):

Should be easy. I've done similar ones while golfing over last few days:

```
lemma nine_equals_3_times_3 : (9:ℝ) = (3:ℝ)*(3:ℝ) :=
begin
linarith,
end
lemma a_squared_equals_a_times_a (a:ℝ) : a*a = a^(2:ℕ) :=
begin
linarith,
end
lemma nine_equals_3_squared : (9:ℝ) = ((3:ℝ) ^ (2:ℕ)) :=
begin
have h1 := nine_equals_3_times_3,
have h2 := a_squared_equals_a_times_a 3,
rw h2 at h1,
assumption,
end
```

#### Eric Wieser (Jan 06 2021 at 14:38):

`a_squared_equals_a_times_a `

is docs#pow_two (or rather, its reverse)

#### Eric Wieser (Jan 06 2021 at 14:38):

Always try `library_search`

for trivial lemmas like that first :)

#### Lars Ericson (Jan 07 2021 at 01:02):

How do I prove that 2 = 2? I need it for the 2nd lemma `x_mul_x_pow_y_equals_x_pow_y_plus_y`

:

```
lemma two_equals_two : (2:ℕ) = (2:ℝ) :=
sorry
lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 ≤ x → (x * x)^y = x^(y+y) :=
begin
intro h,
ring,
have h1 := real.rpow_mul h (2:ℝ) y,
rw h1,
sorry,
end
```

The first lemma won't typecheck in the `=`

, giving:

```
type mismatch at application
2 = 2
term
2
has type
ℝ
but is expected to have type
ℕ
```

The 2nd lemma won't go through because I have a mismatch of `2:ℕ`

versus `2:ℝ`

that I can't get rid of because the `2:ℕ`

is coming in under the hood without my control. Here is the goal state on the 2nd lemma:

```
1 goal
xy: ℝ
h: 0 ≤ x
h1: x ^ (2 * y) = (x ^ 2) ^ y
⊢ (x ^ 2) ^ y = (x ^ 2) ^ y
All Messages (8)
```

I should be done but the above-mentioned widget is telling me that not all 2s are alike and I don't know how to coerce my 2:N to a 2:R.

This is all in service of getting closer to the goal of proving the `important`

lemma above. This is where I'm stuck now.

#### Yakov Pechersky (Jan 07 2021 at 01:06):

```
lemma two_equals_two : (2:ℝ) = (2:ℕ) := by norm_num
```

#### Yakov Pechersky (Jan 07 2021 at 01:06):

Not that the real has to be on the LHS for the casting to work properly.

#### Yakov Pechersky (Jan 07 2021 at 01:08):

You might like docs#mul_rpow

#### Lars Ericson (Jan 07 2021 at 01:21):

I'll try going that way. I'm using the other direction `rpow_mul`

. The `two_equals_two`

lemma doesn't work as a rewrite rule. I can't get this lemma to close, the goal definitely has a `2:ℕ`

in it but `rw ← two_equals_two`

won't bind:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
lemma two_equals_two : (2:ℝ) = (2:ℕ) := by norm_num
lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 ≤ x → (x * x)^y = x^(y+y) :=
begin
intro h,
ring,
have h1 := real.rpow_mul h (2:ℝ) y,
have h2 := eq.symm h1,
conv
begin
to_lhs,
rw ← two_equals_two, -- FAIL
end,
end
```

#### Yakov Pechersky (Jan 07 2021 at 01:25):

Your lemma isn't true is `x = 0`

and `y = 0`

#### Yakov Pechersky (Jan 07 2021 at 01:28):

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
lemma two_equals_two : (2:ℝ) = (2:ℕ) := by norm_num
lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 ≤ x → 0 < y → (x * x)^y = x^(y+y) :=
begin
intros hx hy,
rw real.mul_rpow hx hx,
rcases eq_or_lt_of_le hx with rfl|hx,
{ rw real.zero_rpow (ne_of_gt hy),
rw real.zero_rpow (ne_of_gt (add_pos hy hy)),
rw zero_mul },
{ rw real.rpow_add hx }
end
```

#### Yakov Pechersky (Jan 07 2021 at 01:35):

As you can see, no knowledge of some equality of cast nats needed.

#### Lars Ericson (Jan 07 2021 at 01:41):

Thanks I got there the other way but with `x < 0`

, and no 2's using your `rpow_add`

suggestion:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
lemma le_if_leq (x : ℝ) : 0 < x → 0 ≤ x :=
begin
intro h,
linarith,
end
lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 < x → (x * x)^y = x^(y+y) :=
begin
intro h,
have h1 := le_if_leq x h,
have h2 := @real.mul_rpow x x y h1 h1,
rw h2,
have h3 := real.rpow_add h y y,
exact eq.symm h3,
end
```

#### Yakov Pechersky (Jan 07 2021 at 01:44):

The first one is `le_of_lt`

#### Lars Ericson (Jan 07 2021 at 02:05):

@Yakov Pechersky thanks for the help. @Eric Wieser I have now proved `lemma important : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3`

as you suggested, in only 160 lines:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
-- Eric Wieser
/-- The image of `zsqrtd` in `ℝ`. -/
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }
-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr
lemma nine_equals_3_times_3 : (9:ℝ)=(3:ℝ)*(3:ℝ) :=
begin
linarith,
end
lemma three_is_gt_0 : (0:ℝ) < (3:ℝ) :=
begin
linarith,
end
lemma three_is_gte_0 : (0:ℝ) ≤ (3:ℝ) :=
begin
linarith,
end
lemma sqrt_of_9_is_3 : (3:ℝ) = (real.sqrt (9:ℝ)) :=
begin
have h1 := nine_equals_3_times_3,
rw h1,
have h2 := three_is_gte_0,
have h3 := real.sqrt_mul_self h2,
rw ← h1 at h3,
rw ← h1,
exact eq.symm h3,
end
lemma half_plus_half_equals_1: (1/2:ℝ)+(1/2:ℝ)=1 :=
begin
linarith,
end
lemma x_equals_sqrtx_times_sqrtx (x:ℝ): 0 < x → x = x^(1/2:ℝ) * x^(1/2:ℝ) :=
begin
intro h1,
have h2 := real.rpow_add h1,
have h3 := h2 (1/2) (1/2),
have h4 := half_plus_half_equals_1,
rw h4 at h3,
have h5 := real.rpow_one x,
rw h5 at h3,
exact h3,
end
lemma x_is_0 (x:ℝ) : x ≥ 0 → ¬(0 < x) → x = 0 :=
begin
intro h1,
intro h2,
linarith,
end
lemma half_ne_0 : (1/2:ℝ) ≠ (0:ℝ) :=
begin
linarith,
end
lemma zero_le_0 : (0:ℝ) ≤ (0:ℝ) :=
begin
linarith,
end
lemma sqrt_0_equals_0 : real.sqrt 0 = 0 :=
begin
have h1 := zero_le_0,
exact real.sqrt_eq_zero_of_nonpos h1,
end
lemma x_gt_0_implies_sqrt_x_gt_0 (x:ℝ): x ≥ 0 → x^(1/2:ℝ) ≥ 0 :=
begin
intro h1,
exact real.rpow_nonneg_of_nonneg h1 (1 / 2),
end
lemma sqrt_x_equals_sqrt_x (x:ℝ) : x ≥ 0 → x^(1/2:ℝ) = real.sqrt x :=
begin
intro h,
have h1 := x_equals_sqrtx_times_sqrtx x,
by_cases h2 : 0 < x,
{
have h3 := h1 h2,
conv
begin
to_rhs,
rw h3,
end,
have h5 := x_gt_0_implies_sqrt_x_gt_0 x,
have h6 := h5 h,
have h4 := real.sqrt_mul_self h6,
exact eq.symm h4,
},
{
have h3 := x_is_0 x,
have h4 := h3 h,
have h5 := h4 h2,
rw h5,
have h6 := @real.zero_rpow (1/2:ℝ),
have h7 := half_ne_0,
have h8 := h6 h7,
rw h8,
have h9 := sqrt_0_equals_0,
exact eq.symm h9,
}
end
lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 < x → (x * x)^y = x^(y+y) :=
begin
intro h,
have h1 := le_of_lt h,
have h2 := @real.mul_rpow x x y h1 h1,
rw h2,
have h3 := real.rpow_add h y y,
exact eq.symm h3,
end
lemma fourth_root_of_9_equals_sqrt_sqrt : (9:ℝ) ^ (1/4:ℝ) = real.sqrt (real.sqrt (9:ℝ)) :=
begin
have h1 := nine_equals_3_times_3,
have h2 := three_is_gt_0,
have h7 := three_is_gte_0,
have h3 := sqrt_of_9_is_3,
rw ← h3,
rw h1,
have h4 := sqrt_x_equals_sqrt_x (3:ℝ),
have h5 := h4 h7,
rw ← h5,
have h6 := x_mul_x_pow_y_equals_x_pow_y_plus_y 3 (1/4),
have h8 := h6 h2,
rw h8,
ring,
end
lemma important : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 :=
begin
have h1 := fourth_root_of_9_equals_sqrt_sqrt,
rw h1,
have h2 := sqrt_of_9_is_3,
rw h2,
end
```

#### Lars Ericson (Jan 07 2021 at 02:47):

I am back to the main question, which now is how do I prove equality of two sets? Here is the context:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
-- Eric Wieser
/-- The image of `zsqrtd` in `ℝ`. -/
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }
abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr
theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
refine omega.pred_mono_2 rfl _,
sorry,
end
```

Just before the `sorry`

the goal state is:

```
⊢ {x : ℝ | ∃ (a b : ℤ), x = ↑a + ↑b * 9 ^ (1 / 4)} = ↑((zsqrtd.to_real _).range)
```

I don't know where to begin on how to unroll that. `library_search`

times out and `suggest`

gives a long list of possibilities. I haven't done any set equivalence proofs so I don't know what will reduce this to more underlying material:

```
Try this: refine funext _
Try this: refine eq.symm _
Try this: refine set.ext _
Try this: refine eq_comm.mp _
Try this: refine eq_comm.mpr _
Try this: refine eq_of_heq _
Try this: refine congr_arg set_of _
Try this: refine mem_id_rel.mp _
Try this: refine heq_iff_eq.mp _
Try this: refine set.ext_iff.mpr _
Try this: refine plift.up.inj _
Try this: refine ulift.up.inj _
Try this: refine let_value_eq set_of _
Try this: refine compl_inj_iff.mp _
Try this: refine (list.mem_pure {x : ℝ | ∃ (a b : ℤ), x = ↑a + ↑b * 9 ^ (1 / 4)}
↑((zsqrtd.to_real
(show 0 ≤ 3, from
(id (eq_true_intro (norm_num.nonneg_pos 3 (bit1_pos' zero_lt_one')))).mpr trivial)).range)).mp
_
Try this: refine setoid.ker_def.mp _
Try this: refine has_top.mk.inj _
Try this: refine has_one.mk.inj _
Try this: refine has_bot.mk.inj _
Try this: refine has_coe.mk.inj _
Try this: refine option.some_inj.mp _
Try this: refine sum.inl.inj _
Try this: refine sum.inr.inj _
Try this: refine le_antisymm _ _
Try this: refine psum.inr.inj _
Try this: refine le_antisymm' _ _
Try this: refine psum.inl.inj _
Try this: refine (divp_left_inj _).mp _
Try this: refine except.ok.inj _
Try this: refine eq.trans _ _
Try this: refine inv_unique _ _
Try this: refine neg_unique _ _
Try this: refine (eq.congr_left _).mp _
Try this: refine (eq.congr_left _).mpr _
Try this: refine is_glb.unique _ _
Try this: refine is_lub.unique _ _
Try this: refine (eq.congr_right _).mp _
Try this: refine (eq.congr_right _).mpr _
Try this: refine subtype.mk.inj _
Try this: refine (eq.congr _ _).mp _
Try this: refine (eq.congr _ _).mpr _
Try this: refine pequiv.inj _ _ _
Try this: refine add_hom.mk.inj _
Try this: refine one_hom.mk.inj _
Try this: refine rel_hom.mk.inj _
Try this: refine mul_hom.mk.inj _
Try this: refine zero_hom.mk.inj _
Try this: refine subgroup.mk.inj _
Try this: refine subring.mk.inj _
Try this: refine alg_hom.mk.inj _
```

#### Mario Carneiro (Jan 07 2021 at 06:30):

Yakov Pechersky said:

`lemma two_equals_two : (2:ℝ) = (2:ℕ) := by norm_num`

I think `simp`

is doing all the work there

#### Eric Wieser (Jan 07 2021 at 07:45):

I have no idea what docs#omega.pred_mono_2 is, but I'm pretty sure you don't want to use it - it's undoing the progress made by `ext`

#### Lars Ericson (Jan 07 2021 at 17:46):

Thanks, per @Floris van Doorn I backed out the omega and applied docs#set.mem_set_of_eq and that gets me here which gets me back into predicate calculus and out of sets:

```
⊢ (∃ (a b : ℤ), x = ↑a + ↑b * 9 ^ (1 / 4)) ↔ x ∈ ↑((zsqrtd.to_real _).range)
```

I don't see that in the `suggest`

list, so that's a possible improvement for `suggest`

.

#### Alex J. Best (Jan 07 2021 at 18:01):

You can always do `suggest 100`

to get more suggestions, perhaps it shows up with a higher number than the default?

#### Lars Ericson (Jan 09 2021 at 04:38):

I got it this far but I'm out of ideas again:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
/-- The image of `zsqrtd` in `ℝ`. -/ -- Eric Wieser
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }
abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr
lemma fourth_root_of_nine_equals_sqrt_3 : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := sorry
theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw set.mem_set_of_eq,
split,
{
intro h1,
apply exists.intro,
split,
{
cases h1 with a ha,
cases ha with b hb,
exact trivial,
},
{
cases h1 with a ha,
cases ha with b hb,
norm_num,
have h2 := fourth_root_of_nine_equals_sqrt_3,
rw ← h2,
sorry,
},
exact zsqrtd.one,
},
{
intro h,
apply exists.intro,
apply exists.intro,
cases h,
unfold_coes,
sorry,
exact int.one,
exact int.one,
}
end
```

At the first `sorry`

, my tactic state is

```
1 goal
x: ℝ
ab: ℤ
hb: x = ↑a + ↑b * 9 ^ (1 / 4)
h2: 9 ^ (1 / 4) = real.sqrt 3
⊢ ↑(?m_1[_].re) + ↑(?m_1[_].im) * 9 ^ (1 / 4) = x
```

It's asking for real and imaginary parts of an unmatched thing. I haven't been reasoning about complex numbers, that just popped up.

The second `sorry`

also seems to want me to fill in some random number. The goal state is

```
3 goals
x: ℝ
h_w: ℤ√3
h_h: h_w ∈ ⊤.carrier ∧ ⇑(zsqrtd.to_real _) h_w = x
⊢ x = int.cast ?m_1[_] + int.cast ?m_2[_] * 9 ^ (1 / 4)
```

I don't understand how to work with these metavariables and what the tactics or theorems are that would apply.

#### Thomas Browning (Jan 09 2021 at 04:44):

things seem to start to go wrong at `apply exists.intro`

#### Mario Carneiro (Jan 09 2021 at 04:46):

This seems like a good starting point

```
theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw [fourth_root_of_nine_equals_sqrt_3],
simp [zsqrtd.to_real],
sorry
end
```

#### Mario Carneiro (Jan 09 2021 at 04:46):

the proof of the sorry should be very short, just unpacking and repacking the real and imaginary parts

#### Thomas Browning (Jan 09 2021 at 04:47):

By the way, the `re`

and `im`

aren't actually referring to complex numbers here

#### Thomas Browning (Jan 09 2021 at 04:47):

If you look at zsqrtd/basic.lean, you see this:

```
/-- The ring of integers adjoined with a square root of `d`.
These have the form `a + b √d` where `a b : ℤ`. The components
are called `re` and `im` by analogy to the negative `d` case,
but of course both parts are real here since `d` is nonnegative. -/
structure zsqrtd (d : ℤ) :=
(re : ℤ)
(im : ℤ)
```

#### Thomas Browning (Jan 09 2021 at 04:48):

so the `re`

and `im`

are referring to the `a`

and the `b`

in `a + b √d`

#### Lars Ericson (Jan 09 2021 at 14:38):

I have reached an absurdity. It is asking me to prove `⊢ a = b ∨ real.sqrt 3 = 0`

after the `simp *`

:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
/-- The image of `zsqrtd` in `ℝ`. -/ -- Eric Wieser
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }
abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr
lemma fourth_root_of_nine_equals_sqrt_3 : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := sorry
theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw [fourth_root_of_nine_equals_sqrt_3],
simp [zsqrtd.to_real],
split,
{
intro h1,
cases h1 with a ha,
cases ha with b hb,
apply exists.intro,
rw hb,
rotate,
exact {re := a, im := a},
simp *,
-- ⊢ a = b ∨ real.sqrt 3 = 0
},
{
sorry,
}
end
```

#### Kevin Buzzard (Jan 09 2021 at 14:40):

Do you know the maths proof of what you're trying to prove? Lean won't figure out the ideas, it will just check them.

#### Eric Wieser (Jan 09 2021 at 14:44):

I think the maths proof by the time you reach the `split`

is "both sides are obviously the same"

#### Eric Wieser (Jan 09 2021 at 14:45):

But in this case, your mistake is the `exact`

line

#### Eric Wieser (Jan 09 2021 at 14:46):

It should read `im := b`

#### Lars Ericson (Jan 09 2021 at 14:50):

@Kevin Buzzard what I actually wanted to prove is that the ring is closed under addition and multiplication as defined by `<a,b>+<c,d>=<a+b,c+d>`

and `<a,b>*<c,d> = <a*c+3*b*d, a*d+b*c>`

. In the recent above I am following expert suggestions which do not map directly to my original intuition.

#### Lars Ericson (Jan 09 2021 at 14:51):

@Eric Wieser I don't know the syntax to assign directly to the components of the goal. This doesn't work:

```
exact { im := b },
```

where the goal is

```
⊢ ↑(?m_1.re) + ↑(?m_1.im) * real.sqrt 3 = ↑a + ↑b * real.sqrt 3
```

#### Eric Wieser (Jan 09 2021 at 14:57):

You already have `im := a`

in your example code

#### Eric Wieser (Jan 09 2021 at 14:57):

Just change the a for a b

#### Eric Wieser (Jan 09 2021 at 14:57):

`congr`

would probably also solve that goal

#### Eric Wieser (Jan 09 2021 at 15:02):

I think `apply exists.intro`

is a recurring wrong choice you seen to be taking. When you're faced with an existential, your strategy should be to think of the maths proof and work out which object to provide; then use tactic#use

#### Lars Ericson (Jan 09 2021 at 16:16):

Thank you @Eric Wieser I will follow the advice on `exists.intro`

.

#### Lars Ericson (Jan 09 2021 at 18:37):

I got farther on the first half of the split.

On the second half, I'm trying to make `y=0 + 0 * sqrt(3)`

and apply it on the `exist`

which is in the assumptions. It's not going through, I don't know the syntax:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
/-- The image of `zsqrtd` in `ℝ`. -/ -- Eric Wieser
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }
abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr
lemma fourth_root_of_nine_equals_sqrt_3 : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := sorry
theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw [fourth_root_of_nine_equals_sqrt_3],
simp [zsqrtd.to_real],
split,
{
intro h1,
cases h1 with a ha,
cases ha with b hb,
use {re := a, im := b},
rw hb,
},
{
intro h,
use 0,
use 0,
simp *,
have y : ℤ√3 := {re := 0, im := 0},
have h3 := h y, -- ERROR
}
end
```

The goal state is

```
x: ℝ
h: ∃ (y : ℤ√3), ↑(y.re) + ↑(y.im) * real.sqrt 3 = x
y: ℤ√3
⊢ x = 0
```

#### Eric Wieser (Jan 09 2021 at 18:46):

Why did you `use 0`

?

#### Eric Wieser (Jan 09 2021 at 18:49):

Your goal state is unprovable because you used the wrong value

#### Eric Wieser (Jan 09 2021 at 18:50):

What was the goal state before the first `use 0`

?

#### Lars Ericson (Jan 09 2021 at 20:36):

I'm at this tactic state:

```
1 goal
x: ℝ
y: ℤ√3
hy: ↑(y.re) + ↑(y.im) * real.sqrt 3 = x
⊢ ∃ (a b : ℤ), ↑(y.re) + ↑(y.im) * real.sqrt 3 = ↑a + ↑b * real.sqrt 3
```

I want to set `y.re`

to `a`

and `y.im`

to `b`

. using something like

```
have y:ℤ√3 := a + b * real.sqrt 3,
```

and have that get applied to the goal to replace `y.re`

with `a`

and `y.im`

with `b`

. I don't know how to do it. This is just before the `sorry`

in

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
/-- The image of `zsqrtd` in `ℝ`. -/ -- Eric Wieser
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }
abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr
lemma fourth_root_of_nine_equals_sqrt_3 : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 := sorry
theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw [fourth_root_of_nine_equals_sqrt_3],
simp [zsqrtd.to_real],
split,
{
intro h1,
cases h1 with a ha,
cases ha with b hb,
use {re := a, im := b},
rw hb,
},
{
intro h1,
cases h1 with y hy,
rw ← hy,
sorry
}
end
```

#### Eric Wieser (Jan 09 2021 at 21:18):

`use [y.re, y.im]`

#### Lars Ericson (Jan 09 2021 at 22:51):

Exercise 6E, we hardly knew ye:

```
import data.zsqrtd.basic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
-- Eric Wieser
/-- The image of `zsqrtd` in `ℝ`. -/
@[simps]
noncomputable def zsqrtd.to_real {d : ℤ } (h : 0 ≤ d) : ℤ√d →+* ℝ := {
to_fun := λ a, a.1 + a.2*real.sqrt d,
map_zero' := by simp,
map_add' := λ a b, by { simp, ring, },
map_one' := by simp,
map_mul' := λ a b, by {
have : (↑a.re + ↑a.im * real.sqrt d) * (↑b.re + ↑b.im * real.sqrt d) =
↑a.re * ↑b.re + (↑a.re * ↑b.im + ↑a.im * ↑b.re) * real.sqrt d
+ ↑a.im * ↑b.im * (real.sqrt d * real.sqrt d) := by ring,
simp [this, real.mul_self_sqrt (int.cast_nonneg.mpr h)],
ring, } }
-- This definition is what each question in exercise 6 is asking. No need to restate it each time
abbreviation ex6 {α : Type*} [ring α] (s : set α) := ∃ (sr : subring α) [integral_domain sr], s = sr
lemma nine_equals_3_times_3 : (9:ℝ)=(3:ℝ)*(3:ℝ) :=
begin
linarith,
end
lemma three_is_gt_0 : (0:ℝ) < (3:ℝ) :=
begin
linarith,
end
lemma three_is_gte_0 : (0:ℝ) ≤ (3:ℝ) :=
begin
linarith,
end
lemma sqrt_of_9_is_3 : (3:ℝ) = (real.sqrt (9:ℝ)) :=
begin
have h1 := nine_equals_3_times_3,
rw h1,
have h2 := three_is_gte_0,
have h3 := real.sqrt_mul_self h2,
rw ← h1 at h3,
rw ← h1,
exact eq.symm h3,
end
lemma half_plus_half_equals_1: (1/2:ℝ)+(1/2:ℝ)=1 :=
begin
linarith,
end
lemma x_equals_sqrtx_times_sqrtx (x:ℝ): 0 < x → x = x^(1/2:ℝ) * x^(1/2:ℝ) :=
begin
intro h1,
have h2 := real.rpow_add h1,
have h3 := h2 (1/2) (1/2),
have h4 := half_plus_half_equals_1,
rw h4 at h3,
have h5 := real.rpow_one x,
rw h5 at h3,
exact h3,
end
lemma x_is_0 (x:ℝ) : x ≥ 0 → ¬(0 < x) → x = 0 :=
begin
intro h1,
intro h2,
linarith,
end
lemma half_ne_0 : (1/2:ℝ) ≠ (0:ℝ) :=
begin
linarith,
end
lemma zero_le_0 : (0:ℝ) ≤ (0:ℝ) :=
begin
linarith,
end
lemma sqrt_0_equals_0 : real.sqrt 0 = 0 :=
begin
have h1 := zero_le_0,
exact real.sqrt_eq_zero_of_nonpos h1,
end
lemma x_gt_0_implies_sqrt_x_gt_0 (x:ℝ): x ≥ 0 → x^(1/2:ℝ) ≥ 0 :=
begin
intro h1,
exact real.rpow_nonneg_of_nonneg h1 (1 / 2),
end
lemma sqrt_x_equals_sqrt_x (x:ℝ) : x ≥ 0 → x^(1/2:ℝ) = real.sqrt x :=
begin
intro h,
have h1 := x_equals_sqrtx_times_sqrtx x,
by_cases h2 : 0 < x,
{
have h3 := h1 h2,
conv
begin
to_rhs,
rw h3,
end,
have h5 := x_gt_0_implies_sqrt_x_gt_0 x,
have h6 := h5 h,
have h4 := real.sqrt_mul_self h6,
exact eq.symm h4,
},
{
have h3 := x_is_0 x,
have h4 := h3 h,
have h5 := h4 h2,
rw h5,
have h6 := @real.zero_rpow (1/2:ℝ),
have h7 := half_ne_0,
have h8 := h6 h7,
rw h8,
have h9 := sqrt_0_equals_0,
exact eq.symm h9,
}
end
lemma x_mul_x_pow_y_equals_x_pow_y_plus_y (x y : ℝ) : 0 < x → (x * x)^y = x^(y+y) :=
begin
intro h,
have h1 := le_of_lt h,
have h2 := @real.mul_rpow x x y h1 h1,
rw h2,
have h3 := real.rpow_add h y y,
exact eq.symm h3,
end
lemma fourth_root_of_9_equals_sqrt_sqrt : (9:ℝ) ^ (1/4:ℝ) = real.sqrt (real.sqrt (9:ℝ)) :=
begin
have h1 := nine_equals_3_times_3,
have h2 := three_is_gt_0,
have h7 := three_is_gte_0,
have h3 := sqrt_of_9_is_3,
rw ← h3,
rw h1,
have h4 := sqrt_x_equals_sqrt_x (3:ℝ),
have h5 := h4 h7,
rw ← h5,
have h6 := x_mul_x_pow_y_equals_x_pow_y_plus_y 3 (1/4),
have h8 := h6 h2,
rw h8,
ring,
end
lemma fourth_root_of_nine_equals_sqrt_3 : (9:ℝ) ^ (1/4:ℝ) = real.sqrt 3 :=
begin
have h1 := fourth_root_of_9_equals_sqrt_sqrt,
rw h1,
have h2 := sqrt_of_9_is_3,
rw h2,
end
abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr
theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw [fourth_root_of_nine_equals_sqrt_3],
simp [zsqrtd.to_real],
split,
{
intro h1,
cases h1 with a ha,
cases ha with b hb,
use {re := a, im := b},
rw hb,
},
{
intro h1,
cases h1 with y hy,
rw ← hy,
use [y.re, y.im],
}
end
```

#### Kevin Buzzard (Jan 09 2021 at 23:20):

I think it's easier if you just do it directly without using this zsqrtd stuff:

```
import tactic
import ring_theory.subring
import data.real.basic
import analysis.special_functions.pow
abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
∃ (sr : subring α) [integral_domain sr], s = sr
open real
lemma useful : ((9 : ℝ) ^ (4⁻¹ : ℝ)) * (9 ^ (4⁻¹ : ℝ)) = 3 :=
begin
rw ← mul_rpow,
convert pow_nat_rpow_nat_inv (show (0 : ℝ) ≤ 3, by norm_num) (show 0 < 4, by norm_num) using 2,
all_goals {norm_num}
end
def A : subring ℝ :=
{ carrier := {x | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)},
one_mem' := ⟨1, 0, by simp⟩,
mul_mem' := begin
rintro _ _ ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩,
use [a1 * a2 + 3 * b1 * b2, a1 * b2 + a2 * b1],
simp [mul_add, add_mul, mul_assoc, mul_left_comm, useful],
ring,
end,
zero_mem' := ⟨0, 0, by simp⟩,
add_mem' := by { rintro _ _ ⟨a1, b1, rfl⟩ ⟨a2, b2, rfl⟩,
use [a1 + a2, b1 + b2],
simp, ring },
neg_mem' := by { rintro _ ⟨a, b, rfl⟩,
use [-a, -b],
simp, ring },
}
noncomputable instance : integral_domain A := by apply_instance
theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
⟨A, infer_instance, rfl⟩
```

#### Kevin Buzzard (Jan 09 2021 at 23:30):

This way you just isolate the useful lemma and you don't ever need to engage with square roots at all.

#### Mario Carneiro (Jan 09 2021 at 23:31):

I disagree. The first lemma by Eric is supposed to be in mathlib (I think it's PR'd), and the rest is a few lines

#### Kevin Buzzard (Jan 09 2021 at 23:36):

Fair enough. My construction of the subring shouldn't be in mathlib and that's most of the work. I guess your way you still need to prove 9^{1/4}=sqrt(3), that just looked unappealing to me for some reason, but now I see we already have `sqrt_eq_rpow`

#### Kevin Buzzard (Jan 09 2021 at 23:39):

BTW we're missing `pow_inj : a^x=b^x -> a=b`

(modulo edge cases) (at least as far as I can see)

#### Mario Carneiro (Jan 09 2021 at 23:50):

```
theorem ex6e : is_an_integral_domain {x : ℝ | ∃ a b : ℤ, x = a + b * (9:ℝ) ^ (1/4:ℝ)} :=
begin
refine ⟨(zsqrtd.to_real (show 0 ≤ (3 : ℤ), by norm_num)).range, _, _⟩,
apply_instance,
ext,
rw calc (9:ℝ) ^ (1/4:ℝ) = (9:ℝ)^((2:ℕ)⁻¹ * (1/2) : ℝ) : by norm_num
... = ((3^2:ℝ)^((2:ℕ)⁻¹:ℝ)) ^ (1/2:ℝ) : by rw real.rpow_mul; norm_num
... = real.sqrt 3 : by rw [real.pow_nat_rpow_nat_inv, real.sqrt_eq_rpow]; norm_num,
simp [zsqrtd.to_real],
exact ⟨λ ⟨x,y,h⟩, ⟨⟨x,y⟩, h.symm⟩, λ ⟨⟨x,y⟩,h⟩, ⟨x,y, h.symm⟩⟩,
end
```

#### Lars Ericson (Jan 09 2021 at 23:51):

Kevin's proof is easier for me to follow because it directly constructs the subring.

#### Kevin Buzzard (Jan 09 2021 at 23:51):

Mario's proof is the same as yours, he just gets to the point more directly.

#### Mario Carneiro (Jan 09 2021 at 23:53):

There certainly seems to be some friction around `real.rpow`

that could use some automation

#### Kevin Buzzard (Jan 09 2021 at 23:53):

I don't think I've ever seen `rw calc`

before, and it doesn't seem to ever occur in mathlib.

#### Mario Carneiro (Jan 09 2021 at 23:53):

It would be `rw show`

but `calc`

kind of has `show`

built in

#### Kevin Buzzard (Jan 09 2021 at 23:54):

Nice!

#### Eric Wieser (Jan 10 2021 at 00:40):

@Lars Ericson, the point of my approach to the proof is that mathlib already has the ring construction so there is no need to build it yourself

#### Eric Wieser (Jan 10 2021 at 00:40):

Pedagogically of course, you can still do so

#### Lars Ericson (Jan 10 2021 at 01:09):

@Eric Wieser , I'm grateful for your help. In this example, the relevant subring was already mostly in `mathlib`

, except for the multiplication which you define in `zsqrtd.to_real`

. For a beginner like myself, to transfer the techniques to a subring which is not already in `mathlib`

, the pattern of `def A`

seems easier to replicate.

#### Eric Wieser (Jan 27 2021 at 22:47):

docs#zsqrtd.to_real is now merged

Last updated: May 17 2021 at 22:15 UTC