A seemingly bug? side effect of extract_goal

Stream: lean4

[aprilgrimoire]

import Mathlib

suppress_compilation

def φ (n : ℕ) := 2 * Real.pi / n
def α (n : ℕ) := Complex.exp (φ n * Complex.I)
def β (n : ℕ) : ℂ := Real.cos (φ n)

def ℚ_in_ℂ := Subfield.closure (∅ : Set ℂ)
def F (n : ℕ) := Subfield.closure ({α n})
def G (n : ℕ) := Subfield.closure ({β n})
def G' (n : ℕ) := Subfield.comap (Subfield.subtype (F n)) (G n)

lemma G_leq_F (n : ℕ) : G n ≤ F n := sorry

lemma F_spanner_aux_one (n : ℕ) : 1 ∈ F n := sorry

lemma F_spanner_aux_two (n : ℕ) : Real.sin (φ n) * Complex.I ∈ F n := sorry

def F_spanner (n : ℕ) : Fin 2 -> F n :=
  ![⟨1, F_spanner_aux_one n⟩, ⟨(Real.sin (φ n)) * Complex.I, F_spanner_aux_two n⟩]

def comap_pullback {F : Type} [Field F] {G : Type} [Field G] {f : G →+* F} {H : Subfield F}
    (x : H) (hx : (x : F) ∈ (f '' ⊤)) : (Subfield.comap f H) := sorry

lemma comap_pullback_map {F : Type} [Field F] {G : Type} [Field G] {f : G →+* F} {H : Subfield F}
    (x : H) (hx : (x : F) ∈ (f '' ⊤)) : f (comap_pullback x hx) = x := sorry

def F' (n : ℕ) := Submodule.span (G' n) (Set.range (F_spanner n))

theorem extracted_1 (n : ℕ) (x_ : ↥(F n)) (hx_ : x_ ∈ Subfield.closure ↑(F' n)) (x : ↥(F n))
    (hx : x ∈ Subfield.closure ↑(F' n)) :
    (fun x hx ↦ x ∈ F' n) x hx → (fun x hx ↦ x ∈ F' n) x⁻¹ (inv_mem hx) := by
  simp only
  unfold F' at hx
  intro h1
  apply (mem_span_range_iff_exists_fun ↑(G' n)).mp at h1
  let ⟨c, hc⟩ := h1
  unfold F_spanner at hc
  simp only [Complex.ofReal_sin, Fin.sum_univ_two, Fin.isValue, Matrix.cons_val_zero,
    Matrix.cons_val_one, Matrix.head_cons] at hc
  apply_fun (F n).subtype at hc
  simp only [Fin.isValue, Subfield.coe_subtype, Subfield.coe_add] at hc
  repeat rw [Subfield.smul_def] at hc
  simp only [Fin.isValue, smul_eq_mul, Subfield.coe_mul, mul_one] at hc
  let y := (c 0) - (c 1) * (Complex.sin ↑(φ n) * Complex.I)
  let z := x * y
  have h2 : z ∈ G n := by
    unfold z
    rw [← hc]
    unfold y
    ring_nf
    apply Subfield.sub_mem
    . apply Subfield.pow_mem
      apply mem_G
    . apply Subfield.mul_mem
      . apply Subfield.mul_mem
        . apply Subfield.pow_mem
          apply mem_G
        . rw [Complex.sin_sq]
          apply Subfield.sub_mem
          . apply Subfield.one_mem
          . apply Subfield.pow_mem
            exact mem_G_cos_φ n
      . simp only [Complex.I_sq, neg_mem_iff]
        apply one_mem
  let z' := comap_pullback (F := ℂ) (G := ↑(F n)) (H := G n) (f := Subfield.subtype (F n)) ⟨z, h2⟩ (by
    simp only [Subfield.coe_subtype, Set.top_eq_univ, Set.image_univ, Subtype.range_coe_subtype,
      SetLike.setOf_mem_eq, SetLike.mem_coe]
    apply Set.mem_of_subset_of_mem (G_leq_F n)
    exact h2)

  let cx_inv := ![c 0 / ↑z', -c 1 / ↑z']

  have hx_x_inv : (x * ∑ i, cx_inv i • F_spanner n i = 1) := by
    apply_fun (F n).subtype
    unfold cx_inv
    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.sum_univ_two,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, Subfield.coe_subtype,
      Subfield.coe_mul, Subfield.coe_add, OneMemClass.coe_one]

    set_option pp.proofs true in extract_goal

    repeat rw [Subfield.smul_def]
    rw [Subfield.smul_def]

    repeat rw [smul_eq_mul]

    simp only [Fin.isValue, Subfield.coe_div, smul_eq_mul, Subfield.coe_mul]
    conv =>
      lhs
      rhs


    rw [comap_pullback_map]

[aprilgrimoire]

Also after removing the extract_goal line,

    repeat rw [Subfield.smul_def]
    rw [Subfield.smul_def]

seems weird. Why could the second rw succeed?

[aprilgrimoire]

Also replacing

  have h2 : z ∈ G n := by
    unfold z
    rw [← hc]
    unfold y
    ring_nf
    apply Subfield.sub_mem
    . apply Subfield.pow_mem
      apply mem_G
    . apply Subfield.mul_mem
      . apply Subfield.mul_mem
        . apply Subfield.pow_mem
          apply mem_G
        . rw [Complex.sin_sq]
          apply Subfield.sub_mem
          . apply Subfield.one_mem
          . apply Subfield.pow_mem
            exact mem_G_cos_φ n
      . simp only [Complex.I_sq, neg_mem_iff]
        apply one_mem
  let z' := comap_pullback (F := ℂ) (G := ↑(F n)) (H := G n) (f := Subfield.subtype (F n)) ⟨z, h2⟩ (by
    simp only [Subfield.coe_subtype, Set.top_eq_univ, Set.image_univ, Subtype.range_coe_subtype,
      SetLike.setOf_mem_eq, SetLike.mem_coe]
    apply Set.mem_of_subset_of_mem (G_leq_F n)
    exact h2)

with

have h2 : z ∈ G n := sorry

changes the behavior unexpectedly.