use?

Stream: maths

[Ashvni Narayanan]

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]

Try convert g'

[Ashvni Narayanan]

Doesn't work :(

[Anne Baanen]

Does it fail or result in new goals?

[Ashvni Narayanan]

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]

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

[Anne Baanen]

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

[Ashvni Narayanan]

https://github.com/leanprover-community/mathlib/blob/d008b1c22ad3f20f61915a66f95a64615709d07f/src/ring_theory/dedekind_domain.lean#L286

[Ashvni Narayanan]

Ashvni Narayanan said:

https://github.com/leanprover-community/mathlib/blob/d008b1c22ad3f20f61915a66f95a64615709d07f/src/ring_theory/dedekind_domain.lean#L286

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

[Anne Baanen]

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

[Anne Baanen]

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

[Anne Baanen]

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

[Ashvni Narayanan]

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

[Ashvni Narayanan]

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]

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]

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]

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

[Anne Baanen]

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

[Ashvni Narayanan]

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

[Ashvni Narayanan]

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

[Anne Baanen]

You're welcome!