awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r : AdicCompletion I R
x y : AdicCompletion I M
h : ∀ (n : ℕ), (↑(r • (x + y)) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • x + r • y) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ r • (x + y) = r • x + r • y

Tactic:
ext n
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r : AdicCompletion I R
x y : AdicCompletion I M
n : ℕ
⊢ (↑(r • (x + y)) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • x + r • y) : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r s : AdicCompletion I R
x : AdicCompletion I M
h : ∀ (n : ℕ), (↑((r + s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • x + s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (r + s) • x = r • x + s • x

Tactic:
ext n
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r s : AdicCompletion I R
x : AdicCompletion I M
n : ℕ
⊢ (↑((r + s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • x + s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
x : AdicCompletion I M
h :
  ∀ (n : ℕ),
    (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := AdicCompletion I R) 0 x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n =
      (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := AdicCompletion I R) 0 x = 0

Tactic:
ext n
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
x : AdicCompletion I M
n : ℕ
⊢ (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := AdicCompletion I R) 0 x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n =
    (↑0 : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r : R
s : AdicCompletion I R
x : AdicCompletion I M
h : ∀ (n : ℕ), (↑((r • s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (r • s) • x = r • s • x

Tactic:
ext n
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
r : R
s : AdicCompletion I R
x : AdicCompletion I M
n : ℕ
h :
  (↑(r • s) : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
h₁ :
  (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
h₂ :
  (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = r • (↑(s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n
h₃ :
  (r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n) • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n =
    r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
h₄ h₅ :
  r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n =
    r • (↑s : (n : ℕ) → R ⧸ I ^ n • ⊤) n • (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n
⊢ (↑((r • s) • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n = (↑(r • s • x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n

Tactic:
rw [smul_eval, val_smul_apply, val_smul_apply, smul_eval, smul_assoc]

Premises used: smul_assoc, AdicCompletion.smul_eval, AdicCompletion.val_smul_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ Eq (α := Module (AdicCompletion I R) (AdicCompletion I R)) (module I) Algebra.toModule

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I : Ideal R
M : Type u_3
inst_2 : AddCommGroup M
inst_3 : Module R M
⊢ Eq (α := Module (AdicCompletion I R) (AdicCompletion I R)) (module I) Algebra.toModule

Tactic:
with_reducible_and_instances rfl
-- 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 : R
m n : ℕ
hkl : m ≤ n
⊢ Eq (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ m) ⊤)
    ((transitionMap I S hkl : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤)
      ((fun (n : ℕ) ↦
          ((factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x) :
            S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤))
        n))
    ((fun (n : ℕ) ↦
        ((factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x) :
          S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤))
      m)

Tactic:
simp [transitionMap, Submodule.factorPow, ← hf hkl]

Premises used: Submodule.factorPow, AdicCompletion.transitionMap
-- 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
simp :
  Eq.{u_5 + 1} (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) 1) ⋯)
    1
⊢ Eq.{u_5 + 1} (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) 1)) ⋯)
    1

Tactic:
simp only [map_one]

Premises used: map_one
-- 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
h :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
      ((↑(Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
                ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
                (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) 1) ⋯) :
            (n : ℕ) → S ⧸ I ^ n • ⊤)
          n :
        S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
      ((↑1 : (n : ℕ) → S ⧸ I ^ n • ⊤) n : S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
⊢ Eq.{u_5 + 1} (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) 1) ⋯)
    1

Tactic:
ext
-- 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
n : ℕ
⊢ Eq.{u_5 + 1} (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
    ((↑(Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
              ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
              (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) 1) ⋯) :
          (n : ℕ) → S ⧸ I ^ n • ⊤)
        n :
      S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
    ((↑1 : (n : ℕ) → S ⧸ I ^ n • ⊤) n : S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)

Tactic:
simp
-- 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
simp :
  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)) ⋯)
⊢ Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) (x * y))) ⋯ =
    HMul.hMul (α := AdicCompletion I S)
      (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (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), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y)) ⋯)

Tactic:
simp only [mapQ_eq_factor, factor_eq_factor, map_mul]

Premises used: Submodule.factor_eq_factor, Submodule.mapQ_eq_factor, map_mul
-- 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
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

Tactic:
simp
-- 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
simp :
  Eq.{u_5 + 1} (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ 0) ⋯)
    0
⊢ Eq.{u_5 + 1} (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) 0)) ⋯)
    0

Tactic:
simp only [map_zero]

Premises used: map_zero
-- 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
h :
  ∀ (n : ℕ),
    Eq.{u_5 + 1} (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
      ((↑(Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
                ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
                (fun (n : ℕ) ↦ 0) ⋯) :
            (n : ℕ) → S ⧸ I ^ n • ⊤)
          n :
        S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
      ((↑0 : (n : ℕ) → S ⧸ I ^ n • ⊤) n : S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
⊢ Eq.{u_5 + 1} (α := AdicCompletion I S)
    (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ 0) ⋯)
    0

Tactic:
ext
-- 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
n : ℕ
⊢ Eq.{u_5 + 1} (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
    ((↑(Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
              ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
              (fun (n : ℕ) ↦ 0) ⋯) :
          (n : ℕ) → S ⧸ I ^ n • ⊤)
        n :
      S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
    ((↑0 : (n : ℕ) → S ⧸ I ^ n • ⊤) n : S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)

Tactic:
simp
-- 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
simp :
  Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦
        HAdd.hAdd (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (β :=
          S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
          ((factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x) :
            S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
          ((factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y) :
            S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤))
      ⋯ =
    HAdd.hAdd (α := AdicCompletion I S)
      (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (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), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y)) ⋯)
⊢ Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
      ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
      (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) (x + y))) ⋯ =
    HAdd.hAdd (α := AdicCompletion I S)
      (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
        ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (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), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
        (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y)) ⋯)

Tactic:
simp only [map_add]

Premises used: map_add
-- 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
n : ℕ
⊢ (↑(Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
            ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
            (fun (n : ℕ) ↦
              HAdd.hAdd (α := S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) (β :=
                S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
                ((factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) x) :
                  S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤)
                ((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 =
    (↑(HAdd.hAdd (α := AdicCompletion I S)
            (Subtype.mk (p := fun (f : (n : ℕ) → S ⧸ HSMul.hSMul (β := Submodule S S) (I ^ n) ⊤) ↦
              ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
              (fun (n : ℕ) ↦ (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), (transitionMap I S hmn : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ m • ⊤) (f n) = f m)
              (fun (n : ℕ) ↦ (factor ⋯ : (a : S ⧸ I ^ n) → S ⧸ I ^ n • ⊤) ((f n : (a : R) → S ⧸ I ^ n) y)) ⋯)) :
        (n : ℕ) → S ⧸ I ^ n • ⊤)
      n

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : 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
n : ℕ
x : R
h : HSMul.hSMul (β := Ideal S) (I ^ n) ⊤ ≤ I ^ n
⊢ Eq (α := S ⧸ I ^ n)
    ((factor h : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
        ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤)
          ((liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x)) :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
simp [liftRingHom, eval]

Premises used: AdicCompletion.liftRingHom, AdicCompletion.eval
-- Module: Mathlib.RingTheory.AdicCompletion.Algebra
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : 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
n : ℕ
x : R
rw :
  Eq (α := S ⧸ I ^ n)
    ((factor ⋯ : (a : S ⧸ I ^ n • ⊤) → S ⧸ I ^ n)
        ((eval I S n : (a : AdicCompletion I S) → S ⧸ I ^ n • ⊤)
          ((liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x)) :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)
⊢ Eq (α := S ⧸ I ^ n)
    ((evalₐ I n : (a : AdicCompletion I S) → S ⧸ I ^ n) ((liftRingHom I f ⋯ : (a : R) → AdicCompletion I S) x) :
      S ⧸ I ^ n)
    ((f n : (a : R) → S ⧸ I ^ n) x : S ⧸ I ^ n)

Tactic:
rw [← factor_eval_eq_evalₐ I _ (le_of_eq (Ideal.mul_top _))]

Premises used: AdicCompletion.factor_eval_eq_evalₐ, Ideal.mul_top, le_of_eq