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)
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:
exact ⟨d, y, hdmem, hdy⟩
-- 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 : ℕ
d : N :=
  Exists.choose (p := fun (d : N) ↦
    ∃ (y : M), d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + 0)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + 0) - d) ⋯
y : M :=
  Exists.choose (p := fun (y : M) ↦
    Exists.choose (p := fun (d : N) ↦
          ∃ (y : M),
            d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + 0)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + 0) - d)
          ⋯ ∈
        HSMul.hSMul (β := Submodule R N) (I ^ (k + 0)) ⊤ ∧
      (f : (a : M) → N) y =
        (↑x : ℕ → N) (k + 0) -
          Exists.choose (p := fun (d : N) ↦
            ∃ (y : M),
              d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + 0)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + 0) - d)
            ⋯)
    ⋯
hdy : (f : (a : M) → N) y = (↑x : ℕ → N) (k + 0) - d
hdmem :
  Exists.choose (p := fun (d : N) ↦
      ∃ (y : M), d ∈ HSMul.hSMul (β := Submodule R N) (I ^ (k + 0)) ⊤ ∧ (f : (a : M) → N) y = (↑x : ℕ → N) (k + 0) - d)
      ⋯ ∈
    HSMul.hSMul (β := Submodule R N) (I ^ (k + 0)) ⊤
⊢ Membership.mem (γ := Set M)
    {a : M |
      HSub.hSub (α := N) ((f : (a : M) → N) a : N) ((↑x : ℕ → N) (k + Nat.zero)) ∈
        HSMul.hSMul (β := Submodule R N) (I ^ (k + Nat.zero)) ⊤}
    y

Tactic:
simpa [hdy]
-- 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)
⊢ 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)

Tactic:
LinearMap.exact_of_comp_eq_zero_of_ker_le_range ?_ (fun y ↦ ?_)

Premises used: LinearMap.exact_of_comp_eq_zero_of_ker_le_range
-- 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)
refine_1 : map I g ∘ₗ map I f = 0
refine_2 : ∀ y ∈ (map I g).ker, y ∈ (map I f).range
⊢ 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)

Tactic:
refine LinearMap.exact_of_comp_eq_zero_of_ker_le_range ?_ (fun y ↦ ?_)

Premises used: LinearMap.exact_of_comp_eq_zero_of_ker_le_range
-- 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)
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
refine_1₂ refine_1₃ :
  Eq.{u + 1} (α :=
    LinearMap (R := AdicCompletion I R) (RingHom.id (AdicCompletion I R)) (AdicCompletion I M) (AdicCompletion I P)) 0 0
⊢ map I g ∘ₗ map I f = 0

Tactic:
rw [map_comp, hfg.linearMap_comp_eq_zero, AdicCompletion.map_zero]

Premises used: AdicCompletion.map_comp, Function.Exact.linearMap_comp_eq_zero, AdicCompletion.map_zero
-- 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)
y : AdicCompletion I N
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)
⊢ y ∈ (map I g).ker → y ∈ (map I f).range

Tactic:
apply AdicCompletion.induction_on I N y (fun b ↦ ?_)

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
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)
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)
⊢ 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)

Premises used: LinearMap.range, Ideal.exists_pow_inf_eq_pow_smul
-- 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)
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)
n : ℕ
⊢ Membership.mem (α := P) (HSMul.hSMul (β := Submodule R P) (I ^ n) ⊤) ((g : (a : N) → P) ((↑b : ℕ → N) n) : P)

Tactic:
simpa using congrArg (fun x ↦ x.val n) hz

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
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)
⊢ ∀ (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
-- 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)
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)

Tactic:
⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩

Premises used: Set.Mem, setOf, AdicCompletion.mk, Exists.intro, Set.range, Subtype.val, AdicCompletion.AdicCauchySequence.mk, 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)
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) ⊤]
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)) ⋯)) :
      AdicCompletion I N)
    ((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:
refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩
-- 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)
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) ⊤]

Tactic:
fun n ↦ SModEq.symm ?_

Premises used: SModEq.symm
-- 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)
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 + 1) ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) n [SMOD
      HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]
⊢ ∀ (n : ℕ),
    (fun (n : ℕ) ↦ (↑(a n) : M)) n ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) (n + 1) [SMOD
      HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
refine fun n ↦ SModEq.symm ?_

Premises used: SModEq.symm
-- 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)
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 + 1) ≡ (fun (n : ℕ) ↦ (↑(a n) : M)) n [SMOD
    HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤]

Tactic:
simp [a, mapExactAux, SModEq]

Premises used: _private.0.AdicCompletion.mapExactAux, SModEq
-- 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)
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_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)) ⋯))) :
          (n : ℕ) → N ⧸ I ^ n • ⊤)
        n)
      ((↑((mk I N : (a : AdicCauchySequence I N) → AdicCompletion I N) b) : (n : ℕ) → N ⧸ I ^ n • ⊤) n)
⊢ 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)

Tactic:
ext 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)
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 : ℕ
h :
  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) ⊤)
⊢ n ≤ k + n

Tactic:
lia