awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
this : Finite.{u_1 + 1} (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)}))
g : Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) →
  Set (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  SetLike.coe
⊢ (g '' f '' {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}).Finite

Tactic:
Set.Finite.subset Set.finite_univ (Set.subset_univ _)

Premises used: Set.subset_univ, Set.Finite.subset, Set.finite_univ
-- 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
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
this : Finite.{u_1 + 1} (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)}))
g : Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) →
  Set (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  SetLike.coe
⊢ (g '' f '' {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n}).Finite

Tactic:
exact Set.Finite.subset Set.finite_univ (Set.subset_univ _)

Premises used: Set.subset_univ, Set.Finite.subset, Set.finite_univ
-- 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
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
inr : Finite.{u_1 + 1} (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)}))
⊢ (f '' {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) 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 _)
-- 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
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
inr : Int.natAbs ((Algebra.norm ℤ : (a : S) → ℤ) (↑n : S)) ≠ 0
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)}))

Tactic:
rw [← absNorm_ne_zero_iff, absNorm_span_singleton]

Premises used: Ideal.absNorm_ne_zero_iff, Ideal.absNorm_span_singleton
-- 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
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
⊢ Int.natAbs ((Algebra.norm ℤ : (a : S) → ℤ) (↑n : S)) ≠ 0

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

Premises used: ne_of_gt, Ne, Int.natAbs_eq_zero, Nat.cast_eq_zero, Algebra.norm_eq_zero_iff
-- 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
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
I : Ideal S
hI : Membership.mem (γ := Set (Ideal S)) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n} I
J : Ideal S
hJ : Membership.mem (γ := Set (Ideal S)) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n} J
h : f I = f J
inr :
  Eq (α := Ideal S)
    (comap (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)}))
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I))
    (comap (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)}))
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) 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]

Premises used: Ideal.comap_map_mk, Eq.symm, Ideal.span_singleton_absNorm_le
-- 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
inst_5 : CharZero S
n : ℕ
hn : n > 0
f : (I : Ideal S) → Ideal (HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) :=
  fun (I : Ideal S) ↦
    map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I
I : Ideal S
hI : Membership.mem (γ := Set (Ideal S)) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n} I
J : Ideal S
hJ : Membership.mem (γ := Set (Ideal S)) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = n} J
h : f I = f J
⊢ Eq (α := Ideal S)
    (comap (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)}))
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) I))
    (comap (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)}))
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (span {(↑n : S)})) (Quotient.mk (span {(↑n : S)})) J))

Tactic:
congr
-- 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
inst_5 : CharZero S
n : ℕ
h :
  ∀ (x : Ideal S),
    Membership.mem (γ := Set (Ideal S)) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I ≤ n} x ↔
      Membership.mem (γ := Set (Ideal S)) (⋃ i ∈ Set.Icc 0 n, {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = i}) x
⊢ Eq.{u_1 + 1} (α := Set (Ideal S)) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I ≤ n}
    (⋃ i ∈ Set.Icc 0 n, {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = i})

Tactic:
ext
-- 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
inst_5 : CharZero S
n : ℕ
x : Ideal S
⊢ Membership.mem (γ := Set (Ideal S)) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I ≤ n} x ↔
    Membership.mem (γ := Set (Ideal S)) (⋃ i ∈ Set.Icc 0 n, {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = i}) x

Tactic:
simp
-- 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
inst_5 : CharZero S
n : ℕ
rw : Set.Finite.{u_1} (α := Ideal S) (⋃ i ∈ Set.Icc 0 n, {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = i})
⊢ Set.Finite.{u_1} (α := Ideal S) {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I ≤ n}

Tactic:
rw [show {I : Ideal S | Ideal.absNorm I ≤ n} =
    (⋃ i ∈ Set.Icc 0 n, {I : Ideal S | Ideal.absNorm I = i}) by ext; simp]
-- 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
inst_5 : CharZero S
n : ℕ
⊢ Set.Finite.{u_1} (α := Ideal S) (⋃ i ∈ Set.Icc 0 n, {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = i})

Tactic:
Set.Finite.biUnion (Set.finite_Icc 0 n) (fun i _ => Ideal.finite_setOf_absNorm_eq i)

Premises used: Ideal.finite_setOf_absNorm_eq, Set.finite_Icc, Set.Finite.biUnion, OfNat.ofNat
-- 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
inst_5 : CharZero S
n : ℕ
⊢ Set.Finite.{u_1} (α := Ideal S) (⋃ i ∈ Set.Icc 0 n, {I : Ideal S | (absNorm : (a : Ideal S) → ℕ) I = i})

Tactic:
refine Set.Finite.biUnion (Set.finite_Icc 0 n) (fun i _ => Ideal.finite_setOf_absNorm_eq i)

Premises used: Ideal.finite_setOf_absNorm_eq, Set.finite_Icc, Set.Finite.biUnion, OfNat.ofNat
-- 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
inst_5 : CharZero S
n : ℕ
⊢ Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }

Tactic:
have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
-- 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
inst_5 : CharZero S
n : ℕ
this :
  Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
⊢ Set.Finite.{u_1} (α := ↥(Ideal S)⁰) {I : ↥(Ideal S)⁰ | (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n}

Tactic:
Finite.of_equiv _ (Equiv.subtypeSubtypeEquivSubtypeInter _ (fun I ↦ absNorm I ≤ n)).symm

Premises used: Finite.of_equiv, Ideal.absNorm, Set.Finite, LE.le, Equiv.subtypeSubtypeEquivSubtypeInter, Equiv.symm, DFunLike.coe
-- 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
inst_5 : CharZero S
n : ℕ
this :
  Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
⊢ Set.Finite.{u_1} (α := ↥(Ideal S)⁰) {I : ↥(Ideal S)⁰ | (absNorm : (a : Ideal S) → ℕ) (↑I : Ideal S) ≤ n}

Tactic:
exact Finite.of_equiv _ (Equiv.subtypeSubtypeEquivSubtypeInter _ (fun I ↦ absNorm I ≤ n)).symm

Premises used: Finite.of_equiv, Ideal.absNorm, LE.le, Equiv.subtypeSubtypeEquivSubtypeInter, Equiv.symm, DFunLike.coe
-- 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
⊢ Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }

Tactic:
have : Finite {I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
-- 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
this :
  Finite.{max 1 (u_1 + 1)}
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }
⊢ Finite.{max 1 (u_1 + 1)} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }

Tactic:
have : Finite {I : Ideal S // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n} :=
    (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
-- 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
this_1 :
  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 }
rw :
  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
⊢ 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:
rw [Nat.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ I ∈ (Ideal S)⁰)
    (fun I ↦ absNorm I ≤ n))]

Premises used: Ideal.absNorm, Membership.mem, nonZeroDivisors, LE.le, Ideal, Nat.card_congr, Equiv.subtypeSubtypeEquivSubtypeInter, DFunLike.coe
-- 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
this_1 :
  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 }
refine_1 :
  ∀ (x : Ideal S),
    (absNorm : (a : Ideal S) → ℕ) x ≤ n ↔
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n
refine_2 :
  Disjoint.{u_1} (α := Ideal S → Prop)
    (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
    fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n
⊢ { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
    { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
      { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n }

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

Premises used: Equiv.trans, subtypeOrEquiv, Equiv.subtypeEquivRight
-- 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
this_1 :
  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 }
x : Ideal S
refine_1 :
  (absNorm : (a : Ideal S) → ℕ) x ≤ n ↔
    (Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∨ x ∉ (Ideal S)⁰) ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n
refine_1₁ : (absNorm : (a : Ideal S) → ℕ) x ≤ n ↔ True ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n
⊢ (absNorm : (a : Ideal S) → ℕ) x ≤ n ↔
    Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
      x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n

Tactic:
simp_rw [← or_and_right, em, true_and]

Premises used: em, or_and_right, true_and
-- 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
this_1 :
  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 }
I : Ideal S
tauto :
  Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I →
    (absNorm : (a : Ideal S) → ℕ) I ≤ n → I ∉ (Ideal S)⁰ → (absNorm : (a : Ideal S) → ℕ) I ≤ n → False
⊢ ¬((Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ∧
      I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)

Tactic:
tauto
-- 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
this_1 :
  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 }
⊢ Disjoint.{u_1} (α := Ideal S → Prop)
    (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
    fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n

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

Premises used: Iff.mpr, Prop.disjoint_iff, Pi.disjoint_iff
-- 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
this_1 :
  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 }
e : { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
  { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
    { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } :=
  Equiv.trans
    (Equiv.subtypeEquivRight (p := fun (I : Ideal S) ↦ (absNorm : (a : Ideal S) → ℕ) I ≤ n) (q := fun (x : Ideal S) ↦
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n)
      ⋯)
    (subtypeOrEquiv
      (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
      (fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ⋯)
simp_rw : Nat.card.{u_1} { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } = 1
⊢ 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

Tactic:
simp_rw [Nat.card_congr e, Nat.card_sum, add_right_inj]

Premises used: Nat.card_sum, Nat.card_congr, add_right_inj
-- 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
this_1 :
  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 }
e : { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
  { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
    { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } :=
  Equiv.trans
    (Equiv.subtypeEquivRight (p := fun (I : Ideal S) ↦ (absNorm : (a : Ideal S) → ℕ) I ≤ n) (q := fun (x : Ideal S) ↦
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n)
      ⋯)
    (subtypeOrEquiv
      (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
      (fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ⋯)
h : ∀ (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 }

Tactic:
enter [1, 1, I]
-- 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
this_1 :
  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 }
e : { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
  { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
    { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } :=
  Equiv.trans
    (Equiv.subtypeEquivRight (p := fun (I : Ideal S) ↦ (absNorm : (a : Ideal S) → ℕ) I ≤ n) (q := fun (x : Ideal S) ↦
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n)
      ⋯)
    (subtypeOrEquiv
      (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
      (fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ⋯)
I : Ideal S
h : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
rw : 0 ≤ n
⊢ (absNorm : (a : Ideal S) → ℕ) I ≤ n

Tactic:
rw [h]
-- 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
this_1 :
  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 }
e : { I : Ideal S // (absNorm : (a : Ideal S) → ℕ) I ≤ n } ≃
  { I : Ideal S // Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } ⊕
    { I : Ideal S // I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n } :=
  Equiv.trans
    (Equiv.subtypeEquivRight (p := fun (I : Ideal S) ↦ (absNorm : (a : Ideal S) → ℕ) I ≤ n) (q := fun (x : Ideal S) ↦
      Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n ∨
        x ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) x ≤ n)
      ⋯)
    (subtypeOrEquiv
      (fun (I : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n)
      (fun (I : Ideal S) ↦ I ∉ (Ideal S)⁰ ∧ (absNorm : (a : Ideal S) → ℕ) I ≤ n) ⋯)
I : Ideal S
h : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ)
⊢ 0 ≤ n

Tactic:
Nat.zero_le n

Premises used: Nat.zero_le