-- 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)ˣ
⊢ ∀ᶠ (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 ℤ))
have 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
Tactic: filter_upwards [(RestrictedProduct.unitsEquiv _ a).2] using fun _ h ↦
    adicCompletionIntegers.mem_units_iff_valued_eq_one.1 h