tidy issue

Stream: general

[Kevin Buzzard]

This works

import tactic

variables (X Y : Type)


example : ∀ (T : Type) (f : T → X) (g : T → Y),
∃! h : T → X × Y, prod.fst ∘ h = f ∧ prod.snd ∘ h = g :=
begin
  intros,
  use [λ t, (f t, g t)],
  tidy, -- works fine
end

but if you bump the tidy above the use the tactic reports that it's solved the goal but the kernel doesn't buy it. The error if you just prove the example by tidy is

type mismatch at application
  f a
term
  a
has type
  T_1
but is expected to have type
  T
types contain aliased name(s): T
remark: the tactic `dedup` can be used to rename aliases

Is this a known issue?

[Bhavik Mehta]

Curiously enough, the issue disappears if you use

example (T : Type) (f : T → X) (g : T → Y) :
∃! h : T → X × Y, prod.fst ∘ h = f ∧ prod.snd ∘ h = g :=
begin
  tidy,
end

[Bhavik Mehta]

Here's a more minimal example, showing that it's not an issue with tidy (but maybe an issue with dsimp?)

example : ∀ (T : Type) (f : T → X) (g : T → Y),
∃! h : T → X × Y, prod.fst ∘ h = f ∧ prod.snd ∘ h = g :=
begin
  intros,
  refine ⟨λ t, ⟨_, _⟩, _, _⟩,
  work_on_goal 2 { dsimp at *, refine ⟨rfl, rfl⟩ },
  rintros _ ⟨rfl, rfl⟩,
  dsimp at *,
  simp at *,
end

fails, but if you remove the dsimp inside the work_on_goal, it's fine

[Kevin Buzzard]

Nice! I only put the foralls in explicitly because I was imagining explaining it to a class.

[Bhavik Mehta]

This reminds me of: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20and.20dedup