eq.rec with dependent types

Stream: general

[Winston Yin]

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]

Can you give a mwe?

[Eric Wieser]

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

[Winston Yin]

Eric Wieser said:

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

Fixed. Those should be Sigmas

[Eric Wieser]

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

[Winston Yin]

That works! Could you explain the heuristic behind this?

[Eric Wieser]

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]

Also I am not familiar with dsimp or at *

[Eric Wieser]

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

[Eric Wieser]

at * does it at all the hypotheses

[Winston Yin]

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

[Winston Yin]

Thanks a lot.

[Kyle Miller]

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]

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

[Kyle Miller]

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

[Winston Yin]

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

[Reid Barton]

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