awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_3
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : ι → R
i : ι
a : AdicCauchySequence I M
n : ℕ
H :
  HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
      (((algebraMap R (R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) :
              R →+* R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) :
            (a : R) → R ⧸ I ^ n • ⊤)
          (f i) :
        R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((↑a : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) (f i)
      (Submodule.Quotient.mk ((↑a : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
H₁ H₂ :
  HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) (f i)
      (Submodule.Quotient.mk ((↑a : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) (f i)
      (Submodule.Quotient.mk ((↑a : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
⊢ HSMul.hSMul (α := R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (β :=
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
      ((Ideal.Quotient.mk (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) : (a : R) → R ⧸ I ^ n • ⊤) (f i) :
        R ⧸ HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((↑a : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) =
    HSMul.hSMul (β := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) (f i)
      (Submodule.Quotient.mk ((↑a : ℕ → M) n) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)

Tactic:
rw [← Ideal.Quotient.algebraMap_eq, algebraMap_smul]

Premises used: Ideal.Quotient.algebraMap_eq, algebraMap_smul
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
h : I.FG
⊢ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤ = LinearMap.ker (eval I M n)

Tactic:
le_antisymm (pow_smul_top_le_ker_eval ..) ?_

Premises used: le_antisymm, AdicCompletion.pow_smul_top_le_ker_eval
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
h : I.FG
refine : LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤
⊢ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤ = LinearMap.ker (eval I M n)

Tactic:
refine le_antisymm (pow_smul_top_le_ker_eval ..) ?_

Premises used: le_antisymm, AdicCompletion.pow_smul_top_le_ker_eval
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
h : I.FG
⊢ (I ^ n).FG

Tactic:
replace h := Ideal.FG.pow (n := n) h
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
h : (I ^ n).FG
rcases :
  ∀ (s : Finset R) (hs : Ideal.span (↑s : Set R) = I ^ n),
    LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤
⊢ LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤

Tactic:
rcases h with ⟨s, hs⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
simp : LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (↑s : Set R) ⊤
⊢ LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤

Tactic:
simp only [← hs, span_smul_eq]

Premises used: Submodule.span_smul_eq
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
rw :
  LE.le (α := Submodule.{u_1, u_2} (AdicCompletion I R) (AdicCompletion I M)) (LinearMap.range (ofPowSMul I M n))
    (LinearMap.range (R := AdicCompletion I R) (M := Finsupp.{u_1, u_2} (↑(↑s : Set R) : Type u_1) (AdicCompletion I M))
      (τ₁₂ := RingHom.id (AdicCompletion I R))
      ((lsum (AdicCompletion I R) :
          (a : (↑(↑s : Set R) : Type u_1) → AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I M) →
            ((↑(↑s : Set R) : Type u_1) →₀ AdicCompletion I M) →ₗ[AdicCompletion I R] AdicCompletion I M)
        fun (i : (↑(↑s : Set R) : Type u_1)) ↦
        HSMul.hSMul (α := AdicCompletion I R) (β :=
          LinearMap.{u_1, u_1, u_2, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
            (AdicCompletion I M) (AdicCompletion I M))
          ((algebraMap R (AdicCompletion I R) : (a : R) → AdicCompletion I R) (↑i : R) : AdicCompletion I R)
          LinearMap.id))
⊢ LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (↑s : Set R) ⊤

Tactic:
rw [← restrictScalars_top R (AdicCompletion I R) (AdicCompletion I M),
    ← restrictScalars_image_smul_eq (R := AdicCompletion I R),
    ← restrictScalars_range_ofPowSMul_eq_ker_eval, restrictScalars_le,
    image_smul_top_eq_range_lsum]

Premises used: Submodule.restrictScalars_top, Submodule.restrictScalars_image_smul_eq, Submodule.restrictScalars_le, AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval, AdicCompletion, Submodule.image_smul_top_eq_range_lsum
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
⊢ Eq (α := Submodule (AdicCompletion I R) (Finsupp.{u_1, u_2} (↥s) (AdicCompletion I M)))
    (LinearMap.range
      (↑(LinearEquiv.symm (finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ↥s)) :
        (DirectSum ↥s fun (x : ↥s) ↦ AdicCompletion I M) →ₗ[AdicCompletion I R] ↥s →₀ AdicCompletion I M))
    ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
x : AdicCompletion I (Finsupp.{u_1, u_2} (↥s) M)
⊢ (map I (↑(LinearEquiv.symm (finsuppLEquivDirectSum R M ↥s)) : (DirectSum ↥s fun (x : ↥s) ↦ M) →ₗ[R] ↥s →₀ M) :
        (a : AdicCompletion I (DirectSum ↥s fun (x : ↥s) ↦ M)) → AdicCompletion I (↥s →₀ M))
      ((map I (↑(finsuppLEquivDirectSum R M ↥s) : (↥s →₀ M) →ₗ[R] DirectSum ↥s fun (x : ↥s) ↦ M) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I (DirectSum ↥s fun (x : ↥s) ↦ M))
        x) =
    x

Tactic:
simp [← LinearMap.comp_apply, map_comp]

Premises used: AdicCompletion.map_comp, LinearMap.comp_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
rw :
  LE.le (α := Submodule.{u_1, u_2} (AdicCompletion I R) (AdicCompletion I M)) (LinearMap.range (ofPowSMul I M n))
    (LinearMap.range (M := AdicCompletion I (Finsupp.{u_1, u_2} (↥s) M))
      (map I
        ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
          HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)))
⊢ LE.le (α := Submodule.{u_1, u_2} (AdicCompletion I R) (AdicCompletion I M)) (LinearMap.range (ofPowSMul I M n))
    (LinearMap.range (R := AdicCompletion I R) (M := Finsupp.{u_1, u_2} (↥s) (AdicCompletion I M)) (τ₁₂ :=
      RingHom.id (AdicCompletion I R))
      ((lsum (AdicCompletion I R) :
          (a : ↥s → AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I M) →
            (↥s →₀ AdicCompletion I M) →ₗ[AdicCompletion I R] AdicCompletion I M)
        fun (i : ↥s) ↦
        HSMul.hSMul (α := AdicCompletion I R) (β :=
          LinearMap.{u_1, u_1, u_2, u_2} (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R))
            (AdicCompletion I M) (AdicCompletion I M))
          ((algebraMap R (AdicCompletion I R) : (a : R) → AdicCompletion I R) (↑i : R) : AdicCompletion I R)
          LinearMap.id))

Tactic:
rw [← LinearMap.range_comp_of_range_eq_top (f := (finsuppLEquivDirectSum ..).symm.toLinearMap)
    _ (by simp), lsum_smul_comp_finsuppLEquivDirectSum_symm,
    LinearMap.range_comp_of_range_eq_top _ (LinearEquiv.range _),
    LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_eq_top_of_surjective _ <|
      Function.RightInverse.surjective (g := map I (finsuppLEquivDirectSum R M s)) (fun _ ↦ by
      simp [← LinearMap.comp_apply, map_comp]))]

Premises used: LinearMap.range_comp_of_range_eq_top, LinearMap.range_eq_top_of_surjective, Function.RightInverse.surjective, LinearEquiv.range, _private.0.AdicCompletion.lsum_smul_comp_finsuppLEquivDirectSum_symm
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
x_1 : Finsupp.{u_1, u_2} (↥s) M
⊢ Membership.mem (α := M) (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
            HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id :
          (a : ↥s →₀ M) → M)
        x_1 :
      M)

Tactic:
simp [← hs, span_smul_eq, smul_top_eq_range_lsum]

Premises used: Submodule.smul_top_eq_range_lsum, Submodule.span_smul_eq
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
rw :
  Eq.{u_2 + 1} (α :=
    Submodule R
      ↥(LinearMap.range (R := R) (M := Finsupp.{u_1, u_2} (↑(↑s : Set R) : Type u_1) M) (τ₁₂ := RingHom.id R)
          ((lsum R : (a : (↑(↑s : Set R) : Type u_1) → M →ₗ[R] M) → ((↑(↑s : Set R) : Type u_1) →₀ M) →ₗ[R] M)
            fun (i : (↑(↑s : Set R) : Type u_1)) ↦ HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)))
    (comap
      (Submodule.subtype
        (LinearMap.range (R := R) (M := Finsupp.{u_1, u_2} (↑(↑s : Set R) : Type u_1) M) (τ₁₂ := RingHom.id R)
          ((lsum R : (a : (↑(↑s : Set R) : Type u_1) → M →ₗ[R] M) → ((↑(↑s : Set R) : Type u_1) →₀ M) →ₗ[R] M)
            fun (i : (↑(↑s : Set R) : Type u_1)) ↦ HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)))
      (LinearMap.range (R := R) (M := Finsupp.{u_1, u_2} (↥s) M) (τ₁₂ := RingHom.id R)
        ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
          HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)))
    ⊤
⊢ Function.Surjective (α := Finsupp.{u_1, u_2} (↥s) M) (β := ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    (⇑(LinearMap.codRestrict (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
          ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
            HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)
          ⋯) :
      (a : ↥s →₀ M) → ↥(I ^ n • ⊤))

Tactic:
rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, ← hs, span_smul_eq,
      smul_top_eq_range_lsum]

Premises used: LinearMap.range_eq_top, Submodule.smul_top_eq_range_lsum, Submodule.span_smul_eq, LinearMap.range_codRestrict
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
⊢ Eq.{u_2 + 1} (α :=
    Submodule R
      ↥(LinearMap.range (R := R) (M := Finsupp.{u_1, u_2} (↑(↑s : Set R) : Type u_1) M) (τ₁₂ := RingHom.id R)
          ((lsum R : (a : (↑(↑s : Set R) : Type u_1) → M →ₗ[R] M) → ((↑(↑s : Set R) : Type u_1) →₀ M) →ₗ[R] M)
            fun (i : (↑(↑s : Set R) : Type u_1)) ↦ HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)))
    (comap
      (Submodule.subtype
        (LinearMap.range (R := R) (M := Finsupp.{u_1, u_2} (↑(↑s : Set R) : Type u_1) M) (τ₁₂ := RingHom.id R)
          ((lsum R : (a : (↑(↑s : Set R) : Type u_1) → M →ₗ[R] M) → ((↑(↑s : Set R) : Type u_1) →₀ M) →ₗ[R] M)
            fun (i : (↑(↑s : Set R) : Type u_1)) ↦ HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)))
      (LinearMap.range (R := R) (M := Finsupp.{u_1, u_2} (↥s) M) (τ₁₂ := RingHom.id R)
        ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
          HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)))
    ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
⊢ Function.Surjective (α := Finsupp.{u_1, u_2} (↥s) M) (β := ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    (⇑(LinearMap.codRestrict (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
          ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
            HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)
          ⋯) :
      (a : ↥s →₀ M) → ↥(I ^ n • ⊤))

Tactic:
have : Function.Surjective ((lsum R fun i : s ↦ i.val • (LinearMap.id : M →ₗ[R] M)).codRestrict
    (I ^ n • ⊤) (fun _ ↦ by simp [← hs, span_smul_eq, smul_top_eq_range_lsum])) := by
    rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, ← hs, span_smul_eq,
      smul_top_eq_range_lsum]
    simp
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
this :
  Function.Surjective (α := Finsupp.{u_1, u_2} (↥s) M) (β := ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    (⇑(LinearMap.codRestrict (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
          ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
            HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)
          ⋯) :
      (a : ↥s →₀ M) → ↥(I ^ n • ⊤))
rcases :
  ∀ (x : AdicCompletion I (Finsupp.{u_1, u_2} (↥s) M)),
    Membership.mem (α := AdicCompletion I M) (γ := Submodule.{u_1, u_2} (AdicCompletion I R) (AdicCompletion I M))
      (LinearMap.range (M := AdicCompletion I (Finsupp.{u_1, u_2} (↥s) M))
        (map I
          ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
            HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)))
      ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M)
          ((map I
                (LinearMap.codRestrict (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
                  ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
                    HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)
                  ⋯) :
              (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I ↥(I ^ n • ⊤))
            x) :
        AdicCompletion I M)
⊢ Membership.mem (α := AdicCompletion I M) (γ := Submodule.{u_1, u_2} (AdicCompletion I R) (AdicCompletion I M))
    (LinearMap.range (M := AdicCompletion I (Finsupp.{u_1, u_2} (↥s) M))
      (map I
        ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
          HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)))
    ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) x : AdicCompletion I M)

Tactic:
rcases map_surjective I this x with ⟨x, rfl⟩

Premises used: rfl, AdicCompletion.map_surjective
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
this :
  Function.Surjective (α := Finsupp.{u_1, u_2} (↥s) M) (β := ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    (⇑(LinearMap.codRestrict (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
          ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
            HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)
          ⋯) :
      (a : ↥s →₀ M) → ↥(I ^ n • ⊤))
x : AdicCompletion I (Finsupp.{u_1, u_2} (↥s) M)
⊢ Membership.mem (α := AdicCompletion I M) (γ := Submodule.{u_1, u_2} (AdicCompletion I R) (AdicCompletion I M))
    (LinearMap.range (M := AdicCompletion I (Finsupp.{u_1, u_2} (↥s) M))
      (map I
        ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
          HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)))
    ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M)
        ((map I
              (LinearMap.codRestrict (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
                ((lsum R : (a : ↥s → M →ₗ[R] M) → (↥s →₀ M) →ₗ[R] M) fun (i : ↥s) ↦
                  HSMul.hSMul (β := M →ₗ[R] M) (↑i : R) LinearMap.id)
                ⋯) :
            (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I ↥(I ^ n • ⊤))
          x) :
      AdicCompletion I M)

Tactic:
exact ⟨x, by rw [← LinearMap.comp_apply, map_comp, LinearMap.subtype_comp_codRestrict]⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ m) ⊤]
m n : ℕ
h' : m ≤ n
simp : (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
    ((transitionMap I M h' : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤)
      ((fun (i : ℕ) ↦ (↑(x i) : (n : ℕ) → M ⧸ I ^ n • ⊤) i) n))
    ((fun (i : ℕ) ↦ (↑(x i) : (n : ℕ) → M ⧸ I ^ n • ⊤) i) m)

Tactic:
simp only [transitionMap_comp_eval_apply]

Premises used: AdicCompletion.transitionMap_comp_eval_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ m) ⊤]
m n : ℕ
h' : m ≤ n
⊢ x m ≡ x n [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ m) ⊤]

Tactic:
specialize hx h'
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
h' : m ≤ n
hx : x m ≡ x n [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ m) ⊤]
rwa :
  ∀ (hx : x m - x n ∈ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ m) ⊤),
    (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
rwa₁ :
  ∀ (hx : Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M m)) (x m - x n)),
    (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
rwa₂ :
  ∀
    (hx :
      Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
        ((eval I M m : (a : AdicCompletion I M) → M ⧸ I ^ m • ⊤) (x m - x n) :
          M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
        (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)),
    (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
rwa₃ :
  ∀
    (hx :
      HSub.hSub (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) (β :=
          M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
          ((eval I M m : (a : AdicCompletion I M) → M ⧸ I ^ m • ⊤) (x m) :
            M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
          ((eval I M m : (a : AdicCompletion I M) → M ⧸ I ^ m • ⊤) (x n) :
            M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) =
        0),
    (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
rwa₄ :
  ∀
    (hx :
      Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
        ((eval I M m : (a : AdicCompletion I M) → M ⧸ I ^ m • ⊤) (x m) : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)
        ((eval I M m : (a : AdicCompletion I M) → M ⧸ I ^ m • ⊤) (x n) :
          M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)),
    (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
rwa₅ :
  ∀ (hx : (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (eval I M m : (a : AdicCompletion I M) → M ⧸ I ^ m • ⊤) (x n)),
    (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
rwa₆ :
  ∀ (hx : (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m),
    (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
rwa₇ rwa₈ rwa₉ rwa₁₀ :
  ∀ (hx : (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m),
    (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
⊢ (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m

Tactic:
rwa [SModEq.sub_mem, pow_smul_top_eq_ker_eval h, LinearMap.mem_ker, _root_.map_sub,
          sub_eq_zero, eval_apply, eval_apply, eq_comm] at hx

Premises used: map_sub, sub_eq_zero, SModEq.sub_mem, eq_comm, AdicCompletion.pow_smul_top_eq_ker_eval, LinearMap.mem_ker, AdicCompletion.eval_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ m) ⊤]
L : AdicCompletion I M :=
  Subtype.mk (p := fun (f : (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (i : ℕ) ↦ (↑(x i) : (n : ℕ) → M ⧸ I ^ n • ⊤) i) ⋯
h₁ : ∀ (n : ℕ), x n ≡ L [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤]
⊢ ∃ (L : AdicCompletion I M), ∀ (n : ℕ), x n ≡ L [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤]

Tactic:
use L
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ m) ⊤]
L : AdicCompletion I M :=
  Subtype.mk (p := fun (f : (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (i : ℕ) ↦ (↑(x i) : (n : ℕ) → M ⧸ I ^ n • ⊤) i) ⋯
i : ℕ
h₁ : Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M i)) (x i - L)
⊢ x i ≡ L [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ i) ⊤]

Tactic:
rw [SModEq.sub_mem, pow_smul_top_eq_ker_eval h]

Premises used: SModEq.sub_mem, AdicCompletion.pow_smul_top_eq_ker_eval
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ m) ⊤]
L : AdicCompletion I M :=
  Subtype.mk (p := fun (f : (n : ℕ) → M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ↦
    ∀ {m n : ℕ} (hmn : m ≤ n), (transitionMap I M hmn : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ m • ⊤) (f n) = f m)
    (fun (i : ℕ) ↦ (↑(x i) : (n : ℕ) → M ⧸ I ^ n • ⊤) i) ⋯
i : ℕ
⊢ Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M i)) (x i - L)

Tactic:
simp [L]