awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
rw :
  Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((f : (a : M) → N) x) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₁ :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk y0 : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₂ :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) y0 :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₃ :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤)
        (((HSMul.hSMul (β := Submodule R N) (I ^ n.succ) ⊤).mkQ : (a : N) → N ⧸ I ^ n.succ • ⊤) y0) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₄ :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    ((factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
rw₅ : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
⊢ (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
have rw₆ : y = y
Tactic: rw [SModEq, ← mkQ_apply, ← mkQ_apply, ← factor_mk (pow_smul_top_le I N n.le_succ) y0,
        hy0, hyy', hxy]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
⊢ ∃ (x' : M),
    x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) x') =
        y'
have this : (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
Tactic: have : f x ≡ y0 [SMOD (I ^ n • ⊤ : Submodule R N)] := by
    rw [SModEq, ← mkQ_apply, ← mkQ_apply, ← factor_mk (pow_smul_top_le I N n.le_succ) y0,
        hy0, hyy', hxy]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
this : (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
⊢ ∃ (x' : M),
    x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) x') =
        y'
have obtain : ∀ (x' : M) (hxx' : x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤])
  (hx'y0 : (f : (a : M) → N) x' ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]),
  ∃ (x' : M),
    x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) x') =
        y'
Tactic: obtain ⟨x', hxx', hx'y0⟩ :=
    exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top h this
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
this : (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
x' : M
hxx' : x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
hx'y0 : (f : (a : M) → N) x' ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ∃ (x' : M),
    x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) x') =
        y'
have right : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) x') = y'
Tactic: use x', hxx'
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
this : (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
x' : M
hxx' : x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
hx'y0 : (f : (a : M) → N) x' ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
⊢ ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) x') = y'
have right : Submodule.Quotient.mk ((f : (a : M) → N) x') = y'
Tactic: rwa [mkQ_apply, hx'y0]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
x : M
n : ℕ
y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
y' : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤
hyy' : (factor ⋯ : (a : N ⧸ I ^ n.succ • ⊤) → N ⧸ I ^ n • ⊤) y' = y
hxy : ((HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤).mkQ : (a : N) → N ⧸ I ^ n • ⊤) ((f : (a : M) → N) x) = y
y0 : N
hy0 : ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) y0 = y'
this : (f : (a : M) → N) x ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
x' : M
hxx' : x ≡ x' [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
hx'y0 : (f : (a : M) → N) x' ≡ y0 [SMOD HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤]
right : Submodule.Quotient.mk ((f : (a : M) → N) x') = y'
⊢ ((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤) ((f : (a : M) → N) x') = y'
have right₁ : Submodule.Quotient.mk y0 = y'
Tactic: rwa [mkQ_apply, hx'y0]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h_1 :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : AdicCompletion I N
h :
  ∃ (x : ℕ → M),
    ∀ (n : ℕ),
      x n ≡ x (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
        Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          (Submodule.Quotient.mk ((f : (a : M) → N) (x n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ ∃ (a : AdicCompletion I M), (map I f : (a : AdicCompletion I M) → AdicCompletion I N) a = y
have obtain : ∀ (x : ℕ → M)
  (hx :
    ∀ (n : ℕ),
      x n ≡ x (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
        Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          (Submodule.Quotient.mk ((f : (a : M) → N) (x n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)),
  ∃ (a : AdicCompletion I M), (map I f : (a : AdicCompletion I M) → AdicCompletion I N) a = y
Tactic: obtain ⟨x, hx⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : AdicCompletion I N
x : ℕ → M
hx :
  ∀ (n : ℕ),
    x n ≡ x (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
        (Submodule.Quotient.mk ((f : (a : M) → N) (x n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
        ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ ∃ (a : AdicCompletion I M), (map I f : (a : AdicCompletion I M) → AdicCompletion I N) a = y
have h₁ : (map I f : (a : AdicCompletion I M) → AdicCompletion I N)
    ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
      (Subtype.mk (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f) x sorry)) =
  y
Tactic: use AdicCompletion.mk I M ⟨x, fun h ↦
        eq_factor_of_eq_factor_succ (fun _ _ ↦ pow_smul_top_le I M) _ (fun n ↦ (hx n).1) h⟩
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : AdicCompletion I N
x : ℕ → M
hx :
  ∀ (n : ℕ),
    x n ≡ x (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
        (Submodule.Quotient.mk ((f : (a : M) → N) (x n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
        ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
⊢ (map I f : (a : AdicCompletion I M) → AdicCompletion I N)
      ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
        (Subtype.mk (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f) x ⋯)) =
    y
have h₁ : ∀ (n : ℕ),
  (↑((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
            ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
              (Subtype.mk (p := fun (f : ℕ → M) ↦ IsAdicCauchy I M f) x sorry))) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n =
    (↑y : (n : ℕ) → N ⧸ I ^ n • ⊤) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : AdicCompletion I N
⊢ ∃ (a : AdicCompletion I M), (map I f : (a : AdicCompletion I M) → AdicCompletion I N) a = y
have suffices : ∃ (x : ℕ → M),
  ∀ (n : ℕ),
    x n ≡ x (n + 1) [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
      Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
        (Submodule.Quotient.mk ((f : (a : M) → N) (x n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
        ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
Tactic: suffices h : ∃ x : ℕ → M, ∀ n, x n ≡ x (n + 1) [SMOD (I ^ n • ⊤ : Submodule R M)] ∧
      Submodule.Quotient.mk (f (x n)) = eval I _ n y by
    obtain ⟨x, hx⟩ := h
    use AdicCompletion.mk I M ⟨x, fun h ↦
        eq_factor_of_eq_factor_succ (fun _ _ ↦ pow_smul_top_le I M) _ (fun n ↦ (hx n).1) h⟩
    ext n
    simp [hx n]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : AdicCompletion I N
⊢ { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
      ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y :
        N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) }
have property : Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
  (Submodule.Quotient.mk ((f : (a : M) → N) 0) : N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
  ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y :
    N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : AdicCompletion I N
⊢ Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
    (Submodule.Quotient.mk ((f : (a : M) → N) 0) : N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
    ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y :
      N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
have property : Eq (α := HasQuotient.Quotient N (B := Submodule R N) ⊤)
  (((Quotient.equiv (HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) ⊤ (LinearEquiv.refl R N) sorry).toEquiv :
        (a : N ⧸ I ^ 0 • ⊤) → N ⧸ ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) 0)) :
    HasQuotient.Quotient N (B := Submodule R N) ⊤)
  (((Quotient.equiv (HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) ⊤ (LinearEquiv.refl R N) sorry).toEquiv :
        (a : N ⧸ I ^ 0 • ⊤) → N ⧸ ⊤)
      ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y) :
    HasQuotient.Quotient N (B := Submodule R N) ⊤)
Tactic: apply_fun (Submodule.Quotient.equiv (I ^ 0 • ⊤) ⊤ (.refl R N) (by simp)).toEquiv
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : AdicCompletion I N
n : ℕ
xn :
  { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) }
⊢ { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
      ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤) }
have succ : (z : M) →
  (hz :
      (↑xn : M) ≡ z [SMOD HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤] ∧
        Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
          (((HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤).mkQ : (a : N) → N ⧸ I ^ (n + 1) • ⊤)
              ((f : (a : M) → N) z) :
            N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
          ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y :
            N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)) →
    { m : M //
      Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
        (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
        ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y :
          N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤) }
Tactic: choose z hz using exists_smodEq_pow_smul_top_and_mkQ_eq h
          (y' := eval _ _ (n + 1) y) (by simp) xn.2
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : AdicCompletion I N
n : ℕ
⊢ { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) }
have zero : { m : M //
  Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
    (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
    ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y :
      N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) }
Tactic: induction n with
    | zero =>
      use 0
      apply_fun (Submodule.Quotient.equiv (I ^ 0 • ⊤) ⊤ (.refl R N) (by simp)).toEquiv
      exact Subsingleton.elim _ _
    | succ n xn =>
      choose z hz using exists_smodEq_pow_smul_top_and_mkQ_eq h
          (y' := eval _ _ (n + 1) y) (by simp) xn.2
      exact ⟨z, hz.2⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Functoriality (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 : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N ⧸ HSMul.hSMul (β := Submodule R N) I ⊤)
    (⇑((HSMul.hSMul (β := Submodule R N) I ⊤).mkQ ∘ₗ f) : (a : M) → N ⧸ I • ⊤)
y : AdicCompletion I N
n : ℕ
zero :
  { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤)
      ((eval I N 0 : (a : AdicCompletion I N) → N ⧸ I ^ 0 • ⊤) y :
        N ⧸ HSMul.hSMul (β := Submodule R N) (HPow.hPow (β := ℕ) I 0) ⊤) }
⊢ { m : M //
    Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
      ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) }
have succ : (n : ℕ) →
  (xn :
      { m : M //
        Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
          ((eval I N n : (a : AdicCompletion I N) → N ⧸ I ^ n • ⊤) y :
            N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤) }) →
    { m : M //
      Eq.{u_3 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
        (Submodule.Quotient.mk ((f : (a : M) → N) m) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤)
        ((eval I N (n + 1) : (a : AdicCompletion I N) → N ⧸ I ^ (n + 1) • ⊤) y :
          N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (n + 1)) ⊤) }
Tactic: induction n with
    | zero =>
      use 0
      apply_fun (Submodule.Quotient.equiv (I ^ 0 • ⊤) ⊤ (.refl R N) (by simp)).toEquiv
      exact Subsingleton.elim _ _
    | succ n xn =>
      choose z hz using exists_smodEq_pow_smul_top_and_mkQ_eq h
          (y' := eval _ _ (n + 1) y) (by simp) xn.2
      exact ⟨z, hz.2⟩
Cleared hypotheses: n