-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
I_1 : Ideal R_1
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
R : Type u_4
S : Type u_5
inst_4 : NonAssocSemiring R
inst_5 : CommRing S
I : Ideal S
f : (n : ℕ) → RingHom.{u_4, u_5} R (S ⧸ I ^ n)
hf : ∀ {m n : ℕ} (hle : m ≤ n), RingHom.comp (Ideal.Quotient.factorPow I hle) (f n) = f m
x y : R
h :
  ∀ (n : ℕ),
    (↑(Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
              ∀ {m n : ℕ} (hmn : m ≤ n), (Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
              (fun (n : ℕ) ↦
                HMul.hMul (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (β :=
                  S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
                  ((Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x) :
                    S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
                  ((Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y) :
                    S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤))
              ⋯) :
          (n : ℕ) → S ⧸ I ^ n • ⊤)
        n =
      (↑(HMul.hMul (α := AdicCompletion I S)
              (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
                ∀ {m n : ℕ} (hmn : m ≤ n), (Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
                (fun (n : ℕ) ↦
                  (Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x))
                ⋯)
              (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
                ∀ {m n : ℕ} (hmn : m ≤ n), (Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
                (fun (n : ℕ) ↦
                  (Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y))
                ⋯)) :
          (n : ℕ) → S ⧸ I ^ n • ⊤)
        n
⊢ Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦
        HMul.hMul (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (β :=
          S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
          ((Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x) :
            S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
          ((Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y) :
            S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤))
      ⋯ =
    HMul.hMul (α := AdicCompletion I S)
      (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x)) ⋯)
      (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (Ideal.Quotient.factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y)) ⋯)

Tactic:
ext