obtain and red error lines

Stream: mathlib4

[Kevin Buzzard]

This code

import Mathlib.RingTheory.DedekindDomain.Ideal

variable (A : Type*) [CommRing A] (B : Type*) [CommRing B] [Algebra A B]

instance : MulAction (B ≃ₐ[A] B) (Ideal B) where
  smul σ I := Ideal.comap σ.symm I
  one_smul I := I.comap_id
  mul_smul _ _ _ := rfl

lemma DedekindDomain.exists_generator [IsDedekindDomain B] [Fintype (B ≃ₐ[A] B)]
    (Q : Ideal B) [Q.IsMaximal] (b : B) : ∃ y : B,
    y - b ∈ Q ∧ ∀ Q' : Ideal B, Q' ∈ MulAction.orbit (B ≃ₐ[A] B) Q → Q' ≠ Q → y ∈ Q' := by
  let O : Set (Ideal B) := MulAction.orbit (B ≃ₐ[A] B) Q
  have hO : O.Finite := Set.finite_range _
  have hisPrime : ∀ Q' ∈ O, Q'.IsPrime := fun Q' ⟨σ, hσ⟩ ↦ hσ ▸ (Ideal.comap_isPrime _ _)
  have hPrime : ∀ Q' ∈ hO.toFinset, Prime Q' := fun Q' hQ' ↦ Q'.prime_of_isPrime sorry sorry
  classical
  obtain ⟨y, hy⟩ := IsDedekindDomain.exists_forall_sub_mem_ideal (s := hO.toFinset) id (fun _ ↦ 1)
    hPrime (fun _ _ _ _ ↦ id) (fun Q' ↦ if Q' = Q then b else 0)
  --refine ⟨y, ?_, ?_⟩
  sorry

compiles fine. There's a sorry at the end but also two sorries in a have line in the middle. If I change the sorrys in the middle to underlines _ then I get errors which I would expect:

Screenshot-from-2024-05-27-18-12-17.png

and if I change them to ?_ then they appear as new goals. All of this I expect.

Now put the sorrys back. If I now change the have hPrime to obtain hPrime, then the code still compiles fine:

lemma DedekindDomain.exists_generator [IsDedekindDomain B] [Fintype (B ≃ₐ[A] B)]
    (Q : Ideal B) [Q.IsMaximal] (b : B) : ∃ y : B,
    y - b ∈ Q ∧ ∀ Q' : Ideal B, Q' ∈ MulAction.orbit (B ≃ₐ[A] B) Q → Q' ≠ Q → y ∈ Q' := by
  let O : Set (Ideal B) := MulAction.orbit (B ≃ₐ[A] B) Q
  have hO : O.Finite := Set.finite_range _
  have hisPrime : ∀ Q' ∈ O, Q'.IsPrime := fun Q' ⟨σ, hσ⟩ ↦ hσ ▸ (Ideal.comap_isPrime _ _)
  obtain hPrime : ∀ Q' ∈ hO.toFinset, Prime Q' := fun Q' hQ' ↦ Q'.prime_of_isPrime sorry sorry
  classical
  obtain ⟨y, hy⟩ := IsDedekindDomain.exists_forall_sub_mem_ideal (s := hO.toFinset) id (fun _ ↦ 1)
    hPrime (fun _ _ _ _ ↦ id) (fun Q' ↦ if Q' = Q then b else 0)
  --refine ⟨y, ?_, ?_⟩
  sorry

but now if I change the sorrys in the middle to _ then I get a lot of red underlines all over the argument

Screenshot-from-2024-05-27-18-16-49.png

and if I change them to ?_ then the red lines all over the argument don't go away and I don't get new goals in the local context.

Is this difference expected?

[Ruben Van de Velde]

Is this https://github.com/leanprover-community/mathlib4/issues/5732 ?

[Kevin Buzzard]

Maybe? :-) Thanks!