awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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)
⊢ Eq.{u_2 + 1} (α := AdicCompletion I 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) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
        x :
      AdicCompletion I M)
    ((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)
have rw : Eq.{u_2 + 1} (α := AdicCompletion I 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) :
        (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
      x :
    AdicCompletion I M)
  ((ofPowSMul I M n ∘ₗ
          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)
              sorry) :
        (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
      x :
    AdicCompletion I M)
Tactic: rw [← LinearMap.comp_apply, map_comp, LinearMap.subtype_comp_codRestrict]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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)
rw :
  Eq.{u_2 + 1} (α := AdicCompletion I 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) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
        x :
      AdicCompletion I M)
    ((ofPowSMul I M n ∘ₗ
            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 M)
        x :
      AdicCompletion I M)
⊢ Eq.{u_2 + 1} (α := AdicCompletion I 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) :
          (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
        x :
      AdicCompletion I M)
    ((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)
have rw₁ : Eq.{u_2 + 1} (α := AdicCompletion I 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) :
        (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
      x :
    AdicCompletion I M)
  ((map I
          ((HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤).subtype ∘ₗ
            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)
              sorry) :
        (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I M)
      x :
    AdicCompletion I M)
Tactic: rw [← LinearMap.comp_apply, map_comp, LinearMap.subtype_comp_codRestrict]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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
⊢ 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)
have simp : (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
Tactic: simp only [transitionMap_comp_eval_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (hypothesis)
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 n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
have hx₁ : x m ≡ x n [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ m) ⊤]
Tactic: specialize hx h'
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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) ⊤]
⊢ (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
have 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
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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
⊢ (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
have 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
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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
⊢ (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
have 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
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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
⊢ (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
have 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
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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
⊢ (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
have 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
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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
⊢ (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
have 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
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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
⊢ (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
have 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
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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
⊢ (↑(x n) : (n : ℕ) → M ⧸ I ^ n • ⊤) m = (↑(x m) : (n : ℕ) → M ⧸ I ^ n • ⊤) m
have 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
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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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) ⋯
⊢ ∃ (L : AdicCompletion I M), ∀ (n : ℕ), x n ≡ L [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤]
have h₁ : ∀ (n : ℕ), x n ≡ L [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤]
Tactic: use L
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
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 : ℕ
⊢ x i ≡ L [SMOD HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ i) ⊤]
have h₁ : Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M i)) (x i - L)
Tactic: rw [SModEq.sub_mem, pow_smul_top_eq_ker_eval h]