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
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
⊢ Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (Ideal.map (R := MvPowerSeries σ R) (F :=
      MvPowerSeries σ R ≃+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) (Ideal.span (Set.range X)))
    (Ideal.map (R := MvPolynomial σ R) (F :=
      MvPolynomial σ R →+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (algebraMap (MvPolynomial σ R)
        (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R))
have simp_rw : Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
  (Ideal.span
    (Set.range (ι := σ)
      (Function.comp (β := MvPowerSeries σ R)
        (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
          (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        X)))
  (Ideal.span
    (Set.range (ι := σ)
      (Function.comp (β := MvPolynomial σ R)
        (⇑(algebraMap (MvPolynomial σ R)
              (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
          (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
        MvPolynomial.X)))
Tactic: simp_rw [Ideal.map_span, ← Set.range_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
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
⊢ Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (Ideal.span
      (Set.range (ι := σ)
        (Function.comp (β := MvPowerSeries σ R)
          (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
            (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
          X)))
    (Ideal.span
      (Set.range (ι := σ)
        (Function.comp (β := MvPolynomial σ R)
          (⇑(algebraMap (MvPolynomial σ R)
                (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
            (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
          MvPolynomial.X)))
have e_s : Eq (α := σ → AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
  (Function.comp (β := MvPowerSeries σ R)
    (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
      (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    X)
  (Function.comp (β := MvPolynomial σ R)
    (⇑(algebraMap (MvPolynomial σ R)
          (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
      (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    MvPolynomial.X)
Tactic: congr 2
-- 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
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
⊢ Eq (α := σ → AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    (Function.comp (β := MvPowerSeries σ R)
      (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
        (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      X)
    (Function.comp (β := MvPolynomial σ R)
      (⇑(algebraMap (MvPolynomial σ R)
            (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
        (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      MvPolynomial.X)
have e_s : ∀ (x : σ),
  Eq (α := AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    (Function.comp (β := MvPowerSeries σ R)
      (⇑(AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) :
        (a : MvPowerSeries σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      X x)
    (Function.comp (β := MvPolynomial σ R)
      (⇑(algebraMap (MvPolynomial σ R)
            (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) :
        (a : MvPolynomial σ R) → AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      MvPolynomial.X x)
Tactic: ext1
-- 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
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
⊢ IsAdicComplete (R := MvPowerSeries σ R) (Ideal.span (Set.range X)) (MvPowerSeries σ R)
have this : Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
  (Ideal.map (R := MvPowerSeries σ R) (F :=
    MvPowerSeries σ R ≃+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    (AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) (Ideal.span (Set.range X)))
  (Ideal.map (R := MvPolynomial σ R) (F :=
    MvPolynomial σ R →+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
    (algebraMap (MvPolynomial σ R)
      (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (MvPolynomial.idealOfVars σ R))
Tactic: have : Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    (MvPolynomial.idealOfVars σ R).map (algebraMap ..):= by
    simp_rw [Ideal.map_span, ← Set.range_comp]
    congr 2; ext1
    simp [AdicCompletion.algebraMap_apply, ← MvPolynomial.coe_X, toAdicCompletion_coe]
-- 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
a b c : ℕ
σ : Type u_3
inst_3 : Finite σ
this :
  Eq (α := Ideal (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
    (Ideal.map (R := MvPowerSeries σ R) (F :=
      MvPowerSeries σ R ≃+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (AlgEquiv.toRingEquiv (toAdicCompletionAlgEquiv σ R)) (Ideal.span (Set.range X)))
    (Ideal.map (R := MvPolynomial σ R) (F :=
      MvPolynomial σ R →+* AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
      (algebraMap (MvPolynomial σ R)
        (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R))
⊢ IsAdicComplete (R := MvPowerSeries σ R) (Ideal.span (Set.range X)) (MvPowerSeries σ R)
have rw : IsAdicComplete (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R)
  (AdicCompletion (R := MvPolynomial σ R) (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))
Tactic: rw [← IsAdicComplete.congr_ringEquiv _ (toAdicCompletionAlgEquiv σ R).toRingEquiv, this,
    IsAdicComplete.map_algebraMap_iff]
-- 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
a b c : ℕ
⊢ IsAdicComplete (R := R⟦X⟧) (Ideal.span {X}) R⟦X⟧
have this : IsAdicComplete.{u_1, u_1} (R := MvPowerSeries Unit R) (Ideal.span (Set.range MvPowerSeries.X)) (MvPowerSeries Unit R)
Tactic: have : IsAdicComplete (.span (.range MvPowerSeries.X) : Ideal (MvPowerSeries Unit R))
    (MvPowerSeries Unit R) := inferInstance
-- 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
a b c : ℕ
this :
  IsAdicComplete.{u_1, u_1} (R := MvPowerSeries Unit R) (Ideal.span (Set.range MvPowerSeries.X)) (MvPowerSeries Unit R)
⊢ IsAdicComplete (R := R⟦X⟧) (Ideal.span {X}) R⟦X⟧
have rwa : ∀ (this : IsAdicComplete (R := MvPowerSeries Unit R) (Ideal.span {MvPowerSeries.X default}) (MvPowerSeries Unit R)),
  IsAdicComplete (R := R⟦X⟧) (Ideal.span {X}) R⟦X⟧
Tactic: rwa [Set.range_unique] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : AdicCauchySequence I N
n : ℕ
y yₙ : M
hy : (f : (a : M) → N) y = (↑x : ℕ → N) (n + 1)
hyₙ : (f : (a : M) → N) yₙ = (↑x : ℕ → N) n
⊢ Membership.mem (α := N) (Submodule.map f (HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    ((f : (a : M) → N) (yₙ - y) : N)
have rw : (↑x : ℕ → N) (n + 1) ≡ (↑x : ℕ → N) n [SMOD HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤]
Tactic: rw [Submodule.map_smul'', Submodule.map_top, LinearMap.range_eq_top.2 hf,
      map_sub, hyₙ, hy, ← Submodule.neg_mem_iff, neg_sub, ← SModEq.sub_mem]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
⊢ ∃ (a : AdicCompletion I M), (map I f : (a : AdicCompletion I M) → AdicCompletion I N) a = y
have apply : ∀ (b : AdicCauchySequence I N),
  ∃ (a : AdicCompletion I M),
    Eq.{w + 1} (α := AdicCompletion I N)
      ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) a : AdicCompletion I N)
      ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
Tactic: apply AdicCompletion.induction_on I N y (fun b ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → (↑(Set.preimage (β := N) (⇑f : (a : M) → N) {(↑b : ℕ → N) n}) : Type v) := mapPreimage hf b
⊢ ∃ (a : AdicCompletion I M),
    Eq.{w + 1} (α := AdicCompletion I N)
      ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) a : AdicCompletion I N)
      ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
have refine_1 : ∀ (n : ℕ),
  (fun (n : ℕ) ↦ (↑(a n) : M)) n ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) [SMOD
    HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
Tactic: refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → (↑(Set.preimage (β := N) (⇑f : (a : M) → N) {(↑b : ℕ → N) n}) : Type v) := mapPreimage hf b
refine_1 :
  ∀ (n : ℕ),
    (fun (n : ℕ) ↦ (↑(a n) : M)) n ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) [SMOD
      HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ ∃ (a : AdicCompletion I M),
    Eq.{w + 1} (α := AdicCompletion I N)
      ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) a : AdicCompletion I N)
      ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
have refine_2 : Eq.{w + 1} (α := AdicCompletion I N)
  ((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
      ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M)
        (AdicCauchySequence.mk I M (fun (n : ℕ) ↦ (↑(a n) : M)) sorry)) :
    AdicCompletion I N)
  ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
Tactic: refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑f : (a : M) → N)
y : AdicCompletion I N
b : AdicCauchySequence I N
a : (n : ℕ) → (↑(Set.preimage (β := N) (⇑f : (a : M) → N) {(↑b : ℕ → N) n}) : Type v) := mapPreimage hf b
⊢ ∀ (n : ℕ),
    (fun (n : ℕ) ↦ (↑(a n) : M)) n ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) [SMOD
      HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
have refine_1 : ∀ (n : ℕ),
  (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) n [SMOD
    HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
Tactic: refine fun n ↦ SModEq.symm ?_
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Function.Injective (α := AdicCompletion I M) (β := AdicCompletion I N)
    (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)
have obtain : ∀ (k : ℕ)
  (hk :
    ∀ n ≥ k,
      HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
        I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)),
  Function.Injective (α := AdicCompletion I M) (β := AdicCompletion I N)
    (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)
Tactic: obtain ⟨k, hk⟩ := Ideal.exists_pow_inf_eq_pow_smul I (range f)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
k : ℕ
hk :
  ∀ n ≥ k,
    HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
      I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)
⊢ Function.Injective (α := AdicCompletion I M) (β := AdicCompletion I N)
    (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)
have rw : ∀ (m : AdicCompletion I M),
  Eq (α := AdicCompletion I N) ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) m : AdicCompletion I N)
      (0 : AdicCompletion I N) →
    m = 0
Tactic: rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
k : ℕ
hk :
  ∀ n ≥ k,
    HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
      I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)
x : AdicCompletion I M
⊢ Eq (α := AdicCompletion I N) ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) x : AdicCompletion I N)
      (0 : AdicCompletion I N) →
    x = 0
have apply : ∀ (a : AdicCauchySequence I M),
  Eq (α := AdicCompletion I N)
      ((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
          ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a) :
        AdicCompletion I N)
      (0 : AdicCompletion I N) →
    Eq (α := AdicCompletion I M) ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a : AdicCompletion I M)
      (0 : AdicCompletion I M)
Tactic: apply AdicCompletion.induction_on I M x (fun a ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
k : ℕ
hk :
  ∀ n ≥ k,
    HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
      I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)
x : AdicCompletion I M
a : AdicCauchySequence I M
hx :
  Eq (α := AdicCompletion I N)
    ((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
        ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a) :
      AdicCompletion I N)
    (0 : AdicCompletion I N)
⊢ Eq (α := AdicCompletion I M) ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a : AdicCompletion I M)
    (0 : AdicCompletion I M)
have refine : ∀ n ≥ 42, (↑a : ℕ → M) (n + k) ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
Tactic: refine AdicCompletion.mk_zero_of _ _ _ ⟨42, fun n _ ↦ ⟨n + k, by lia, n, by lia, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
k : ℕ
hk :
  ∀ n ≥ k,
    HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
      I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)
x : AdicCompletion I M
a : AdicCauchySequence I M
hx :
  Eq (α := AdicCompletion I N)
    ((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
        ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a) :
      AdicCompletion I N)
    (0 : AdicCompletion I N)
n : ℕ
h : n ≥ 42
⊢ (↑a : ℕ → M) (n + k) ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
have rw : (↑a : ℕ → M) (n + k) ∈ Submodule.comap f (I ^ n • f.range)
Tactic: rw [← Submodule.comap_map_eq_of_injective hf (I ^ n • ⊤ : Submodule R M),
    Submodule.map_smul'', Submodule.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
k : ℕ
hk :
  ∀ n ≥ k,
    HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
      I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)
x : AdicCompletion I M
a : AdicCauchySequence I M
hx :
  Eq (α := AdicCompletion I N)
    ((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
        ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a) :
      AdicCompletion I N)
    (0 : AdicCompletion I N)
n : ℕ
h : n ≥ 42
⊢ (↑a : ℕ → M) (n + k) ∈ Submodule.comap f (I ^ n • f.range)
have a₁ : Membership.mem (α := N) (I ^ n • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range))
  ((f : (a : M) → N) ((↑a : ℕ → M) (n + k)) : N)
Tactic: apply (smul_mono_right _ inf_le_right : I ^ n • (I ^ k • ⊤ ⊓ (range f)) ≤ _)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
k : ℕ
hk :
  ∀ n ≥ k,
    HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
      I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)
x : AdicCompletion I M
a : AdicCauchySequence I M
hx :
  Eq (α := AdicCompletion I N)
    ((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
        ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a) :
      AdicCompletion I N)
    (0 : AdicCompletion I N)
n : ℕ
h : n ≥ 42
⊢ Membership.mem (α := N) (I ^ n • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range))
    ((f : (a : M) → N) ((↑a : ℕ → M) (n + k)) : N)
have a₁ : Membership.mem (α := N) (I ^ (n + k - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range))
  ((f : (a : M) → N) ((↑a : ℕ → M) (n + k)) : N)
Tactic: nth_rw 1 [show n = n + k - k by lia]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsNoetherianRing R
inst_6 : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
k : ℕ
hk :
  ∀ n ≥ k,
    HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
      I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)
x : AdicCompletion I M
a : AdicCauchySequence I M
hx :
  Eq (α := AdicCompletion I N)
    ((map I f : (a : AdicCompletion I M) → AdicCompletion I N)
        ((mk I M : (a : AdicCauchySequence I M) → AdicCompletion I M) a) :
      AdicCompletion I N)
    (0 : AdicCompletion I N)
n : ℕ
h : n ≥ 42
⊢ Membership.mem (α := N) (I ^ (n + k - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range))
    ((f : (a : M) → N) ((↑a : ℕ → M) (n + k)) : N)
have a₁ : Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (n + k)) ⊤ ⊓ f.range)
  ((f : (a : M) → N) ((↑a : ℕ → M) (n + k)) : N)
Tactic: rw [← hk (n + k) (show n + k ≥ k by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R
M : Type u
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u
inst_3 : AddCommGroup N
inst_4 : Module R N
P : Type u
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : IsNoetherianRing R
inst_8 : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
hfg : Function.Exact (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Function.Surjective (α := N) (β := P) (⇑g : (a : N) → P)
k : ℕ
hkn :
  ∀ n ≥ k,
    HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤ ⊓ f.range =
      I ^ (n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker :
  ∀ (n : ℕ),
    Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤) ((g : (a : N) → P) ((↑x : ℕ → N) n) : P)
n : ℕ
d : N
hdmem : d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n + 1)) ⊤
y yₙ : M
hd : (f : (a : M) → N) y = (↑x : ℕ → N) (k + n + 1) - d
hyₙ :
  HSub.hSub (α := N) ((f : (a : M) → N) yₙ : N) ((↑x : ℕ → N) (k + n)) ∈
    HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤
⊢ Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) ((f : (a : M) → N) (y - yₙ) : N)
have simp : HSub.hSub (β := N) ((↑x : ℕ → N) (k + n + 1) - d) ((f : (a : M) → N) yₙ : N) ∈
  HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤
Tactic: simp only [map_sub, hd]