-- 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)ˣ
h :
  ∀ (a_1 : HeightOneSpectrum R),
    Membership.mem (γ := Set (HeightOneSpectrum R))
      {x : HeightOneSpectrum R |
        Membership.mem (γ := Set (HeightOneSpectrum R))
            {x : HeightOneSpectrum R |
              (fun (i : HeightOneSpectrum R) ↦
                  Membership.mem.{u_2, u_2} (γ :=
                    Set ((fun (i : HeightOneSpectrum R) ↦ Units.{u_2} (adicCompletion K i)) i))
                    ((fun (i : HeightOneSpectrum R) ↦
                        (↑(Submonoid.units
                              (Submonoid.ofClass (S := ValuationSubring (adicCompletion K i))
                                (adicCompletionIntegers K i))) :
                          Set ((fun (i : HeightOneSpectrum R) ↦ (adicCompletion K i)ˣ) i)))
                      i)
                    ((↑((RestrictedProduct.unitsEquiv (adicCompletion K) (S := fun (i : HeightOneSpectrum R) ↦
                                ValuationSubring (adicCompletion K i)) :
                              (a :
                                  Πʳ (i : HeightOneSpectrum R), [adicCompletion K i,
                                      (↑(adicCompletionIntegers K i) :
                                        Set ((fun (i : HeightOneSpectrum R) ↦ adicCompletion K i) i))]ˣ) →
                                Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                                  (↑(Submonoid.ofClass (adicCompletionIntegers K i)).units :
                                    Set ((fun (i : HeightOneSpectrum R) ↦ (adicCompletion K i)ˣ) i))])
                            a) :
                        (i : HeightOneSpectrum R) → (fun (i : HeightOneSpectrum R) ↦ (adicCompletion K i)ˣ) i)
                      i))
                x}
            x →
          Membership.mem (γ := Set (HeightOneSpectrum R))
            {x : HeightOneSpectrum R |
              (fun (v : HeightOneSpectrum R) ↦
                  Eq (α := WithZero (Multiplicative ℤ))
                    (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
                          (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
                        (↑((((RestrictedProduct.unitsEquiv (adicCompletion K) (S := fun (i : HeightOneSpectrum R) ↦
                                        ValuationSubring (adicCompletion K i)) :
                                      (a :
                                          Πʳ (i : HeightOneSpectrum R), [adicCompletion K i,
                                              (↑(adicCompletionIntegers K i) :
                                                Set ((fun (i : HeightOneSpectrum R) ↦ adicCompletion K i) i))]ˣ) →
                                        Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                                          (↑(Submonoid.ofClass (adicCompletionIntegers K i)).units :
                                            Set ((fun (i : HeightOneSpectrum R) ↦ (adicCompletion K i)ˣ) i))])
                                    a :
                                  Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                                    (↑(Submonoid.units
                                          (Submonoid.ofClass (S := ValuationSubring (adicCompletion K i))
                                            (adicCompletionIntegers K i))) :
                                      Set ((fun (i : HeightOneSpectrum R) ↦ (adicCompletion K i)ˣ) i))]) :
                                (a : HeightOneSpectrum R) → (adicCompletion K a)ˣ)
                              v) :
                          adicCompletion K v) :
                      WithZero (Multiplicative ℤ))
                    (1 : WithZero (Multiplicative ℤ)))
                x}
            x}
      a_1
h₁ :
  ∀ (a_1 : HeightOneSpectrum R),
    (↑((RestrictedProduct.unitsEquiv (adicCompletion K) (S := fun (i : HeightOneSpectrum R) ↦
                    ValuationSubring (adicCompletion K i)) :
                  (a :
                      Πʳ (i : HeightOneSpectrum R), [adicCompletion K i,
                          (↑(adicCompletionIntegers K i) : Set (adicCompletion K i))]ˣ) →
                    Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                      (↑(Submonoid.ofClass (adicCompletionIntegers K i)).units : Set (adicCompletion K i)ˣ)])
                a) :
            (i : HeightOneSpectrum R) → (adicCompletion K i)ˣ)
          a_1 ∈
        (↑(Submonoid.units
              (Submonoid.ofClass (S := ValuationSubring (adicCompletion K a_1)) (adicCompletionIntegers K a_1))) :
          Set (adicCompletion K a_1)ˣ) →
      Eq (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation (adicCompletion K a_1) (WithZero (Multiplicative ℤ))) :
              (a : adicCompletion K a_1) → WithZero (Multiplicative ℤ))
            (↑((((RestrictedProduct.unitsEquiv (adicCompletion K) (S := fun (i : HeightOneSpectrum R) ↦
                            ValuationSubring (adicCompletion K i)) :
                          (a :
                              Πʳ (i : HeightOneSpectrum R), [adicCompletion K i,
                                  (↑(adicCompletionIntegers K i) : Set (adicCompletion K i))]ˣ) →
                            Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                              (↑(Submonoid.ofClass (adicCompletionIntegers K i)).units : Set (adicCompletion K i)ˣ)])
                        a :
                      Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                        (↑(Submonoid.units
                              (Submonoid.ofClass (S := ValuationSubring (adicCompletion K i))
                                (adicCompletionIntegers K i))) :
                          Set (adicCompletion K i)ˣ)]) :
                    (a : HeightOneSpectrum R) → (adicCompletion K a)ˣ)
                  a_1) :
              adicCompletion K a_1) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (adicCompletion K v) (WithZero (Multiplicative ℤ))) :
            (a : adicCompletion K v) → WithZero (Multiplicative ℤ))
          (↑((((RestrictedProduct.unitsEquiv (adicCompletion K) (S := fun (i : HeightOneSpectrum R) ↦
                          ValuationSubring (adicCompletion K i)) :
                        (a :
                            Πʳ (i : HeightOneSpectrum R), [adicCompletion K i,
                                (↑(adicCompletionIntegers K i) :
                                  Set ((fun (i : HeightOneSpectrum R) ↦ adicCompletion K i) i))]ˣ) →
                          Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                            (↑(Submonoid.ofClass (adicCompletionIntegers K i)).units :
                              Set ((fun (i : HeightOneSpectrum R) ↦ (adicCompletion K i)ˣ) i))])
                      a :
                    Πʳ (i : HeightOneSpectrum R), [(adicCompletion K i)ˣ,
                      (↑(Submonoid.units
                            (Submonoid.ofClass (S := ValuationSubring (adicCompletion K i))
                              (adicCompletionIntegers K i))) :
                        Set ((fun (i : HeightOneSpectrum R) ↦ (adicCompletion K i)ˣ) i))]) :
                  (a : HeightOneSpectrum R) → (adicCompletion K a)ˣ)
                v) :
            adicCompletion K v) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
filter_upwards [(RestrictedProduct.unitsEquiv _ a).2] using fun _ h ↦
    adicCompletionIntegers.mem_units_iff_valued_eq_one.1 h

Premises used: Iff.mp, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, DFunLike.coe, RestrictedProduct.unitsEquiv, Subtype.property