awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ℤ)) (1 : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
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 ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (1 : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))

Tactic:
rw [← hk, mul_comm]

Premises used: mul_comm
-- 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 ℤ)) (1 : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) 0 1

Tactic:
simp
-- 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 ℤ)) (1 : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (0 : WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) k :
      WithZero (Multiplicative ℤ))

Tactic:
simp
-- 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 ℤ)) (1 : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
⊢ 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:
exact (lt_mul_of_one_lt_right (by simp) hv).trans_le <|
      mul_le_mul_of_nonneg_right this (by simp)

Premises used: mul_le_mul_of_nonneg_right, LT.lt.trans_le, lt_mul_of_one_lt_right
-- 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
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 ℤ))}
⊢ Set.Finite (α := HeightOneSpectrum R) (Support R k)

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)
-- 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
simp_rw : Set.Finite.{u_1} (α := HeightOneSpectrum R) {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {d}}
⊢ 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:
simp_rw [valuation_lt_one_iff_dvd]

Premises used: IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd
-- 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
hI : Ne (α := Ideal R) (Ideal.span {d}) 0
⊢ Set.Finite.{u_1} (α := HeightOneSpectrum R) {v : HeightOneSpectrum R | v.asIdeal ∣ Ideal.span {d}}

Tactic:
apply Ideal.finite_factors

Premises used: Ideal.finite_factors
-- 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
⊢ Ne (α := Ideal R) (Ideal.span {d}) 0

Tactic:
simpa only [Submodule.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, ne_eq, Submodule.zero_eq_bot
-- 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
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 ℤ))}
⊢ ∀ᶠ (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)

Tactic:
simp only [Filter.eventually_cofinite, SetLike.mem_coe, mem_adicCompletionIntegers R K,
     adicCompletion, Valued.valuedCompletion_apply, not_le]

Premises used: not_le, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, Filter.eventually_cofinite, Valued.valuedCompletion_apply, SetLike.mem_coe, IsDedekindDomain.HeightOneSpectrum.adicCompletion
-- 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
⊢ 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:
HeightOneSpectrum.Support.finite R k

Premises used: setOf, IsDedekindDomain.HeightOneSpectrum.Support, IsDedekindDomain.HeightOneSpectrum.Support.finite
-- 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
⊢ 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:
exact HeightOneSpectrum.Support.finite R k

Premises used: IsDedekindDomain.HeightOneSpectrum.Support.finite
-- 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
v : HeightOneSpectrum R
⊢ (((algebraMap K (FiniteAdeleRing R K) : (a : K) → FiniteAdeleRing R K) k : FiniteAdeleRing R K) :
        (a : HeightOneSpectrum R) → adicCompletion K a)
      v =
    (↑((RingEquiv.symm (WithVal.equiv (valuation K v)) : (a : K) → WithVal (valuation K v)) k) :
      UniformSpace.Completion (WithVal (valuation K v)))

Tactic:
rfl

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, rfl
-- 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
⊢ IsScalarTower R K (FiniteAdeleRing R K)

Tactic:
IsScalarTower.of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', rfl
-- 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
a₁ a₂ : FiniteAdeleRing R K
h :
  ∀ (v : HeightOneSpectrum R),
    (a₁ : (a : HeightOneSpectrum R) → adicCompletion K a) v = (a₂ : (a : HeightOneSpectrum R) → adicCompletion K a) v
⊢ a₁ = a₂

Tactic:
Subtype.ext <| funext h

Premises used: IsDedekindDomain.FiniteAdeleRing, RestrictedProduct, funext, Subtype.ext
-- 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
⊢ IsTopologicalRing (FiniteAdeleRing R K)

Tactic:
haveI : Fact (∀ v : HeightOneSpectrum R,
      IsOpen (v.adicCompletionIntegers K : Set (v.adicCompletion K))) :=
    ⟨fun _ ↦ Valued.isOpen_valuationSubring _⟩
  RestrictedProduct.isTopologicalRing (fun (v : HeightOneSpectrum R) ↦ v.adicCompletion K)

Premises used: IsDedekindDomain.FiniteAdeleRing, Set.Mem, RestrictedProduct.isTopologicalRing, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.instTopologicalSpaceFiniteAdeleRing._aux_1
-- 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
a : FiniteAdeleRing R K
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 ℤ))
⊢ 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 ℤ))

Tactic:
rw [RestrictedProduct.isUnit_iff]

Premises used: RestrictedProduct.isUnit_iff
-- 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
a : FiniteAdeleRing R K
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 ℤ))}
⊢ ((∀ (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:
simp only [isUnit_iff_ne_zero, adicCompletionIntegers.isUnit_iff_valued_eq_one, exists_prop,
    Filter.eventually_cofinite, not_and_or, Set.setOf_or]

Premises used: Filter.eventually_cofinite, isUnit_iff_ne_zero, exists_prop, not_and_or, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, Set.setOf_or
-- 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
a : FiniteAdeleRing R K
⊢ (∀ (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:
simpa using fun _ _ ↦ a.2

Premises used: Subtype.property