ext produces fewer goals when passed more arguments

Stream: general

[Eric Wieser]

What's going on here?

import linear_algebra.basic

variables {R : Type*} {M : Type*} {M₂ : Type*} {M₃ : Type*} {M₄ : Type*}
variables [semiring R]
variables [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M₄]
variables [semimodule R M] [semimodule R M₂] [semimodule R M₃] [semimodule R M₄]

open linear_map

@[ext] theorem prod_ext {f g : M × M₂ →ₗ[R] M₃}
  (hl : f.comp (inl _ _ _) = g.comp (inl _ _ _))
  (hr : f.comp (inr _ _ _) = g.comp (inr _ _ _)) :
  f = g :=
begin
  apply (coprod_equiv ℕ).symm.injective,
  simp only [coprod_equiv_symm_apply, hl, hr],
  apply_instance, apply_instance,
end

example {f g : M × M₂ × M₃ →ₗ[R] M₄ } : f = g :=
begin
  ext x y z, -- 2 goals
  sorry, sorry,
end

example {f g : M × M₂ × M₃ →ₗ[R] M₄ } : f = g :=
begin
  ext, -- 3 goals, with x: M, x: M₂, x: M₃
  sorry, sorry,  sorry,
end

[Eric Wieser]

Ah, the problem is that in src#tactic.interactive.ext, only the trace [] none branch calls repeat1, which is the only path that recurses into multiple goals

[Eric Wieser]

Filed #6123