-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
calc :
  { a : (↑(idealSet K J) : Type u_1) //
      Eq (α := ℝ) ((mixedEmbedding.norm : (a : mixedSpace K) → ℝ) (↑a : mixedSpace K) : ℝ) ((↑i : ℝ) : ℝ) } ≃
    { a : (↑(idealSet K J) : Type u_1) //
      intNorm.{u_1} (K := K)
          (↑((idealSetEquiv K J :
                  (a : (↑(idealSet K J) : Type u_1)) →
                    (↑{a : (↑(integerSet K) : Type u_1) |
                          (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                      Type u_1))
                a) :
            (↑(integerSet K) : Type u_1)) =
        i }
⊢ { a :
      { I : ↥(Ideal (𝓞 K))⁰ //
          (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
            IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ ⌊s⌋₊ } ×
        ↥(Units.torsion K) //
      (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑(↑a.1 : ↥(Ideal (𝓞 K))⁰) : Ideal (𝓞 K)) = i } ≃
    { b :
      { a : (↑(idealSet K J) : Type u_1) //
        intNorm.{u_1} (K := K)
            (↑((idealSetEquiv K J :
                    (a : (↑(idealSet K J) : Type u_1)) →
                      (↑{a : (↑(integerSet K) : Type u_1) |
                            (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                        Type u_1))
                  a) :
              (↑(integerSet K) : Type u_1)) ≤
          ⌊s⌋₊ } //
      intNorm.{u_1} (K := K)
          (↑((idealSetEquiv K J :
                  (a : (↑(idealSet K J) : Type u_1)) →
                    (↑{a : (↑(integerSet K) : Type u_1) |
                          (↑(preimageOfMemIntegerSet a) : 𝓞 K) ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))} :
                      Type u_1))
                (↑b : (↑(idealSet K J) : Type u_1))) :
            (↑(integerSet K) : Type u_1)) =
        i }

Tactic:
calc _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // _ ∧ _ ∧ _} // absNorm I.1.1 = i} × torsion K :=
        Equiv.prodSubtypeFstEquivSubtypeProd
      _ ≃ {I : (Ideal (𝓞 K))⁰ // (_ ∧ _ ∧ absNorm I.1 ≤ ⌊s⌋₊) ∧ absNorm I.1 = i}
            × torsion K := Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeSubtypeEquivSubtypeInter
        (p := fun I : (Ideal (𝓞 K))⁰ ↦ J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 ≤ ⌊s⌋₊)
        (q := fun I ↦ absNorm I.1 = i))
      _ ≃ {I : (Ideal (𝓞 K))⁰ // J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 = i}
            × torsion K := Equiv.prodCongrLeft fun _ ↦ Equiv.subtypeEquivRight fun _ ↦ by grind
      _ ≃ {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) = i} :=
            (idealSetEquivNorm K J i).symm
      _ ≃ {a : idealSet K J // intNorm (idealSetEquiv K J a).1 = i} := by
        simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj]
        rfl
      _ ≃ {b : {a : idealSet K J // intNorm (idealSetEquiv K J a).1 ≤ ⌊s⌋₊} //
            intNorm (idealSetEquiv K J b).1 = i} :=
        (Equiv.subtypeSubtypeEquivSubtype fun h ↦ Finset.mem_Iic.mp (h ▸ hi)).symm

Premises used: Dvd.dvd, Ideal.absNorm, Equiv.prodSubtypeFstEquivSubtypeProd, Finset.mem_Iic, NumberField.mixedEmbedding.fundamentalCone.idealSetEquivNorm, Equiv.subtypeSubtypeEquivSubtype, LE.le, Equiv.subtypeEquivRight, Ideal, Equiv.prodCongrLeft, And, Iff.mp, Nat.floor, Equiv.subtypeSubtypeEquivSubtypeInter, Equiv.symm, NumberField.RingOfIntegers, NumberField.mixedEmbedding.fundamentalCone.idealSet, Subtype.val, Eq, DFunLike.coe, Submodule.IsPrincipal