-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem card_norm_le_eq_card_norm_le_add_one (n : ℕ) [CharZero S] :
    Nat.card {I : Ideal S // absNorm I ≤ n} =
      Nat.card {I : (Ideal S)⁰ // absNorm (I : Ideal S) ≤ n} + 1

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I => I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I => I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
I : Ideal S
h : absNorm I = 0
⊢ absNorm I ≤ n

Tactic:
rw [h]

Result:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I => I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I => I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
I : Ideal S
h : absNorm I = 0
⊢ 0 ≤ n

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }

Tactic:
refine (Equiv.subtypeEquivRight ?_).trans (subtypeOrEquiv _ _ ?_)

Result:
case refine_1
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ ∀ (x : Ideal S), absNorm x ≤ n ↔ x ∈ (Ideal S)⁰ ∧ absNorm x ≤ n ∨ x ∉ (Ideal S)⁰ ∧ absNorm x ≤ n

case refine_2
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ Disjoint (fun I => I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) fun I => I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n

Proof state:
case refine_2
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ Disjoint (fun I => I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) fun I => I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n

Tactic:
exact Pi.disjoint_iff.mpr fun I ↦ Prop.disjoint_iff.mpr (by tauto)

Result:
no goals

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I => I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I => I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
I : Ideal S
h : absNorm I = 0
⊢ 0 ≤ n

Tactic:
exact Nat.zero_le n

Result:
no goals

Proof state:
case refine_1
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
x✝ : Ideal S
⊢ absNorm x✝ ≤ n ↔ x✝ ∈ (Ideal S)⁰ ∧ absNorm x✝ ≤ n ∨ x✝ ∉ (Ideal S)⁰ ∧ absNorm x✝ ≤ n

Tactic:
simp_rw [← or_and_right, em, true_and]

Result:
no goals

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { I // absNorm ↑I ≤ n } + 1

Tactic:
have : Finite {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
  (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h

Result:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { I // absNorm ↑I ≤ n } + 1

Proof state:
case refine_1
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ ∀ (x : Ideal S), absNorm x ≤ n ↔ x ∈ (Ideal S)⁰ ∧ absNorm x ≤ n ∨ x ∉ (Ideal S)⁰ ∧ absNorm x ≤ n

Tactic:
intro _

Result:
case refine_1
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
x✝ : Ideal S
⊢ absNorm x✝ ≤ n ↔ x✝ ∈ (Ideal S)⁰ ∧ absNorm x✝ ≤ n ∨ x✝ ∉ (Ideal S)⁰ ∧ absNorm x✝ ≤ n

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { I // absNorm ↑I ≤ n } + 1

Tactic:
rw [Nat.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ I ∈ (Ideal S)⁰)
  (fun I ↦ absNorm I ≤ n))]

Result:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { x // x ∈ (Ideal S)⁰ ∧ absNorm x ≤ n } + 1

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I => I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I => I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
⊢ Nat.card { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } = 1

Tactic:
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]

Result:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I => I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I => I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
⊢ Nat.card { I // I = ⊥ } = 1