awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
inst_3 : IsAdicComplete I S
inst_4 : CommRing A
inst_5 : Algebra R A
f g : A →ₐ[R] S
H :
  ∀ (n : ℕ),
    Eq (α := AlgHom.{u_3, u_5, u_4} R A (S ⧸ I ^ n)) (AlgHom.comp (Quotient.mkₐ R (I ^ n)) f)
      (AlgHom.comp (Quotient.mkₐ R (I ^ n)) g)
H₁ :
  ∀ (x : A),
    Eq.{u_4 + 1} (α := AdicCompletion I S)
      (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) f :
              AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
            (a : A) → AdicCompletion I S)
          x :
        AdicCompletion I S)
      (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) g :
              AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
            (a : A) → AdicCompletion I S)
          x :
        AdicCompletion I S)
⊢ Eq (α := AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S))
    (AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) f)
    (AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) g)

Tactic:
ext1 x
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
inst_3 : IsAdicComplete I S
inst_4 : CommRing A
inst_5 : Algebra R A
f g : A →ₐ[R] S
H :
  ∀ (n : ℕ),
    Eq (α := AlgHom.{u_3, u_5, u_4} R A (S ⧸ I ^ n)) (AlgHom.comp (Quotient.mkₐ R (I ^ n)) f)
      (AlgHom.comp (Quotient.mkₐ R (I ^ n)) g)
x : A
⊢ Eq.{u_4 + 1} (α := AdicCompletion I S)
    (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) f :
            AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
          (a : A) → AdicCompletion I S)
        x :
      AdicCompletion I S)
    (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) g :
            AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
          (a : A) → AdicCompletion I S)
        x :
      AdicCompletion I S)

Tactic:
AdicCompletion.ext_evalₐ fun n ↦ ?_

Premises used: AdicCompletion.ext_evalₐ
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
inst_3 : IsAdicComplete I S
inst_4 : CommRing A
inst_5 : Algebra R A
f g : A →ₐ[R] S
H :
  ∀ (n : ℕ),
    Eq (α := AlgHom.{u_3, u_5, u_4} R A (S ⧸ I ^ n)) (AlgHom.comp (Quotient.mkₐ R (I ^ n)) f)
      (AlgHom.comp (Quotient.mkₐ R (I ^ n)) g)
x : A
H₁ :
  ∀ (n : ℕ),
    Eq (α := S ⧸ I ^ n)
      ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n)
          (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) f :
                AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
              (a : A) → AdicCompletion I S)
            x) :
        S ⧸ I ^ n)
      ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n)
          (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) g :
                AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
              (a : A) → AdicCompletion I S)
            x) :
        S ⧸ I ^ n)
⊢ Eq.{u_4 + 1} (α := AdicCompletion I S)
    (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) f :
            AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
          (a : A) → AdicCompletion I S)
        x :
      AdicCompletion I S)
    (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) g :
            AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
          (a : A) → AdicCompletion I S)
        x :
      AdicCompletion I S)

Tactic:
refine AdicCompletion.ext_evalₐ fun n ↦ ?_

Premises used: AdicCompletion.ext_evalₐ
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Ideal S
inst_3 : IsAdicComplete I S
inst_4 : CommRing A
inst_5 : Algebra R A
f g : A →ₐ[R] S
H :
  ∀ (n : ℕ),
    Eq (α := AlgHom.{u_3, u_5, u_4} R A (S ⧸ I ^ n)) (AlgHom.comp (Quotient.mkₐ R (I ^ n)) f)
      (AlgHom.comp (Quotient.mkₐ R (I ^ n)) g)
x : A
n : ℕ
⊢ Eq (α := S ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n)
        (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) f :
              AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
            (a : A) → AdicCompletion I S)
          x) :
      S ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n)
        (((AlgHom.comp (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I)) : S →ₐ[R] AdicCompletion I S) g :
              AlgHom.{u_3, u_5, u_4} R A (AdicCompletion I S)) :
            (a : A) → AdicCompletion I S)
          x) :
      S ⧸ I ^ n)

Tactic:
simpa using congr($(H n) x)
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
m n : ℕ
hle : m ≤ n
a₁ :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S ⧸ I ^ a m)
      (((RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ a m)) : (a_1 : R) → S ⧸ I ^ a m) x :
        S ⧸ I ^ a m)
      ((f m : (a_1 : R) → S ⧸ I ^ a m) x : S ⧸ I ^ a m)
⊢ RingHom.comp (factorPow I ⋯) (f n) = f m

Tactic:
ext x
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
m n : ℕ
hle : m ≤ n
x : R
a₁ :
  Eq.{u_2 + 1} (α := S ⧸ I ^ a m) ((f m : (a_1 : R) → S ⧸ I ^ a m) x : S ⧸ I ^ a m)
    (((RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ a m)) : (a_1 : R) → S ⧸ I ^ a m) x :
      S ⧸ I ^ a m)
⊢ Eq.{u_2 + 1} (α := S ⧸ I ^ a m)
    (((RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ a m)) : (a_1 : R) → S ⧸ I ^ a m) x :
      S ⧸ I ^ a m)
    ((f m : (a_1 : R) → S ⧸ I ^ a m) x : S ⧸ I ^ a m)

Tactic:
symm
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
m n : ℕ
hle : m ≤ n
x : R
⊢ Eq.{u_2 + 1} (α := S ⧸ I ^ a m) ((f m : (a_1 : R) → S ⧸ I ^ a m) x : S ⧸ I ^ a m)
    (((RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ a m)) : (a_1 : R) → S ⧸ I ^ a m) x :
      S ⧸ I ^ a m)

Tactic:
Submodule.eq_factor_of_eq_factor_succ ?_ (fun n ↦ f n x) ?_ hle

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Submodule.eq_factor_of_eq_factor_succ, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
m n : ℕ
hle : m ≤ n
x : R
a₁ : Antitone.{0, u_2} (β := Submodule S S) fun (n : ℕ) ↦ I ^ a n
a₂ :
  ∀ (m : ℕ),
    Eq.{u_2 + 1} (α := S ⧸ I ^ a m) ((fun (n : ℕ) ↦ ((f n : (a_1 : R) → S ⧸ I ^ a n) x : S ⧸ I ^ a n)) m)
      ((Submodule.factor ⋯ : (a_1 : S ⧸ I ^ a m.succ) → S ⧸ I ^ a m)
        ((fun (n : ℕ) ↦ ((f n : (a_1 : R) → S ⧸ I ^ a n) x : S ⧸ I ^ a n)) (m + 1)))
⊢ Eq.{u_2 + 1} (α := S ⧸ I ^ a m) ((f m : (a_1 : R) → S ⧸ I ^ a m) x : S ⧸ I ^ a m)
    (((RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ a m)) : (a_1 : R) → S ⧸ I ^ a m) x :
      S ⧸ I ^ a m)

Tactic:
refine Submodule.eq_factor_of_eq_factor_succ ?_ (fun n ↦ f n x) ?_ hle

Premises used: Submodule.eq_factor_of_eq_factor_succ, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
m n : ℕ
hle : m ≤ n
x : R
⊢ Antitone.{0, u_2} (β := Submodule S S) fun (n : ℕ) ↦ I ^ a n

Tactic:
fun _ _ le ↦ Ideal.pow_le_pow_right (ha.monotone le)

Premises used: StrictMono.monotone, Set.Mem, Ideal.pow_le_pow_right, Antitone
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
m n : ℕ
hle : m ≤ n
x : R
⊢ Antitone.{0, u_2} (β := Submodule S S) fun (n : ℕ) ↦ I ^ a n

Tactic:
exact fun _ _ le ↦ Ideal.pow_le_pow_right (ha.monotone le)

Premises used: StrictMono.monotone, Ideal.pow_le_pow_right
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
m n : ℕ
hle : m ≤ n
x : R
s : ℕ
⊢ ∀ {m : ℕ} (x : R),
    Eq.{u_2 + 1} (α := S ⧸ I ^ a m)
      (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
                (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) :
              RingHom.{u_1, u_2} R (S ⧸ I ^ a m)) :
            (a_1 : R) → S ⧸ I ^ a m)
          x :
        S ⧸ I ^ a m)
      ((f m : (a_1 : R) → S ⧸ I ^ a m) x : S ⧸ I ^ a m)

Tactic:
simp only [RingHom.ext_iff] at hf

Premises used: RingHom.ext_iff
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
m n : ℕ
hle : m ≤ n
x : R
s : ℕ
hf :
  ∀ {m : ℕ} (x : R),
    Eq.{u_2 + 1} (α := S ⧸ I ^ a m)
      (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
                (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) :
              RingHom.{u_1, u_2} R (S ⧸ I ^ a m)) :
            (a_1 : R) → S ⧸ I ^ a m)
          x :
        S ⧸ I ^ a m)
      ((f m : (a_1 : R) → S ⧸ I ^ a m) x : S ⧸ I ^ a m)
⊢ Eq.{u_2 + 1} (α := S ⧸ I ^ a s) ((fun (n : ℕ) ↦ ((f n : (a_1 : R) → S ⧸ I ^ a n) x : S ⧸ I ^ a n)) s)
    ((Submodule.factor ⋯ : (a_1 : S ⧸ I ^ a s.succ) → S ⧸ I ^ a s)
      ((fun (n : ℕ) ↦ ((f n : (a_1 : R) → S ⧸ I ^ a n) x : S ⧸ I ^ a n)) (s + 1)))

Tactic:
simpa using (hf x).symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
inst_2 : IsAdicComplete I S
m n : ℕ
hle : m ≤ n
a₁ :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S ⧸ I ^ m)
      (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I hle : S ⧸ I ^ n →+* S ⧸ I ^ m)
                ((fun (n : ℕ) ↦ (RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ id n))) n :
                  RingHom.{u_1, u_2} R (S ⧸ I ^ id n)) :
              RingHom.{u_1, u_2} R (S ⧸ I ^ m)) :
            (a : R) → S ⧸ I ^ m)
          x :
        S ⧸ I ^ m)
      ((((fun (n : ℕ) ↦ (RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ id n))) m :
              RingHom.{u_1, u_2} R (S ⧸ I ^ id m)) :
            (a : R) → S ⧸ I ^ m)
          x :
        S ⧸ I ^ m)
⊢ Eq (α := RingHom.{u_1, u_2} R (S ⧸ I ^ m))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I hle : S ⧸ I ^ n →+* S ⧸ I ^ m)
        ((fun (n : ℕ) ↦ (RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ id n))) n :
          RingHom.{u_1, u_2} R (S ⧸ I ^ id n)) :
      RingHom.{u_1, u_2} R (S ⧸ I ^ m))
    ((fun (n : ℕ) ↦ (RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ id n))) m :
      RingHom.{u_1, u_2} R (S ⧸ I ^ id m))

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
inst_2 : IsAdicComplete I S
m n : ℕ
hle : m ≤ n
x : R
⊢ Eq.{u_2 + 1} (α := S ⧸ I ^ m)
    (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I hle : S ⧸ I ^ n →+* S ⧸ I ^ m)
              ((fun (n : ℕ) ↦ (RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ id n))) n :
                RingHom.{u_1, u_2} R (S ⧸ I ^ id n)) :
            RingHom.{u_1, u_2} R (S ⧸ I ^ m)) :
          (a : R) → S ⧸ I ^ m)
        x :
      S ⧸ I ^ m)
    ((((fun (n : ℕ) ↦ (RingHom.comp (factorPow I ⋯) (f n) : RingHom.{u_1, u_2} R (S ⧸ I ^ id n))) m :
            RingHom.{u_1, u_2} R (S ⧸ I ^ id m)) :
          (a : R) → S ⧸ I ^ m)
        x :
      S ⧸ I ^ m)

Tactic:
simp [← factorPow_comp_eq_of_factorPow_comp_succ_eq' ha f hf hle]

Premises used: IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq'
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
inst_2 : IsAdicComplete I S
n : ℕ
x : R
⊢ Eq (α := S ⧸ I ^ a n)
    ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n) ((liftRingHom I ha f ⋯ : (a : R) → S) x) : S ⧸ I ^ a n)
    ((f n : (a_1 : R) → S ⧸ I ^ a n) x : S ⧸ I ^ a n)

Tactic:
simp [liftRingHom, IsAdicComplete.liftRingHom,
      factorPow_comp_eq_of_factorPow_comp_succ_eq' ha f hf ha.le_apply]

Premises used: StrictMono.le_apply, IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq', IsAdicComplete.liftRingHom, IsAdicComplete.StrictMono.liftRingHom
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
inst_2 : IsAdicComplete I S
n : ℕ
a₁ :
  ∀ (x : R),
    Eq.{u_2 + 1} (α := S ⧸ I ^ a n)
      (((RingHom.comp (Ideal.Quotient.mk (I ^ a n)) (liftRingHom I ha f ⋯) : RingHom.{u_1, u_2} R (S ⧸ I ^ a n)) :
            (a_1 : R) → S ⧸ I ^ a n)
          x :
        S ⧸ I ^ a n)
      ((f n : (a_1 : R) → S ⧸ I ^ a n) x : S ⧸ I ^ a n)
⊢ RingHom.comp (Ideal.Quotient.mk (I ^ a n)) (liftRingHom I ha f ⋯) = f n

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
inst_2 : IsAdicComplete I S
n : ℕ
x : R
⊢ Eq.{u_2 + 1} (α := S ⧸ I ^ a n)
    (((RingHom.comp (Ideal.Quotient.mk (I ^ a n)) (liftRingHom I ha f ⋯) : RingHom.{u_1, u_2} R (S ⧸ I ^ a n)) :
          (a_1 : R) → S ⧸ I ^ a n)
        x :
      S ⧸ I ^ a n)
    ((f n : (a_1 : R) → S ⧸ I ^ a n) x : S ⧸ I ^ a n)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
inst_2 : IsAdicComplete I S
F : R →+* S
hF : ∀ (n : ℕ), RingHom.comp (Ideal.Quotient.mk (I ^ a n)) F = f n
a₁ :
  Eq (α := (a : R) → S) ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) F)
    ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) (liftRingHom I ha f ⋯))
⊢ F = liftRingHom I ha f ⋯

Tactic:
apply DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
inst_2 : IsAdicComplete I S
F : R →+* S
hF : ∀ (n : ℕ), RingHom.comp (Ideal.Quotient.mk (I ^ a n)) F = f n
a₁ :
  ∀ (n : ℕ) (r : R),
    Eq (α := S ⧸ I ^ a n)
      ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n)
        ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) F r))
      ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n)
        ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) (liftRingHom I ha f ⋯) r))
⊢ Eq (α := (a : R) → S) ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) F)
    ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) (liftRingHom I ha f ⋯))

Tactic:
apply IsHausdorff.StrictMono.funext' I ha

Premises used: IsHausdorff.StrictMono.funext'
-- Module: Mathlib.RingTheory.AdicCompletion.RingHom
Goal:
R : Type u_1
S : Type u_2
inst : NonAssocSemiring R
inst_1 : CommRing S
I : Ideal S
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → RingHom.{u_1, u_2} R (S ⧸ I ^ a n)
hf :
  ∀ {m : ℕ},
    @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (factorPow I ⋯ : S ⧸ I ^ a (m + 1) →+* S ⧸ I ^ a m)
        (f (m + 1) : RingHom.{u_1, u_2} R (S ⧸ I ^ a (m + 1))) =
      f m
inst_2 : IsAdicComplete I S
F : R →+* S
hF : ∀ (n : ℕ), RingHom.comp (Ideal.Quotient.mk (I ^ a n)) F = f n
n : ℕ
m : R
⊢ Eq (α := S ⧸ I ^ a n)
    ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n)
      ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) F m))
    ((Ideal.Quotient.mk (I ^ a n) : (a_1 : S) → S ⧸ I ^ a n)
      ((fun (f : R →+* S) ↦ ((⇑f : (a : R) → S) : (a : R) → S)) (liftRingHom I ha f ⋯) m))

Tactic:
simp [← hF n]
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
I : Ideal R
hI : IsAdic I
rw :
  (∀ (x : R), (∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) x 0) → x = 0) ↔
    Subset (α := Set R) (⋂₀ FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _)) {0}
⊢ IsHausdorff I R ↔ T2Space R

Tactic:
rw [I.ringFilterBasis.t2Space_iff_sInter_subset hI.symm, isHausdorff_iff]

Premises used: isHausdorff_iff, Eq.symm, AddGroupFilterBasis.t2Space_iff_sInter_subset, RingFilterBasis.toAddGroupFilterBasis
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
I : Ideal R
hI : IsAdic I
⊢ (∀ (x : R), (∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) x 0) → x = 0) ↔
    Subset (α := Set R) (⋂₀ FilterBasis.sets (@AddGroupFilterBasis.toFilterBasis _ AddGroupWithOne.toAddGroup _)) {0}

Tactic:
simp +instances [SModEq.zero, Ideal.ringFilterBasis, RingSubgroupsBasis.toRingFilterBasis]

Premises used: SModEq.zero, RingSubgroupsBasis.toRingFilterBasis, Ideal.ringFilterBasis
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
⊢ Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)

Tactic:
have := hI.hasBasis_nhds_zero.isCountablyGenerated
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
⊢ (𝓤 R).IsCountablyGenerated

Tactic:
have : (𝓤 R).IsCountablyGenerated := IsUniformAddGroup.uniformity_countably_generated
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
simp :
  (∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n) ↔ CompleteSpace R
⊢ IsPrecomplete I R ↔ CompleteSpace R

Tactic:
simp only [isPrecomplete_iff, smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]

Premises used: SModEq.sub_mem, isPrecomplete_iff, smul_eq_mul, Ideal.mul_top
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
mp : (∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n) → CompleteSpace R
mpr : CompleteSpace R → ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
⊢ (∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n) ↔ CompleteSpace R

Tactic:
constructor
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
⊢ CompleteSpace R

Tactic:
UniformSpace.complete_of_cauchySeq_tendsto fun u hu ↦ ?_

Premises used: UniformSpace.complete_of_cauchySeq_tendsto
-- Module: Mathlib.RingTheory.AdicCompletion.Topology
Goal:
R : Type u_1
inst : CommRing R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this_1 : Filter.IsCountablyGenerated.{u_1} (α := R) (𝓝 0)
this : (𝓤 R).IsCountablyGenerated
H : ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ (L : R), ∀ (n : ℕ), f n - L ∈ I ^ n
mp : ∀ (u : ℕ → R) (hu : CauchySeq u), ∃ (a : R), Filter.Tendsto u Filter.atTop (𝓝 a)
⊢ CompleteSpace R

Tactic:
refine UniformSpace.complete_of_cauchySeq_tendsto fun u hu ↦ ?_

Premises used: UniformSpace.complete_of_cauchySeq_tendsto