-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone (goal)
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⌋₊
⊢ { 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) //
      (fun
              (I :
                { I : ↥(Ideal (𝓞 K))⁰ //
                    (↑J : Ideal (𝓞 K)) ∣ (↑I : Ideal (𝓞 K)) ∧
                      IsPrincipal (↑I : Ideal (𝓞 K)) ∧ (absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K)) ≤ ⌊s⌋₊ } ×
                  ↥(Units.torsion K)) ↦
            (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.Iic ⌊s⌋₊)
                ((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑(↑I.1 : ↥(Ideal (𝓞 K))⁰) : Ideal (𝓞 K))) ⋯ :
              ↥(Finset.Iic ⌊s⌋₊)))
          a =
        Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.Iic ⌊s⌋₊) i hi } ≃
    { 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⌋₊ } //
      (fun
              (a :
                { 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⌋₊ }) ↦
            (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.Iic ⌊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))
                        (↑a : (↑(idealSet K J) : Type u_1))) :
                    (↑(integerSet K) : Type u_1)))
                ⋯ :
              ↥(Finset.Iic ⌊s⌋₊)))
          b =
        Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.Iic ⌊s⌋₊) i hi }
have inl : { 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: simp_rw [Subtype.mk.injEq]