awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : I ≠ 0 ∧ I' ≠ 0
pos : (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
pos₁ : count K v I + count K v I' = 0
pos₂ : 0 + count K v I' = 0
pos₃ : HAdd.hAdd (α := ℤ) 0 0 = 0
⊢ count K v (I * I') = 0
have pos₄ : Eq (α := ℤ) 0 0
Tactic: rw [count_mul' K v, if_pos h, hI, hI', add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : ¬(I ≠ 0 ∧ I' ≠ 0)
⊢ count K v (I * I') = 0
have neg : (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
Tactic: rw [count_mul' K v, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
h : ¬(I ≠ 0 ∧ I' ≠ 0)
neg : (if I ≠ 0 ∧ I' ≠ 0 then count K v I + count K v I' else 0) = 0
⊢ count K v (I * I') = 0
have neg₁ : Eq (α := ℤ) 0 0
Tactic: rw [count_mul' K v, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
⊢ count K v (I * I') = 0
have pos : ∀ (h : I ≠ 0 ∧ I' ≠ 0), count K v (I * I') = 0
Tactic: classical
    by_cases h : I ≠ 0 ∧ I' ≠ 0
    · rw [count_mul' K v, if_pos h, hI, hI', add_zero]
    · rw [count_mul' K v, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
I I' : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
pos : ∀ (h : I ≠ 0 ∧ I' ≠ 0), count K v (I * I') = 0
⊢ count K v (I * I') = 0
have neg : ∀ (h : ¬(I ≠ 0 ∧ I' ≠ 0)), count K v (I * I') = 0
Tactic: classical
    by_cases h : I ≠ 0 ∧ I' ≠ 0
    · rw [count_mul' K v, if_pos h, hI, hI', add_zero]
    · rw [count_mul' K v, if_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
w : HeightOneSpectrum R
hw : Membership.mem (γ := Set (HeightOneSpectrum R)) (fun (i : HeightOneSpectrum R) ↦ i = v → False) w
⊢ count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) (exps w)) = 0
have hp₂ : exps w * count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
Tactic: rw [count_zpow, count_maximal_coprime K v hw, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
w : HeightOneSpectrum R
hw : Membership.mem (γ := Set (HeightOneSpectrum R)) (fun (i : HeightOneSpectrum R) ↦ i = v → False) w
hp₂ : exps w * count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
⊢ count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) (exps w)) = 0
have hp₃ : exps w * 0 = 0
Tactic: rw [count_zpow, count_maximal_coprime K v hw, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
w : HeightOneSpectrum R
hw : Membership.mem (γ := Set (HeightOneSpectrum R)) (fun (i : HeightOneSpectrum R) ↦ i = v → False) w
hp₂ : exps w * count K v (↑w.asIdeal : FractionalIdeal R⁰ K) = 0
hp₃ : exps w * 0 = 0
⊢ count K v (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑w.asIdeal : FractionalIdeal R⁰ K) (exps w)) = 0
have hp₄ : Eq (α := ℤ) 0 0
Tactic: rw [count_zpow, count_maximal_coprime K v hw, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
⊢ count K v
      (exps.prod fun (x1 : HeightOneSpectrum R) (x2 : ℤ) ↦
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x1.asIdeal : FractionalIdeal R⁰ K) x2) =
    (exps : (a : HeightOneSpectrum R) → ℤ) v
have rw : Eq (α := ℤ)
  (∑ i ∈ exps.support,
      count K v
        (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
          ((exps : (a : HeightOneSpectrum R) → ℤ) i : ℤ)) :
    ℤ)
  ((exps : (a : HeightOneSpectrum R) → ℤ) v : ℤ)
Tactic: rw [Finsupp.prod, count_prod]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R →₀ ℤ
rw :
  Eq (α := ℤ)
    (∑ i ∈ exps.support,
        count K v
          (HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
            ((exps : (a : HeightOneSpectrum R) → ℤ) i : ℤ)) :
      ℤ)
    ((exps : (a : HeightOneSpectrum R) → ℤ) v : ℤ)
⊢ count K v
      (exps.prod fun (x1 : HeightOneSpectrum R) (x2 : ℤ) ↦
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x1.asIdeal : FractionalIdeal R⁰ K) x2) =
    (exps : (a : HeightOneSpectrum R) → ℤ) v
have hS : ∀ i ∈ exps.support,
  HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑i.asIdeal : FractionalIdeal R⁰ K)
      ((exps : (a : HeightOneSpectrum R) → ℤ) i : ℤ) ≠
    0
Tactic: rw [Finsupp.prod, count_prod]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ count K v
      (∏ᶠ (v : HeightOneSpectrum R),
        HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) (exps v)) =
    exps v
have h : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (∏ᶠ (v : HeightOneSpectrum R),
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) (exps v))
  (Finsupp.prod
    {
      support :=
        Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps,
      toFun := exps, mem_support_toFun := sorry }
    fun (x1 : HeightOneSpectrum R) (x2 : ℤ) ↦
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x1.asIdeal : FractionalIdeal R⁰ K) x2)
Tactic: convert! count_finsuppProd K v (Finsupp.mk h_exps.toFinset exps (fun _ ↦ h_exps.mem_toFinset))
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) (exps v))
    (Finsupp.prod
      {
        support :=
          Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps,
        toFun := exps, mem_support_toFun := ⋯ }
      fun (x1 : HeightOneSpectrum R) (x2 : ℤ) ↦
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x1.asIdeal : FractionalIdeal R⁰ K) x2)
have h : Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
  (∏ i ∈ Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps,
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑i.asIdeal : FractionalIdeal R⁰ K) (exps i))
  (∏
    a ∈
      Finsupp.support
        {
          support :=
            Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps,
          toFun := exps, mem_support_toFun := sorry : HeightOneSpectrum R →₀ ℤ },
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑a.asIdeal : FractionalIdeal R⁰ K)
      (({
              support :=
                Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ)
                  h_exps,
              toFun := exps, mem_support_toFun := sorry } :
            (a : HeightOneSpectrum R) → ℤ)
          a :
        ℤ))
Tactic: rw [finprod_eq_finsetProd_of_mulSupport_subset (s := h_exps.toFinset), Finsupp.prod]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
h :
  Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ i ∈ Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps,
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑i.asIdeal : FractionalIdeal R⁰ K) (exps i))
    (∏
      a ∈
        Finsupp.support
          {
            support :=
              Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps,
            toFun := exps, mem_support_toFun := ⋯ : HeightOneSpectrum R →₀ ℤ },
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := ℤ) (↑a.asIdeal : FractionalIdeal R⁰ K)
        (({
                support :=
                  Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ)
                    h_exps,
                toFun := exps, mem_support_toFun := ⋯ } :
              (a : HeightOneSpectrum R) → ℤ)
            a :
          ℤ))
⊢ Eq.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (∏ᶠ (v : HeightOneSpectrum R),
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) (exps v))
    (Finsupp.prod
      {
        support :=
          Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps,
        toFun := exps, mem_support_toFun := ⋯ }
      fun (x1 : HeightOneSpectrum R) (x2 : ℤ) ↦
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑x1.asIdeal : FractionalIdeal R⁰ K) x2)
have h₁ : (mulSupport.{u_1, u_2} (M := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) fun (v : HeightOneSpectrum R) ↦
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) (exps v)) ⊆
  (↑(Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps) :
    Set (HeightOneSpectrum R))
Tactic: rw [finprod_eq_finsetProd_of_mulSupport_subset (s := h_exps.toFinset), Finsupp.prod]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport.{u_1, u_2} (M := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) fun (v : HeightOneSpectrum R) ↦
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) (exps v)) ⊆
    (↑(Finite.toFinset (s := {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ) h_exps) :
      Set (HeightOneSpectrum R))
have h : Subset.{u_1} (α := Set (HeightOneSpectrum R))
  (mulSupport.{u_1, u_2} (M := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) fun (v : HeightOneSpectrum R) ↦
    HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) (exps v))
  {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x}ᶜ
Tactic: rw [Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v_1 : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
v : HeightOneSpectrum R
hv :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    (mulSupport.{u_1, u_2} (M := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) fun (v : HeightOneSpectrum R) ↦
      HPow.hPow (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑v.asIdeal : FractionalIdeal R⁰ K) (exps v))
    v
h :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x} v
⊢ False
have hv₁ : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 1
Tactic: rw [mem_mulSupport, h, zpow_zero] at hv
Cleared hypotheses: hv, h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J ≠ 0
⊢ count K v (↑J : FractionalIdeal R⁰ K) =
    (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
have hI : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J : FractionalIdeal R⁰ K) 0
Tactic: rw [count_well_defined K (J := J) (a := 1), Ideal.span_singleton_one, sub_eq_self,
    Nat.cast_eq_zero, ← Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
    Associates.count_zero v.associates_irreducible]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J ≠ 0
hI : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J : FractionalIdeal R⁰ K) 0
⊢ count K v (↑J : FractionalIdeal R⁰ K) =
    (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
have h_aJ : (↑J : FractionalIdeal R⁰ K) =
  HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) 1)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
    ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
Tactic: rw [count_well_defined K (J := J) (a := 1), Ideal.span_singleton_one, sub_eq_self,
    Nat.cast_eq_zero, ← Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
    Associates.count_zero v.associates_irreducible]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
⊢ 0 ≤ count K v (↑J : FractionalIdeal R⁰ K)
have pos : ∀ (hJ : J = 0), 0 ≤ count K v (↑J : FractionalIdeal R⁰ K)
Tactic: by_cases hJ : J = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
pos : ∀ (hJ : J = 0), 0 ≤ count K v (↑J : FractionalIdeal R⁰ K)
⊢ 0 ≤ count K v (↑J : FractionalIdeal R⁰ K)
have neg : ∀ (hJ : ¬J = 0), 0 ≤ count K v (↑J : FractionalIdeal R⁰ K)
Tactic: by_cases hJ : J = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
h : I ≤ J
⊢ count K v J ≤ count K v I
have pos : ∀ (hJ : J = 0), count K v J ≤ count K v I
Tactic: by_cases hJ : J = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
h : I ≤ J
pos : ∀ (hJ : J = 0), count K v J ≤ count K v I
⊢ count K v J ≤ count K v I
have neg : ∀ (hJ : ¬J = 0), count K v J ≤ count K v I
Tactic: by_cases hJ : J = 0
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
⊢ count K v J ≤ count K v I
have this : J⁻¹ * I ≤ J⁻¹ * J
Tactic: have := mul_le_mul_right h J⁻¹
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
this : J⁻¹ * I ≤ J⁻¹ * J
⊢ count K v J ≤ count K v I
have this₁ : ∃ (I_1 : Ideal R), (↑I_1 : FractionalIdeal R⁰ K) = J⁻¹ * I
Tactic: rw [inv_mul_cancel₀ hJ, FractionalIdeal.le_one_iff_exists_coeIdeal] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
this : ∃ (I_1 : Ideal R), (↑I_1 : FractionalIdeal R⁰ K) = J⁻¹ * I
⊢ count K v J ≤ count K v I
have neg : ∀ (J' : Ideal R) (hJ' : (↑J' : FractionalIdeal R⁰ K) = J⁻¹ * I), count K v J ≤ count K v I
Tactic: obtain ⟨J', hJ'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : (↑J' : FractionalIdeal R⁰ K) = J⁻¹ * I
⊢ count K v J ≤ count K v I
have neg : 0 ≤ count K v (↑J' : FractionalIdeal R⁰ K)
Tactic: rw [← mul_inv_cancel_left₀ hJ I, ← hJ', count_mul K v hJ, le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
v : HeightOneSpectrum R
I J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
J' : Ideal R
hJ' : (↑J' : FractionalIdeal R⁰ K) = J⁻¹ * I
neg : 0 ≤ count K v (↑J' : FractionalIdeal R⁰ K)
⊢ count K v J ≤ count K v I
have neg₁ : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K) 0
Tactic: rw [← mul_inv_cancel_left₀ hJ I, ← hJ', count_mul K v hJ, le_add_iff_nonneg_right]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ) =
      0
have ha_ne_zero : Ne (α := Ideal R) (Ideal.span {a}) 0
Tactic: have ha_ne_zero : Ideal.span {a} ≠ 0 := constant_factor_ne_zero hI haJ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
ha_ne_zero : Ne (α := Ideal R) (Ideal.span {a}) 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
        (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ) =
      0
have hJ_ne_zero : J ≠ 0
Tactic: have hJ_ne_zero : J ≠ 0 := ideal_factor_ne_zero hI haJ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
inst_4 : IsDedekindDomain R
I : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ :
  I =
    HMul.hMul (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (β := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      (spanSingleton R⁰ ((algebraMap R K : (a : R) → K) a)⁻¹ : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
      ((↑J : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) : FractionalIdeal.{u_1, u_2} (R := R) R⁰ K)
ha_ne_zero : Ne (α := Ideal R) (Ideal.span {a}) 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    {v : HeightOneSpectrum R |
      ¬HSub.hSub (α := ℤ) (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)
            (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {a})))) : ℤ) =
          0}
    v
⊢ Membership.mem (γ := Set (HeightOneSpectrum R))
    ({v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪ {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}}) v
have hv_irred : Irreducible v.asIdeal
Tactic: have hv_irred : Irreducible v.asIdeal := v.irreducible