-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem finite_setOf_absNorm_eq [CharZero S] (n : ℕ) :
    {I : Ideal S | Ideal.absNorm I = n}.Finite

Proof state:
case inr.refine_2
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
hJ : J ∈ {I | absNorm I = n}
h : f I = f J
⊢ I = J

Tactic:
rw [← comap_map_mk (span_singleton_absNorm_le I), ← hI.symm, ←
  comap_map_mk (span_singleton_absNorm_le J), ← hJ.symm]

Result:
case inr.refine_2
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
hJ : J ∈ {I | absNorm I = n}
h : f I = f J
⊢ comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) I) =
    comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) J)

Proof state:
case inr.refine_1
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ Finite (S ⧸ span {↑n})

Tactic:
rw [← absNorm_ne_zero_iff, absNorm_span_singleton]

Result:
case inr.refine_1
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ ((Algebra.norm ℤ) ↑n).natAbs ≠ 0

Proof state:
case inr.refine_1
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ ((Algebra.norm ℤ) ↑n).natAbs ≠ 0

Tactic:
simpa only [Ne, Int.natAbs_eq_zero, Algebra.norm_eq_zero_iff, Nat.cast_eq_zero] using
  ne_of_gt hn

Result:
no goals

Proof state:
case inr.refine_2
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ Set.InjOn f {I | absNorm I = n}

Tactic:
intro I hI J hJ h

Result:
case inr.refine_2
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
hJ : J ∈ {I | absNorm I = n}
h : f I = f J
⊢ I = J

Proof state:
case inl
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n = 0
⊢ {I | absNorm I = n}.Finite

Tactic:
simp only [hn, absNorm_eq_zero_iff, Set.setOf_eq_eq_singleton, Set.finite_singleton]

Result:
no goals

Proof state:
case inr.refine_1
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ (f '' {I | absNorm I = n}).Finite

Tactic:
suffices Finite (S ⧸ @Ideal.span S _ {↑n}) by
  let g := ((↑) : Ideal (S ⧸ @Ideal.span S _ {↑n}) → Set (S ⧸ @Ideal.span S _ {↑n}))
  refine Set.Finite.of_finite_image (f := g) ?_ SetLike.coe_injective.injOn
  exact Set.Finite.subset Set.finite_univ (Set.subset_univ _)

Result:
case inr.refine_1
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ Finite (S ⧸ span {↑n})

Proof state:
case inr
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ {I | absNorm I = n}.Finite

Tactic:
refine Set.Finite.of_finite_image (f := f) ?_ ?_

Result:
case inr.refine_1
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ (f '' {I | absNorm I = n}).Finite

case inr.refine_2
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ Set.InjOn f {I | absNorm I = n}

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
this : Finite (S ⧸ span {↑n})
⊢ (f '' {I | absNorm I = n}).Finite

Tactic:
let g := ((↑) : Ideal (S ⧸ @Ideal.span S _ {↑n}) → Set (S ⧸ @Ideal.span S _ {↑n}))

Result:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
this : Finite (S ⧸ span {↑n})
g : Ideal (S ⧸ span {↑n}) → Set (S ⧸ span {↑n}) := SetLike.coe
⊢ (f '' {I | absNorm I = n}).Finite

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
⊢ {I | absNorm I = n}.Finite

Tactic:
obtain hn | hn := Nat.eq_zero_or_pos n

Result:
case inl
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n = 0
⊢ {I | absNorm I = n}.Finite

case inr
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
⊢ {I | absNorm I = n}.Finite

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
this : Finite (S ⧸ span {↑n})
g : Ideal (S ⧸ span {↑n}) → Set (S ⧸ span {↑n}) := SetLike.coe
⊢ (f '' {I | absNorm I = n}).Finite

Tactic:
refine Set.Finite.of_finite_image (f := g) ?_ SetLike.coe_injective.injOn

Result:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
this : Finite (S ⧸ span {↑n})
g : Ideal (S ⧸ span {↑n}) → Set (S ⧸ span {↑n}) := SetLike.coe
⊢ (g '' (f '' {I | absNorm I = n})).Finite