# Zulip Chat Archive

## Stream: general

### Topic: result contains metavariables

#### Kevin Buzzard (Mar 18 2020 at 20:46):

I've been around for long enough to have seen the situation where you have no goals but `end`

doesn't work because

tactic failed, result contains meta-variables state: no goals

You can try and get out of this hole with the `recover`

tactic.

I've been playing with the category theory library this evening, and something pretty cool happened, and I have no idea why. We're in one of these situations where the goal should be relatively straightforward when you work out what it says. My strategy in such situations is to do a mass of unfolding, and when `dsimp`

suddenly tidies a bunch of stuff up, save my position with `show [blah]`

and then press on. So I managed to fill in a sorry this evening, and my first complete proof looked like this:

@[simp] lemma right_unitor_hom {M : Module R} (r : R) (m : M) : ((ρ_ M).hom : M ⊗ 𝟙_ (Module R) ⟶ M) (m ⊗ₜ r) = r • m := begin show (linear_equiv.to_linear_map (tensor_product.rid R ↥M)) (m ⊗ₜ[R] r) = r • m, dunfold tensor_product.rid, dunfold tensor_product.comm, unfold_coes, unfold linear_map.flip, unfold_coes, unfold linear_map.mk₂, unfold tensor_product.mk, dsimp, unfold_coes, -- unfold tensor_product.lift, unfold linear_equiv.of_linear, unfold linear_equiv.trans, dunfold linear_equiv.to_linear_map, dsimp, unfold tensor_product.lid, unfold linear_equiv.of_linear, dsimp, unfold_coes, unfold linear_map.lsmul, unfold linear_map.mk₂, dsimp, squeeze_simp, -- tensor_product.lift.tmul used here show (tensor_product.lift {to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun (r ⊗ₜ[R] m) = r • m, squeeze_simp, -- tensor_product.lift.tmul' refl, end

This proof is actually just two lines long -- each `squeeze_simp`

just does one rewrite (`tmul`

and `tmul'`

are definitionally equal, one has `to_fun`

in and the other has a coercion), and all the definitional unfolding is just to get things into a shape where the rewrite can happen. This proof compiles no problem. So then I refactored the proof so it was just `show X, rw tensor_product.lift.tmul', show Y, rw tensor_product.lift.tmul'`

:

lemma right_unitor_hom {M : Module R} (r : R) (m : M) : ((ρ_ M).hom : M ⊗ 𝟙_ (Module R) ⟶ M) (m ⊗ₜ r) = r • m := begin show (tensor_product.lift {to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun ((tensor_product.lift {to_fun := λ (m : ↥M), {to_fun := λ (m_1 : R), m_1 ⊗ₜ[R] m, add := _, smul := _}, add := _, smul := _}).to_fun (m ⊗ₜ[R] r)) = r • m, rw tensor_product.lift.tmul', show (tensor_product.lift {to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun (r ⊗ₜ[R] m) = r • m, rw tensor_product.lift.tmul', refl, -- no goals! end

and I got the `result contains metavariables`

error. I was really surprised when I tried `recover`

though -- four goals, some of which weren't definitional. I killed them all and *still* I got the error! A second `recover`

and they were finally gone. My proof ended up looking like this:

lemma right_unitor_hom {M : Module R} (r : R) (m : M) : ((ρ_ M).hom : M ⊗ 𝟙_ (Module R) ⟶ M) (m ⊗ₜ r) = r • m := begin show (tensor_product.lift {to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun ((tensor_product.lift {to_fun := λ (m : ↥M), {to_fun := λ (m_1 : R), m_1 ⊗ₜ[R] m, add := _, smul := _}, add := _, smul := _}).to_fun (m ⊗ₜ[R] r)) = r • m, rw tensor_product.lift.tmul', show (tensor_product.lift {to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun (r ⊗ₜ[R] m) = r • m, rw tensor_product.lift.tmul', refl, -- no goals! recover, -- four goals! simp, intros, congr', intros, ext, simp, apply tensor_product.tmul_add, -- no goals! recover, -- two goals! intros, rw tensor_product.smul_tmul c x m_1, simp, intros, apply tensor_product.add_tmul, end

My question: How come I managed to avoid these six secret metavariables in my first proof? Where did they come from?

One cannot immediately reproduce this at home, but because of the new tooling it is *much* easier than before. The following commands (run in a directory where there's not a subdirectory called `mathlib`

):

leanproject get mathlib cd mathlib/ git checkout enriched leanproject get-cache

will give you Scott's branch, fully compiled. The `right_unitor_hom`

lemma is on line 149 of `src/algebra/category/Module/monoidal.lean`

#### Kevin Buzzard (Mar 18 2020 at 21:17):

Some of the random goals are I think the `add := _`

and `smul := _`

. I tried replacing the first `show`

with

show (tensor_product.lift {to_fun := λ (a : R), {to_fun := λ (m : ↥M), a • m, add := _, smul := _}, add := _, smul := _}).to_fun ((tensor_product.lift {to_fun := _, add := _, smul := _}).to_fun (m ⊗ₜ[R] r)) = r • m,

and I get

LEAN ASSERTION VIOLATION File: /home/travis/build/leanprover-community/lean/src/frontends/lean/elaborator.cpp Line: 3174 Task: /home/buzzard/Encfs/Computer_languages/Lean/lean-projects/mathlib/src/algebra/category/Module/monoidal.lean: Module.monoidal_category.right_unitor_hom m_ctx.match(e, *val2)

Something is a bit weird here.

#### Bryan Gin-ge Chen (Mar 18 2020 at 21:18):

Looks like https://github.com/leanprover-community/lean/issues/123 again.

#### Kevin Buzzard (Mar 18 2020 at 21:22):

no, you can do set-theoretic trickery. Wait, we're on the wrong thread.

Last updated: May 16 2021 at 21:11 UTC