test: add regression test for structure-extends-class congr (#12187)

This PR adds regression tests that catch issues where structures/classes
with class-typed fields produce HEq goals in `congr` instead of handling
Prop fields automatically.

Both tests pass on v4.28.0-rc1 (before isInstance detection changes).

## Test 1: Structure extending classes (mirrors Mathlib's GroupTopology)

```lean
structure MyGroupTopology (α : Type) extends MyTopology α, IsContinuousMul α

theorem MyGroupTopology.toMyTopology_injective {α : Type} :
    Function.Injective (MyGroupTopology.toMyTopology : MyGroupTopology α → MyTopology α) := by
  intro f g h
  cases f
  cases g
  congr
```

**Failure mode:** `⊢ toIsContinuousMul✝¹ ≍ toIsContinuousMul✝`

## Test 2: Class with explicit class-typed field (mirrors Mathlib's
PseudoEMetricSpace)

```lean
class MyMetricSpace (α : Type) extends MyDist α where
  dist_self : ∀ x : α, dist x x = 0
  toMyUniformity : MyUniformity α  -- explicit class-typed field (NOT from extends)
  uniformity_dist : toMyUniformity.uniformity (fun x y => dist x y = 0)

protected theorem MyMetricSpace.ext {α : Type} {m m' : MyMetricSpace α}
    (h : m.toMyDist = m'.toMyDist) (hU : m.toMyUniformity = m'.toMyUniformity) : m = m' := by
  cases m
  cases m'
  congr 1 <;> assumption
```

**Failure mode:** `⊢ dist_self✝¹ ≍ dist_self✝` and `⊢ uniformity_dist✝¹
≍ uniformity_dist✝`

## Context

These tests are related to #12172, which changes instance parameter
detection from binder-based to `isClass?`-based. That change can affect
how structure fields are classified in congruence lemma generation.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>

tests/lean/run/isInstanceCongrRegression.lean

@@ -0,0 +1,82 @@
+/-!
+# Regression tests for isInstance changes in congruence lemma generation
+
+These tests verify that `congr` works correctly for structures and classes
+with class-typed fields. They catch regressions from changes to how instance
+parameters are detected (e.g., using `isClass?` instead of binder info).
+
+Both tests pass on v4.28.0-rc1 (before the isInstance changes).
+
+## Test 1: Structure extending classes (mirrors Mathlib's GroupTopology)
+
+When a structure extends both a data class and a Prop class, the parent class
+field may be marked as `isInstance = true`. If this causes `.fixed` treatment
+in congruence lemma generation, dependent Prop fields will require HEq.
+
+**Failure mode:** `⊢ toIsContinuousMul✝¹ ≍ toIsContinuousMul✝`
+
+## Test 2: Class with explicit class-typed field (mirrors Mathlib's PseudoEMetricSpace)
+
+When a class has an explicit class-typed field (not from `extends`), that field
+may be marked as `isInstance = true`. If this causes `.fixed` treatment, then
+dependent Prop fields whose types mention that field will require HEq.
+
+**Failure mode:** `⊢ dist_self✝¹ ≍ dist_self✝` and `⊢ uniformity_dist✝¹ ≍ uniformity_dist✝`
+-/
+
+/-! ### Test 1: Structure extending classes -/
+
+-- Setup: mimic Mathlib's GroupTopology structure
+class MyTopology (α : Type) where
+  isOpen : (α → Prop) → Prop
+
+-- A Prop-valued class that depends on MyTopology
+class IsContinuousMul (α : Type) [MyTopology α] : Prop where
+  continuous_mul : True  -- simplified
+
+-- Structure extending both a data class and a Prop class
+structure MyGroupTopology (α : Type) extends MyTopology α, IsContinuousMul α
+
+-- Key test: proving injectivity of the parent projection using `congr`
+-- If the toMyTopology field gets `.fixed` treatment, the Prop-valued
+-- toIsContinuousMul field will require HEq: `⊢ toIsContinuousMul✝¹ ≍ toIsContinuousMul✝`
+theorem MyGroupTopology.toMyTopology_injective {α : Type} :
+    Function.Injective (MyGroupTopology.toMyTopology : MyGroupTopology α → MyTopology α) := by
+  intro f g h
+  cases f
+  cases g
+  congr
+
+/-! ### Test 2: Class with explicit class-typed field -/
+
+-- Setup: mimic Mathlib's PseudoEMetricSpace pattern
+-- A class that extends one class but has another class-typed field explicitly
+
+class MyDist (α : Type) where
+  dist : α → α → Nat
+
+class MyUniformity (α : Type) where
+  uniformity : (α → α → Prop) → Prop
+
+-- Class that extends MyDist but has an explicit MyUniformity field
+-- This mirrors PseudoEMetricSpace which extends EDist but has explicit toUniformSpace
+class MyMetricSpace (α : Type) extends MyDist α where
+  dist_self : ∀ x : α, dist x x = 0
+  -- Explicit class-typed field (NOT from extends)
+  toMyUniformity : MyUniformity α
+  -- Prop field whose type depends on toMyUniformity
+  uniformity_dist : toMyUniformity.uniformity (fun x y => dist x y = 0)
+
+-- Key test: extensionality theorem using `congr`
+-- If toMyUniformity gets `.fixed` treatment (because it's class-typed but not
+-- a subobject field), then `congr` will produce HEq goals for dependent fields
+protected theorem MyMetricSpace.ext {α : Type} {m m' : MyMetricSpace α}
+    (h : m.toMyDist = m'.toMyDist) (hU : m.toMyUniformity = m'.toMyUniformity) : m = m' := by
+  cases m
+  cases m'
+  -- After cases, we need to prove the constructors are equal
+  -- `congr` should produce goals for data fields (dist, toMyUniformity)
+  -- and automatically handle Prop fields (dist_self, uniformity_dist) via casting
+  -- If toMyUniformity gets `.fixed` treatment, we'd see HEq goals like:
+  --   `⊢ dist_self✝¹ ≍ dist_self✝` or `⊢ uniformity_dist✝¹ ≍ uniformity_dist✝`
+  congr 1 <;> assumption