# Zulip Chat Archive

## Stream: new members

### Topic: classical.some

#### Anya Michaelsen (Jul 24 2020 at 21:56):

Hi! I've been working on writing a theorem for the Chinese Remainder Theorem ring isomorphism. I already have a theorem that gives the existence of a solution to a pair of congruences and want to use that to define one of the isomorphism maps. When proving that this map and the projection are inverses for the ring isomorphism, I ran into `classical.some _' in my goal and am not sure how to work with this, i.e. access the properties that it has. I looked at the docs for classical.some and classical.some_spec but since I didn't create the classical.some (it seems to have been generated by the function.inverse goal on simplification), I'm not sure how to use these. Here is a snap shot of the code:

```
theorem CRTwith2 (n m : ℕ) (H: coprime n m) (npos: n > 0) (mpos: m > 0) : zmod (n*m) ≃+* zmod n × zmod m :=
begin
--define maps
use (λ x, (x, x)),
intro xy,
have CRT := CRTwith2exist xy.1.val xy.2.val n m npos mpos H,
/-theorem CRTwith2exist (a1 a2 M1 M2 : ℕ ) (M1pos : 0 < M1) (M2pos : 0 < M2) (H : coprime M1 M2) :
∃ x : ℕ , modeq M1 x a1 ∧ modeq M2 x a2 -/
choose x Hx using CRT,
use x,
-- show inverses (needs classical.some)
{
intro y,
simp,
-- Goal here: ⊢ ↑(classical.some _) = y
},
--show other proprties...
end
```

Clicking on 'classical.some _' in Lean Infoview yields this picture

#### Kevin Buzzard (Jul 24 2020 at 22:18):

@Anya Michaelsen can you post complete working code (i.e. include all imports)?

#### Scott Morrison (Jul 24 2020 at 23:19):

You might like the definition

```
/--
A convenience method for extracting the property satisfied by a term which is merely equal to
`classical.some _`.
-/
lemma classical.spec_of_eq_some
{α : Type*} {p : α → Prop} {a : α} {w : ∃ x, p x} (h : a = classical.some w) : p a :=
begin
subst h,
apply classical.some_spec,
end
```

that Johan and I recently wanted while working on sheaves, to deal with something just like this.

#### Scott Morrison (Jul 24 2020 at 23:19):

(It will eventually be PR'd to mathlib, but you can copy and paste it and use already.)

#### Anya Michaelsen (Jul 25 2020 at 00:00):

Here the full code for this file. The other version of `CRTwith2exists`

is in a file CRT.lean (the first import)

```
import CRT
import data.nat.basic
import data.nat.modeq
import data.nat.gcd
import data.zmod.basic
import tactic
import data.equiv.ring
noncomputable theory
open nat nat.modeq zmod CRT
-------------------------ISOMORPHISM VERSION--------------------------
theorem CRTwith2 (n m : ℕ) (H: coprime n m) (npos: n > 0) (mpos: m > 0) : zmod (n*m) ≃+* zmod n × zmod m :=
begin
--define maps
use (λ x, (x, x)),
intro xy,
have CRT := CRTwith2exist xy.1.val xy.2.val n m npos mpos H,
/-theorem CRTwith2exist (a1 a2 M1 M2 : ℕ ) (M1pos : 0 < M1) (M2pos : 0 < M2) (H : coprime M1 M2) :
∃ x : ℕ , modeq M1 x a1 ∧ modeq M2 x a2 -/
choose x Hx using CRT,
use x,
-- show inverses (needs classical.some)
{
intro y,
simp,
-- Goal here: ⊢ ↑(classical.some _) = y
},
--show other proprties...
end
```

#### Scott Morrison (Jul 25 2020 at 00:31):

Unfortunately this doesn't help us as a #mwe.

#### Scott Morrison (Jul 25 2020 at 00:32):

The point is to give us a chunk of code to copy and paste into VSCode, so we can play with it.

#### Reid Barton (Jul 25 2020 at 00:37):

This is difficult partly because you're using tactics to create data. In fact `CRTwith2`

should be a `def`

, not a `theorem`

.

#### Reid Barton (Jul 25 2020 at 00:38):

is there a way to construct `≃+*`

where you only give the forward map?

#### Reid Barton (Jul 25 2020 at 00:40):

this pattern (product a ring isomorphism by giving a ring map that's bijective) ought to be in the library already

#### Reid Barton (Jul 25 2020 at 00:52):

So there's docs#equiv.of_bijective and the extra fields of `ring_hom`

only pertain to the forward map, so this should work. I suggest defining a plain `equiv`

using `equiv.of_bijective`

first and then extending it to a `ring_hom`

.

#### Scott Morrison (Jul 25 2020 at 00:55):

I recently constructed a `≃+*`

using the antipattern `{ ..f, ..e}`

, where `f`

was a `ring_hom`

and `e`

an `equiv`

. I'd also be happy to have a named constructor for this, or to learn where it is.

#### Mario Carneiro (Jul 25 2020 at 00:59):

why is that an antipattern? It's actually doing something you can't achieve with a named constructor, namely verifying a defeq

#### Reid Barton (Jul 25 2020 at 01:12):

does it actually verify a defeq, or does it just check that the `ring_hom`

proofs also type check against the `equiv`

fields (or vice versa?)

#### Reid Barton (Jul 25 2020 at 01:13):

But yeah, since `ring_hom`

only has extra `Prop`

fields, it would make sense to have a constructor from `equiv`

and `ring_hom`

plus a hypothesis of `=`

#### Scott Morrison (Jul 25 2020 at 01:45):

Hmm, okay, I see it's not so bad.

#### Kevin Buzzard (Jul 25 2020 at 08:50):

Maybe we should switch to `is_ring_hom`

? Oh wait...

#### Reid Barton (Jul 25 2020 at 12:21):

Well, the issue was never really `is_ring_hom`

existing, it was being a class

Last updated: May 14 2021 at 04:22 UTC