How does `cc` manage this goal

Stream: new members

[Patrick Stevens]

At rw eq, I have in scope eq : i a1 h1 = i a2 h2 and I need to prove j (i a1 h1) _ = j (i a2 h2) _. This is "obviously" by eq, except that "motive is not type correct". Nevertheless, cc instead of rw eq does manage to close the goal. How did it do it?

@[to_additive]
lemma prod_bij' {s : finset α} {t : finset γ} {f : α → β} {g : γ → β}
  (i : Πa∈s, γ) (hi : ∀a ha, i a ha ∈ t) (h : ∀a ha, f a = g (i a ha))
  (j : Πa∈t, α) (hj : ∀a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a)
  (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) :
  (∏ x in s, f x) = (∏ x in t, g x) :=
begin
  refine prod_bij i hi h _ _,
  {intros a1 a2 h1 h2 eq, rw [←left_inv a1 h1, ←left_inv a2 h2], rw eq,},
  {sorry}
end

[Scott Morrison]

#mwe

[Scott Morrison]

(Without trying cc myself here, I'm not sure. Have you tried #print prod_bij', or replacing cc with show_term { cc }?)

[Patrick Stevens]

Oh, show_term is a thing - thanks. The output is utterly impenetrable, but I should probably expect that of any tactic

[Patrick Stevens]

Were you objecting to the "working" or the "minimal" axes?

[Alex J. Best]

Both! Working as in define what alpha beta gamma are, and minimal so its easier to read.

[Bryan Gin-ge Chen]

In particular, from the #mwe link:

Please make sure that your code snippet has:
- correct imports; and
- all the relevant definitions / theorems.

[Patrick Stevens]

Oh, I am still not used to the fact that mathlib has lots of ambient variables floating around - it hadn't even occurred to me that this might not build, it's lifted verbatim out of a PR to algebra/big_operators.lean, sorry

[Patrick Stevens]

And I made the terrible mistake of editing a file in mathlib and now the entire world is building again :(

[Yury G. Kudryashov]

The problem is that the type of _ depends on the argument.

[Yury G. Kudryashov]

And you're trying to rewrite this argument.

[Yury G. Kudryashov]

Try congr.

[Alex J. Best]

simp only [eq] works also.

[Patrick Stevens]

Indeed I am, I was hoping the types would also be rewritten - but of course now you mention it, it'll only rewrite the goal, not the assumptions

[Patrick Stevens]

memo to self: Agda's rewrite is nothing like rw

[Yury G. Kudryashov]

Yes, if simp or rw fails, try the other one.

[Patrick Stevens]

Thanks!