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 : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
i : ℕ
h : i < n
neg : 0 = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
neg₁ :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤)
    ((transitionMap I M ⋯ : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ i • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤)
⊢ (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      i =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
have neg₂ : Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) 0
  ((transitionMap I M sorry : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ i • ⊤) 0)
Tactic: rw [ofPowSMul_val_apply_eq_zero _ h.le, ← x.prop h.le, hxn, _root_.map_zero]
-- 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 : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
i : ℕ
h : i < n
neg : 0 = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
neg₁ :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤)
    ((transitionMap I M ⋯ : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ i • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤)
neg₂ :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) 0
    ((transitionMap I M ⋯ : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ i • ⊤) 0)
⊢ (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      i =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
have neg₃ : Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) 0 0
Tactic: rw [ofPowSMul_val_apply_eq_zero _ h.le, ← x.prop h.le, hxn, _root_.map_zero]
-- 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 : ℕ
⊢ Eq (α := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n)))
    (LinearMap.ker (eval I M n))
have refine_1 : ∀ (x : AdicCompletion I M)
  (hx :
    Membership.mem (γ := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n))) x),
  Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n)) x
Tactic: refine le_antisymm (fun x hx ↦ ?_) (fun x 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
n : ℕ
refine_1 :
  ∀ (x : AdicCompletion I M)
    (hx :
      Membership.mem (γ := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n))) x),
    Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n)) x
⊢ Eq (α := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n)))
    (LinearMap.ker (eval I M n))
have refine_2 : ∀ (x : AdicCompletion I M) (hx : Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n)) x),
  Membership.mem (γ := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n))) x
Tactic: refine le_antisymm (fun x hx ↦ ?_) (fun x 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
n : ℕ
x : AdicCompletion I M
hx : Membership.mem (γ := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n))) x
⊢ Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n)) x
have refine_1 : ∀ (y : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)),
  Membership.mem (α := AdicCompletion I M) (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n))
    ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y : AdicCompletion I M)
Tactic: rcases hx with ⟨y, rfl⟩
Cleared hypotheses: x, 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
n : ℕ
y : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
⊢ Membership.mem (α := AdicCompletion I M) (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n))
    ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y : AdicCompletion I M)
have refine_1 : Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
  ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤)
      ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y) :
    M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
  (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
Tactic: rw [LinearMap.mem_ker, eval_apply, ofPowSMul_val_apply_eq_zero _ (by rfl)]
-- 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 : ℕ
y : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
refine_1 :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤)
        ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
⊢ Membership.mem (α := AdicCompletion I M) (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n))
    ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y : AdicCompletion I M)
have refine_1₁ : Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
  ((↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y) : (n : ℕ) → M ⧸ I ^ n • ⊤) n) 0
Tactic: rw [LinearMap.mem_ker, eval_apply, ofPowSMul_val_apply_eq_zero _ (by rfl)]
-- 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 : ℕ
y : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
refine_1 :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤)
        ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
refine_1₁ :
  Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y) : (n : ℕ) → M ⧸ I ^ n • ⊤) n) 0
⊢ Membership.mem (α := AdicCompletion I M) (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n))
    ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y : AdicCompletion I M)
have refine_1₂ : Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) 0 0
Tactic: rw [LinearMap.mem_ker, eval_apply, ofPowSMul_val_apply_eq_zero _ (by rfl)]
-- 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
n : ℕ
x : AdicCompletion I M
hx : Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n)) x
⊢ Membership.mem (γ := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n))) x
have hx₁ : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
Tactic: simp only [LinearMap.mem_ker, coe_eval] 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
n : ℕ
x : AdicCompletion I M
hx : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
⊢ Membership.mem (γ := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n))) x
have h : (ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hx) = x
Tactic: use ofValEqZero I 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
ι : Type u_3
inst_3 : DecidableEq ι
inst_4 : Fintype ι
f : ι → R
i : ι
a : AdicCauchySequence I M
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) ⊤)
have 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) ⊤)
Tactic: rw [← Ideal.Quotient.algebraMap_eq, algebraMap_smul]
-- 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
ι : 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) ⊤)
⊢ 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) ⊤)
have 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) ⊤)
Tactic: rw [← Ideal.Quotient.algebraMap_eq, algebraMap_smul]
-- 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 : ℕ
h : I.FG
⊢ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤ = LinearMap.ker (eval I M n)
have refine : LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤
Tactic: refine le_antisymm (pow_smul_top_le_ker_eval ..) ?_
-- 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
n : ℕ
h : I.FG
⊢ LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤
have h₁ : (I ^ n).FG
Tactic: replace h := Ideal.FG.pow (n := n) h
Cleared hypotheses: h
-- 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 : ℕ
h : (I ^ n).FG
⊢ LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤
have 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) ⊤
Tactic: rcases h with ⟨s, hs⟩
Cleared hypotheses: h
-- 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
⊢ LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (I ^ n) ⊤
have simp : LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (↑s : Set R) ⊤
Tactic: simp only [← hs, span_smul_eq]
-- 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
⊢ LinearMap.ker (eval I M n) ≤ HSMul.hSMul (β := Submodule R (AdicCompletion I M)) (↑s : Set R) ⊤
have 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))
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]
-- 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
⊢ 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))
have 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)))
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]))]
-- 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
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 • ⊤))
have 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)))
  ⊤
Tactic: rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, ← hs, span_smul_eq,
      smul_top_eq_range_lsum]
-- 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
n : ℕ
s : Finset R
hs : Ideal.span (↑s : Set R) = I ^ n
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
⊢ 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)
have 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)
        sorry) :
    (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
-- 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
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 • ⊤))
⊢ 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)
have 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)
                sorry) :
            (a : AdicCompletion I (↥s →₀ M)) → AdicCompletion I ↥(I ^ n • ⊤))
          x) :
      AdicCompletion I M)
Tactic: rcases map_surjective I this x with ⟨x, rfl⟩
Cleared hypotheses: x