apply_instance and reducibility flag

apply_instance fails to find an instance, although it finds one for another problem which is defeq to the first one, even with the flag tactic.transparency.instances. MWE, based on mathlib:

import analysis.normed_space.basic

section normed_module
set_option default_priority 100 -- see Note [default priority]
class normed_module (α : Type*) (β : Type*) [normed_ring α] [normed_group β]
  extends semimodule α β :=
(norm_smul_le : ∀ (a:α) (b:β), ∥a • b∥ ≤ ∥a∥ * ∥b∥)
end normed_module

variables {𝕜 : Type}  {n : ℕ} {E : fin n → Type}
[A : normed_field 𝕜] [N : ∀i, normed_group (E i)] [∀i, normed_module 𝕜 (E i)]

-- Two different ways to say: Π (i : fin n), module 𝕜 (E i)

set_option trace.class_instances true

lemma all_right :
Π (i : fin n),
    @module.{0} 𝕜 (E i)
      (@normed_ring.to_ring.{0} 𝕜
         (@normed_field.to_normed_ring.{0} 𝕜 A))
      (@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by apply_instance

lemma fails :
Π (i : fin n),
    @module.{0} 𝕜 (E i)
      (@comm_ring.to_ring.{0} 𝕜
          (@field.to_comm_ring.{0} 𝕜
              (@normed_field.to_field.{0} 𝕜 A)))
      (@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by apply_instance -- fails
-- all_right  -- works

The two terms in the two lemmas are defeq with tactic.transparency.instances, and the subterms are also defeq with tactic.transparency.instances, but they are not defeq with tactic.transparency.reducible, as shown by the following:

lemma outer_works_with_transparency.instances :
  (Π (i : fin n),
    @module.{0} 𝕜 (E i)
      (@normed_ring.to_ring.{0} 𝕜
         (@normed_field.to_normed_ring.{0} 𝕜 A))
      (@normed_group.to_add_comm_group.{0} (E i) (N i)))
   =
  Π (i : fin n),
    @module.{0} 𝕜 (E i)
      (@comm_ring.to_ring.{0} 𝕜
          (@field.to_comm_ring.{0} 𝕜
              (@normed_field.to_field.{0} 𝕜 A)))
      (@normed_group.to_add_comm_group.{0} (E i) (N i)) :=
by tactic.reflexivity tactic.transparency.instances -- works

lemma inner_works_with_transparency.instances :
  (@normed_ring.to_ring.{0} 𝕜
         (@normed_field.to_normed_ring.{0} 𝕜 A))
  =
  (@comm_ring.to_ring.{0} 𝕜
          (@field.to_comm_ring.{0} 𝕜
              (@normed_field.to_field.{0} 𝕜 A))) :=
by tactic.reflexivity tactic.transparency.instances --works

lemma inner_fails_with_transparency.reducible :
  (@normed_ring.to_ring.{0} 𝕜
         (@normed_field.to_normed_ring.{0} 𝕜 A))
  =
  (@comm_ring.to_ring.{0} 𝕜
          (@field.to_comm_ring.{0} 𝕜
              (@normed_field.to_field.{0} 𝕜 A))) :=
by tactic.reflexivity tactic.transparency.reducible -- fails

Mario's guess on Zulip is that apply_instance probably passes the wrong flag to subproblems (see discussion at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Normed.20spaces/near/197786186)

Tested on Lean 3.11 and 3.13.1

(Example edited for 3.16.0)

Start with the supplied minimal working example and compare apply_instance's handling of the all_right and fails goals under tactic.transparency.instances. Trace the transparency flag passed to subproblems, using the included reflexivity examples as checks; done means the failing apply_instance succeeds without changing the example's intended declarations.