awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ count p.asIdeal (normalizedFactors (normalizedFactors I ∩ normalizedFactors J).prod) =
    min (count p.asIdeal (normalizedFactors I)) (count p.asIdeal (normalizedFactors J))
have rw : count p.asIdeal (normalizedFactors I ∩ normalizedFactors J) =
  min (count p.asIdeal (normalizedFactors I)) (count p.asIdeal (normalizedFactors J))
Tactic: rw [normalizedFactors_prod_inter_eq_inter]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
have inl : emultiplicity p.asIdeal (⊥ ⊔ J) = min (emultiplicity p.asIdeal ⊥) (emultiplicity p.asIdeal J)
Tactic: rcases eq_or_ne I ⊥ with rfl | hI
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
inl : emultiplicity p.asIdeal (⊥ ⊔ J) = min (emultiplicity p.asIdeal ⊥) (emultiplicity p.asIdeal J)
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
have inr : ∀ (hI : I ≠ ⊥), emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
Tactic: rcases eq_or_ne I ⊥ with rfl | hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
have inr : emultiplicity p.asIdeal (I ⊔ ⊥) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal ⊥)
Tactic: rcases eq_or_ne J ⊥ with rfl | hJ
Cleared hypotheses: J
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
inr : emultiplicity p.asIdeal (I ⊔ ⊥) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal ⊥)
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
have inr₁ : ∀ (hJ : J ≠ ⊥), emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
Tactic: rcases eq_or_ne J ⊥ with rfl | hJ
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
have this : I ⊔ J ≠ ⊥
Tactic: have : I ⊔ J ≠ ⊥ := by grind
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
have H : ∀ {I' : Ideal R} (h : I' ≠ ⊥), FiniteMultiplicity p.asIdeal I'
Tactic: have H {I' : Ideal R} (h : I' ≠ ⊥) : FiniteMultiplicity p.asIdeal I' :=
    FiniteMultiplicity.of_prime_left (prime p) h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : I ⊔ J ≠ ⊥
H : ∀ {I' : Ideal R} (h : I' ≠ ⊥), FiniteMultiplicity p.asIdeal I'
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
have inr : Eq (α := ℕ∞) (↑(min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)) : ℕ∞)
  (min (↑(multiplicity p.asIdeal I) : ℕ∞) (↑(multiplicity p.asIdeal J) : ℕ∞))
Tactic: rw [(H this).emultiplicity_eq_multiplicity, (H hI).emultiplicity_eq_multiplicity,
    (H hJ).emultiplicity_eq_multiplicity, multiplicity_sup _ hI hJ]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
I : PEmpty.{u_4 + 1} → Ideal R
⊢ emultiplicity p.asIdeal (⨆ (i : PEmpty.{u_4 + 1}), I i) = ⨅ (i : PEmpty.{u_4 + 1}), emultiplicity p.asIdeal (I i)
have h_empty : emultiplicity p.asIdeal ⊥ = ⊤
Tactic: rw [iSup_of_empty, iInf_of_empty]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α β : Type u_4
e : α ≃ β
ih : ∀ (I : α → Ideal R), emultiplicity p.asIdeal (⨆ (i : α), I i) = ⨅ (i : α), emultiplicity p.asIdeal (I i)
I : β → Ideal R
⊢ emultiplicity p.asIdeal (⨆ (i : β), I i) = ⨅ (i : β), emultiplicity p.asIdeal (I i)
have ih₁ : emultiplicity p.asIdeal (⨆ (i : α), (I ∘ (⇑e : (a : α) → β)) i) =
  ⨅ (i : α), emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i)
Tactic: specialize ih (I ∘ e)
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α β : Type u_4
e : α ≃ β
I : β → Ideal R
ih :
  emultiplicity p.asIdeal (⨆ (i : α), (I ∘ (⇑e : (a : α) → β)) i) =
    ⨅ (i : α), emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i)
⊢ emultiplicity p.asIdeal (⨆ (i : β), I i) = ⨅ (i : β), emultiplicity p.asIdeal (I i)
have ih₁ : emultiplicity p.asIdeal (sSup (range fun (i : α) ↦ (I ∘ (⇑e : (a : α) → β)) i)) =
  sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i))
Tactic: rw [← sSup_range, ← sInf_range] at ih ⊢
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α β : Type u_4
e : α ≃ β
I : β → Ideal R
ih :
  emultiplicity p.asIdeal (sSup (range fun (i : α) ↦ (I ∘ (⇑e : (a : α) → β)) i)) =
    sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i))
⊢ emultiplicity p.asIdeal (sSup (range fun (i : β) ↦ I i)) = sInf (range fun (i : β) ↦ emultiplicity p.asIdeal (I i))
have ih₁ : emultiplicity p.asIdeal (sSup (range I)) =
  sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i))
Tactic: rw [EquivLike.range_comp I e] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α β : Type u_4
e : α ≃ β
I : β → Ideal R
ih :
  emultiplicity p.asIdeal (sSup (range I)) =
    sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i))
⊢ emultiplicity p.asIdeal (sSup (range fun (i : β) ↦ I i)) = sInf (range fun (i : β) ↦ emultiplicity p.asIdeal (I i))
have of_equiv : Eq (α := ℕ∞) (sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i)))
  (sInf (range fun (i : β) ↦ emultiplicity p.asIdeal (I i)))
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α : Type u_4
inst_3 : Fintype α
ih : ∀ (I : α → Ideal R), emultiplicity p.asIdeal (⨆ (i : α), I i) = ⨅ (i : α), emultiplicity p.asIdeal (I i)
I : Option α → Ideal R
⊢ emultiplicity p.asIdeal (⨆ (i : Option α), I i) = ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
have h_option : emultiplicity p.asIdeal (I none ⊔ ⨆ (b : α), I (some b)) = ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
Tactic: rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α : Type u_4
inst_3 : Fintype α
ih : ∀ (I : α → Ideal R), emultiplicity p.asIdeal (⨆ (i : α), I i) = ⨅ (i : α), emultiplicity p.asIdeal (I i)
I : Option α → Ideal R
h_option : emultiplicity p.asIdeal (I none ⊔ ⨆ (b : α), I (some b)) = ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
⊢ emultiplicity p.asIdeal (⨆ (i : Option α), I i) = ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
have h_option₁ : min (emultiplicity p.asIdeal (I none)) (emultiplicity p.asIdeal (⨆ (b : α), I (some b))) =
  ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
Tactic: rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α : Type u_4
inst_3 : Fintype α
ih : ∀ (I : α → Ideal R), emultiplicity p.asIdeal (⨆ (i : α), I i) = ⨅ (i : α), emultiplicity p.asIdeal (I i)
I : Option α → Ideal R
h_option : emultiplicity p.asIdeal (I none ⊔ ⨆ (b : α), I (some b)) = ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
h_option₁ :
  min (emultiplicity p.asIdeal (I none)) (emultiplicity p.asIdeal (⨆ (b : α), I (some b))) =
    ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
⊢ emultiplicity p.asIdeal (⨆ (i : Option α), I i) = ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
have h_option₂ : min (emultiplicity p.asIdeal (I none)) (⨅ (i : α), emultiplicity p.asIdeal (I (some i))) =
  ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
Tactic: rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
α : Type u_4
inst_3 : Fintype α
ih : ∀ (I : α → Ideal R), emultiplicity p.asIdeal (⨆ (i : α), I i) = ⨅ (i : α), emultiplicity p.asIdeal (I i)
I : Option α → Ideal R
h_option : emultiplicity p.asIdeal (I none ⊔ ⨆ (b : α), I (some b)) = ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
h_option₁ :
  min (emultiplicity p.asIdeal (I none)) (emultiplicity p.asIdeal (⨆ (b : α), I (some b))) =
    ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
h_option₂ :
  min (emultiplicity p.asIdeal (I none)) (⨅ (i : α), emultiplicity p.asIdeal (I (some i))) =
    ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
⊢ emultiplicity p.asIdeal (⨆ (i : Option α), I i) = ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
have h_option₃ : min (emultiplicity p.asIdeal (I none)) (⨅ (i : α), emultiplicity p.asIdeal (I (some i))) =
  min (emultiplicity p.asIdeal (I none)) (⨅ (b : α), emultiplicity p.asIdeal (I (some b)))
Tactic: rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
I : ι → Ideal R
⊢ emultiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), emultiplicity p.asIdeal (I i)
have h_empty : ∀ (I : PEmpty.{u_4 + 1} → Ideal R),
  emultiplicity p.asIdeal (⨆ (i : PEmpty.{u_4 + 1}), I i) = ⨅ (i : PEmpty.{u_4 + 1}), emultiplicity p.asIdeal (I i)
Tactic: induction ι using Finite.induction_empty_option with
  | h_empty =>
    rw [iSup_of_empty, iInf_of_empty]
    exact emultiplicity_zero _
  | of_equiv e ih =>
    specialize ih (I ∘ e)
    rw [← sSup_range, ← sInf_range] at ih ⊢
    rw [EquivLike.range_comp I e] at ih
    rw [ih]
    exact congrArg _ <| EquivLike.range_comp (emultiplicity p.asIdeal <| I ·) e
  | h_option ih =>
    rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
I : ι → Ideal R
h_empty :
  ∀ (I : PEmpty.{u_4 + 1} → Ideal R),
    emultiplicity p.asIdeal (⨆ (i : PEmpty.{u_4 + 1}), I i) = ⨅ (i : PEmpty.{u_4 + 1}), emultiplicity p.asIdeal (I i)
⊢ emultiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), emultiplicity p.asIdeal (I i)
have of_equiv : ∀ {α β : Type u_4} (e : α ≃ β)
  (ih : ∀ (I : α → Ideal R), emultiplicity p.asIdeal (⨆ (i : α), I i) = ⨅ (i : α), emultiplicity p.asIdeal (I i))
  (I : β → Ideal R), emultiplicity p.asIdeal (⨆ (i : β), I i) = ⨅ (i : β), emultiplicity p.asIdeal (I i)
Tactic: induction ι using Finite.induction_empty_option with
  | h_empty =>
    rw [iSup_of_empty, iInf_of_empty]
    exact emultiplicity_zero _
  | of_equiv e ih =>
    specialize ih (I ∘ e)
    rw [← sSup_range, ← sInf_range] at ih ⊢
    rw [EquivLike.range_comp I e] at ih
    rw [ih]
    exact congrArg _ <| EquivLike.range_comp (emultiplicity p.asIdeal <| I ·) e
  | h_option ih =>
    rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
I : ι → Ideal R
h_empty :
  ∀ (I : PEmpty.{u_4 + 1} → Ideal R),
    emultiplicity p.asIdeal (⨆ (i : PEmpty.{u_4 + 1}), I i) = ⨅ (i : PEmpty.{u_4 + 1}), emultiplicity p.asIdeal (I i)
of_equiv :
  ∀ {α β : Type u_4} (e : α ≃ β)
    (ih : ∀ (I : α → Ideal R), emultiplicity p.asIdeal (⨆ (i : α), I i) = ⨅ (i : α), emultiplicity p.asIdeal (I i))
    (I : β → Ideal R), emultiplicity p.asIdeal (⨆ (i : β), I i) = ⨅ (i : β), emultiplicity p.asIdeal (I i)
⊢ emultiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), emultiplicity p.asIdeal (I i)
have h_option : ∀ {α : Type u_4} [Fintype α]
  (ih : ∀ (I : α → Ideal R), emultiplicity p.asIdeal (⨆ (i : α), I i) = ⨅ (i : α), emultiplicity p.asIdeal (I i))
  (I : Option α → Ideal R),
  emultiplicity p.asIdeal (⨆ (i : Option α), I i) = ⨅ (i : Option α), emultiplicity p.asIdeal (I i)
Tactic: induction ι using Finite.induction_empty_option with
  | h_empty =>
    rw [iSup_of_empty, iInf_of_empty]
    exact emultiplicity_zero _
  | of_equiv e ih =>
    specialize ih (I ∘ e)
    rw [← sSup_range, ← sInf_range] at ih ⊢
    rw [EquivLike.range_comp I e] at ih
    rw [ih]
    exact congrArg _ <| EquivLike.range_comp (emultiplicity p.asIdeal <| I ·) e
  | h_option ih =>
    rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
inst_3 : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
⊢ multiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), multiplicity p.asIdeal (I i)
have H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
Tactic: have H i : FiniteMultiplicity p.asIdeal (I i) :=
    FiniteMultiplicity.of_prime_left (prime p) <| hI i
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
inst_3 : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
⊢ FiniteMultiplicity p.asIdeal (⨆ (i : ι), I i)
have refine : Ne.{u_3 + 1} (α := Ideal R) (⨆ (i : ι), I i) 0
Tactic: refine FiniteMultiplicity.of_prime_left (prime p) ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
inst_3 : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
⊢ Ne.{u_3 + 1} (α := Ideal R) (⨆ (i : ι), I i) 0
have contrapose! : ∀ (hI : Eq.{u_3 + 1} (α := Ideal R) (⨆ (i : ι), I i) 0), ∃ (i : ι), I i = ⊥
Tactic: contrapose! hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
inst_3 : Nonempty ι
I : ι → Ideal R
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
hI : Eq.{u_3 + 1} (α := Ideal R) (⨆ (i : ι), I i) 0
⊢ ∃ (i : ι), I i = ⊥
have hI₁ : ∀ (i : ι), I i = ⊥
Tactic: rw [← bot_eq_zero, iSup_eq_bot] at hI
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
inst_3 : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
⊢ multiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), multiplicity p.asIdeal (I i)
have H' : FiniteMultiplicity p.asIdeal (⨆ (i : ι), I i)
Tactic: have H' : FiniteMultiplicity p.asIdeal (⨆ i, I i) := by
    refine FiniteMultiplicity.of_prime_left (prime p) ?_
    contrapose! hI
    rw [← bot_eq_zero, iSup_eq_bot] at hI
    exact ⟨Classical.ofNonempty, hI _⟩
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
inst_3 : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
H' : FiniteMultiplicity p.asIdeal (⨆ (i : ι), I i)
⊢ multiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), multiplicity p.asIdeal (I i)
have this : emultiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), emultiplicity p.asIdeal (I i)
Tactic: have := emultiplicity_iSup p I
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Factorization (hypothesis)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst_2 : Finite ι
inst_3 : Nonempty ι
I : ι → Ideal R
hI : ∀ (i : ι), I i ≠ ⊥
H : ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)
H' : FiniteMultiplicity p.asIdeal (⨆ (i : ι), I i)
this : emultiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), emultiplicity p.asIdeal (I i)
⊢ multiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), multiplicity p.asIdeal (I i)
have this₁ : Eq (α := ℕ∞) (↑(multiplicity p.asIdeal (⨆ (i : ι), I i)) : ℕ∞) (⨅ (i : ι), (↑(multiplicity p.asIdeal (I i)) : ℕ∞))
Tactic: simp only [H'.emultiplicity_eq_multiplicity, (H _).emultiplicity_eq_multiplicity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
k : K
⊢ Set.Finite (α := HeightOneSpectrum R) (Support R k)
have obtain : ∀ (n d : R) (hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d)
  (hk :
    HMul.hMul (β := K) k
        ((algebraMap R K : (a : R) → K)
            (↑(n,
                    Subtype.mk (p := fun (x : R) ↦
                      Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd).2 :
              R) :
          K) =
      (algebraMap R K : (a : R) → K)
        (n,
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d
              hd).1),
  Set.Finite (α := HeightOneSpectrum R) (Support R k)
Tactic: obtain ⟨⟨n, ⟨d, hd⟩⟩, hk⟩ := IsLocalization.surj (nonZeroDivisors R) k
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
k : K
n d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
hk :
  HMul.hMul (β := K) k
      ((algebraMap R K : (a : R) → K)
          (↑(n,
                  Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x)
                    d hd).2 :
            R) :
        K) =
    (algebraMap R K : (a : R) → K)
      (n, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd).1
⊢ Set.Finite (α := HeightOneSpectrum R) (Support R k)
have hd' : d ≠ 0
Tactic: have hd' : d ≠ 0 := nonZeroDivisors.ne_zero hd
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
k : K
n d : R
hd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) d
hk :
  HMul.hMul (β := K) k
      ((algebraMap R K : (a : R) → K)
          (↑(n,
                  Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x)
                    d hd).2 :
            R) :
        K) =
    (algebraMap R K : (a : R) → K)
      (n, Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (nonZeroDivisors R : Submonoid R) x) d hd).1
hd' : d ≠ 0
this :
  Set.Finite.{u_1} (α := HeightOneSpectrum R)
    {v : HeightOneSpectrum R |
      LT.lt (α := WithZero (Multiplicative ℤ))
        (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
            ((algebraMap R K : (a : R) → K) d) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))}
⊢ Set.Finite (α := HeightOneSpectrum R) (Support R k)
have apply : Subset (α := Set (HeightOneSpectrum R)) (Support R k)
  {v : HeightOneSpectrum R |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap R K : (a : R) → K) d) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))}
Tactic: apply Set.Finite.subset this