awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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))
⊢ Eq (α := ℕ∞) (sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i)))
    (sInf (range fun (i : β) ↦ emultiplicity p.asIdeal (I i)))

Tactic:
congrArg _ <| EquivLike.range_comp (emultiplicity p.asIdeal <| I ·) e

Premises used: congrArg, IsDedekindDomain.HeightOneSpectrum.asIdeal, EquivLike.range_comp, emultiplicity
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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))
⊢ Eq (α := ℕ∞) (sInf (range fun (i : α) ↦ emultiplicity p.asIdeal ((I ∘ (⇑e : (a : α) → β)) i)))
    (sInf (range fun (i : β) ↦ emultiplicity p.asIdeal (I i)))

Tactic:
exact congrArg _ <| EquivLike.range_comp (emultiplicity p.asIdeal <| I ·) e

Premises used: congrArg, IsDedekindDomain.HeightOneSpectrum.asIdeal, EquivLike.range_comp, emultiplicity
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)
h_option₃ 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)))
⊢ emultiplicity p.asIdeal (⨆ (i : Option α), I i) = ⨅ (i : Option α), emultiplicity p.asIdeal (I i)

Tactic:
rw [iSup_option, emultiplicity_sup p .., ih, iInf_option]

Premises used: iInf_option, IsDedekindDomain.HeightOneSpectrum.emultiplicity_sup, iSup_option
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)
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)
⊢ 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]

Premises used: iInf_of_empty, Finite.induction_empty_option, congrArg, iInf_option, emultiplicity_zero, IsDedekindDomain.HeightOneSpectrum.emultiplicity_sup, sSup_range, iSup_option, iSup_of_empty, sInf_range
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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 ≠ ⊥
⊢ ∀ (i : ι), FiniteMultiplicity p.asIdeal (I i)

Tactic:
have H i : FiniteMultiplicity p.asIdeal (I i) :=
    FiniteMultiplicity.of_prime_left (prime p) <| hI i
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)

Tactic:
FiniteMultiplicity.of_prime_left (prime p) ?_

Premises used: Set.Mem, IsDedekindDomain.HeightOneSpectrum.prime, FiniteMultiplicity.of_prime_left
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)
refine : Ne.{u_3 + 1} (α := Ideal R) (⨆ (i : ι), I i) 0
⊢ FiniteMultiplicity p.asIdeal (⨆ (i : ι), I i)

Tactic:
refine FiniteMultiplicity.of_prime_left (prime p) ?_

Premises used: IsDedekindDomain.HeightOneSpectrum.prime, FiniteMultiplicity.of_prime_left
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)
contrapose! : ∀ (hI : Eq.{u_3 + 1} (α := Ideal R) (⨆ (i : ι), I i) 0), ∃ (i : ι), I i = ⊥
⊢ Ne.{u_3 + 1} (α := Ideal R) (⨆ (i : ι), I i) 0

Tactic:
contrapose! hI
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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 = ⊥

Tactic:
rw [← bot_eq_zero, iSup_eq_bot] at hI

Premises used: iSup_eq_bot, bot_eq_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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 : ∀ (i : ι), I i = ⊥
⊢ ∃ (i : ι), I i = ⊥

Tactic:
⟨Classical.ofNonempty, hI _⟩

Premises used: Classical.ofNonempty, Exists.intro
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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 : ∀ (i : ι), I i = ⊥
⊢ ∃ (i : ι), I i = ⊥

Tactic:
exact ⟨Classical.ofNonempty, hI _⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)

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 _⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)
⊢ emultiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), emultiplicity p.asIdeal (I i)

Tactic:
have := emultiplicity_iSup p I
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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)
⊢ 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

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity
-- Module: Mathlib.RingTheory.DedekindDomain.Factorization
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 :
  Eq (α := ℕ∞) (↑(multiplicity p.asIdeal (⨆ (i : ι), I i)) : ℕ∞) (⨅ (i : ι), (↑(multiplicity p.asIdeal (I i)) : ℕ∞))
⊢ multiplicity p.asIdeal (⨆ (i : ι), I i) = ⨅ (i : ι), multiplicity p.asIdeal (I i)

Tactic:
exact_mod_cast this
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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
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)
⊢ Set.Finite (α := HeightOneSpectrum R) (Support R k)

Tactic:
obtain ⟨⟨n, ⟨d, hd⟩⟩, hk⟩ := IsLocalization.surj (nonZeroDivisors R) k

Premises used: IsLocalization.surj, nonZeroDivisors
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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
⊢ d ≠ 0

Tactic:
have hd' : d ≠ 0 := nonZeroDivisors.ne_zero hd
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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 ℤ))}
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 ℤ))}
⊢ Set.Finite (α := HeightOneSpectrum R) (Support R k)

Tactic:
apply Set.Finite.subset this

Premises used: Set.Finite.subset
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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 ℤ))}
v : HeightOneSpectrum R
hv : Membership.mem (γ := Set (HeightOneSpectrum R)) (Support R k) v
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (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)) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        ((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) :
      WithZero (Multiplicative ℤ))

Tactic:
apply_fun v.valuation K at hk

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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
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 ℤ))}
v : HeightOneSpectrum R
hv : Membership.mem (γ := Set (HeightOneSpectrum R)) (Support R k) v
hk :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (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)) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        ((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) :
      WithZero (Multiplicative ℤ))
⊢ HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) k :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ)) =
    (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n

Tactic:
simp only [Valuation.map_mul, valuation_of_algebraMap] at hk

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, Valuation.map_mul
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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
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 ℤ))}
v : HeightOneSpectrum R
hv : Membership.mem (γ := Set (HeightOneSpectrum R)) (Support R k) v
hk :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) k :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ)) =
    (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n
rw :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ Membership.mem (γ := Set (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 ℤ))}
    v

Tactic:
rw [Set.mem_setOf_eq, valuation_of_algebraMap]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, Set.mem_setOf_eq
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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
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 ℤ))}
v : HeightOneSpectrum R
hv : Membership.mem (γ := Set (HeightOneSpectrum R)) (Support R k) v
hk :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) k :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ)) =
    (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
have := intValuation_le_one v n
-- Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
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
hd' : d ≠ 0
this_1 :
  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 ℤ))}
v : HeightOneSpectrum R
hv : Membership.mem (γ := Set (HeightOneSpectrum R)) (Support R k) v
hk :
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) k :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ)) =
    (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n
this :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
contrapose! :
  ∀
    (this :
      LE.le (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
        ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))),
    LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
contrapose! this