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)
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) ∈
    HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤
have 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))
Tactic: convert_to x (k + n + 1) - x (k + n) - d - (f yₙ - x (k + n)) ∈ I ^ (k + 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)
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))
⊢ HSub.hSub (β := N) ((↑x : ℕ → N) (k + n + 1) - d) ((f : (a : M) → N) yₙ : N) ∈
    HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤
have 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)) ⊤
Tactic: convert_to x (k + n + 1) - x (k + n) - d - (f yₙ - x (k + n)) ∈ I ^ (k + 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)
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)) ⊤
have convert_6 : (↑x : ℕ → N) (k + n + 1) - (↑x : ℕ → N) (k + n) ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤
Tactic: refine Submodule.sub_mem _ (Submodule.sub_mem _ ?_ ?_) hyₙ
-- 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)) ⊤
convert_6 : (↑x : ℕ → N) (k + n + 1) - (↑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)) ⊤
have convert_6₁ : d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤
Tactic: refine Submodule.sub_mem _ (Submodule.sub_mem _ ?_ ?_) hyₙ
-- 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)) ⊤
⊢ (↑x : ℕ → N) (k + n + 1) - (↑x : ℕ → N) (k + n) ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤
have 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)) ⊤)
Tactic: rw [← Submodule.Quotient.eq]
-- 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)) ⊤
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
⊢ y - yₙ ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
have h₁ : HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤ = HSMul.hSMul (β := Submodule R M) (I ^ (k + n - k)) ⊤
Tactic: convert_to y - yₙ ∈ (I ^ (k + n - k) • ⊤ : Submodule R 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)
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)) ⊤
⊢ y - yₙ ∈ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤
have convert_to : y - yₙ ∈ HSMul.hSMul (β := Submodule R M) (I ^ (k + n - k)) ⊤
Tactic: convert_to y - yₙ ∈ (I ^ (k + n - k) • ⊤ : Submodule R 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)
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
⊢ y - yₙ ∈ HSMul.hSMul (β := Submodule R M) (I ^ (k + n - k)) ⊤
have rw : y - yₙ ∈ Submodule.comap f (I ^ (k + n - k) • f.range)
Tactic: rw [← Submodule.comap_map_eq_of_injective hf (I ^ (k + n - k) • ⊤ : 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
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) (I ^ (k + n - k) • (HSMul.hSMul (β := Submodule R N) (I ^ k) ⊤ ⊓ f.range))
    ((f : (a : M) → N) (y - yₙ) : N)
have a : Membership.mem (α := N) (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ⊓ f.range) ((f : (a : M) → N) (y - yₙ) : N)
Tactic: rw [← hkn (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)
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) (Submodule.map g (HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤))
    ((g : (a : N) → P) ((↑x : ℕ → N) (k + n)) : P)
have rw : Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ (k + n)) ⊤)
  ((g : (a : N) → P) ((↑x : ℕ → N) (k + n)) : P)
Tactic: rw [map_smul'', Submodule.map_top, range_eq_top.mpr hg]
-- 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)
x_1 n : ℕ
⊢ ∃ (d : N) (y : M),
    d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + n) - d
have 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
Tactic: obtain ⟨d, hdmem, hd⟩ := h1 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)
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)
⊢ ∃ (d : N) (y : M),
    d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + n)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + n) - d
have 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
Tactic: obtain ⟨y, hdy⟩ := (hfg (x (k + n) - d)).mp (by simp [hd])
-- 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)
⊢ Function.Exact (M := AdicCompletion I M) (N := AdicCompletion I N) (P := AdicCompletion I P)
    (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)
    (⇑(map I g) : (a : AdicCompletion I N) → AdicCompletion I P)
have refine_1 : map I g ∘ₗ map I f = 0
Tactic: refine LinearMap.exact_of_comp_eq_zero_of_ker_le_range ?_ (fun y ↦ ?_)
-- 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)
refine_1 : map I g ∘ₗ map I f = 0
⊢ Function.Exact (M := AdicCompletion I M) (N := AdicCompletion I N) (P := AdicCompletion I P)
    (⇑(map I f) : (a : AdicCompletion I M) → AdicCompletion I N)
    (⇑(map I g) : (a : AdicCompletion I N) → AdicCompletion I P)
have refine_2 : ∀ y ∈ (map I g).ker, y ∈ (map I f).range
Tactic: refine LinearMap.exact_of_comp_eq_zero_of_ker_le_range ?_ (fun y ↦ ?_)
-- 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)
⊢ map I g ∘ₗ map I f = 0
have refine_1 : map I (g ∘ₗ f) = 0
Tactic: rw [map_comp, hfg.linearMap_comp_eq_zero, AdicCompletion.map_zero]
-- 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)
refine_1 : map I (g ∘ₗ f) = 0
⊢ map I g ∘ₗ map I f = 0
have refine_1₁ : Eq (α :=
  LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I M) (AdicCompletion I P))
  (map I 0) 0
Tactic: rw [map_comp, hfg.linearMap_comp_eq_zero, AdicCompletion.map_zero]
-- 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)
refine_1 : map I (g ∘ₗ f) = 0
refine_1₁ :
  Eq (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I M) (AdicCompletion I P))
    (map I 0) 0
⊢ map I g ∘ₗ map I f = 0
have refine_1₂ : Eq.{u + 1} (α :=
  LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I M) (AdicCompletion I P)) 0 0
Tactic: rw [map_comp, hfg.linearMap_comp_eq_zero, AdicCompletion.map_zero]