feat: @[instance_reducible]

[leodemoura]

This PR adds the new transparency setting @[instance_reducible]. We used to check whether a declaration had instance reducibility by using the isInstance predicate. However, this was not a robust solution because:

• We have scoped instances, and isInstance returns true only if the scope is active.

• We have auxiliary declarations used to construct instances manually, such as:

    def lt_wfRel : WellFoundedRelation Nat

isInstance also returns false for this kind of declaration.

In both cases, the declaration may be (or may have been) used to construct an instance, but isInstance
returns false. Thus, we claim it is a mistake to check the reducibility status using isInstance.
isInstance indicates whether a declaration is available for the type class resolution mechanism,
not its transparency status.

We are decoupling whether a declaration is available for type class resolution from its transparency status.

Remak: We need a update stage0 to complete this feature.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-01-30 05:29:19)

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-12247 build failed against this PR. (2026-01-30 05:33:46) View Log

[kim-em]

This panics all through Mathlib, here's an example:

section Mathlib.Logic.Basic

variable {a b : Prop}

theorem not_imp_not : ¬a → ¬b ↔ b → a := sorry

end Mathlib.Logic.Basic

section Mathlib.Logic.Nontrivial.Defs

class Nontrivial (α : Type) : Prop where
  exists_pair_ne : ∃ x y : α, x ≠ y

theorem not_subsingleton (α) [Nontrivial α] : ¬Subsingleton α := sorry

end Mathlib.Logic.Nontrivial.Defs

open Function

variable {α β : Sort} {f : α → β}

/-- PANIC -/
#guard_msgs (substring := true) in
theorem injective_comp_right_iff_surjective {γ : Type} [Nontrivial γ] :
    Injective (fun g : β → γ ↦ g ∘ f) ↔ Surjective f := by
  refine ⟨not_imp_not.mp fun not_surj inj ↦ not_subsingleton γ ⟨fun c c' ↦ ?_⟩,
    (·.injective_comp_right)⟩
  have ⟨b₀, hb⟩ := not_forall.mp not_surj
  classical have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_
  sorry

[leodemoura]

This panics all through Mathlib, here's an example:

@kim-em It is the same panic that was affecting our stage2. It has been fixed.