## Stream: maths

### Topic: use?

#### Ashvni Narayanan (Oct 27 2020 at 09:18):

I am trying to prove

?m_1 ∈ submodule.comap (localization_map.lin_coe (fraction_ring.of A)) I.val


and I have

g': y ∈ submodule.comap (localization_map.lin_coe (fraction_ring.of A)) I.val


where ?m_1 must be of type A, and y is of type A. However, none of exact, refine, assumption or use work.

Any help is appreciated. Thank you!

#### Anne Baanen (Oct 27 2020 at 09:19):

Try convert g'

Doesn't work :(

#### Anne Baanen (Oct 27 2020 at 09:20):

Does it fail or result in new goals?

#### Ashvni Narayanan (Oct 27 2020 at 09:20):

invalid type ascription, term has type
?m_1
but is expected to have type
?m_1 ∈ submodule.comap (localization_map.lin_coe (fraction_ring.of A)) I.val


#### Ashvni Narayanan (Oct 27 2020 at 09:21):

Well the next goal is to prove that ?m_1 : A.

#### Anne Baanen (Oct 27 2020 at 09:21):

Hmm, could you post a #mwe? It looks like Lean is getting confused earlier on.

#### Ashvni Narayanan (Oct 27 2020 at 09:24):

Ashvni Narayanan said:

Does this help? If not, I'll make an mwe.

#### Anne Baanen (Oct 27 2020 at 09:26):

That should be enough, thanks! One moment please...

#### Anne Baanen (Oct 27 2020 at 09:30):

Aha, the problem seems to be this: you define y in one subgoal, but it should be used in another subgoal.

#### Anne Baanen (Oct 27 2020 at 09:32):

(I'm guessing you did this because you got errors when writing cases (g : ∃ (x : localization (non_zero_divisors A)), x ∈ I)?

#### Ashvni Narayanan (Oct 27 2020 at 09:32):

I did try rotate, but that ended up giving me other issues with using cases, hence I did not proceed..

#### Ashvni Narayanan (Oct 27 2020 at 09:32):

Anne Baanen said:

(I'm guessing you did this because you got errors when writing cases (g : ∃ (x : localization (non_zero_divisors A)), x ∈ I)?

Haha yes exactly

#### Anne Baanen (Oct 27 2020 at 09:36):

Hmm, I don't know to fix the proof because I'm not quite sure what you're trying to prove here actually. Your goal ↥(submodule.comap (localization_map.lin_coe (fraction_ring.of A)) I.val) means "we can compute an element of the ideal" (let's just call it J), but surely we have 0 \in J?

#### Ashvni Narayanan (Oct 27 2020 at 09:39):

What I actually want to prove is that if we have a fractional ideal I, and I \leq 1, then (the preimage of) I must be an ideal of A.

#### Anne Baanen (Oct 27 2020 at 09:40):

Ah, this turns out to be called submodule.comap, as in the function you used to construct your goal :)

#### Anne Baanen (Oct 27 2020 at 09:42):

(In fact, this holds for all fractional ideals: everything outside of A is just discarded by comap.)

#### Ashvni Narayanan (Oct 27 2020 at 09:46):

Ah I see, hence the I \le 1 is not needed!

#### Ashvni Narayanan (Oct 27 2020 at 09:46):

Apologies for this, and thank you for your help! :)

#### Anne Baanen (Oct 27 2020 at 09:47):

You're welcome!

Last updated: May 11 2021 at 16:22 UTC