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
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)) ⊤
⊢ d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤

Tactic:
exact (Submodule.smul_mono_left (Ideal.pow_le_pow_right (by lia))) hdmem

Premises used: Ideal.pow_le_pow_right, Submodule.smul_mono_left
-- 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 : Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) ((f : (a : M) → N) (y - yₙ) : N)
hincl : I ^ (k + n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
h₁ : HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤ = HSMul.hSMul (β := Submodule R M) (I ^ (k + n - k)) ⊤
convert_to : y - yₙ ∈ HSMul.hSMul (β := Submodule R M) (I ^ (k + n - k)) ⊤
⊢ y - yₙ ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤

Tactic:
convert_to y - yₙ ∈ (I ^ (k + n - k) • ⊤ : Submodule R M)

Premises used: HSub.hSub, HPow.hPow, HAdd.hAdd, 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
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 : Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) ((f : (a : M) → N) (y - yₙ) : N)
hincl : I ^ (k + n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
⊢ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤ = HSMul.hSMul (β := Submodule R M) (I ^ (k + n - k)) ⊤

Tactic:
simp
-- 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 : Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) ((f : (a : M) → N) (y - yₙ) : N)
hincl : I ^ (k + n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
rw : y - yₙ ∈ Submodule.comap f (I ^ (k + n - k) • f.range)
⊢ y - yₙ ∈ HSMul.hSMul (β := Submodule R M) (I ^ (k + n - k)) ⊤

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

Premises used: Submodule.comap_map_eq_of_injective, Submodule.map_smul'', Submodule.map_top, HSub.hSub, HPow.hPow, HAdd.hAdd, 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
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 : Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) ((f : (a : M) → N) (y - yₙ) : N)
hincl : I ^ (k + n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
⊢ k + n ≥ 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
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 : Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) ((f : (a : M) → N) (y - yₙ) : N)
hincl : I ^ (k + n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
a :
  Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ⊓ f.range) ((f : (a : M) → N) (y - yₙ) : N)
⊢ Membership.mem (α := N) (I ^ (k + n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range))
    ((f : (a : M) → N) (y - yₙ) : N)

Tactic:
rw [← hkn (k + n) (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
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 : Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) ((f : (a : M) → N) (y - yₙ) : N)
hincl : I ^ (k + n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
⊢ Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ⊓ f.range) ((f : (a : M) → N) (y - yₙ) : N)

Tactic:
⟨h, ⟨y - yₙ, rfl⟩⟩

Premises used: Set.Mem, setOf, HSub.hSub, Set.inter, And.intro, Exists.intro, 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)) ⊤
h : Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) ((f : (a : M) → N) (y - yₙ) : N)
hincl : I ^ (k + n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
⊢ Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ⊓ f.range) ((f : (a : M) → N) (y - yₙ) : N)

Tactic:
exact ⟨h, ⟨y - yₙ, 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)) ⊤
h : Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) ((f : (a : M) → N) (y - yₙ) : N)
hincl : I ^ (k + n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range) ≤ I ^ (k + n - k) • f.range
hyyₙ : y - yₙ ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
⊢ Membership.mem (γ := Set ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤))
    {d : ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) |
      HSub.hSub (α := N) ((f : (a : M) → N) (yₙ + (↑d : M)) : N) ((↑x : ℕ → N) (k + n + 1)) ∈
        HSMul.hSMul (β := Submodule R N) (I ^ (k + n + 1)) ⊤}
    (Subtype.mk (p := fun (x : M) ↦ x ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) (y - yₙ) hyyₙ)

Tactic:
simpa [hd, Nat.succ_eq_add_one, Nat.add_assoc]

Premises used: Nat.succ_eq_add_one, Nat.add_assoc
-- 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)
x_1 n : ℕ
rw :
  Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ (k + n)) ⊤)
    ((g : (a : N) → P) ((↑x : ℕ → N) (k + n)) : P)
⊢ Membership.mem (α := P) (Submodule.map g (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤))
    ((g : (a : N) → P) ((↑x : ℕ → N) (k + n)) : P)

Tactic:
rw [map_smul'', Submodule.map_top, range_eq_top.mpr hg]

Premises used: Iff.mpr, Submodule.map_smul'', Submodule.map_top, LinearMap.range_eq_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
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)
x_1 n : ℕ
⊢ Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ (k + n)) ⊤)
    ((g : (a : N) → P) ((↑x : ℕ → N) (k + n)) : P)

Tactic:
hker (k + n)

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
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)
x_1 n : ℕ
⊢ Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ (k + n)) ⊤)
    ((g : (a : N) → P) ((↑x : ℕ → N) (k + n)) : P)

Tactic:
exact hker (k + n)

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
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)
x_1 n : ℕ
obtain :
  ∀ (d : N) (hdmem : d ∈ (↑(HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) : Set N))
    (hd : Eq (α := P) ((g : (a : N) → P) d : P) ((g : (a : N) → P) ((↑x : ℕ → N) (k + n)) : P)),
    ∃ (d : N) (y : M),
      d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + n) - d
⊢ ∃ (d : N) (y : M),
    d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + n) - d

Tactic:
obtain ⟨d, hdmem, hd⟩ := h1 n
-- 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)
x_1 n : ℕ
d : N
hdmem : d ∈ (↑(HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) : Set N)
hd : Eq (α := P) ((g : (a : N) → P) d : P) ((g : (a : N) → P) ((↑x : ℕ → N) (k + n)) : P)
⊢ Eq (α := P) ((g : (a : N) → P) ((↑x : ℕ → N) (k + n) - d) : P) (0 : P)

Tactic:
simp [hd]
-- 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)
x_1 n : ℕ
d : N
hdmem : d ∈ (↑(HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) : Set N)
hd : Eq (α := P) ((g : (a : N) → P) d : P) ((g : (a : N) → P) ((↑x : ℕ → N) (k + n)) : P)
obtain :
  ∀ (y : M) (hdy : (f : (a : M) → N) y = (↑x : ℕ → N) (k + n) - d),
    ∃ (d : N) (y : M),
      d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + n) - d
⊢ ∃ (d : N) (y : M),
    d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + n) - d

Tactic:
obtain ⟨y, hdy⟩ := (hfg (x (k + n) - d)).mp (by simp [hd])

Premises used: HSub.hSub, HAdd.hAdd, Iff.mp, Subtype.val
-- 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)
x_1 n : ℕ
d : N
hdmem : d ∈ (↑(HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤) : Set N)
hd : Eq (α := P) ((g : (a : N) → P) d : P) ((g : (a : N) → P) ((↑x : ℕ → N) (k + n)) : P)
y : M
hdy : (f : (a : M) → N) y = (↑x : ℕ → N) (k + n) - d
⊢ ∃ (d : N) (y : M),
    d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + n) - d

Tactic:
⟨d, y, hdmem, hdy⟩

Premises used: And.intro, Exists.intro