`ext` recurses into subgoals, `ext x y z` and `ext : n` do not

[eric-wieser]

Reproduction (on mathlib 8fd86366a4472716b25100e831a2ba0f266b28b8)

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 : 1000, -- 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

The cause is these lines:

https://github.com/leanprover-community/mathlib/blob/8fd86366a4472716b25100e831a2ba0f266b28b8/src/tactic/ext.lean#L533-L537

Only the repeat1 branch goes on to call ext on all subgoals.

[eric-wieser]

Zulip

[gebner]

I don't think that's so much a bug report as a UI question.

The way I understand it, the idea is that ext by itself does something useful, and if you want to customize it, then you can add additional arguments. I think there's a reasonable case to be made for changing the UI, but maybe we should wait until Lean 4.