Weirdness in product of groupoids attempt

Stream: general

[Praneeth Kolichala]

I'm trying to show that the product of groupoids is a groupoid. In words, this is because for groupoids $X$ and $Y$, if $x,y \in X\times Y$ are objects and $(f, g)$ a morphism between them, then $(f, g)$ has an inverse, namely $(f^{-1}, g^{-1})$.

This is a very simple fact, and it might already be in mathlib. In any case, I'm (re)proving it, and I have this so far (which works correctly):

universe u

abbreviation inv := @category_theory.groupoid.inv

instance groupoid_prod {X : Type u} [category_theory.groupoid.{u} X]
                    {Y : Type u} [category_theory.groupoid.{u} Y]
                  : category_theory.groupoid.{u} (X × Y) :=
{
  inv := λ (x y : X × Y) (f : (x.1 ⟶ y.1) × (x.2 ⟶ y.2)),
            (inv f.1, inv f.2),
  inv_comp' :=
  begin
    intros x y f,
    -- change ((inv f.1, inv f.2) : y ⟶ x) ≫ ((f.1, f.2) : x ⟶ y) = 𝟙 y,
    let inv_f : y ⟶ x := (inv f.1, inv f.2),
    let f_hom : x ⟶ y := (f.1, f.2),
    change inv_f ≫ f_hom = 𝟙 y,
    have prodcomp : (inv_f ≫ f_hom = _)
    := @category_theory.prod_comp _ _ _ _
      _ _ _ _ _ _ inv_f f_hom,
    rw prodcomp,
    simpa,
  end,

  comp_inv' :=
  begin
    -- Removed for clarity, essentially the same as inv_comp'
  end,
}

This works, but it feels very clunky. For example, I wanted to use the line change ((inv f.1, inv f.2) : y ⟶ x) ≫ ((f.1, f.2) : x ⟶ y) = 𝟙 y,
but for some reason Lean gives a type error. My workaround (after lots of tinkering) was to use two let statements with explicit types. I don't understand why this works but the other way doesn't.

Next, something even more mysterious (to me). I wanted to use something like:
rw category_theory.prod_comp inv_f f_hom

Unfortunately, the only way I could make it work was as shown in the original code. Specifically, I had to move it to a variable prodcomp, which also has to have an explicit type, and use @ even though all the parameters are underscores. If I don't give it an explicit type, Lean infers the correct type (in fact, the type doesn't change at all!), but the rewrite fails for some reason.

Can anyone explain what's going on?

Also, I noticed that if I put enough blank lines after the begin statement, the goal randomly changes according to VS Code (to ∀ {X_1 Y_1 : X × Y} (f : X_1 ⟶ Y_1), 𝟙 X_1 ≫ f = f, which I guess is easier to prove). This doesn't help in proving the theorem, because as soon as you do a tactic like intro, it changes back to what it was supposed to be, so this is probably a small bug in Lean/VS Code. Still, it's not helping my suspicion that my version of Lean is haunted.

[Praneeth Kolichala]

I'm able to reproduce the blank lines bug in the online WebAssembly version of Lean here.

You have to use the exact number of blank lines; no more, no less. The skip is not necessary, it just illustrates the goal change. Any tactic which creates a new node in the syntax tree will do I think.