-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Asymptotics (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : ℝ
hs : 0 ≤ s
this : Fintype { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }
e : (C : ClassGroup (𝓞 K)) →
  { x : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } //
      (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑x : ↥(Ideal (𝓞 K))⁰) = C } ≃
    { x : ↥(Ideal (𝓞 K))⁰ //
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑x : Ideal (𝓞 K))) : ℝ) ≤ s ∧
        (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) x = C } :=
  fun (C : ClassGroup (𝓞 K)) ↦
    Equiv.subtypeSubtypeEquivSubtypeInter
      (fun (I : ↥(Ideal (𝓞 K))⁰) ↦ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s)
      fun (I : ↥(Ideal (𝓞 K))⁰) ↦ (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C
h :
  ∑ x : ClassGroup (𝓞 K),
      (↑(Finset.card.{u_1} (α :=
              { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s })
              {x_1 : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } |
                (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑x_1 : ↥(Ideal (𝓞 K))⁰) = x}) :
          ℝ) /
        s =
    (↑(Finset.card.{u_1} (α :=
            { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) Finset.univ) :
        ℝ) /
      s
h₁ :
  ∑ x : ClassGroup (𝓞 K),
      (↑(Finset.card.{u_1} (α :=
              { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s })
              {x_1 : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } |
                (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑x_1 : ↥(Ideal (𝓞 K))⁰) = x}) :
          ℝ) /
        s =
    (↑(∑ b : ClassGroup (𝓞 K),
            Finset.card.{u_1} (α :=
              { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s })
              {a : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } |
                (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑a : ↥(Ideal (𝓞 K))⁰) = b}) :
        ℝ) /
      s
⊢ ∑ x : ClassGroup (𝓞 K),
      (↑(Finset.card.{u_1} (α :=
              { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s })
              {x_1 : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } |
                (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑x_1 : ↥(Ideal (𝓞 K))⁰) = x}) :
          ℝ) /
        s =
    (↑(Fintype.card.{u_1}
            { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s }) :
        ℝ) /
      s
have h₂ : ∑ x : ClassGroup (𝓞 K),
    (↑(Finset.card.{u_1} (α :=
            { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s })
            {x_1 : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } |
              (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑x_1 : ↥(Ideal (𝓞 K))⁰) = x}) :
        ℝ) /
      s =
  (∑ x : ClassGroup (𝓞 K),
      (↑(Finset.card.{u_1} (α :=
            { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s })
            {a : { I : ↥(Ideal (𝓞 K))⁰ // (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤ s } |
              (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) (↑a : ↥(Ideal (𝓞 K))⁰) = x}) :
        ℝ)) /
    s
Tactic: rw [Fintype.card, Finset.card_eq_sum_card_fiberwise (f := fun I ↦ ClassGroup.mk0 I.1)
      (t := Finset.univ) (fun _ _ ↦ Finset.mem_univ _), Nat.cast_sum, Finset.sum_div]