awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
y : AdicCompletion I N
⊢ y ∈ (map I g).ker → y ∈ (map I f).range
have apply : ∀ (b : AdicCauchySequence I N),
  Membership.mem (α := AdicCompletion I N) (map I g).ker
      ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N) →
    Membership.mem (α := AdicCompletion I N) (map I f).range
      ((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 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)
y : AdicCompletion I N
b : AdicCauchySequence I N
hz :
  Membership.mem (α := AdicCompletion I N) (map I g).ker
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
⊢ Membership.mem (α := AdicCompletion I N) (map I f).range
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : 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)),
  Membership.mem (α := AdicCompletion I N) (map I f).range
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
Tactic: obtain ⟨k, hk⟩ := Ideal.exists_pow_inf_eq_pow_smul I (LinearMap.range f)
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (hypothesis)
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)
y : AdicCompletion I N
b : AdicCauchySequence I N
hz :
  Membership.mem (α := AdicCompletion I N) (map I g).ker
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I 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)
⊢ Membership.mem (α := AdicCompletion I N) (map I f).range
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
have hb : ∀ (n : ℕ), Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤) ((g : (a : N) → P) ((↑b : ℕ → N) n) : P)
Tactic: have hb (n : ℕ) : g (b n) ∈ (I ^ n • ⊤ : Submodule R P) := by
      simpa using congrArg (fun x ↦ x.val n) hz
-- 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)
y : AdicCompletion I N
b : AdicCauchySequence I N
hz :
  Membership.mem (α := AdicCompletion I N) (map I g).ker
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I 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)
hb :
  ∀ (n : ℕ),
    Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤) ((g : (a : N) → P) ((↑b : ℕ → N) n) : P)
a : (n : ℕ) →
  (↑{a : M |
        HSub.hSub (α := N) ((f : (a : M) → N) a : N) ((↑b : ℕ → N) (k + n)) ∈
          HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤} :
    Type u) :=
  mapExactAux hf hfg hg hk b hb
⊢ Membership.mem (α := AdicCompletion I N) (map I f).range
    ((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 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)
y : AdicCompletion I N
b : AdicCauchySequence I N
hz :
  Membership.mem (α := AdicCompletion I N) (map I g).ker
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I 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)
hb :
  ∀ (n : ℕ),
    Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤) ((g : (a : N) → P) ((↑b : ℕ → N) n) : P)
a : (n : ℕ) →
  (↑{a : M |
        HSub.hSub (α := N) ((f : (a : M) → N) a : N) ((↑b : ℕ → N) (k + n)) ∈
          HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤} :
    Type u) :=
  mapExactAux hf hfg hg hk b hb
refine_1 :
  ∀ (n : ℕ),
    (fun (n : ℕ) ↦ (↑(a n) : M)) n ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) [SMOD
      HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ Membership.mem (α := AdicCompletion I N) (map I f).range
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
have refine_2 : Eq (α := 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 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)
y : AdicCompletion I N
b : AdicCauchySequence I N
hz :
  Membership.mem (α := AdicCompletion I N) (map I g).ker
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I 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)
hb :
  ∀ (n : ℕ),
    Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤) ((g : (a : N) → P) ((↑b : ℕ → N) n) : P)
a : (n : ℕ) →
  (↑{a : M |
        HSub.hSub (α := N) ((f : (a : M) → N) a : N) ((↑b : ℕ → N) (k + n)) ∈
          HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤} :
    Type u) :=
  mapExactAux hf hfg hg hk b hb
⊢ ∀ (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
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)
y : AdicCompletion I N
b : AdicCauchySequence I N
hz :
  Membership.mem (α := AdicCompletion I N) (map I g).ker
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I 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)
hb :
  ∀ (n : ℕ),
    Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤) ((g : (a : N) → P) ((↑b : ℕ → N) n) : P)
a : (n : ℕ) →
  (↑{a : M |
        HSub.hSub (α := N) ((f : (a : M) → N) a : N) ((↑b : ℕ → N) (k + n)) ∈
          HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤} :
    Type u) :=
  mapExactAux hf hfg hg hk b hb
⊢ Eq (α := 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)) ⋯)) :
      AdicCompletion I N)
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I N)
have refine_2 : ∀ (n : ℕ),
  Eq.{u + 1} (α := 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)
              (AdicCauchySequence.mk I M (fun (n : ℕ) ↦ (↑(a n) : M)) sorry))) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n)
    ((↑((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b) : (n : ℕ) → N ⧸ I ^ n • ⊤) n)
Tactic: ext n
-- 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)
y : AdicCompletion I N
b : AdicCauchySequence I N
hz :
  Membership.mem (α := AdicCompletion I N) (map I g).ker
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I 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)
hb :
  ∀ (n : ℕ),
    Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤) ((g : (a : N) → P) ((↑b : ℕ → N) n) : P)
a : (n : ℕ) →
  (↑{a : M |
        HSub.hSub (α := N) ((f : (a : M) → N) a : N) ((↑b : ℕ → N) (k + n)) ∈
          HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤} :
    Type u) :=
  mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ Eq.{u + 1} (α := 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)
              (AdicCauchySequence.mk I M (fun (n : ℕ) ↦ (↑(a n) : M)) ⋯))) :
        (n : ℕ) → N ⧸ I ^ n • ⊤)
      n)
    ((↑((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b) : (n : ℕ) → N ⧸ I ^ n • ⊤) n)
have refine_2 : Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (Submodule.Quotient.mk ((f : (a : M) → N) (↑(a n) : M)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
  (Submodule.Quotient.mk ((↑b : ℕ → N) (k + n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
Tactic: suffices h : Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (f (a n)) =
            Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (b (k + n)) by
        simp [h, AdicCauchySequence.mk_eq_mk (show n ≤ k + 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
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)
y : AdicCompletion I N
b : AdicCauchySequence I N
hz :
  Membership.mem (α := AdicCompletion I N) (map I g).ker
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I 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)
hb :
  ∀ (n : ℕ),
    Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤) ((g : (a : N) → P) ((↑b : ℕ → N) n) : P)
a : (n : ℕ) →
  (↑{a : M |
        HSub.hSub (α := N) ((f : (a : M) → N) a : N) ((↑b : ℕ → N) (k + n)) ∈
          HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤} :
    Type u) :=
  mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((f : (a : M) → N) (↑(a n) : M)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
    (Submodule.Quotient.mk ((↑b : ℕ → N) (k + n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤)
have refine_2 : HSub.hSub (α := N) ((f : (a : M) → N) (↑(a n) : M) : N) ((↑b : ℕ → N) (k + n)) ∈
  HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
Tactic: rw [Submodule.Quotient.eq]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Exactness (hypothesis)
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)
y : AdicCompletion I N
b : AdicCauchySequence I N
hz :
  Membership.mem (α := AdicCompletion I N) (map I g).ker
    ((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b : AdicCompletion I 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)
hb :
  ∀ (n : ℕ),
    Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤) ((g : (a : N) → P) ((↑b : ℕ → N) n) : P)
a : (n : ℕ) →
  (↑{a : M |
        HSub.hSub (α := N) ((f : (a : M) → N) a : N) ((↑b : ℕ → N) (k + n)) ∈
          HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤} :
    Type u) :=
  mapExactAux hf hfg hg hk b hb
n : ℕ
⊢ HSub.hSub (α := N) ((f : (a : M) → N) (↑(a n) : M) : N) ((↑b : ℕ → N) (k + n)) ∈
    HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
have hle : HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ≤ HSMul.hSMul (β := Submodule R N) (I ^ n) ⊤
Tactic: have hle : (I ^ (k + n) • ⊤ : Submodule R N) ≤ (I ^ n • ⊤ : Submodule R N) :=
        Submodule.smul_mono_left (Ideal.pow_le_pow_right (by lia))
-- 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
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I ⊤
⊢ x ∈ Submodule.comap f (HSMul.hSMul (β := Submodule R N) I ⊤)
have refine_1 : ∀ (r : R) (hr : r ∈ I) (x : M),
  Membership.mem (γ := Submodule R M) ⊤ x → r • x ∈ Submodule.comap f (HSMul.hSMul (β := Submodule R N) I ⊤)
Tactic: refine Submodule.smul_induction_on hx (fun r hr x _ ↦ ?_) (fun x y hx hy ↦ ?_)
-- 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
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
x : M
hx : x ∈ HSMul.hSMul (β := Submodule R M) I ⊤
refine_1 :
  ∀ (r : R) (hr : r ∈ I) (x : M),
    Membership.mem (γ := Submodule R M) ⊤ x → r • x ∈ Submodule.comap f (HSMul.hSMul (β := Submodule R N) I ⊤)
⊢ x ∈ Submodule.comap f (HSMul.hSMul (β := Submodule R N) I ⊤)
have refine_2 : ∀ (x y : M) (hx : x ∈ Submodule.comap f (HSMul.hSMul (β := Submodule R N) I ⊤))
  (hy : y ∈ Submodule.comap f (HSMul.hSMul (β := Submodule R N) I ⊤)),
  x + y ∈ Submodule.comap f (HSMul.hSMul (β := Submodule R N) I ⊤)
Tactic: refine Submodule.smul_induction_on hx (fun r hr x _ ↦ ?_) (fun x y hx hy ↦ ?_)
-- 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
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
a : AdicCauchySequence I M
m n : ℕ
hmn : m ≤ n
⊢ Submodule.map f (HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ≤ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤
have rw : I ^ m • Submodule.map f ⊤ ≤ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤
Tactic: rw [Submodule.map_smul'']
-- 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
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
a : AdicCauchySequence I M
m n : ℕ
hmn : m ≤ n
⊢ (fun (n : ℕ) ↦ ((f : (a : M) → N) ((↑a : ℕ → M) n) : N)) m ≡
    (fun (n : ℕ) ↦ ((f : (a : M) → N) ((↑a : ℕ → M) n) : N)) n [SMOD HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤]
have hm : Submodule.map f (HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ≤ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤
Tactic: have hm : Submodule.map f (I ^ m • ⊤ : Submodule R M) ≤ (I ^ m • ⊤ : Submodule R N) := by
      rw [Submodule.map_smul'']
      exact smul_mono_right _ le_top
-- 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
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
a : AdicCauchySequence I M
m n : ℕ
hmn : m ≤ n
hm : Submodule.map f (HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤) ≤ HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤
⊢ (fun (n : ℕ) ↦ ((f : (a : M) → N) ((↑a : ℕ → M) n) : N)) m ≡
    (fun (n : ℕ) ↦ ((f : (a : M) → N) ((↑a : ℕ → M) n) : N)) n [SMOD HSMul.hSMul (β := Submodule R N) (I ^ m) ⊤]
have apply : (fun (n : ℕ) ↦ ((f : (a : M) → N) ((↑a : ℕ → M) n) : N)) m ≡
  (fun (n : ℕ) ↦ ((f : (a : M) → N) ((↑a : ℕ → M) n) : N)) n [SMOD
  Submodule.map f (HSMul.hSMul (β := Submodule R M) (I ^ m) ⊤)]
Tactic: apply SModEq.mono hm
-- 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
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
a b : AdicCauchySequence I M
⊢ Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑(a + b) : ℕ → M) n)) ⋯ =
    HAdd.hAdd (α := AdicCauchySequence I N)
      (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑a : ℕ → M) n)) ⋯)
      (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑b : ℕ → M) n)) ⋯)
have h : ∀ (n : ℕ),
  (↑(Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑(a + b) : ℕ → M) n))
            sorry) :
        ℕ → N)
      n =
    (↑(HAdd.hAdd (α := AdicCauchySequence I N)
            (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑a : ℕ → M) n))
              sorry)
            (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑b : ℕ → M) n))
              sorry)) :
        ℕ → 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
P : Type u_4
inst_5 : AddCommGroup P
inst_6 : Module R P
T : Type u_5
inst_7 : AddCommGroup T
inst_8 : Module.{u_1, u_5} (AdicCompletion I R) T
f : M →ₗ[R] N
r : R
a : AdicCauchySequence I M
⊢ Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑(r • a) : ℕ → M) n)) ⋯ =
    HSMul.hSMul (α := R) (β := AdicCauchySequence I N) ((RingHom.id R : (a : R) → R) r : R)
      (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑a : ℕ → M) n)) ⋯)
have h : ∀ (n : ℕ),
  (↑(Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑(r • a) : ℕ → M) n))
            sorry) :
        ℕ → N)
      n =
    (↑(HSMul.hSMul (α := R) (β := AdicCauchySequence I N) ((RingHom.id R : (a : R) → R) r : R)
            (Subtype.mk (p := fun (f : ℕ → N) ↦ IsAdicCauchy I N f) (fun (n : ℕ) ↦ (f : (a : M) → N) ((↑a : ℕ → M) n))
              sorry)) :
        ℕ → N)
      n
Tactic: ext n