awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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
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)
⊢ Eq (α := AdicCompletion I N) ((map I f : (a : AdicCompletion I M) → AdicCompletion I N) x : AdicCompletion I N)
      (0 : AdicCompletion I N) →
    x = 0

Tactic:
apply AdicCompletion.induction_on I M x (fun a ↦ ?_)

Premises used: AdicCompletion.induction_on
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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
⊢ n + k ≥ n

Tactic:
lia
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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
⊢ n ≥ n

Tactic:
lia
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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)
refine : ∀ n ≥ 42, (↑a : ℕ → M) (n + k) ∈ HSMul.hSMul (β := Submodule R M) (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:
refine AdicCompletion.mk_zero_of _ _ _ ⟨42, fun n _ ↦ ⟨n + k, by lia, n, by lia, ?_⟩⟩

Premises used: AdicCompletion.mk_zero_of, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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
rw : (↑a : ℕ → M) (n + k) ∈ Submodule.comap f (I ^ n • f.range)
⊢ (↑a : ℕ → M) (n + k) ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤

Tactic:
rw [← Submodule.comap_map_eq_of_injective hf (I ^ n • ⊤ : Submodule R M),
    Submodule.map_smul'', Submodule.map_top]

Premises used: Submodule.comap_map_eq_of_injective, Submodule.map_smul'', Submodule.map_top, HPow.hPow, HSMul.hSMul, Top.top
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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₁ :
  Membership.mem (α := N) (I ^ n • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range))
    ((f : (a : M) → N) ((↑a : ℕ → M) (n + k)) : N)
⊢ (↑a : ℕ → M) (n + k) ∈ Submodule.comap f (I ^ n • f.range)

Tactic:
apply (smul_mono_right _ inf_le_right : I ^ n • (I ^ k • ⊤ ⊓ (range f)) ≤ _)

Premises used: inf_le_right, smul_mono_right
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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
⊢ n = n + k - k

Tactic:
lia
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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₁ :
  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)
⊢ Membership.mem (α := N) (I ^ n • (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]
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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
⊢ n + k ≥ k

Tactic:
lia
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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₁ :
  Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (n + k)) ⊤ ⊓ f.range)
    ((f : (a : M) → N) ((↑a : ℕ → M) (n + k)) : N)
⊢ 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:
rw [← hk (n + k) (show n + k ≥ k by lia)]

Premises used: HAdd.hAdd
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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) (↑(HSMul.hSMul (β := Submodule R N) (I ^ (n + k)) ⊤) : Set N)
    ((f : (a : M) → N) ((↑a : ℕ → M) (n + k)) : N)

Tactic:
simpa using congrArg (fun x ↦ x.val (n + k)) hx

Premises used: congrArg
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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) (HSMul.hSMul (β := Submodule R N) (I ^ (n + k)) ⊤ ⊓ f.range)
    ((f : (a : M) → N) ((↑a : ℕ → M) (n + k)) : N)

Tactic:
exact ⟨by simpa using congrArg (fun x ↦ x.val (n + k)) hx, ⟨a (n + k), rfl⟩⟩
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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)) ⊤
simp :
  HSub.hSub (β := N) ((↑x : ℕ → N) (k + n + 1) - d) ((f : (a : M) → N) yₙ : 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)

Tactic:
simp only [map_sub, hd]

Premises used: map_sub
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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)) ⊤
h :
  HSub.hSub (β := N) ((↑x : ℕ → N) (k + n + 1) - d) ((f : (a : M) → N) yₙ : N) =
    (↑x : ℕ → N) (k + n + 1) - (↑x : ℕ → N) (k + n) - d -
      HSub.hSub (α := N) ((f : (a : M) → N) yₙ : N) ((↑x : ℕ → N) (k + n))
convert_6 :
  (↑x : ℕ → N) (k + n + 1) - (↑x : ℕ → N) (k + n) - d -
      HSub.hSub (α := N) ((f : (a : M) → N) yₙ : N) ((↑x : ℕ → N) (k + n)) ∈
    HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤
⊢ HSub.hSub (β := N) ((↑x : ℕ → N) (k + n + 1) - d) ((f : (a : M) → N) yₙ : N) ∈
    HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤

Tactic:
convert_to x (k + n + 1) - x (k + n) - d - (f yₙ - x (k + n)) ∈ I ^ (k + n) • ⊤

Premises used: HSub.hSub, HAdd.hAdd, OfNat.ofNat, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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)) ⊤
⊢ HSub.hSub (β := N) ((↑x : ℕ → N) (k + n + 1) - d) ((f : (a : M) → N) yₙ : N) =
    (↑x : ℕ → N) (k + n + 1) - (↑x : ℕ → N) (k + n) - d -
      HSub.hSub (α := N) ((f : (a : M) → N) yₙ : N) ((↑x : ℕ → N) (k + n))

Tactic:
abel
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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)) ⊤
⊢ (↑x : ℕ → N) (k + n + 1) - (↑x : ℕ → N) (k + n) - d -
      HSub.hSub (α := N) ((f : (a : M) → N) yₙ : N) ((↑x : ℕ → N) (k + n)) ∈
    HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤

Tactic:
Submodule.sub_mem _ (Submodule.sub_mem _ ?_ ?_) hyₙ

Premises used: Set.Mem, Submodule.sub_mem
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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)) ⊤
convert_6 : (↑x : ℕ → N) (k + n + 1) - (↑x : ℕ → N) (k + n) ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤
convert_6₁ : d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤
⊢ (↑x : ℕ → N) (k + n + 1) - (↑x : ℕ → N) (k + n) - d -
      HSub.hSub (α := N) ((f : (a : M) → N) yₙ : N) ((↑x : ℕ → N) (k + n)) ∈
    HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤

Tactic:
refine Submodule.sub_mem _ (Submodule.sub_mem _ ?_ ?_) hyₙ

Premises used: Submodule.sub_mem
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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)) ⊤
convert_6 :
  Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤)
    (Submodule.Quotient.mk ((↑x : ℕ → N) (k + n + 1)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤)
    (Submodule.Quotient.mk ((↑x : ℕ → N) (k + n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤)
⊢ (↑x : ℕ → N) (k + n + 1) - (↑x : ℕ → N) (k + n) ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤

Tactic:
rw [← Submodule.Quotient.eq]

Premises used: Submodule.Quotient.eq
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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)) ⊤
⊢ k + n ≤ k + n + 1

Tactic:
lia
-- Module: Mathlib.RingTheory.AdicCompletion.Exactness
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)) ⊤
⊢ Eq (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤)
    (Submodule.Quotient.mk ((↑x : ℕ → N) (k + n + 1)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤)
    (Submodule.Quotient.mk ((↑x : ℕ → N) (k + n)) : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤)

Tactic:
exact AdicCauchySequence.mk_eq_mk (by lia) _

Premises used: AdicCompletion.AdicCauchySequence.mk_eq_mk