-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
inst_4 : Module.Finite ℤ S
n : ℕ
inst_5 : CharZero S
have have₁ have₂ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S //
          Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
      Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
have₃ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n })
    (this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
      Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1
have₄ have₅ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n })
    (this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
      Nat.card.{u_1}
          { x : Ideal S //
            Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n } +
        1
have₆ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n })
    (this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } = 1
have₇ :
  ∀
    (this :
      Finite.{max 1 (u_1 + 1)}
        { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n })
    (this : Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }),
    Nat.card.{u_1} { I : Ideal S // I = ⊥ } = 1
⊢ Nat.card.{u_1} { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } =
    Nat.card.{u_1} { I : ↥(Ideal S)⁰ // (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n } + 1

Tactic:
classical
  have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  have : Finite {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  rw [Nat.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ I ∈ (Ideal S)⁰)
    (fun I ↦ absNorm I ≤ n))]
  let e : {I : Ideal S // absNorm I ≤ n} ≃ {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} ⊕
      {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} := by
    refine (Equiv.subtypeEquivRight ?_).trans (subtypeOrEquiv _ _ ?_)
    · intro _
      simp_rw [← or_and_right, em, true_and]
    · exact Pi.disjoint_iff.mpr fun I ↦ Prop.disjoint_iff.mpr (by tauto)
  simp_rw [Nat.card_congr e, Nat.card_sum, add_right_inj]
  conv_lhs =>
    enter [1, 1, I]
    rw [← absNorm_ne_zero_iff_mem_nonZeroDivisors, ne_eq, not_not, and_iff_left_iff_imp.mpr
      (fun h ↦ by rw [h]; exact Nat.zero_le n), absNorm_eq_zero_iff]
  rw [Nat.card_unique]

Premises used: Iff.mpr, Ideal.absNorm, Classical.not_not, Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors, Nat.card_sum, Membership.mem, nonZeroDivisors, LE.le, Ideal, ne_eq, Nat.card_congr, Nat.card_unique, Ideal.absNorm_eq_zero_iff, Equiv.subtypeSubtypeEquivSubtypeInter, DFunLike.coe, and_iff_left_iff_imp, add_right_inj