help fixing a proof in Mathlib.GroupTheory.CoprodI?

Stream: mathlib4

[Kim Morrison]

The proof

theorem induction_on {C : CoprodI M → Prop} (m : CoprodI M) (h_one : C 1)
    (h_of : ∀ (i) (m : M i), C (of m)) (h_mul : ∀ x y, C x → C y → C (x * y)) : C m := by
  let S : Submonoid (CoprodI M) :=
    { carrier := setOf C
      mul_mem' := h_mul _ _
      one_mem' := h_one }
  have : C _ := Subtype.prop (lift (fun i => of.codRestrict S (h_of i)) m)
  convert this
  change MonoidHom.id _ m = S.subtype.comp _ m
  congr
  ext i
  rfl

in Mathlib.GroupTheory.CoprodI is currently breaking on nightly-testing, but I'm a bit hesitant to put effort into tracking down the cause for the change, because the proof looks sort of icky to begin with! (In particular, the convert / change / congr steps.)

Would anyone be interested in writing a new proof here? Either just coming up with something cleaner on master, or working on nightly-testing so you can be sure you're dealing with the error there (on change) would be great.

[Yury G. Kudryashov]

I'm on it

[Yury G. Kudryashov]

I'm bad at fixing a proof without touching theorems around it: #12391

[Johan Commelin]

LGTM! :peace_sign: