awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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
have 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 ℤ))
Tactic: apply_fun v.valuation K at hk
Cleared hypotheses: hk
-- 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
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 ℤ))
⊢ 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
have 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
Tactic: simp only [Valuation.map_mul, valuation_of_algebraMap] at hk
Cleared hypotheses: hk
-- 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
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
⊢ 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
have rw : LT.lt (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [Set.mem_setOf_eq, valuation_of_algebraMap]
-- 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
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
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have this₁ : LE.le (α := WithZero (Multiplicative ℤ))
  ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: have := intValuation_le_one v n
-- 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
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 ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have 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 ℤ))
Tactic: contrapose! 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
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 ℤ)) (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 ℤ))
have rw : 1 <
  HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) k :
      WithZero (Multiplicative ℤ))
Tactic: rw [← hk, mul_comm]
-- 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
⊢ Set.Finite (α := HeightOneSpectrum R) (Support R k)
have suffices : 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 ℤ))}
Tactic: suffices {v : HeightOneSpectrum R | v.valuation K (algebraMap R K d) < 1}.Finite by
    apply Set.Finite.subset this
    intro v hv
    apply_fun v.valuation K at hk
    simp only [Valuation.map_mul, valuation_of_algebraMap] at hk
    rw [Set.mem_setOf_eq, valuation_of_algebraMap]
    have := intValuation_le_one v n
    contrapose! this
    rw [← hk, mul_comm]
    exact (lt_mul_of_one_lt_right (by simp) hv).trans_le <|
      mul_le_mul_of_nonneg_right this (by simp)
-- 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
⊢ 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 ℤ))}
have simp_rw : Set.Finite.{u_1} (α := HeightOneSpectrum R) {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {d}}
Tactic: simp_rw [valuation_lt_one_iff_dvd]
-- 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
⊢ Set.Finite.{u_1} (α := HeightOneSpectrum R) {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {d}}
have hI : Ne (α := Ideal R) (Ideal.span {d}) 0
Tactic: apply Ideal.finite_factors
-- 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
⊢ ∀ᶠ (i : HeightOneSpectrum R) in Filter.cofinite,
    Membership.mem (γ := Set ((fun (v : HeightOneSpectrum R) ↦ adicCompletion K v) i))
      ((fun (v : HeightOneSpectrum R) ↦
          (↑(adicCompletionIntegers K v) : Set ((fun (v : HeightOneSpectrum R) ↦ adicCompletion K v) v)))
        i)
      ((fun (i : HeightOneSpectrum R) ↦
          ((↑((RingEquiv.symm (WithVal.equiv (valuation K i)) : (a : K) → WithVal (valuation K i)) k) :
              UniformSpace.Completion (WithVal (valuation K i))) :
            UniformSpace.Completion (WithVal (valuation K i))))
        i)
have simp : Set.Finite.{u_1} (α := HeightOneSpectrum R)
  {x : HeightOneSpectrum R |
    LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (WithVal (valuation K x)) (WithZero (Multiplicative ℤ))) :
            (a : WithVal (valuation K x)) → WithZero (Multiplicative ℤ))
          ((RingEquiv.symm (WithVal.equiv (valuation K x)) : (a : K) → WithVal (valuation K x)) k) :
        WithZero (Multiplicative ℤ))}
Tactic: simp only [Filter.eventually_cofinite, SetLike.mem_coe, mem_adicCompletionIntegers R K,
     adicCompletion, Valued.valuedCompletion_apply, not_le]
-- 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
a : FiniteAdeleRing R K
⊢ IsUnit a ↔
    (∀ (v : HeightOneSpectrum R), (a : (a : HeightOneSpectrum R) → adicCompletion K a) v ≠ 0) ∧
      ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
        Eq (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
              ((a : (a : HeightOneSpectrum R) → adicCompletion K a) v) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ))
have rw : ((∀ (i : HeightOneSpectrum R), IsUnit ((a : (a : HeightOneSpectrum R) → adicCompletion K a) i)) ∧
    ∀ᶠ (i : HeightOneSpectrum R) in Filter.cofinite,
      ∃ (h :
        Membership.mem (γ := ValuationSubring (adicCompletion K i)) (adicCompletionIntegers K i)
          ((a : (a : HeightOneSpectrum R) → adicCompletion K a) i)),
        IsUnit
          (Subtype.mk (p := fun (x : adicCompletion K i) ↦
            Membership.mem (γ := ValuationSubring (adicCompletion K i)) (adicCompletionIntegers K i) x)
            ((a : (a : HeightOneSpectrum R) → adicCompletion K a) i) h)) ↔
  (∀ (v : HeightOneSpectrum R), (a : (a : HeightOneSpectrum R) → adicCompletion K a) v ≠ 0) ∧
    ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
      Eq (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            ((a : (a : HeightOneSpectrum R) → adicCompletion K a) v) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
Tactic: rw [RestrictedProduct.isUnit_iff]
-- 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
a : FiniteAdeleRing R K
⊢ ((∀ (i : HeightOneSpectrum R), IsUnit ((a : (a : HeightOneSpectrum R) → adicCompletion K a) i)) ∧
      ∀ᶠ (i : HeightOneSpectrum R) in Filter.cofinite,
        ∃ (h :
          Membership.mem (γ := ValuationSubring (adicCompletion K i)) (adicCompletionIntegers K i)
            ((a : (a : HeightOneSpectrum R) → adicCompletion K a) i)),
          IsUnit
            (Subtype.mk (p := fun (x : adicCompletion K i) ↦
              Membership.mem (γ := ValuationSubring (adicCompletion K i)) (adicCompletionIntegers K i) x)
              ((a : (a : HeightOneSpectrum R) → adicCompletion K a) i) h)) ↔
    (∀ (v : HeightOneSpectrum R), (a : (a : HeightOneSpectrum R) → adicCompletion K a) v ≠ 0) ∧
      ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
        Eq (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
              ((a : (a : HeightOneSpectrum R) → adicCompletion K a) v) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ))
have simp : (∀ (i : HeightOneSpectrum R), (a : (a : HeightOneSpectrum R) → adicCompletion K a) i ≠ 0) ∧
    Set.Finite.{u_1} (α := HeightOneSpectrum R)
      ({a_1 : HeightOneSpectrum R |
          (a : (a : HeightOneSpectrum R) → adicCompletion K a) a_1 ∉ adicCompletionIntegers K a_1} ∪
        {a_1 : HeightOneSpectrum R |
          ¬Eq (α := WithZero (Multiplicative ℤ))
              (((Valued.v : Valuation (adicCompletion K a_1) (WithZero (Multiplicative ℤ))) :
                    (a : adicCompletion K a_1) → WithZero (Multiplicative ℤ))
                  ((a : (a : HeightOneSpectrum R) → adicCompletion K a) a_1) :
                WithZero (Multiplicative ℤ))
              (1 : WithZero (Multiplicative ℤ))}) ↔
  (∀ (v : HeightOneSpectrum R), (a : (a : HeightOneSpectrum R) → adicCompletion K a) v ≠ 0) ∧
    Set.Finite.{u_1} (α := HeightOneSpectrum R)
      {x : HeightOneSpectrum R |
        ¬Eq (α := WithZero (Multiplicative ℤ))
            (((Valued.v : Valuation (adicCompletion K x) (WithZero (Multiplicative ℤ))) :
                  (a : adicCompletion K x) → WithZero (Multiplicative ℤ))
                ((a : (a : HeightOneSpectrum R) → adicCompletion K a) x) :
              WithZero (Multiplicative ℤ))
            (1 : WithZero (Multiplicative ℤ))}
Tactic: simp only [isUnit_iff_ne_zero, adicCompletionIntegers.isUnit_iff_valued_eq_one, exists_prop,
    Filter.eventually_cofinite, not_and_or, Set.setOf_or]
-- 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
a : FiniteAdeleRing R K
ha₀ : ∀ (v : HeightOneSpectrum R), (a : (a : HeightOneSpectrum R) → adicCompletion K a) v ≠ 0
ha : ¬IsUnit a
⊢ Set.Infinite.{u_1} (α := HeightOneSpectrum R)
    {v : HeightOneSpectrum R |
      Ne (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
            ((a : (a : HeightOneSpectrum R) → adicCompletion K a) v) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))}
have contrapose! : ∀
  (ha :
    Set.Finite.{u_1} (α := HeightOneSpectrum R)
      {v : HeightOneSpectrum R |
        Ne (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
              ((a : (a : HeightOneSpectrum R) → adicCompletion K a) v) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ))}),
  IsUnit a
Tactic: contrapose! ha
Cleared hypotheses: ha