-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem card_isPrincipal_dvd_norm_le (s : ℝ) :
    Nat.card {I : (Ideal (𝓞 K))⁰ // (J : Ideal (𝓞 K)) ∣ I ∧ IsPrincipal (I : Ideal (𝓞 K)) ∧
      absNorm (I : Ideal (𝓞 K)) ≤ s} * torsionOrder K =
        Nat.card {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) ≤ s}

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ absNorm ↑I ≤ ⌊s⌋₊ } * ↑(torsionOrder K) =
    Nat.card { a // intNorm ↑((idealSetEquiv K J) a) ≤ ⌊s⌋₊ }

Tactic:
rw [torsionOrder, PNat.mk_coe, ← Nat.card_eq_fintype_card, ← Nat.card_prod]

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card ({ I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ absNorm ↑I ≤ ⌊s⌋₊ } × ↥(Units.torsion K)) =
    Nat.card { a // intNorm ↑((idealSetEquiv K J) a) ≤ ⌊s⌋₊ }

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 > s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * ↑(torsionOrder K) =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

Tactic:
simp_rw [lt_iff_not_le.mp (lt_of_lt_of_le hs (Nat.cast_nonneg _)), lt_iff_not_le.mp
  (lt_of_lt_of_le hs (mixedEmbedding.norm_nonneg _)), and_false, Nat.card_of_isEmpty,
  zero_mul]

Result:
no goals

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * ↑(torsionOrder K) =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

Tactic:
simp_rw [← intNorm_idealSetEquiv_apply, ← Nat.le_floor_iff hs]

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ absNorm ↑I ≤ ⌊s⌋₊ } * ↑(torsionOrder K) =
    Nat.card { a // intNorm ↑((idealSetEquiv K J) a) ≤ ⌊s⌋₊ }

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : { x // x ∈ Finset.Iic ⌊s⌋₊ }
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // mixedEmbedding.norm ↑a = ↑i } ≃ { a // intNorm ↑((idealSetEquiv K J) a) = i }

Tactic:
simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : { x // x ∈ Finset.Iic ⌊s⌋₊ }
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // intNorm ↑((idealSetEquiv K J) a) = i } ≃ { a // intNorm ↑((idealSetEquiv K J) a) = i }

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : { x // x ∈ Finset.Iic ⌊s⌋₊ }
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // absNorm ↑↑a.1 = i } ≃ { b // intNorm ↑((idealSetEquiv K J) ↑b) = 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 aesop
  _   ≃ {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

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * ↑(torsionOrder K) =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

Tactic:
obtain hs | hs := le_or_gt 0 s

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * ↑(torsionOrder K) =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 > s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * ↑(torsionOrder K) =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card ({ I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ absNorm ↑I ≤ ⌊s⌋₊ } × ↥(Units.torsion K)) =
    Nat.card { a // intNorm ↑((idealSetEquiv K J) a) ≤ ⌊s⌋₊ }

Tactic:
refine Nat.card_congr <| @Equiv.ofFiberEquiv _ (γ := Finset.Iic ⌊s⌋₊) _
  (fun I ↦ ⟨absNorm I.1.val.1, Finset.mem_Iic.mpr I.1.prop.2.2⟩)
  (fun a ↦ ⟨intNorm (idealSetEquiv K J a.1).1, Finset.mem_Iic.mpr a.prop⟩) fun ⟨i, hi⟩ ↦ ?_

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : { x // x ∈ Finset.Iic ⌊s⌋₊ }
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // (fun I => ⟨absNorm ↑↑I.1, ⋯⟩) a = ⟨i, hi⟩ } ≃
    { b // (fun a => ⟨intNorm ↑((idealSetEquiv K J) ↑a), ⋯⟩) b = ⟨i, hi⟩ }

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝² : { x // x ∈ Finset.Iic ⌊s⌋₊ }
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
x✝¹ : ↥(Units.torsion K)
x✝ : ↥(Ideal (𝓞 K))⁰
⊢ (↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ ≤ ⌊s⌋₊) ∧ absNorm ↑x✝ = i ↔ ↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = i

Tactic:
aesop

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : { x // x ∈ Finset.Iic ⌊s⌋₊ }
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // intNorm ↑((idealSetEquiv K J) a) = i } ≃ { a // intNorm ↑((idealSetEquiv K J) a) = i }

Tactic:
rfl

Result:
no goals

Proof state:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : { x // x ∈ Finset.Iic ⌊s⌋₊ }
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // (fun I => ⟨absNorm ↑↑I.1, ⋯⟩) a = ⟨i, hi⟩ } ≃
    { b // (fun a => ⟨intNorm ↑((idealSetEquiv K J) ↑a), ⋯⟩) b = ⟨i, hi⟩ }

Tactic:
simp_rw [Subtype.mk.injEq]

Result:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝ : { x // x ∈ Finset.Iic ⌊s⌋₊ }
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
⊢ { a // absNorm ↑↑a.1 = i } ≃ { b // intNorm ↑((idealSetEquiv K J) ↑b) = i }