Zulip Chat Archive
Stream: triage
Topic: issue !4#11187: Porting note: was `infer_instance`
Random Issue Bot (Oct 19 2025 at 14:11):
Today I chose issue #11187 for discussion!
Porting note: was infer_instance
Created by @Pietro Monticone (@pitmonticone) on 2024-03-05
Labels: porting-notes
Is this issue still relevant? Any recent updates? Anyone making progress?
Yaël Dillies (Oct 19 2025 at 14:17):
This issue appears in exactly one place now: docs#AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset. Would someone like to try squashing it?
Ruben Van de Velde (Oct 19 2025 at 15:40):
I had a look, but the proof looks nothing like the mathlib3 one
Random Issue Bot (Oct 29 2025 at 14:13):
Today I chose issue #11187 for discussion!
Porting note: was infer_instance
Created by @Pietro Monticone (@pitmonticone) on 2024-03-05
Labels: porting-notes
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2025 at 21:32 UTC