awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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⟧
have succ : Eq (α := S ⧸ P)
  ((fun (c' : ↥(map (mkQ (P ^ i.succ)) (P ^ i))) ↦
      (Quotient.mk'' (f (k (↑c' : S ⧸ P ^ i.succ) sorry) sorry) : 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: refine ⟨⟨_, hd'⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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)
⊢ 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⟧
have succ : f (k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) sorry) sorry - d ∈ P
Tactic: simp only [Submodule.Quotient.mk''_eq_mk, Ideal.Quotient.mk_eq_mk, Ideal.Quotient.eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
have succ : a * f (k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) sorry) sorry +
      g (k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) hd') sorry -
    (a * d + 0) ∈
  P ^ (i + 1)
Tactic: refine
      Ideal.mul_add_mem_pow_succ_unique hP a _ _ _ _ a_notMem (hg _ (hk_mem _ hd')) (zero_mem _) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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 * 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)
have succ : k ((mkQ (P ^ i.succ) : (a : S) → S ⧸ P ^ i.succ) (a * d)) sorry - a * d ∈ P ^ (i + 1)
Tactic: rw [hf, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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
⊢ 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
have this : Infinite S
Tactic: haveI : Infinite S := Infinite.of_surjective _ b.repr.toEquiv.surjective
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) 0 = 0
have this : Infinite S
Tactic: have : Infinite S := Module.Free.infinite ℤ S
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
this : Infinite S
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) 0 = 0
have rw : cardQuot.{u_1, u_1} (R := S) (M := S) ⊥ = 0
Tactic: rw [Ideal.zero_eq_bot, cardQuot_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) 0 = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [Ideal.zero_eq_bot, cardQuot_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) 1 = 1
have rw : cardQuot.{u_1, u_1} (R := S) (M := S) ⊤ = 1
Tactic: rw [Ideal.one_eq_top, cardQuot_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ cardQuot.{u_1, u_1} (R := S) (M := S) 1 = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [Ideal.one_eq_top, cardQuot_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I J : Ideal 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
have 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
Tactic: rw [cardQuot_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) ⊥ : ℕ) (0 : ℕ)
have rw : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) 0 : ℕ) (0 : ℕ)
Tactic: rw [← Ideal.zero_eq_bot, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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 : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) ⊥ : ℕ) (0 : ℕ)
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [← Ideal.zero_eq_bot, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) ⊤ : ℕ) (1 : ℕ)
have rw : Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) 1 : ℕ) (1 : ℕ)
Tactic: rw [← Ideal.one_eq_top, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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 : ℕ)
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) ⊤ : ℕ) (1 : ℕ)
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [← Ideal.one_eq_top, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
Goal:
S : Type u_1
inst : CommRing S
inst_1 : Nontrivial S
inst_2 : IsDedekindDomain S
inst_3 : Free ℤ S
I : Ideal S
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (1 : ℕ) ↔ I = ⊤
have rw : cardQuot.{u_1, u_1} (R := S) (M := S) I = 1 ↔ I = ⊤
Tactic: rw [absNorm_apply, cardQuot_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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 = ⊤
⊢ Eq (α := ℕ) ((absNorm : (a : Ideal S) → ℕ) I : ℕ) (1 : ℕ) ↔ I = ⊤
have rw₁ : I = ⊤ ↔ I = ⊤
Tactic: rw [absNorm_apply, cardQuot_eq_one_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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) : S) ∈ I
have rw : (↑(cardQuot.{u_1, u_1} (R := S) (M := S) I) : S) ∈ I
Tactic: rw [absNorm_apply, cardQuot, ← Ideal.Quotient.eq_zero_iff_mem, map_natCast,
    Quotient.index_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ (↑((absNorm : (a : Ideal S) → ℕ) I) : S) ∈ I
have rw₁ : (↑(AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I)) : S) ∈ I
Tactic: rw [absNorm_apply, cardQuot, ← Ideal.Quotient.eq_zero_iff_mem, map_natCast,
    Quotient.index_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ (↑((absNorm : (a : Ideal S) → ℕ) I) : S) ∈ I
have rw₂ : Eq (α := S ⧸ I) ((Quotient.mk I : (a : S) → S ⧸ I) (↑(AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I)) : S)) 0
Tactic: rw [absNorm_apply, cardQuot, ← Ideal.Quotient.eq_zero_iff_mem, map_natCast,
    Quotient.index_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ (↑((absNorm : (a : Ideal S) → ℕ) I) : S) ∈ I
have rw₃ : Eq.{u_1 + 1} (α := S ⧸ I) (↑(AddSubgroup.index.{u_1} (G := S) (toAddSubgroup I)) : S ⧸ I) 0
Tactic: rw [absNorm_apply, cardQuot, ← Ideal.Quotient.eq_zero_iff_mem, map_natCast,
    Quotient.index_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
⊢ (↑((absNorm : (a : Ideal S) → ℕ) I) : S) ∈ I
have rw₄ : Eq.{u_1 + 1} (α := S ⧸ I) 0 0
Tactic: rw [absNorm_apply, cardQuot, ← Ideal.Quotient.eq_zero_iff_mem, map_natCast,
    Quotient.index_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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) : ℤ)})
have rwa : Prime (M := ℤ) (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)
Tactic: rwa [Ideal.span_singleton_prime (Int.ofNat_ne_zero.mpr hI.ne_zero), ← Nat.prime_iff_prime_int]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (hypothesis)
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)
⊢ Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (comap (F := ℤ →+* S) (algebraMap ℤ S) I)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
⊢ Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (comap (F := ℤ →+* S) (algebraMap ℤ S) I)
have hJ : Ne (α := Ideal ℤ) (comap (F := ℤ →+* S) (algebraMap ℤ S) I) ⊤
Tactic: apply (this.isMaximal _).eq_of_le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
hJ : Ne (α := Ideal ℤ) (comap (F := ℤ →+* S) (algebraMap ℤ S) I) ⊤
⊢ Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (comap (F := ℤ →+* S) (algebraMap ℤ S) I)
have IJ : LE.le (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (comap (F := ℤ →+* S) (algebraMap ℤ S) I)
Tactic: apply (this.isMaximal _).eq_of_le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
hJ : Ne (α := Ideal ℤ) (comap (F := ℤ →+* S) (algebraMap ℤ S) I) ⊤
IJ : LE.le (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (comap (F := ℤ →+* S) (algebraMap ℤ S) I)
⊢ Eq (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (comap (F := ℤ →+* S) (algebraMap ℤ S) I)
have apply : Ne (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) ⊥
Tactic: apply (this.isMaximal _).eq_of_le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
⊢ LE.le (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) (comap (F := ℤ →+* S) (algebraMap ℤ S) I)
have IJ : (↑((absNorm : (a : Ideal S) → ℕ) I) : S) ∈ I
Tactic: rw [span_singleton_le_iff_mem, mem_comap, algebraMap_int_eq, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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)
this : IsPrime (α := ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)})
⊢ Ne (α := Ideal ℤ) (span {(↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ)}) ⊥
have rw : ¬Eq (α := ℤ) (↑((absNorm : (a : Ideal S) → ℕ) I) : ℤ) 0
Tactic: rw [Ne, span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
I : Ideal S
E : Type u_2
inst_5 : EquivLike E S ↥I
inst_6 : AddEquivClass E S ↥I
e : E
⊢ Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module ℤ M] →
                          [inst_11 : Module ℤ M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype I) ∘ₗ
          AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
    (absNorm : (a : Ideal S) → ℕ) I
have pos : ∀ (hI : I = ⊥),
  Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module ℤ M] →
                          [inst_11 : Module ℤ M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype I) ∘ₗ
          AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
    (absNorm : (a : Ideal S) → ℕ) I
Tactic: by_cases hI : I = ⊥
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.AbsNorm (goal)
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
I : Ideal S
E : Type u_2
inst_5 : EquivLike E S ↥I
inst_6 : AddEquivClass E S ↥I
e : E
pos :
  ∀ (hI : I = ⊥),
    Int.natAbs
        ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
          ((↑ℤ :
                {S M M₂ : Type u_1} →
                  [inst : Semiring ℤ] →
                    [inst_7 : Semiring S] →
                      [inst_8 : AddCommMonoid M] →
                        [inst_9 : AddCommMonoid M₂] →
                          [inst_10 : Module ℤ M] →
                            [inst_11 : Module ℤ M₂] →
                              [inst_12 : Module S M] →
                                [inst_13 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
              (Submodule.subtype I) ∘ₗ
            AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
      (absNorm : (a : Ideal S) → ℕ) I
⊢ Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module ℤ M] →
                          [inst_11 : Module ℤ M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype I) ∘ₗ
          AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
    (absNorm : (a : Ideal S) → ℕ) I
have neg : ∀ (hI : ¬I = ⊥),
  Int.natAbs
      ((LinearMap.det : (a : S →ₗ[ℤ] S) → ℤ)
        ((↑ℤ :
              {S M M₂ : Type u_1} →
                [inst : Semiring ℤ] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module ℤ M] →
                          [inst_11 : Module ℤ M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ ℤ S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[ℤ] M₂)
            (Submodule.subtype I) ∘ₗ
          AddMonoidHom.toIntLinearMap (↑e : S →+ ↥I))) =
    (absNorm : (a : Ideal S) → ℕ) I
Tactic: by_cases hI : I = ⊥