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