awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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 :
          ℤ))
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))
⊢ 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)

Tactic:
rw [finprod_eq_finsetProd_of_mulSupport_subset (s := h_exps.toFinset), Finsupp.prod]

Premises used: Finsupp.prod, finprod_eq_finsetProd_of_mulSupport_subset
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)
    (∏ 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 :
          ℤ))

Tactic:
rfl
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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 :
  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}ᶜ
⊢ (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 [Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 1

Tactic:
rw [mem_mulSupport, h, zpow_zero] at hv

Premises used: zpow_zero, Function.mem_mulSupport
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
hv₁ : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 1
⊢ Membership.mem (γ := Set (HeightOneSpectrum R))
    {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x} v

Tactic:
rw [mem_mulSupport, h, zpow_zero] at hv

Premises used: zpow_zero, Function.mem_mulSupport
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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 : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 1
h :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x} v
⊢ False

Tactic:
hv (Eq.refl 1)

Premises used: Eq.refl, OfNat.ofNat
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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 : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) 1 1
h :
  Membership.mem (γ := Set (HeightOneSpectrum R))
    {x : HeightOneSpectrum R | (fun (v : HeightOneSpectrum R) ↦ exps v = 0) x} v
⊢ False

Tactic:
exact hv (Eq.refl 1)

Premises used: Eq.refl, OfNat.ofNat
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
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)
⊢ count K v (↑J : FractionalIdeal R⁰ K) =
    (↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk J))) : ℤ)

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]

Premises used: Ideal.one_eq_top, FractionalIdeal.count_well_defined, Ideal.span_singleton_one, Associates.count_zero, Associates.mk_one, sub_eq_self, Nat.cast_eq_zero, Associates.factors_one, IsDedekindDomain.HeightOneSpectrum.associates_irreducible
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J : FractionalIdeal R⁰ K) 0

Tactic:
simpa only [ne_eq, coeIdeal_eq_zero]

Premises used: ne_eq, FractionalIdeal.coeIdeal_eq_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ (↑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:
simp only [map_one, inv_one, spanSingleton_one, one_mul]

Premises used: inv_one, map_one, FractionalIdeal.spanSingleton_one, one_mul
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)
neg : ∀ (hJ : ¬J = 0), 0 ≤ count K v (↑J : FractionalIdeal R⁰ K)
⊢ 0 ≤ count K v (↑J : FractionalIdeal R⁰ K)

Tactic:
by_cases hJ : J = 0
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ 0 ≤ count K v (↑J : FractionalIdeal R⁰ K)

Tactic:
simp only [hJ, Submodule.zero_eq_bot, coeIdeal_bot, count_zero, le_refl]

Premises used: le_refl, FractionalIdeal.coeIdeal_bot, FractionalIdeal.count_zero, Submodule.zero_eq_bot
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ 0 ≤ count K v (↑J : FractionalIdeal R⁰ K)

Tactic:
simp only [count_coe K v hJ, Nat.cast_nonneg]

Premises used: Nat.cast_nonneg, FractionalIdeal.count_coe
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ 0 ≤ count K v (↑J : FractionalIdeal R⁰ K)

Tactic:
classical simp only [count_coe K v hJ, Nat.cast_nonneg]

Premises used: Nat.cast_nonneg, FractionalIdeal.count_coe
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
neg : ∀ (hJ : ¬J = 0), count K v J ≤ count K v I
⊢ count K v J ≤ count K v I

Tactic:
by_cases hJ : J = 0
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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

Tactic:
(hI (FractionalIdeal.le_zero_iff.mp (h.trans hJ.le))).elim

Premises used: FractionalIdeal.le_zero_iff, False.elim, Eq.le, Iff.mp, LE.le.trans
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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

Tactic:
exact (hI (FractionalIdeal.le_zero_iff.mp (h.trans hJ.le))).elim

Premises used: FractionalIdeal.le_zero_iff, False.elim, Eq.le, Iff.mp, LE.le.trans
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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⁻¹ * I ≤ J⁻¹ * J

Tactic:
have := mul_le_mul_right h J⁻¹
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ ∃ (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

Premises used: FractionalIdeal.le_one_iff_exists_coeIdeal, inv_mul_cancel₀
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
neg : ∀ (J' : Ideal R) (hJ' : (↑J' : FractionalIdeal R⁰ K) = J⁻¹ * I), count K v J ≤ count K v I
⊢ count K v J ≤ count K v I

Tactic:
obtain ⟨J', hJ'⟩ := this
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)
neg₁ : Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K) 0
⊢ count K v J ≤ count K v I

Tactic:
rw [← mul_inv_cancel_left₀ hJ I, ← hJ', count_mul K v hJ, le_add_iff_nonneg_right]

Premises used: le_add_iff_nonneg_right, mul_inv_cancel_left₀, FractionalIdeal.count_mul
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ 0 ≤ count K v (↑J' : FractionalIdeal R⁰ K)

Tactic:
count_coe_nonneg K v J'

Premises used: FractionalIdeal.count_coe_nonneg
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ 0 ≤ count K v (↑J' : FractionalIdeal R⁰ K)

Tactic:
exact count_coe_nonneg K v J'

Premises used: FractionalIdeal.count_coe_nonneg
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K) 0

Tactic:
hJ' ▸ mul_ne_zero (inv_ne_zero hJ) hI

Premises used: Eq.rec, inv_ne_zero, mul_ne_zero, Eq.symm
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ Ne.{u_2 + 1} (α := FractionalIdeal.{u_1, u_2} (R := R) R⁰ K) (↑J' : FractionalIdeal R⁰ K) 0

Tactic:
exact hJ' ▸ mul_ne_zero (inv_ne_zero hJ) hI
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)
⊢ Ne (α := Ideal R) (Ideal.span {a}) 0

Tactic:
have ha_ne_zero : Ideal.span {a} ≠ 0 := constant_factor_ne_zero hI haJ
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ J ≠ 0

Tactic:
have hJ_ne_zero : J ≠ 0 := ideal_factor_ne_zero hI haJ
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
⊢ Irreducible v.asIdeal

Tactic:
have hv_irred : Irreducible v.asIdeal := v.irreducible
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
hv_irred : Irreducible v.asIdeal
by_contra :
  ∀
    (h_notMem :
      ¬Membership.mem (γ := Set (HeightOneSpectrum R))
          ({v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪ {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}}) v),
    False
⊢ Membership.mem (γ := Set (HeightOneSpectrum R))
    ({v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪ {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}}) v

Tactic:
by_contra h_notMem
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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
hv_irred : Irreducible v.asIdeal
h_notMem :
  ¬Membership.mem (γ := Set (HeightOneSpectrum R))
      ({v : HeightOneSpectrum R | v.asIdeal ∣ J} ∪ {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {a}}) v
⊢ ¬(v.asIdeal ∣ J ∨ v.asIdeal ∣ Ideal.span {a})

Tactic:
rw [mem_union, mem_setOf_eq, mem_setOf_eq] at h_notMem

Premises used: Set.mem_union, Set.mem_setOf_eq