How to multiply an integer times a real

Stream: new members

[Lars Ericson]

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]

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]

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]

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]

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]

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]

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

[Eric Wieser]

You seem to be mixing the proof with the theorem statement

[Bryan Gin-ge Chen]

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]

I think your statement can be proved with use [\top], ... which shows your statement is wrong

[Lars Ericson]

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]

The proof of closure is s.mul_mem for your subring lemma

[Lars Ericson]

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]

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]

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

[Lars Ericson]

6E:
Screenshot-from-2021-01-05-21-23-27.png

[Lars Ericson]

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]

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]

or use subring.closure _

[Yakov Pechersky]

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]

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

[Alex J. Best]

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]

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

[Alex J. Best]

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]

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]

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]

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]

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]

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]

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]

but I think there might be some lemmas missing about subring.closure to show this

[Yakov Pechersky]

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]

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]

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]

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]

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]

For sure, for any (a b : ℤ), a + b * (9 ^ 1 / 4) ∈ ℝ (to use set theory notation.

[Yakov Pechersky]

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]

@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]

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]

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

[Yakov Pechersky]

It does remember! It'll show ↑1 for my (1 : ℤ) which is in an expression that expects an ℝ.

[Alex J. Best]

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]

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]

In other words we are spending a lot of time on coercions and has_pows 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]

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]

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]

It's what Eric remarked on earlier.

[Alex J. Best]

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]

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

[Alex J. Best]

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

[Yakov Pechersky]

Ideally, the lemmas about subring.closure should allow you to say:

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

instead

[Alex J. Best]

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]

btw the last line can be expressed as:

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

[Yakov Pechersky]

because the parent ring on ℝ is also an integral domain

[Yakov Pechersky]

But I guess proving that is part of the exercise

[Alex J. Best]

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]

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

[Eric Wieser]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Alex J. Best]

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

[Eric Wieser]

I'll make a pr

[Eric Wieser]

/-- 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]

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]

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]

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

[Kevin Buzzard]

Both should ;-)

[Kevin Buzzard]

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]

#5640

[Eric Wieser]

I only added to_real because we only have real.sqrt

[Eric Wieser]

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

[Kevin Buzzard]

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

[Alex J. Best]

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]

I've solved the lemma in the PR

[Eric Wieser]

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

[Eric Wieser]

@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]

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]

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

[Eric Wieser]

However, you can still use the abbreviation ex6definition without the PR

[Lars Ericson]

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]

Yes, you need import analysis.special_functions.pow

[Lars Ericson]

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]

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]

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

[Lars Ericson]

It wants a d.

[Lars Ericson]

Should I add variable d: ℕ in context?

[Eric Wieser]

Just add {d : ℕ} after the word to_real

[Lars Ericson]

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]

d should be a \Z

[Lars Ericson]

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]

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

[Lars Ericson]

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]

a_squared_equals_a_times_a is docs#pow_two (or rather, its reverse)

[Eric Wieser]

Always try library_search for trivial lemmas like that first :)

[Lars Ericson]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

You might like docs#mul_rpow

[Lars Ericson]

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]

Your lemma isn't true is x = 0 and y = 0

[Yakov Pechersky]

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]

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

[Lars Ericson]

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]

The first one is le_of_lt

[Lars Ericson]

@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]

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]

Yakov Pechersky said:

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

I think simp is doing all the work there

[Eric Wieser]

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]

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]

You can always do suggest 100 to get more suggestions, perhaps it shows up with a higher number than the default?

[Lars Ericson]

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]

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

[Mario Carneiro]

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]

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

[Thomas Browning]

By the way, the re and im aren't actually referring to complex numbers here

[Thomas Browning]

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]

so the re and im are referring to the a and the b in a + b √d

[Lars Ericson]

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]

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]

I think the maths proof by the time you reach the split is "both sides are obviously the same"

[Eric Wieser]

But in this case, your mistake is the exact line

[Eric Wieser]

It should read im := b

[Lars Ericson]

@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]

@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]

You already have im := a in your example code

[Eric Wieser]

Just change the a for a b

[Eric Wieser]

congr would probably also solve that goal

[Eric Wieser]

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]

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

[Lars Ericson]

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]

Why did you use 0?

[Eric Wieser]

Your goal state is unprovable because you used the wrong value

[Eric Wieser]

What was the goal state before the first use 0?

[Lars Ericson]

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]

use [y.re, y.im]

[Lars Ericson]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

There certainly seems to be some friction around real.rpow that could use some automation

[Kevin Buzzard]

I don't think I've ever seen rw calc before, and it doesn't seem to ever occur in mathlib.

[Mario Carneiro]

It would be rw show but calc kind of has show built in

[Kevin Buzzard]

Nice!

[Eric Wieser]

@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]

Pedagogically of course, you can still do so

[Lars Ericson]

@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]

docs#zsqrtd.to_real is now merged