## Stream: general

### Topic: eq.rec with dependent types

#### Winston Yin (Jun 20 2022 at 22:11):

I'm having some trouble using rw on goals that involve many dependent types. I have (omitting some for clarity):

ι : Type*
V : ι → Type*
f : Π i : ι, V i →ₗ[k] V i
n : ι → Type*
b : Π i : ι, basis (n i) k (V i)
x y : n
h : x.1 = y.1


I've gotten to a point where the goal is:

eq.rec (⇑((b y.1).repr) (⇑(f y.1) (⇑(b y.1) y.2))) _ = ⇑((b x.1).repr) (⇑(f x.1) (⇑(b x.1) (cast _ y.2)))


The underscore on the LHS is a proof of y.1 = x.1. How can I finish such a goal?

rw h throws motive is not type correct. After I add a further hypothesis hn : n x.1 = n y.1 and use simp_rw h, it is still unable to simplify the expression further.

#### Eric Wieser (Jun 20 2022 at 22:17):

Can you give a mwe?

#### Eric Wieser (Jun 20 2022 at 22:17):

x y : n feels like nonsense there given n : ι → Type*

#### Winston Yin (Jun 20 2022 at 22:18):

Eric Wieser said:

x y : n feels like nonsense there given n : ι → Type*

Fixed. Those should be Sigmas

#### Eric Wieser (Jun 20 2022 at 22:18):

cases x, cases y, dsimp only at *, subst h might help

#### Winston Yin (Jun 20 2022 at 22:21):

That works! Could you explain the heuristic behind this?

#### Eric Wieser (Jun 20 2022 at 22:21):

You want to get your equalities to have a single variable on one side, so that you can use subst (aka cases h)

#### Winston Yin (Jun 20 2022 at 22:22):

Also I am not familiar with dsimp or at *

#### Eric Wieser (Jun 20 2022 at 22:22):

dsimp only at * turns annoying (sigma.mk x y).fst goals into x

#### Eric Wieser (Jun 20 2022 at 22:23):

at * does it at all the hypotheses

#### Winston Yin (Jun 20 2022 at 22:25):

I see. Basically Lean can't substitute x.1 = y.1 but can substitute x_fst = y_fst once I've cases-ed on x, y

Thanks a lot.

#### Kyle Miller (Jun 20 2022 at 22:27):

tactic#dsimp is a like tactic#simp but only uses simp lemmas that are definitionally true (so it's as if you did a sequence of change tactics). https://leanprover-community.github.io/extras/simp.html mentions dsimp

#### Kyle Miller (Jun 20 2022 at 22:27):

Something else that can be helpful is using tactic#generalize to turn certain expressions into variables so you can subst them

#### Kyle Miller (Jun 20 2022 at 22:28):

Yet another thing that can be helpful is stepping back and wondering how you got into this eq.rec business anyway :wink:

#### Winston Yin (Jun 20 2022 at 22:29):

I'm doing my best to avoid proving things about dfinsupp because scary things happen when I try.

#### Reid Barton (Jun 20 2022 at 22:47):

Kyle Miller said:

Yet another thing that can be helpful is stepping back and wondering how you got into this eq.rec business anyway :wink:

For example, it might have been better to do this cases x, cases y, subst h business before eq.rec appeared

Last updated: Aug 03 2023 at 10:10 UTC