## Stream: new members

### Topic: substitution within a lambda

#### Winston Yin (Jun 22 2021 at 14:57):

I have a hypothesis h : ∀ x : A, f x = c, where c doesn't depend on x, and I have a goal some_prop (λ x : A, g (f x)). How can I rewrite the goal to some_prop (λ x : A, g c)? Just writing rw h doesn't seem to work

#### Anne Baanen (Jun 22 2021 at 14:58):

You can try simp_rw h

#### Anne Baanen (Jun 22 2021 at 14:59):

tactic#simp_rw uses the simplifier to do rewrites, so it works better under binders like λ or ∀

#### Winston Yin (Jun 22 2021 at 14:59):

Hmm that didn't seem to do anything

#### Anne Baanen (Jun 22 2021 at 15:00):

Maybe g is a dependent function? That's usually a problem for simp

#### Anne Baanen (Jun 22 2021 at 15:01):

Alternatively, try something like suffices : some_prop (λ x, g c), { convert this, ext, rw h },

#### Winston Yin (Jun 22 2021 at 15:01):

You mean a type-dependent function? Yep

#### Winston Yin (Jun 22 2021 at 15:04):

I also have the problem that the types of f x and c are equal only because of h. I think it has something to do with subtypes

#### Eric Rodriguez (Jun 22 2021 at 15:05):

heq time ? :shock: can you post a #mwe?

#### Winston Yin (Jun 22 2021 at 15:06):

Let me see if I can even write a mwe, as I'm on line 50 of this (probably unnecessarily long) proof

#### Anne Baanen (Jun 22 2021 at 15:07):

There is tactic#extract_goal for turning the current goal into a separate example, and the #where for the list of imports and variables etc.

#### Winston Yin (Jun 22 2021 at 15:11):

Here's a mwe:

variables
{ι : Type*} [decidable_eq ι]
{G : Type*} [monoid G]
{k : Type*} {M : Type*}
[semiring k] [add_comm_monoid M] [module k M] [repre k G M]
{p : ι → submodule k M} (h : ∀ i : ι, p i = (⊤ : submodule k M))
#check direct_sum.to_module k ι M (λ (i : ι), (p i).subtype) = direct_sum.to_module k ι M (λ (i : ι), (⊤ : submodule k M).subtype)


#### Winston Yin (Jun 22 2021 at 15:12):

The equality in #check fails because of type mismatch

#### Winston Yin (Jun 22 2021 at 15:14):

Very useful tool, Anne! To be more precise, I actually have another hypothesis h2 that I'm trying to rw h at h2, but the thing I'm trying to rewrite hides behind a lambda _and_ has a dependent type

#### Anne Baanen (Jun 22 2021 at 15:41):

Hmm, I suspect that you're trying to do "the wrong thing": if you get a goal to prove two module structures are equal, you probably want to define a linear_equiv between the two modules instead, and prove that property is preserved by an equiv (or a surjective linear map, etc)

#### Winston Yin (Jun 22 2021 at 15:52):

I have a hypothesis function.injective (direct_sum.to_module k ι M (λ (i : ι), (p i).subtype)) obtained from submodule_is_internal. All I want to do is to turn it into a hypothesis function.injective (direct_sum.to_module k ι M (λ (i : ι), (⊤ : submodule k M).subtype)), so I can apply it to x y : ⊤, which I have constructed earlier...

#### Winston Yin (Jun 22 2021 at 15:54):

This is the last step of a long proof :cry:

#### Kevin Buzzard (Jun 22 2021 at 16:16):

I don't think you can use equality for this. You need to write down the isomorphism of modules and show that the diagram commutes.

#### Eric Wieser (Jun 22 2021 at 21:27):

The approach here should probably be to show that the function you're showing the injectivity of is just the other function composed with an equiv

#### Eric Wieser (Jun 22 2021 at 21:28):

Since an injective function composed with an equiv is injective

#### Eric Wieser (Jun 22 2021 at 21:29):

I'm curious what the high level statement you're working on is - it looks like it might be very similar to some of the things Kevin and I were looking at a month or so ago

#### Winston Yin (Jun 23 2021 at 02:11):

I managed to show it in an ugly way using a convert, which produced 29 goals, which were easily solved in two any_goals. I'm sure this could be done in a much better way

#### Winston Yin (Jun 23 2021 at 02:46):

I posted about this before as well, in my previous attempt to implement the basics of representation. I defined the direct sum of a collection of representations (I found dfinsupp pretty hard to deal with). The statement I'm trying to prove is that the existence of a nontrivial decomposition of a representation in terms of its subrepresentations (via something like submodule_is_internal) implies not irreducible

#### Winston Yin (Jun 23 2021 at 02:47):

A cursory note that turns out to be really tricky to prove in Lean

#### Alex Zhang (Jun 23 2021 at 02:54):

Is simp_rw more powerful than simp?

#### Winston Yin (Jun 23 2021 at 02:54):

Eric Wieser said:

Since an injective function composed with an equiv is injective

I could try this approach next time. It was just slightly frustrating that I couldn't just make the substitution even when the two types are literally equal according to a hypothesis.

#### Winston Yin (Jun 23 2021 at 02:55):

simp_rw didn't manage to work in this case

#### Winston Yin (Jun 23 2021 at 02:57):

Hypotheses:

h_eq : ∀ (i : ι), p i = ⊤
hinj : function.injective (direct_sum.to_module k ι M (λ (i : ι), (p i).subtype))


Goal:

function.injective (direct_sum.to_module k ι M (λ (i : ι), (⊤ : submodule k M).subtype))


#### Eric Wieser (Jun 23 2021 at 07:22):

Can you make that a #mwe, perhaps with extract_goal?

#### Anne Baanen (Jun 23 2021 at 10:11):

Alex Zhang said:

Is simp_rw more powerful than simp?

Not really: simp_rw [a, b, c] should do exactly the same as simp only [a], simp only [b], simp only [c]. (This is not the same as simp only [a, b, c]!)

Last updated: Dec 20 2023 at 11:08 UTC