awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot.{u_1, u_1} (R := S) (M := S) (P ^ i) = cardQuot.{u_1, u_1} (R := S) (M := S) P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → (hc : c ∈ P ^ i) → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k :
  (c' : S ⧸ P ^ i.succ) →
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c') → S
hk_mem :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'),
    (mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (k c' hc') = c'
d : S
⊢ Membership.mem (α := S ⧸ P ^ i.succ) (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i))
    ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d) : S ⧸ P ^ i.succ)

Tactic:
have hd' := (mem_map (f := mkQ (P ^ i.succ))).mpr ⟨a * d, Ideal.mul_mem_right d _ a_mem, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot.{u_1, u_1} (R := S) (M := S) (P ^ i) = cardQuot.{u_1, u_1} (R := S) (M := S) P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → (hc : c ∈ P ^ i) → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k :
  (c' : S ⧸ P ^ i.succ) →
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c') → S
hk_mem :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'),
    (mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (k c' hc') = c'
d : S
hd' :
  Membership.mem (α := S ⧸ P ^ i.succ) (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i))
    ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d) : S ⧸ P ^ i.succ)
⊢ ∃ (a : ↥(map (mkQ (P ^ i.succ)) (P ^ i))),
    Eq (α := S ⧸ P)
      ((fun (c' : ↥(map (mkQ (P ^ i.succ)) (P ^ i))) ↦
          (Quotient.mk'' (f (k (↑c' : S ⧸ P ^ i.succ) ⋯) ⋯) : Quotient (α := S) (quotientRel (R := S) P)))
        a)
      ⟦d⟧

Tactic:
⟨⟨_, hd'⟩, ?_⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot.{u_1, u_1} (R := S) (M := S) (P ^ i) = cardQuot.{u_1, u_1} (R := S) (M := S) P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → (hc : c ∈ P ^ i) → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k :
  (c' : S ⧸ P ^ i.succ) →
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c') → S
hk_mem :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'),
    (mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (k c' hc') = c'
d : S
hd' :
  Membership.mem (α := S ⧸ P ^ i.succ) (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i))
    ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d) : S ⧸ P ^ i.succ)
succ :
  Eq (α := S ⧸ P)
    ((fun (c' : ↥(map (mkQ (P ^ i.succ)) (P ^ i))) ↦
        (Quotient.mk'' (f (k (↑c' : S ⧸ P ^ i.succ) ⋯) ⋯) : Quotient (α := S) (quotientRel (R := S) P)))
      (Subtype.mk (p := fun (x : S ⧸ P ^ i.succ) ↦
        Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) x)
        ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) hd'))
    ⟦d⟧
⊢ ∃ (a : ↥(map (mkQ (P ^ i.succ)) (P ^ i))),
    Eq (α := S ⧸ P)
      ((fun (c' : ↥(map (mkQ (P ^ i.succ)) (P ^ i))) ↦
          (Quotient.mk'' (f (k (↑c' : S ⧸ P ^ i.succ) ⋯) ⋯) : Quotient (α := S) (quotientRel (R := S) P)))
        a)
      ⟦d⟧

Tactic:
refine ⟨⟨_, hd'⟩, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot.{u_1, u_1} (R := S) (M := S) (P ^ i) = cardQuot.{u_1, u_1} (R := S) (M := S) P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → (hc : c ∈ P ^ i) → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k :
  (c' : S ⧸ P ^ i.succ) →
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c') → S
hk_mem :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'),
    (mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (k c' hc') = c'
d : S
hd' :
  Membership.mem (α := S ⧸ P ^ i.succ) (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i))
    ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d) : S ⧸ P ^ i.succ)
succ : f (k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) ⋯) ⋯ - d ∈ P
⊢ Eq (α := S ⧸ P)
    ((fun (c' : ↥(map (mkQ (P ^ i.succ)) (P ^ i))) ↦
        (Quotient.mk'' (f (k (↑c' : S ⧸ P ^ i.succ) ⋯) ⋯) : Quotient (α := S) (quotientRel (R := S) P)))
      (Subtype.mk (p := fun (x : S ⧸ P ^ i.succ) ↦
        Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) x)
        ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) hd'))
    ⟦d⟧

Tactic:
simp only [Submodule.Quotient.mk''_eq_mk, Ideal.Quotient.mk_eq_mk, Ideal.Quotient.eq]

Premises used: Ideal.Quotient.eq, Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk''_eq_mk
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot.{u_1, u_1} (R := S) (M := S) (P ^ i) = cardQuot.{u_1, u_1} (R := S) (M := S) P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → (hc : c ∈ P ^ i) → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k :
  (c' : S ⧸ P ^ i.succ) →
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c') → S
hk_mem :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'),
    (mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (k c' hc') = c'
d : S
hd' :
  Membership.mem (α := S ⧸ P ^ i.succ) (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i))
    ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d) : S ⧸ P ^ i.succ)
⊢ f (k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) ⋯) ⋯ - d ∈ P

Tactic:
Ideal.mul_add_mem_pow_succ_unique hP a _ _ _ _ a_notMem (hg _ (hk_mem _ hd')) (zero_mem _) ?_

Premises used: Set.Mem, Ideal.mul_add_mem_pow_succ_unique, ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot.{u_1, u_1} (R := S) (M := S) (P ^ i) = cardQuot.{u_1, u_1} (R := S) (M := S) P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → (hc : c ∈ P ^ i) → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k :
  (c' : S ⧸ P ^ i.succ) →
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c') → S
hk_mem :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'),
    (mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (k c' hc') = c'
d : S
hd' :
  Membership.mem (α := S ⧸ P ^ i.succ) (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i))
    ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d) : S ⧸ P ^ i.succ)
succ :
  a * f (k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) ⋯) ⋯ +
        g (k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) hd') ⋯ -
      (a * d + 0) ∈
    P ^ (i + 1)
⊢ f (k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) ⋯) ⋯ - d ∈ P

Tactic:
refine
      Ideal.mul_add_mem_pow_succ_unique hP a _ _ _ _ a_notMem (hg _ (hk_mem _ hd')) (zero_mem _) ?_

Premises used: Ideal.mul_add_mem_pow_succ_unique, ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot.{u_1, u_1} (R := S) (M := S) (P ^ i) = cardQuot.{u_1, u_1} (R := S) (M := S) P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → (hc : c ∈ P ^ i) → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k :
  (c' : S ⧸ P ^ i.succ) →
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c') → S
hk_mem :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'),
    (mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (k c' hc') = c'
d : S
hd' :
  Membership.mem (α := S ⧸ P ^ i.succ) (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i))
    ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d) : S ⧸ P ^ i.succ)
succ : k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) ⋯ - a * d ∈ P ^ (i + 1)
⊢ a * f (k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) ⋯) ⋯ +
        g (k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) hd') ⋯ -
      (a * d + 0) ∈
    P ^ (i + 1)

Tactic:
rw [hf, add_zero]

Premises used: add_zero
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot.{u_1, u_1} (R := S) (M := S) (P ^ i) = cardQuot.{u_1, u_1} (R := S) (M := S) P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → (hc : c ∈ P ^ i) → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k :
  (c' : S ⧸ P ^ i.succ) →
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c') → S
hk_mem :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'),
    (mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (k c' hc') = c'
d : S
hd' :
  Membership.mem (α := S ⧸ P ^ i.succ) (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i))
    ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d) : S ⧸ P ^ i.succ)
⊢ k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) ⋯ - a * d ∈ P ^ (i + 1)

Tactic:
(Submodule.Quotient.eq _).mp (hk_eq _ hd')

Premises used: Submodule.Quotient.eq, Set.Mem, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst_1 : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot.{u_1, u_1} (R := S) (M := S) (P ^ i) = cardQuot.{u_1, u_1} (R := S) (M := S) P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → (hc : c ∈ P ^ i) → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k :
  (c' : S ⧸ P ^ i.succ) →
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c') → S
hk_mem :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'), k c' hc' ∈ P ^ i
hk_eq :
  ∀ (c' : S ⧸ P ^ i.succ)
    (hc' : Membership.mem (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i)) c'),
    (mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (k c' hc') = c'
d : S
hd' :
  Membership.mem (α := S ⧸ P ^ i.succ) (γ := Submodule S (S ⧸ P ^ i.succ)) (map (mkQ (P ^ i.succ)) (P ^ i))
    ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d) : S ⧸ P ^ i.succ)
⊢ k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) ⋯ - a * d ∈ P ^ (i + 1)

Tactic:
exact (Submodule.Quotient.eq _).mp (hk_eq _ hd')

Premises used: Submodule.Quotient.eq, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Free ℤ S
I J : Ideal S
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
⊢ Infinite S

Tactic:
haveI : Infinite S := Infinite.of_surjective _ b.repr.toEquiv.surjective
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Free ℤ S
I_1 J_1 : Ideal S
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
this : Infinite S
I J : Submodule S S
hI : IsUnit J
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) (I * J) =
    cardQuot.{u_1, u_1} (R := S) (M := S) I * cardQuot.{u_1, u_1} (R := S) (M := S) J

Tactic:
simp [Ideal.isUnit_iff.mp hI, Ideal.mul_top]

Premises used: Ideal.isUnit_iff, Iff.mp, Ideal.mul_top
-- Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm
Goal:
S : Type u_1
inst : CommRing S
inst_1 : IsDedekindDomain S
inst_2 : Free ℤ S
I J : Ideal S
b : Basis (Free.ChooseBasisIndex ℤ S) ℤ S := Free.chooseBasis ℤ S
this : Infinite S
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) (I * J) =
    cardQuot.{u_1, u_1} (R := S) (M := S) I * cardQuot.{u_1, u_1} (R := S) (M := S) J

Tactic:
exact UniqueFactorizationMonoid.multiplicative_of_coprime cardQuot I J (cardQuot_bot _ _)
      (fun {I J} hI => by simp [Ideal.isUnit_iff.mp hI, Ideal.mul_top])
      (fun {I} i hI =>
        have : Ideal.IsPrime I := Ideal.isPrime_of_prime hI
        cardQuot_pow_of_prime hI.ne_zero)
      fun {I J} hIJ => cardQuot_mul_of_coprime <| Ideal.isCoprime_iff_sup_eq.mpr
        (Ideal.isUnit_iff.mp
          (hIJ (Ideal.dvd_iff_le.mpr le_sup_left) (Ideal.dvd_iff_le.mpr le_sup_right)))

Premises used: Iff.mpr, Ideal.dvd_iff_le, le_sup_left, le_sup_right, UniqueFactorizationMonoid.multiplicative_of_coprime, Submodule.cardQuot, cardQuot_pow_of_prime, Submodule.cardQuot_bot, Ideal.isUnit_iff, Prime.ne_zero, Iff.mp, Ideal.isPrime_of_prime, Ideal.isCoprime_iff_sup_eq, cardQuot_mul_of_coprime
-- 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
⊢ Infinite S

Tactic:
have : Infinite S := Module.Free.infinite ℤ S
-- 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
this : Infinite S
rw : cardQuot.{u_1, u_1} (R := S) (M := S) ⊥ = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) 0 = 0

Tactic:
rw [Ideal.zero_eq_bot, cardQuot_bot]

Premises used: Ideal.zero_eq_bot, Submodule.cardQuot_bot
-- 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
rw : cardQuot.{u_1, u_1} (R := S) (M := S) ⊤ = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) 1 = 1

Tactic:
rw [Ideal.one_eq_top, cardQuot_top]

Premises used: Ideal.one_eq_top, Submodule.cardQuot_top
-- 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
I J : Ideal S
rw rw₁ :
  cardQuot.{u_1, u_1} (R := S) (M := S) I * cardQuot.{u_1, u_1} (R := S) (M := S) J =
    cardQuot.{u_1, u_1} (R := S) (M := S) I * cardQuot.{u_1, u_1} (R := S) (M := S) J
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) (I * J) =
    cardQuot.{u_1, u_1} (R := S) (M := S) I * cardQuot.{u_1, u_1} (R := S) (M := S) J

Tactic:
rw [cardQuot_mul]

Premises used: cardQuot_mul
-- 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
I : Ideal S
⊢ (absNorm : (a : Ideal S) → ℕ) I = cardQuot.{u_1, u_1} (R := S) (M := S) I

Tactic:
rfl

Premises used: AddSubgroup.index, Nat.card, Submodule.cardQuot, ENat.toNat, WithTop.untopD, WithTop.recTopCoe, rfl
-- 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
I : Ideal S
⊢ (absNorm : (a : Ideal S) → ℕ) I = AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I)

Tactic:
rfl

Premises used: AddSubgroup.index, Nat.card, Submodule.cardQuot, ENat.toNat, WithTop.untopD, WithTop.recTopCoe, rfl
-- 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
rw : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) 0 : ℕ) (0 : ℕ)
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) ⊥ : ℕ) (0 : ℕ)

Tactic:
rw [← Ideal.zero_eq_bot, map_zero]

Premises used: map_zero, Ideal.zero_eq_bot
-- 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
rw : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) 1 : ℕ) (1 : ℕ)
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) ⊤ : ℕ) (1 : ℕ)

Tactic:
rw [← Ideal.one_eq_top, map_one]

Premises used: Ideal.one_eq_top, map_one
-- 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
I : Ideal S
rw : cardQuot.{u_1, u_1} (R := S) (M := S) I = 1 ↔ I = ⊤
rw₁ rw₂ : I = ⊤ ↔ I = ⊤
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (1 : ℕ) ↔ I = ⊤

Tactic:
rw [absNorm_apply, cardQuot_eq_one_iff]

Premises used: Ideal.absNorm_apply, Submodule.cardQuot_eq_one_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
I : Ideal S
⊢ Ne (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (0 : ℕ) ↔ Finite.{u_1 + 1} (S ⧸ I)

Tactic:
⟨fun h => Nat.finite_of_card_ne_zero h, fun h =>
    (@AddSubgroup.finiteIndex_of_finite_quotient _ _ _ h).index_ne_zero⟩

Premises used: Iff.intro, Nat.finite_of_card_ne_zero, AddSubgroup.FiniteIndex.index_ne_zero
-- 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
I J : Ideal S
h : J ≤ I
⊢ Dvd.dvd (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) ((absNorm : (a : Ideal S) → ℕ) J : ℕ)

Tactic:
map_dvd absNorm (dvd_iff_le.mpr h)

Premises used: Iff.mpr, Ideal.dvd_iff_le, Ideal.absNorm, map_dvd
-- 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
I : Ideal S
hI : Irreducible (M := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
h : IsUnit I
⊢ IsUnit (M := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)

Tactic:
simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using h

Premises used: Nat.isUnit_iff, Ideal.absNorm_eq_one_iff, Ideal.isUnit_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
a b : Ideal S
hI : Irreducible (M := ℕ) ((absNorm : (a : Ideal S) → ℕ) (a * b) : ℕ)
⊢ IsUnit a ∨ IsUnit b

Tactic:
simpa only [Ideal.isUnit_iff, Nat.isUnit_iff, absNorm_eq_one_iff] using
        hI.isUnit_or_isUnit (map_mul absNorm a b)

Premises used: Ideal.absNorm, map_mul, Nat.isUnit_iff, Irreducible.isUnit_or_isUnit, Ideal.absNorm_eq_one_iff, Ideal.isUnit_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
I : Ideal S
hI : Irreducible (M := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ)
⊢ I.IsPrime

Tactic:
isPrime_of_prime
    (UniqueFactorizationMonoid.irreducible_iff_prime.mp (irreducible_of_irreducible_absNorm hI))

Premises used: UniqueFactorizationMonoid.irreducible_iff_prime, Ideal.irreducible_of_irreducible_absNorm, Iff.mp, Ideal.isPrime_of_prime
-- 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
a : S
ha : a ≠ 0
hI : Irreducible (M := ℕ) ((absNorm : (a : Ideal S) → ℕ) (span {a}) : ℕ)
⊢ Prime a

Tactic:
(Ideal.span_singleton_prime ha).mp (isPrime_of_irreducible_absNorm hI)

Premises used: Ideal.isPrime_of_irreducible_absNorm, Iff.mp, Ideal.span_singleton_prime
-- 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
I : Ideal S
rw : (↑(cardQuot.{u_1, u_1} (R := S) (M := S) I) : S) ∈ I
rw₁ : (↑(AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I)) : S) ∈ I
rw₂ : Eq (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) (↑(AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I)) : S)) 0
rw₃ : Eq.{u_1 + 1} (α := S ⧸ I) (↑(AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I)) : S ⧸ I) 0
rw₄ rw₅ : Eq.{u_1 + 1} (α := S ⧸ I) 0 0
⊢ (↑((absNorm : (a : Ideal S) → ℕ) I) : S) ∈ I

Tactic:
rw [absNorm_apply, cardQuot, ← Ideal.Quotient.eq_zero_iff_mem, map_natCast,
    Quotient.index_eq_zero]

Premises used: Ideal.Quotient.index_eq_zero, Submodule.cardQuot, Ideal.Quotient.eq_zero_iff_mem, Ideal.absNorm_apply, map_natCast
-- 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
I : Ideal S
⊢ span {(↑((absNorm : (a : Ideal S) → ℕ) I) : S)} ≤ I

Tactic:
simp only [Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe, Ideal.absNorm_mem I]

Premises used: Ideal.span_le, Set.singleton_subset_iff, Ideal.absNorm_mem, SetLike.mem_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
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
rwa : Prime (M := ℤ) (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
rwa₁ rwa₂ rwa₃ rwa₄ : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
⊢ IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})

Tactic:
rwa [Ideal.span_singleton_prime (Int.ofNat_ne_zero.mpr hI.ne_zero), ← Nat.prime_iff_prime_int]

Premises used: Iff.mpr, Nat.prime_iff_prime_int, Int.ofNat_ne_zero, Nat.Prime.ne_zero, Ideal.span_singleton_prime
-- 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
I : Ideal S
hI : Nat.Prime ((absNorm : (a : Ideal S) → ℕ) I)
⊢ IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})

Tactic:
have : Ideal.IsPrime (Ideal.span (singleton (Ideal.absNorm I : ℤ))) := by
    rwa [Ideal.span_singleton_prime (Int.ofNat_ne_zero.mpr hI.ne_zero), ← Nat.prime_iff_prime_int]