Request for help making proof more robust

Stream: lean4

[Artie Khovanov]

Here is a MWE of me proving a particular (auto-generated!) goal:

import Mathlib

class RingPreorderingClass (S R : Type*) [CommRing R] [SetLike S R]
    extends SubsemiringClass S R : Prop

variable {S F : Type*} [Field F] [SetLike S F] [RingPreorderingClass S F] (P : S) (a : F)

theorem Subsemiring.closure_insert_ringPreordering :
    Subsemiring.closure (insert a P) = {z : F | ∃ x ∈ P, ∃ y ∈ P, z = x + a * y} := sorry

theorem RingPreordering.minus_one_not_mem_adjoin_linear
    (ha : -a ∉ P) (x y : F) (hx : x ∈ P) (hy : y ∈ P) : -1 ≠ x + a * y := sorry

theorem RingPreordering.extracted_goal (a : F) (ha : -a ∉ P) :
    -1 ∉ (Subsemiring.closure (insert a ↑P)).carrier := by
  have : ¬ ∃ x ∈ P, ∃ y ∈ P, -1 = x + a * y :=
    by aesop (add (minus_one_not_mem_adjoin_linear P a ha) norm)
  have : -1 ∉ {z : F | ∃ x ∈ P, ∃ y ∈ P, z = x + a * y} := this
  simpa [Subsemiring.closure_insert_ringPreordering] using this

The proof looks like a straightforward combination of the two lemmas on the face of it. However, as you can see, something very strange is going on with the types, because one of my lines is literally have [type] := this. However, all my attempts to remove this line have failed, due to the simplifier pushing the negation through the quantifiers and then failing to match the results together.

How can I fix this to be nicer? Have I made a design/engineering mistake somewhere?

[Artie Khovanov]

Wait this is so strange
This reduced example allows me to remove that line?
But the original doesn't??

[Yaël Dillies]

Time to bisect :wink:

[Artie Khovanov]

@Yaël Dillies is extract_goal guaranteed to be conservative?

[Yaël Dillies]

No, not at all. It's using pretty-printing, which doesn't round-trip for various reasons

[Artie Khovanov]

oh christ -- well there's my issue
time to make a less minimal but actually working example

[Artie Khovanov]

(deleted)

[Artie Khovanov]

(deleted)

[Artie Khovanov]

it's actually spread notation, and I want to avoid a nonterminal simp

[Artie Khovanov]

import Mathlib

variable (S R : Type*) [CommRing R] [SetLike S R]

class RingPreorderingClass extends SubsemiringClass S R : Prop

structure RingPreordering extends Subsemiring R where
  minus_one_not_mem' : -1 ∉ carrier

instance RingPreordering.instSetLike : SetLike (RingPreordering R) R : =sorry

instance RingPreordering.instRingPreorderingClass : RingPreorderingClass (RingPreordering R) R :=
  sorry

variable {S F : Type*} [Field F] [SetLike S F] [RingPreorderingClass S F] (P : S) (a : F)

def RingPreordering.adjoin_linear : Subsemiring F where
  carrier := {z : F | ∃ x ∈ P, ∃ y ∈ P, z = x + a * y}
  zero_mem' := sorry
  one_mem' := sorry
  add_mem' := sorry
  mul_mem' := sorry

theorem Subsemiring.closure_insert_ringPreordering :
    Subsemiring.closure (insert a P) = RingPreordering.adjoin_linear P a := sorry

theorem RingPreordering.minus_one_not_mem_adjoin_linear
    (ha : -a ∉ P) (x y : F) (hx : x ∈ P) (hy : y ∈ P) : -1 ≠ x + a * y := sorry

def RingPreordering.adjoin (a : F) (ha : -a ∉ P) : RingPreordering F where
  __ := Subsemiring.closure (insert a P)
  minus_one_not_mem' := by
    have : ¬ ∃ x ∈ P, ∃ y ∈ P, -1 = x + a * y :=
      by aesop (add (minus_one_not_mem_adjoin_linear P a ha) norm)
    have : -1 ∉ adjoin_linear P a := this
    simpa [Subsemiring.closure_insert_ringPreordering] using this

[Artie Khovanov]

again, removing the penultimate line breaks the proof

[Damiano Testa]

If you use set_option pp.all true before extract_goal you will get something that has more chances of round-tripping (and is guaranteed to be much longer).