eq.rec goal

Stream: general

[Kevin Buzzard]

If my goal is

eq.rec (finsupp.prod g₂ (λ (r : R) (n : ℤ), minimal_value_group.mk v₂ r ^ n)) _ =
    finsupp.prod g₂ (λ (r : R) (n : ℤ), minimal_value_group.mk v₂ r ^ n)

then did I take a wrong turn or is there some easy way to finish this?

[Johannes Hölzl]

If both sides are definitional equal then you can just apply refl. Proof irrelevance in definitional equality allowseq.rec to compute as long as the data fits.

[Johannes Hölzl]

So the _ (before =) may be an arbitrary proof, even a variable. Still eq.rec can reduce by computation, Lean will interpret an arbitrary proof as refl _ as this always fits

[Kevin Buzzard]

I tried refl and it didn't work, that's why I posted here :-/

[Kevin Buzzard]

dsimp takes me to

⊢ eq.rec (finsupp.prod g₂ (λ (r : R), pow (minimal_value_group.mk v₂ r))) _ =
    finsupp.prod g₂ (λ (r : R), pow (minimal_value_group.mk v₂ r))

[Kevin Buzzard]

I haven't got my head around the goal really.

[Kevin Buzzard]

There are no weird variable names occurring twice:

R : Type u₁,
_inst_4 : comm_ring R,
Γ₁ : Type u₂,
_inst_5 : linear_ordered_comm_group Γ₁,
Γ₂ : Type u₃,
_inst_6 : linear_ordered_comm_group Γ₂,
v₁ : valuation R Γ₁,
v₂ : valuation R Γ₂,
h : is_equiv v₁ v₂,
g₁ g₂ : multiplicative (R →₀ ℤ),
h12 :
  (λ (f : multiplicative (R →₀ ℤ)),
       finsupp.prod f (λ (r : R) (n : ℤ), (λ (r : R), option.get_or_else (⇑v₁ r) 1) r ^ n))
      (g₁⁻¹ * g₂) =
    1,
this :
  finsupp.prod g₁ (λ (r : R) (n : ℤ), minimal_value_group.mk v₂ r ^ n) =
    finsupp.prod g₂ (λ (r : R) (n : ℤ), minimal_value_group.mk v₂ r ^ n)
⊢ eq.rec (finsupp.prod g₂ (λ (r : R), pow (minimal_value_group.mk v₂ r))) _ =
    finsupp.prod g₂ (λ (r : R), pow (minimal_value_group.mk v₂ r))

[Kevin Buzzard]

There might be universe issues. Is this possible?

[Kevin Buzzard]

@Patrick Massot I am scared I am running into problems because of that structure with a new type in the data.

[Mario Carneiro]

you haven't really said all that is needed to identify the problem

[Mario Carneiro]

eq.rec hides a lot of info

[Kevin Buzzard]

https://gist.github.com/kbuzzard/75f316bccc64cb17f5217e02e364b4e8

[Mario Carneiro]

what is the type of the argument in the _?

[Kevin Buzzard]

What's an easy way to find this out?

[Kevin Buzzard]

I don't understand the goal.

[Mario Carneiro]

possibly suffices h, change eq.rec (finsupp.prod g₂ (λ (r : R), pow (minimal_value_group.mk v₂ r))) h = _

[Kevin Buzzard]

invalid 'eq.rec' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables
  ?m_1

[Kevin Buzzard]

If you can explain what the goal means then I can think about the maths and try and figure out what I have done.

[Kevin Buzzard]

The goal appeared when I had a term in a quotient group and I applied the induction tactic on the term.

[Mario Carneiro]

well this is the problem with eq.rec terms, they don't give enough information to be reconstructible

[Kevin Buzzard]

Hmm.

[Kevin Buzzard]

Maybe cases would have been a better tactic.

[Mario Carneiro]

this is the fault of a simp or rw somewhere

[Mario Carneiro]

does @@eq.rec (λ (g : @valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₂} Γ₁ _inst_5 (@valuation.minimal_value_group.{u₁ u₂} R _inst_4 (λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b)) Γ₁ _inst_5 v₁)), @valuation.minimal_valuation.parametrized_subgroup.Γ.{u₁ u₃} Γ₂ _inst_6 (@valuation.minimal_value_group.{u₁ u₃} R _inst_4 (λ (a b : R), classical.prop_decidable (@eq.{u₁+1} R a b)) Γ₂ _inst_6 v₂)) _ h = _ work?

[Kevin Buzzard]

cases doesn't work but perhaps I need to think about the moment the term appeared and try something less naive.

[Mario Carneiro]

for the term in the change

[Mario Carneiro]

That looks like a constant function, meaning you tried to cast a term across an equality of types

[Kevin Buzzard]

type mismatch at application
  eq.rec ?m_2 h
term
  h
has type
  is_equiv v₁ v₂
but is expected to have type
  ?m_1 = ?m_2

[Mario Carneiro]

did you suffices h,?

[Kevin Buzzard]

So the goal originally had an eq.rec with one of the g2's replaced by a g1, and I thought "I don't understand that goal, maybe it's just a stupid way of saying the two terms are equal". So I wrote

  suffices : finsupp.prod g₁ (λ (r : R) (n : ℤ), minimal_value_group.mk v₂ r ^ n) =
             finsupp.prod g₂ (λ (r : R) (n : ℤ), minimal_value_group.mk v₂ r ^ n),
    rw this,

because I fancied my chances at proving this. So I did a rewrite inside an eq.rec and that's what has burnt me.

[Mario Carneiro]

can you show more context? What's the proof

[Mario Carneiro]

that goal doesn't look that bad, you are just proving an equality

[Kevin Buzzard]

This was the goal:

eq.rec (finsupp.prod g₁ (λ (r : R) (n : ℤ), minimal_value_group.mk v₂ r ^ n)) _ =
    finsupp.prod g₂ (λ (r : R) (n : ℤ), minimal_value_group.mk v₂ r ^ n)

and then I wrote the "suffices" stuff above

[Mario Carneiro]

no no, like 6 steps before this

[Mario Carneiro]

how did we get here

[Mario Carneiro]

this isn't very MWE so give some more context

[Kevin Buzzard]

induction g was where things started to go wrong.

[Kevin Buzzard]

g is an element of a quotient group.

[Mario Carneiro]

I have no idea what g is or what induction is proving

[Kevin Buzzard]

but I wanted to get an element of the top group

[Kevin Buzzard]

and the eq.rec is the assertion that my argument is independent of the choice of lift.

[Mario Carneiro]

The _ argument is a quot.sound according to your pp.all

[Johan Commelin]

@Kevin Buzzard Post the entire lemma + proof-attempt + tactic state. I guess that will help more.

[Kevin Buzzard]

-- Notes: if v1 equiv v2 then we need a bijection from the image of v1 to the
-- image of v2; we need that the supports are the same; we need that
-- the minimal_value_group for v2 is isomorphic to the subgroup of Gamma_2 generated
-- by the image of the stuff not in the support.

-- Theorem we almost surely need -- two equivalence valuations have isomorphic
-- value groups.
lemma minimal_valuations_biject_of_equiv {R : Type u₁} [comm_ring R]
{Γ₁ : Type u₂} [linear_ordered_comm_group Γ₁]
{Γ₂ : Type u₃} [linear_ordered_comm_group Γ₂]
(v₁ : valuation R Γ₁) (v₂ : valuation R Γ₂) (h : is_equiv v₁ v₂) :
(minimal_value_group v₁).Γ  → (minimal_value_group v₂).Γ :=
λ g, begin
  induction g with g g₁ g₂ h12,
    exact finsupp.prod g (λ r n,(minimal_value_group.mk v₂ r) ^ n),
  cases h12 with h12 hoops,
    swap,cases hoops,
  -- If φ1 is the function from R to Γ1 which is v1 away from the support and
  -- sends the support to 1, then φ1 extends to a group hom Z[R] -> Γ1 (free ab group on R)
  -- and h12 is the hypothesis that g₁⁻¹g₂ is in the kernel, so g₁ and g₂ get sent to
  -- the same element of Γ1. We need the analogous result for φ2.
  convert rfl,
  suffices : finsupp.prod g₁ (λ (r : R) (n : ℤ), minimal_value_group.mk v₂ r ^ n) =
             finsupp.prod g₂ (λ (r : R) (n : ℤ), minimal_value_group.mk v₂ r ^ n),
   subst this,
    swap,sorry,
  simp,
  dsimp,
  -- I am in eq.rec hell
end

[Kevin Buzzard]

Instead of induction g I could perhaps have used some more suitable approach for working with quotient groups.

[Mario Carneiro]

you are constructing a function by tactics?

[Kevin Buzzard]

oh oops

[Mario Carneiro]

this isn't a lemma

[Kevin Buzzard]

oh yeah

[Kevin Buzzard]

good catch. It used to be a lemma.

[Kevin Buzzard]

dammit

[Mario Carneiro]

I see, you should have used quotient.lift instead of this induction/cases business

[Kevin Buzzard]

even if this worked I wouldn't be able to prove anything about it.

[Kevin Buzzard]

Yes. Do you remember that a few weeks ago I constructed my own quotient types just by using sets of equivalence classes?

[Kevin Buzzard]

And I said "look what I did, what's all this quot axiom stuff?"

[Kevin Buzzard]

and people made comments about computability that I didn't understand.

[Mario Carneiro]

What is (minimal_value_group v₁).Γ?

[Mario Carneiro]

is it a quotient?

[Mario Carneiro]

or more to the point, shouldn't it be hidden behind an API?

[Kevin Buzzard]

Yes

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/why.20is.20quot.20an.20axiom.3F

[Kevin Buzzard]

Can you see that the proof...erm...construction is full of comments? I was just trying to run at it and make notes to see what API I need.

[Kevin Buzzard]

The top down approach, frowned upon by you guys.

[Kevin Buzzard]

I'm not as good as you at working out what API I need, I just try and prove the thing I want and let the API come later when I get stuck.

[Mario Carneiro]

well, minimal_value_group sounds like a thing you want to have an abstract characterization of

[Mario Carneiro]

if it's defined as a quotient, then probably there is a lift like theorem about it, possibly slightly different than the one lean gives you

[Mario Carneiro]

what's the math story here?

[Kevin Buzzard]

The notes above the theorem are intermediate results which I realised I needed precisely because I was getting stuck. There is more than one sorry in the proof.

[Kevin Buzzard]

There is a set-theoretic issue in the definition of a perfectoid space and it is one that we have already talked about at length.

[Mario Carneiro]

right

[Mario Carneiro]

minimal_value_group is the resolution, and it has a UMP that you put some blood/sweat/tears into

[Mario Carneiro]

use it

[Kevin Buzzard]

A valuation on a ring R is a pair consisting of an abelian group G in an arbitrary universe and, lying slightly, a map from R to G.

[Kevin Buzzard]

The blood sweat and tears was replacing G by a group G' in the same universe as R and proving that the new valuation was equivalent to the old one.

[Kevin Buzzard]

I am trying to prove a random thing about this equivalence that I am not ready for, but my idea is that proving it tells me more about the API I need.

[Mario Carneiro]

So G' is minimal_value_group right?

[Mario Carneiro]

You say replacing G by G', what is the relation between them

[Kevin Buzzard]

Let's say two valuations on R are isomorphic if the G's are isomorphic and the diagram commutes.

[Kevin Buzzard]

I am trying to prove that if two valuations are equivalent, then the associated minimal valuations are isomorphic.

[Mario Carneiro]

aha, okay, that sounds like an easy consequence of the right UMP

[Kevin Buzzard]

If R were a group and v were a group homomorphism (which it may as well be for the purposes of this discussion) then the minimal valuation group would be the image of R under v

[Kevin Buzzard]

wait that's exactly wrong

[Kevin Buzzard]

the minimal valuation group would be the quotient of R by the kernel of v

[Kevin Buzzard]

which is in R's universe

[Mario Carneiro]

there should be some kind of commutative diagram here

[Mario Carneiro]

like a map factors through this minimal valuation

[Kevin Buzzard]

I think what I need is a second "minimal" valuation which is the thing I just said, replace G with the subgroup which is the image of R

[Mario Carneiro]

didn't you already do that?

[Kevin Buzzard]

I never introduced the second one.

[Kevin Buzzard]

Given R,G,v I made G1 := R/ker(v)

[Kevin Buzzard]

(here R is a group)

[Kevin Buzzard]

(and v a group hom)

[Kevin Buzzard]

but I never made G2 := im(v)

[Kevin Buzzard]

and I think that I must need it.

[Mario Carneiro]

we don't need it

[Kevin Buzzard]

Oh great!

[Mario Carneiro]

they are iso, right?

[Kevin Buzzard]

Yes

[Mario Carneiro]

what we need is the UMP associated to G1

[Kevin Buzzard]

I see.

[Mario Carneiro]

if you have a suitable map out of R, it factors through the valuation to make a map out of G1

[Kevin Buzzard]

I proved that (v,G) and (v1,G1) were equivalent

[Mario Carneiro]

or something like that

[Kevin Buzzard]

but I need more.

[Kevin Buzzard]

This is really annoying. I might need G2.

[Mario Carneiro]

this should all be a consequence of the fact that you defined G1 := R/ker(v), just unfold what those things mean

[Kevin Buzzard]

The definition of equivalent is really crappy. v:R->G and w:R->H are equivalent if the image of v and the image of w are isomorphic via an isomorphism that makes the diagram commute.

[Mario Carneiro]

sounds fine to me

[Kevin Buzzard]

the problem is that this involves images

[Mario Carneiro]

although maybe it might be good to have the one directional version, make a category kind of setup

[Mario Carneiro]

because then you can talk about initiality

[Kevin Buzzard]

Actually, another problem is that not even this is the definition, this is a lemma which I am only now realising I need.

[Kevin Buzzard]

Dammit the underlying problem is exactly this "mathematicians don't know how to write an API" issue. I write something down and then because so many things are trivially true and their proof does not even need mentioning, I can lecture on it assuming a whole bunch of stuff (like the first isomorphism theorem) and not even notice what I am using.

[Kevin Buzzard]

I can see exactly which lemmas have content and it's those that I prove in a lecture

[Mario Carneiro]

You have a category of valuations and valuation morphisms, where the homs v -> w are ordered group homs f : G->H such that v o f = w

[Kevin Buzzard]

but you want me to prove all the content-free ones.

[Kevin Buzzard]

Is there an issue with this approach because the valuations can take values in an arbitrary universe?

[Mario Carneiro]

you don't have to define this category explicitly, but you should keep it in mind to state the facts

[Kevin Buzzard]

But you're right, this is exactly the thing I should be thinking about. I have not defined a morphism of valuations.

[Mario Carneiro]

as long as you don't try to define the category, the universe thing shouldn't matter

[Kevin Buzzard]

But I need to define the morphisms because I am using them again and again.

[Mario Carneiro]

and an iso in this category should be an equivalence of valuations

[Kevin Buzzard]

It's worse than that

[Mario Carneiro]

and the minimal valuation is an initial object in the category

[Kevin Buzzard]

An iso in this category is an isomorphism of valuations

[Kevin Buzzard]

The equivalences are the ones for which the underlying map G -> H is an injection

[Kevin Buzzard]

no it's not even that

[Kevin Buzzard]

the equivalences are ones for which the underlying map G -> H induces an isomorphism v(R) -> w(R)

[Kevin Buzzard]

The problem is that these groups are "too big" in general

[Kevin Buzzard]

so isomorphism is too strong

[Kevin Buzzard]

We only care about the image of R

[Kevin Buzzard]

hence the notion of equivalence

[Mario Carneiro]

why isn't that the same as I said?

[Kevin Buzzard]

Because if G=R and H is a far larger group containing R and both v and w are the obvious maps

[Mario Carneiro]

for the condition v o f = w only the value on elements of R matters

[Kevin Buzzard]

but there's no map H -> G

[Kevin Buzzard]

which is the identity on G. Groups are harder than that.

[Mario Carneiro]

I see, so you want f : v(R) -> w(R) but otherwise it should be the same

[Mario Carneiro]

is v(R) a subgroup?

[Kevin Buzzard]

yes

[Kevin Buzzard]

I am talking about a toy model where R is a group and v is a group hom

[Kevin Buzzard]

The truth is that R is a ring, G is an ordered group, v goes from R to G union {0} and satisfies some axioms

[Kevin Buzzard]

but that's not the problem as far as I am concerned.

[Kevin Buzzard]

I think the underlying problems I have are all present in the toy model.

[Mario Carneiro]

so does it work like I said? Homs are f : v(R) -> w(R) such that v o f = w

[Kevin Buzzard]

Yes! But you said homs are f : G -> H such that v o f = w I think

[Mario Carneiro]

and now isos are equivalences of valuations

[Kevin Buzzard]

yes

[Kevin Buzzard]

It's a strange category because the f's are not defined on the full groups but this is the way to think about it I think

[Mario Carneiro]

now there are some issues because functions on images are not nice in lean

[Kevin Buzzard]

I think it's important to let G and H be as big as you like, because we don't want to write "WLOG v is surjective" everywhere.

[Mario Carneiro]

that's fine, I think, as long as the homs take this into account

[Kevin Buzzard]

[in the real model, the "image" is actually the subgroup of G generated by v(R') where R' is the subset of R consisting of elements r such that v(r) is not zero]

[Kevin Buzzard]

But I have never once used this image, or even defined it.

[Mario Carneiro]

then what is f?

[Mario Carneiro]

do you let it be 0 outside or something?

[Kevin Buzzard]

I consistently use the quotient of the free abelian group on R -- the thing in the right universe.

[Kevin Buzzard]

There's an auxiliary function v' which is defined to be v on R' and if v(r)=0 then v'(r)=1.

[Kevin Buzzard]

I then look at the map from the free abelian group on R to G extending v' and the minmal value group is the quotient of the free abelian group on R by the kernel of this map.

[Kevin Buzzard]

I only mention these technicalities because you mentioned the image as being hard to work with and actually we have something more complicated than the image. But note that I never constructed the image. We can look at the subgroup of G generated by v' but this object, which is isomorphic to the minimal value group, has never been mentioned before.

[Mario Carneiro]

in a lot of ways the coimage is actually easier to work with

[Kevin Buzzard]

The coimage is what we have, right?

[Kevin Buzzard]

The quotient of the free ab group by the kernel?

[Mario Carneiro]

yes, seems like

[Kevin Buzzard]

When I was saying "pretend R is a group" earlier I was thinking "replace R by the free abelian group on R'"

[Mario Carneiro]

so it sounds like now instead of f : v(R) -> w(R) we have f : R*/ker(v) -> R*/ker(w) where R* is the free ab group

[Kevin Buzzard]

So we need the coimage because it's in the right universe.

[Kevin Buzzard]

yes that's it

[Kevin Buzzard]

We should make R* the free abelian group on R, because R' depends on v, but this is OK.

[Mario Carneiro]

and now v o f = w becomes what?

[Kevin Buzzard]

the obvious diagram commutes

[Kevin Buzzard]

wait that's true by definition

[Kevin Buzzard]

no it isn't

[Kevin Buzzard]

There's a canonical map from R* to R*/ker(v)

[Kevin Buzzard]

and one from R* to R*/ker(w)

[Kevin Buzzard]

and that's the diagram we want to commute

[Mario Carneiro]

Before, we had v : R -> G which restricts to v : R -> v(R). Now we are using the coimage, which is isomorphic, so there should be another canonical construction

[Kevin Buzzard]

we are only allowed to write down maps from R*/ker(v) to R*/ker(w) which commute with the two canonical projections

[Kevin Buzzard]

(projection the way mathematicians use the word)

[Mario Carneiro]

oh, I see, and that's all that's necessary?

[Kevin Buzzard]

I think so

[Mario Carneiro]

okay, so now initiality says that we have v1 such that for any other v there is a map R*/ker(v1) -> R*/ker(v)

[Mario Carneiro]

and that should be min_value_group

[Kevin Buzzard]

I don't think it's quite like that.

[Kevin Buzzard]

Given v, the min-value-group for v is R*/ker(v)

[Kevin Buzzard]

there's an induced valuation v_min:R->(R*/ker(v)) union 0

[Kevin Buzzard]

that's the min valuation associated to v. We love it because it lives in a sensible universe.

[Kevin Buzzard]

What I want is that if v and w are equivalent

[Kevin Buzzard]

which means that the images v(R*) and w(R*) are isomorphic in a way that makes the diagram commute

[Kevin Buzzard]

then v_min and w_min are now equal

[Kevin Buzzard]

and it was in proving this that I got my eq.rec goal

[Kevin Buzzard]

No!

[Kevin Buzzard]

I wasn't proving anything.

[Kevin Buzzard]

You are telling me that what I should be proving is that ker(v)=ker(w)

[Kevin Buzzard]

but if I follow my nose then I end up proving that the images are isomorphic

[Mario Carneiro]

So if v : R -> G and w : R -> H, we have the min-value-group R*/ker(v), and another valuation vmin : R -> R*/ker(v). Initiality is saying that if w respects v in some sense, then there is a group hom lift w : R*/ker(v) -> H

[Kevin Buzzard]

This should translate into a proof that the coimages are isomorphic

[Mario Carneiro]

I think w respects v should be something like ker(v) <= ker(w), which can be translated to something about w and v directly

[Kevin Buzzard]

yes

[Kevin Buzzard]

<= is a set-theoretic containment I assume

[Kevin Buzzard]

in this free abelian group R*

[Mario Carneiro]

in the lattice of subgroups, yes

[Kevin Buzzard]

right

[Kevin Buzzard]

So this more general notion of "respecting v" is defintely not in the repo.

[Mario Carneiro]

I don't think it needs to be given a name and everything, it's just the side condition on lift

[Kevin Buzzard]

The paper says "two valuations are equivalent if im(v) is isomorphic to im(w) in a way that makes the diagrams commute"

[Mario Carneiro]

I'm not thinking about equivalent valuations just yet here

[Kevin Buzzard]

No you're working with a general morphism

[Mario Carneiro]

once you have this lift function, it should be easy to prove the thing about equivalent valuations, just lift wmin

[Kevin Buzzard]

I read the paper and I read it as "coim(v) is isomorphic to coim(w) in a way that makes the diagrams commute" because I can rewrite canonical isomorphisms -- the mathematician's superpower.

[Kevin Buzzard]

and "isomorphic in a way that makes the diagrams commute" is the same as "equal"

[Kevin Buzzard]

It's incredible how much of a kerfuffle it is to get this into dependent type theory. I need to disassociate images and coimages in my mind. Because the coimage is a quotient you have specific tools for writing functions on it and I should use these tools.

[Kevin Buzzard]

It's like the category of open subsets of a topological space again. It's extremely similar in fact. I regard id' U and U as _equal_ but you regard them as distinct but isomorphic elements of this category.

[Kevin Buzzard]

I am not sure that making this distinction ever helps you in mathematics

[Kevin Buzzard]

but it certainly helps you in dependent type theory.

[Kevin Buzzard]

You can write down maps U -> id' U and id' U -> U and prove that they're isomorphisms and two-sided inverses of each other, whilst I watch incredulously.

[Kevin Buzzard]

Then I try to use the fact that they're _equal_ when defining a map on sheaves and get into all kinds of trouble in dependent type theory, which I do not see in mathematics.

[Kevin Buzzard]

This has been very helpful, many thanks Mario. I am back thinking seriously about the perfectoid project now and goodness knows how long I would have spent stuck on this issue had your comments not clarified how someone who knows type theory properly thinks about these questions.

[Kevin Buzzard]

@Patrick Massot I think my fears are unfounded. I just don't have enough API yet.

[Mario Carneiro]

The problem with things being equal in the material set theory sense is that it tends to make the wrong distinctions, like id' U = U but coimage(v) != image(v)

[Mario Carneiro]

If you want to be able to talk about equality when you mean isomorphism, you have to have some kind of background formalism that mimics DTT in some ways

[Mario Carneiro]

because isomorphism doesn't mean unique isomorphism, and there are plenty of examples where the collection of all isomorphisms X -> Y has interesting structure

[Kenny Lau]

oh god what hell is this discussion

[Kenny Lau]

@Kevin Buzzard If you gave me an MWE then I might be able to solve it

[Kevin Buzzard]

It's all pushed to the perfectoid project, in valuations.lean. But I know what I have to do, and it doesn't really involve solving this problem. It involves making more API and not typing induction g to get an element of G from an element of G/H.

[Patrick Massot]

Do you know that rintro is very useful when working with quotients?

[Kenny Lau]

This is a complete XY problem. You only got to eq.rec because you used induction on a quotient.

[Kevin Buzzard]

I know

[Kevin Buzzard]

but I knew that I needed some more API so I've been working on that instead.

[Kenny Lau]

great

[Kevin Buzzard]

Patrick suggested using rintro which I'm sure is better, but I could see that there was no point proceeding anyway because I couldn't prove the thing which reduced me to the eq.rec hell anyway, so I thought I'd work on that instead (Huber 1.27 or so)

[Kevin Buzzard]

Is this true? I was hoping simp would deal with it in my use case but it doesn't. I want to fill in the sorry.

import tactic
import group_theory.subgroup

example (M : Type) [add_comm_group M] (A : ℕ → add_subgroup M) (n : ℕ) (x : M)
  (hx : x ∈ A n) : true :=
begin
  have h : n = 0 + n := by simp,
  have hx' : x ∈ A (0 + n) := by { convert hx, rw ← h },
  have how_to_prove_this :
    (eq.rec (⟨x, hx⟩ : A n) h : A (0 + n)) = ⟨x, hx'⟩,
  { sorry },
  trivial,
end

The state at the sorry is

M : Type
_inst_1 : add_comm_group M
A : ℕ → add_subgroup M
n : ℕ
x : M
hx : x ∈ A n
h : n = 0 + n
hx' : x ∈ A (0 + n)
⊢ eq.rec ⟨x, hx⟩ h = ⟨x, hx'⟩

[Kevin Buzzard]

[background: all I did was make A n an A 0-module by observing that multiplication sends A 0 x A n to A (0 + n)...]

[Bhavik Mehta]

import tactic
import group_theory.subgroup

lemma subtype_heq {α : Type*} (p q : α → Prop) (h : p = q)
  (x : α) (hp : p x) (hq : q x) :
  (⟨x, hp⟩ : subtype p) == (⟨x, hq⟩ : subtype q) :=
begin
  cases h,
  apply heq_of_eq,
  simp
end

example (M : Type) [add_comm_group M] (A : ℕ → add_subgroup M) (n : ℕ) (x : M)
  (hx : x ∈ A n) : true :=
begin
  have h : n = 0 + n := by simp,
  have hx' : x ∈ A (0 + n) := by { convert hx, rw ← h },
  have how_to_prove_this :
    (eq.rec (⟨x, hx⟩ : A n) h : A (0 + n)) = ⟨x, hx'⟩,
  { apply eq_of_heq,
    apply heq.trans (eq_rec_heq _ _),
    apply subtype_heq,
    ext t,
    simp },
  trivial,
end

here's my ungolfed solution, probably can be done better

[Kevin Buzzard]

eq_rec_heq! Thanks!

[Kevin Buzzard]

Oh excellent, this also works in my use case. So the moral is to use heq when dealing with eq.rec?

[Bhavik Mehta]

In my opinion, yeah; and also that separate lemmas with the equality of types abstracted can be helpful

[Kevin Buzzard]

@Eric Wieser This innocuous-looking definition of a module hides a nasty eq.rec which is causing me trouble :-( In the internal direct sum you don't need an eq.rec because you just prove the product is in the right piece. I'm not sure there's much we can do about it though!

[Bhavik Mehta]

I'm not sure it's so innocuous looking when it's data constructed with eq.rec :-)

[Eric Wieser]

subtype_heq already exists with another name

[Eric Wieser]

Perhaps docs#subtype.heq_of_coe_eq?

[Eric Wieser]

Ah, it's #6259

[Eric Wieser]

I think the only way to eliminate that eq.rec would be to allow a second smul data field in gmonoid