Need help with rewriting to unfold the definition of algebra

Stream: mathlib4

[aprilgrimoire]

Hi!

Here I have a ↥G' algebra↥F , derived from G' being a subfield of ↥F. Now I have ⟨⟨a, a_in_F⟩, a_in_G⟩ • ⟨Complex.sin ↑φ * Complex.I, ⋯⟩ = 1, and I wish to unfold the definition of HSMul here to get an equation in ↥F. However, I've tried simp and rw [HSMul.hSMul instHSMul.1] at h1, but neither succeeded. How could I unfold this definition?

Here's the full code:

import Mathlib

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

  let ℚ_in_ℂ := Subfield.closure {(1 : Complex)}
  let F := Subfield.closure (ℚ_in_ℂ ∪ {α})
  let G := Subfield.closure (ℚ_in_ℂ ∪ {β})

  G ≤ F := by
    intros φ α β ℚ_in_ℂ F G
    have hα_inv : α⁻¹ = Complex.exp (-φ * Complex.I) := by
      unfold α
      symm
      conv =>
        lhs
        arg 1
        apply neg_mul
      have h1 := Complex.exp_neg (↑φ * Complex.I)
      exact h1

    have hα_in_F : α ∈ F := by
      have h1 : α ∈ (↑ℚ_in_ℂ ∪ {α} : Set ℂ)
      . apply Set.mem_union_right
        exact Set.mem_singleton α
      apply Subfield.subset_closure
      exact h1

    have hα_inv_in_F : α⁻¹ ∈ F := by
      apply Subfield.inv_mem'
      exact hα_in_F

    have hα_add_α_inv_in_F : α + α⁻¹ ∈ F := by
      apply Subfield.add_mem
      exact hα_in_F
      exact hα_inv_in_F

    have hα_sub_α_inv_in_F : α - α⁻¹ ∈ F := by
      apply Subfield.sub_mem
      exact hα_in_F
      exact hα_inv_in_F

    have h1 : (G ≤ F) := by
      have h2 : (ℚ_in_ℂ ∪ {β} : Set ℂ) ⊆ (↑F : Set ℂ)
      . apply Set.union_subset_iff.mpr
        apply And.intro
        case left =>
          unfold F
          have h3 : (ℚ_in_ℂ : Set ℂ) ⊆ (ℚ_in_ℂ ∪ {α} : Set ℂ)
          apply Set.subset_union_left
          apply subset_trans h3
          apply Subfield.subset_closure

        case right =>
          unfold F
          apply Set.singleton_subset_iff.mpr
          have h3 : β = (α + α⁻¹) / 2
          . unfold β
            rw [hα_inv]
            unfold α
            repeat rw [← Complex.cos_add_sin_I]
            rw [Complex.ofReal_cos]
            simp
            ring
          rw [h3]

          apply Subfield.div_mem
          exact hα_add_α_inv_in_F

          apply Subfield.subset_closure
          apply (Set.mem_union 2 ↑ℚ_in_ℂ {α}).mpr
          apply Or.inl


          have h7 : 1 ∈ ℚ_in_ℂ
          . apply Subfield.subset_closure
            apply Set.mem_singleton

          have h8 : (2 : ℂ) = 1 + 1
          . ring

          rw [h8]

          apply Subfield.add_mem ℚ_in_ℂ h7 h7
      unfold G
      apply Subfield.closure_le.mpr
      exact h2

    let G' := Subfield.comap (Subfield.subtype F) G

    have h2 : (Module.Free G' F) :=
      Module.Free.of_basis (Basis.ofVectorSpace G' F)

    let F_spanner : Fin 2 -> F :=
      have one_in_F : ((1 : ℂ) ∈ F) := by
        have h1 : 1 ∈ (↑ℚ_in_ℂ : Set ℂ) ∪ {α}
        . apply Set.mem_union_left
          unfold ℚ_in_ℂ
          apply Set.mem_of_subset_of_mem Subfield.subset_closure
          simp
        unfold F
        apply Set.mem_of_subset_of_mem Subfield.subset_closure
        exact h1
      have sinφI_in_F : ((Real.sin φ) * Complex.I ∈ F) := by
        have h1 : (Real.sin φ) * Complex.I = (α - α⁻¹) / 2
        . rw [hα_inv]
          unfold α
          repeat rw [← Complex.cos_add_sin_I]
          simp
        have h2 : (α - α⁻¹) / 2 ∈ F
        . apply Subfield.mul_mem
          exact hα_sub_α_inv_in_F
          have h3 := SubfieldClass.ratCast_mem F (2⁻¹ : ℚ)
          conv at h3 =>
            rhs
            simp
          exact h3
        rw [h1]
        exact h2
          -- rw [← WithZero.coe_inv (2 : ℚ)] at h3

      ![⟨1, one_in_F⟩, ⟨(Real.sin φ) * Complex.I, sinφI_in_F⟩]

    have F_spanner_linear_indep : LinearIndependent G' F_spanner := by
      apply linearIndependent_fin2.mpr
      unfold F_spanner
      simp
      apply And.intro
      . apply Subtype.coe_ne_coe.mp
        simp
        have h1 : φ ∈ Set.Ioo 0 Real.pi
        . apply Set.mem_Ioo.mpr
          apply And.intro
          . unfold φ
            apply div_pos
            apply mul_pos
            simp
            exact Real.pi_pos
            have h2 : (0 : ℝ) < 2 := by
              simp
            apply lt_trans h2
            apply GT.gt.lt
            simp
            exact n_gt_2
          . have h2 : Real.pi = 2 * Real.pi / 2
            . simp
            have h3 :=
              have ha : 0 < 2 * Real.pi := by
                apply Left.mul_pos
                simp
                exact Real.pi_pos
              have hb : (0 : ℝ) < 2 := by
                simp
              have hc : (0 : ℝ) < n := by
                simp
                have hc1 : 0 < 2 := by
                  simp
                apply LT.lt.trans hc1
                apply GT.gt.lt
                exact n_gt_2

            (div_lt_div_iff_of_pos_left ha hc hb).mpr
            unfold φ
            nth_rw 2 [h2]
            apply h3
            simp
            apply GT.gt.lt
            exact n_gt_2
        suffices h2 : 0 < Real.sin φ by
          rw [← Complex.ofReal_sin]
          have h3 : (0 : ℂ) = ↑(0 : ℝ) := by
            simp
          rw [h3]
          rw [Complex.ofReal_inj]
          apply ne_of_gt
          exact h2
        apply Real.sin_pos_of_mem_Ioo
        exact h1
      . intro a a_in_F a_in_G
        intro h1
        apply_fun Subtype.val at h1
        simp at h1
        rw [HSMul.hSMul] at h1
        rw [instHSMul.1] at h1


        /-
        rw [← Subfield.coe_one] at h1
        apply_fun Subtype.val at h1
        simp at h1
        -/


    let F' := Submodule.span G' (Set.range F_spanner)

    exact h1

[Kim Morrison]

This thread is perhaps duplicated by #mathlib4 > Rewriting and simplifying yielded inferInstance.1.1 . Perhaps discussion should continue there, where Ruben has asked for a #mwe.