Analytic structure groupoid

Stream: maths

[Michael Lee]

What's the right definition for the pregroupoid that defines the analytic StructureGroupoid on a ModelWithCorners I (leaving aside questions of real vs. complex analyticity)? The requirements are quite a bit stricter than for smoothness, and I would think some problems could potentially arise on the boundary of range I (e.g. that I ∘ I.symm might not be analytic there).

[Michael Lee]

I think I've figured this out: https://github.com/leanprover-community/mathlib4/pull/6386