sorry tactic fails?

Stream: general

[Saif Ghobash]

I get this error message when attempting to use sorry,

import group_theory.free_product
import group_theory.index
universes u
variables {ι : Type u} {G : ι → Type*} [Π (i : ι), group (G i)]

def residually_finite (G : Type u) [group G] : Prop :=
∀ (g : G), g ≠ 1 → ∃ (H : subgroup G), H.index ≠ 0 ∧ g ∉ H

noncomputable example (h : ∀ i, residually_finite (G i)) : residually_finite (free_product G) :=
begin
  classical,
  rw residually_finite,
  rw free_product.word.equiv.forall_congr_left',
  intros w hw,
  rw free_product.word.equiv at hw,
  simp at hw,
  by_cases h' : (w = free_product.word.empty),
  { subst_vars,
    simp at hw,
    contradiction },
  {
    obtain ⟨i, j, w', hw'⟩ := free_product.neword.of_word w h',
    subst_vars,
    clear h',
    induction w',
    specialize h w'_i w'_x w'_hne1,
    rcases h with ⟨H, hH₁, hH₂⟩,
    dsimp at *,
    norm_cast at *,
    sorry
    -- exact tactic failed, failed to assign sorry to metavariable ?m_3 (possible cause: occurs check failed)
  }
end

[Yaël Dillies]

The system won't forgive you

[Eric Rodriguez]

@Bhavik Mehta recently ran into something like this, I think - how was it fixed?

[Kevin Buzzard]

exact sorry gives "Don't know how to synthesize placeholder Π (i : ι), decidable_eq (G i)" but even adding that to the context doesn't fix it.

[Kevin Buzzard]

...
      norm_cast at *,
      recover, -- now 4 goals,
      repeat { sorry },
      sorry,

works.

[Kevin Buzzard]

There should be { } after the induction step, you shouldn't be writing code when there are two goals. This seems unrelated to the problem, but my fix will affect your second goal.

[Ruben Van de Velde]

This also works:

noncomputable example (h : ∀ i, residually_finite (G i)) : residually_finite (free_product G) :=
begin
  classical,
  rw residually_finite,
  rw free_product.word.equiv.forall_congr_left',
  rotate, apply_instance, apply_instance,
  intros w hw,
  rw free_product.word.equiv at hw,
  simp at hw,
  by_cases h' : (w = free_product.word.empty),
  { subst_vars,
    simp at hw,
    contradiction },
  {
    obtain ⟨i, j, w', hw'⟩ := free_product.neword.of_word w h',
    subst_vars,
    clear h',
    induction w',
    { specialize h w'_i w'_x w'_hne1,
      rcases h with ⟨H, hH₁, hH₂⟩,
      dsimp at *,
      norm_cast at *,
      sorry },
    { sorry } }
end

[Bhavik Mehta]

Eric Rodriguez said:

Bhavik Mehta recently ran into something like this, I think - how was it fixed?

I had the same error, but it was from a failing rw. I got around it because the rewrite was in the and of two props and I only needed to rewrite in one, so splitting and doing the focused rewrite worked instead, not really a fix