-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
b : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu :
  Membership.mem (γ := Set (mixedSpace K)) (integerSet K)
    (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
mk :
  (↑(preimageOfMemIntegerSet
            (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
              (HSMul.hSMul (β := mixedSpace K) u
                ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
              hu) *
          (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰)) :
      𝓞 K) =
    (↑x : 𝓞 K)
mk₁ :
  (↑(↑(preimageOfMemIntegerSet
                (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                  (HSMul.hSMul (β := mixedSpace K) u
                    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
                  hu) *
              (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰)) :
          𝓞 K) :
      K) =
    (↑(↑x : 𝓞 K) : K)
mk₂ :
  Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        (↑(↑(preimageOfMemIntegerSet
                    (Subtype.mk (p := fun (x : mixedSpace K) ↦
                      Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                      (HSMul.hSMul (β := mixedSpace K) u
                        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
                      hu) *
                  (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰)) :
              𝓞 K) :
          K) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K)
mk₃ :
  Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        (↑((↑(preimageOfMemIntegerSet
                    (Subtype.mk (p := fun (x : mixedSpace K) ↦
                      Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                      (HSMul.hSMul (β := mixedSpace K) u
                        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
                      hu)) :
                𝓞 K) *
              (↑(↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) : 𝓞 K)) :
          K) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K)
mk₄ :
  HMul.hMul (α := mixedSpace K) (β := mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(preimageOfMemIntegerSet
                  (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
                    (HSMul.hSMul (β := mixedSpace K) u
                      ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
                    hu)) :
              𝓞 K)) :
        mixedSpace K)
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) : 𝓞 K)) :
        mixedSpace K) =
    (mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K)
mk₅ :
  HMul.hMul (β := mixedSpace K)
      (HSMul.hSMul (β := mixedSpace K) u ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) : 𝓞 K)) :
        mixedSpace K) =
    (mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K)
mk₆ :
  HMul.hMul (β := mixedSpace K)
      (HMul.hMul (α := mixedSpace K) (β := mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)) : mixedSpace K)
        ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
      ((mixedEmbedding K : (a : K) → mixedSpace K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (↑(↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) : 𝓞 K)) :
        mixedSpace K) =
    (mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K)
mk₇ :
  Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑u : 𝓞 K) * (↑x : 𝓞 K) *
            (↑(↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) : 𝓞 K))) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K)
mk₈ :
  Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑x : 𝓞 K) * (↑u : 𝓞 K) *
            (↑(↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) : 𝓞 K))) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K)
mk₉ :
  Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          ((↑x : 𝓞 K) * (↑u : 𝓞 K) *
            (↑(↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u)⁻¹ : ↥(𝓞 K)⁰) : 𝓞 K))) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K)
mk₁₀ :
  Eq (α := mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((↑x : 𝓞 K) * (↑u : 𝓞 K) * (↑u⁻¹ : 𝓞 K))) :
      mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K)
⊢ preimageOfMemIntegerSet
        (Subtype.mk (p := fun (x : mixedSpace K) ↦ Membership.mem (γ := Set (mixedSpace K)) (integerSet K) x)
          (HSMul.hSMul (β := mixedSpace K) u
            ((mixedEmbedding K : (a : K) → mixedSpace K) (↑(↑x : 𝓞 K) : K) : mixedSpace K))
          hu) *
      (↑((MulEquiv.symm unitsNonZeroDivisorsEquiv : (a : (𝓞 K)ˣ) → (↥(𝓞 K)⁰)ˣ) u⁻¹) : ↥(𝓞 K)⁰) =
    x

Tactic:
simp_rw [Subtype.ext_iff, RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff,
    Submonoid.coe_mul, map_mul, mixedEmbedding_preimageOfMemIntegerSet,
    unitSMul_smul, ← map_mul, mul_comm, map_inv, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe,
    Units.mul_inv_cancel_right]

Premises used: map_inv, Function.Injective.eq_iff, val_inv_unitsNonZeroDivisorsEquiv_symm_apply_coe, Units.mul_inv_cancel_right, Subtype.ext_iff, map_mul, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, NumberField.mixedEmbedding.unitSMul_smul, NumberField.mixedEmbedding_injective, mul_comm, NumberField.RingOfIntegers.ext_iff, Submonoid.coe_mul