awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun (n : ℕ) ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (f m) (f n)
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 - 0 ∈ I ^ n
have h : (1 + -(x * y)) * L - 1 ∈ I ^ n
Tactic: rw [sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun (n : ℕ) ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (f m) (f n)
L : R
n : ℕ
hL : f n - L ∈ I ^ n
this : (1 - x * y) * f n - 1 ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 ∈ I ^ n
have h : (1 + -(x * y)) * L - 1 = (1 - x * y) * f n - 1 - (1 + -(x * y)) * (f n - L)
Tactic: convert! Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun (n : ℕ) ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (f m) (f n)
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 ∈ I ^ n
have h : (1 - x * y) * f n - 1 ∈ I ^ n
Tactic: suffices (1 - x * y) * f n - 1 ∈ I ^ n by
    convert! Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1
    ring
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun (n : ℕ) ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (f m) (f n)
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 - x * y) * f n - 1 ∈ I ^ n
have h : ∀ (hL : f 0 - L ∈ HPow.hPow (β := ℕ) I 0), (1 - x * y) * f 0 - 1 ∈ HPow.hPow (β := ℕ) I 0
Tactic: cases n
Cleared hypotheses: n, hL
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun (n : ℕ) ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (f m) (f n)
L : R
n : ℕ
hL : f n - L ∈ I ^ n
h : ∀ (hL : f 0 - L ∈ HPow.hPow (β := ℕ) I 0), (1 - x * y) * f 0 - 1 ∈ HPow.hPow (β := ℕ) I 0
⊢ (1 - x * y) * f n - 1 ∈ I ^ n
have h₁ : ∀ (n : ℕ) (hL : f (n + 1) - L ∈ I ^ (n + 1)), (1 - x * y) * f (n + 1) - 1 ∈ I ^ (n + 1)
Tactic: cases n
Cleared hypotheses: n, hL
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun (n : ℕ) ↦ ∑ i ∈ range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (f m) (f n)
L : R
n : ℕ
hL : f (n + 1) - L ∈ I ^ (n + 1)
⊢ (1 - x * y) * f (n + 1) - 1 ∈ I ^ (n + 1)
have h : x ^ (n + 1) * y ^ (n + 1) ∈ I ^ (n + 1)
Tactic: rw [← neg_sub _ (1 : R), neg_mul, mul_geom_sum, neg_sub, sub_sub, add_comm (_ ^ _), ← sub_sub,
      sub_self, zero_sub, @neg_mem_iff, mul_pow]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
h : c = b + a
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
    ((↑((ofPowSMul I M a : (a : AdicCompletion I ↥(I ^ a • ⊤)) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤) c :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
    ((powSMulQuotInclusion I M h ⊤ : (a : ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤) → M ⧸ I ^ c • ⊤)
        ((↑x : (n : ℕ) → ↥(I ^ a • ⊤) ⧸ I ^ n • ⊤) b) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
have rw : Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
  ((LinearMap.reduceModIdeal (I ^ c) (HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤).subtype :
        (a : ↥(I ^ a • ⊤) ⧸ I ^ c • ⊤) → M ⧸ I ^ c • ⊤)
      ((↑x : (n : ℕ) → ↥(I ^ a • ⊤) ⧸ I ^ n • ⊤) c) :
    M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
  ((powSMulQuotInclusion I M h ⊤ : (a : ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤) → M ⧸ I ^ c • ⊤)
      ((transitionMap I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤) sorry :
          (a_1 : ↥(I ^ a • ⊤) ⧸ I ^ c • ⊤) → ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤)
        ((↑x : (n : ℕ) → ↥(I ^ a • ⊤) ⧸ I ^ n • ⊤) c)) :
    M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
Tactic: rw [← x.prop (show b ≤ c by lia), map_val_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c : ℕ
h : c = b + a
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
    ((LinearMap.reduceModIdeal (I ^ c) (HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤).subtype :
          (a : ↥(I ^ a • ⊤) ⧸ I ^ c • ⊤) → M ⧸ I ^ c • ⊤)
        ((↑x : (n : ℕ) → ↥(I ^ a • ⊤) ⧸ I ^ n • ⊤) c) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
    ((powSMulQuotInclusion I M h ⊤ : (a : ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤) → M ⧸ I ^ c • ⊤)
        ((transitionMap I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤) ⋯ :
            (a_1 : ↥(I ^ a • ⊤) ⧸ I ^ c • ⊤) → ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤)
          ((↑x : (n : ℕ) → ↥(I ^ a • ⊤) ⧸ I ^ n • ⊤) c)) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
have refine : ∀ (z : ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)),
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
    ((LinearMap.reduceModIdeal (I ^ c) (HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤).subtype :
          (a : ↥(I ^ a • ⊤) ⧸ I ^ c • ⊤) → M ⧸ I ^ c • ⊤)
        (Submodule.Quotient.mk z) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
    ((powSMulQuotInclusion I M h ⊤ : (a : ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤) → M ⧸ I ^ c • ⊤)
        ((transitionMap I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤) sorry :
            (a_1 : ↥(I ^ a • ⊤) ⧸ I ^ c • ⊤) → ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤)
          (Submodule.Quotient.mk z)) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
Tactic: refine Quotient.induction_on _ (x.val c) fun z ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b : ℕ
h : a ≤ b
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ b) ⊤)
⊢ Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
    ((↑((ofPowSMul I M b : (a : AdicCompletion I ↥(I ^ b • ⊤)) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤) a) 0
have rw : Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
  ((LinearMap.reduceModIdeal (I ^ a) (HSMul.hSMul (β := Submodule R M) (I ^ b) ⊤).subtype :
        (a_1 : ↥(I ^ b • ⊤) ⧸ I ^ a • ⊤) → M ⧸ I ^ a • ⊤)
      ((↑x : (n : ℕ) → ↥(I ^ b • ⊤) ⧸ I ^ n • ⊤) a) :
    M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
  (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
Tactic: rw [map_val_apply]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b : ℕ
h : a ≤ b
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ b) ⊤)
⊢ Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
    ((LinearMap.reduceModIdeal (I ^ a) (HSMul.hSMul (β := Submodule R M) (I ^ b) ⊤).subtype :
          (a_1 : ↥(I ^ b • ⊤) ⧸ I ^ a • ⊤) → M ⧸ I ^ a • ⊤)
        ((↑x : (n : ℕ) → ↥(I ^ b • ⊤) ⧸ I ^ n • ⊤) a) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
    (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
have refine : ∀ (z : ↥(HSMul.hSMul (β := Submodule R M) (I ^ b) ⊤)),
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
    ((LinearMap.reduceModIdeal (I ^ a) (HSMul.hSMul (β := Submodule R M) (I ^ b) ⊤).subtype :
          (a_1 : ↥(I ^ b • ⊤) ⧸ I ^ a • ⊤) → M ⧸ I ^ a • ⊤)
        (Submodule.Quotient.mk z) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
    (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
Tactic: refine Quotient.induction_on _ (x.val a) fun z ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
⊢ Function.Injective (α := AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) (β := AdicCompletion I M)
    (⇑(ofPowSMul I M n) : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M)
have rw : ∀ (m : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)),
  Eq (α := AdicCompletion I M)
      ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) m : AdicCompletion I M)
      (0 : AdicCompletion I M) →
    m = 0
Tactic: rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
hx :
  Eq (α := AdicCompletion I M)
    ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) x : AdicCompletion I M)
    (0 : AdicCompletion I M)
⊢ x = 0
have h : ∀ (i : ℕ), (↑x : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i = (↑0 : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
hx :
  Eq (α := AdicCompletion I M)
    ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) x : AdicCompletion I M)
    (0 : AdicCompletion I M)
i : ℕ
⊢ (↑x : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i = (↑0 : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i
have hx₁ : ∀ (n_1 : ℕ),
  Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n_1) ⊤)
    ((↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤) n_1)
    0
Tactic: simp only [AdicCompletion.ext_iff, val_zero, Pi.zero_apply] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
i : ℕ
hx :
  ∀ (n_1 : ℕ),
    Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n_1) ⊤)
      ((↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤)
        n_1)
      0
⊢ (↑x : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i = (↑0 : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i
have hx₁ : Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ (i + n)) ⊤)
  ((↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤)
    (i + n))
  0
Tactic: specialize hx (i + n)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
i : ℕ
hx :
  Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ (i + n)) ⊤)
    ((↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤)
      (i + n))
    0
⊢ i + n = i + n
have rw : n + i = n + i
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
i : ℕ
hx :
  Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ (i + n)) ⊤)
    ((↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) x) : (n : ℕ) → M ⧸ I ^ n • ⊤)
      (i + n))
    0
⊢ (↑x : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i = (↑0 : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i
have hx₁ : (↑x : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i = 0
Tactic: rw [ofPowSMul_val_apply I (by rw [add_comm]),
    LinearMap.map_eq_zero_iff _ (powSMulQuotInclusion_injective ..)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
i j : ℕ
h : i ≤ j
⊢ Eq.{u_2 + 1} (α :=
    ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ⧸
      HSMul.hSMul (β := Submodule R ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) (I ^ i) ⊤)
    ((transitionMap I (↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) h :
        (a : ↥(I ^ n • ⊤) ⧸ I ^ j • ⊤) → ↥(I ^ n • ⊤) ⧸ I ^ i • ⊤)
      ((fun (i : ℕ) ↦ ofValEqZeroAux I ⋯ hxn) j))
    ((fun (i : ℕ) ↦ ofValEqZeroAux I ⋯ hxn) i)
have obtain : ∀ (k : ℕ) (h : i ≤ i + k),
  Eq.{u_2 + 1} (α :=
    ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ⧸
      HSMul.hSMul (β := Submodule R ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) (I ^ i) ⊤)
    ((transitionMap I (↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) h :
        (a : ↥(I ^ n • ⊤) ⧸ I ^ (i + k) • ⊤) → ↥(I ^ n • ⊤) ⧸ I ^ i • ⊤)
      ((fun (i : ℕ) ↦ ofValEqZeroAux I sorry hxn) (i + k)))
    ((fun (i : ℕ) ↦ ofValEqZeroAux I sorry hxn) i)
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
a b c n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
i k : ℕ
h : i ≤ i + k
⊢ Eq.{u_2 + 1} (α :=
    ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ⧸
      HSMul.hSMul (β := Submodule R ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) (I ^ i) ⊤)
    ((transitionMap I (↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) h :
        (a : ↥(I ^ n • ⊤) ⧸ I ^ (i + k) • ⊤) → ↥(I ^ n • ⊤) ⧸ I ^ i • ⊤)
      ((fun (i : ℕ) ↦ ofValEqZeroAux I ⋯ hxn) (i + k)))
    ((fun (i : ℕ) ↦ ofValEqZeroAux I ⋯ hxn) i)
have rw : (factorPow I M sorry : (a : M ⧸ I ^ (i + k + n) • ⊤) → M ⧸ I ^ (i + n) • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (i + k + n)) =
  (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (i + n)
Tactic: rw [← (powSMulQuotInclusion_injective I (by rfl) ⊤).eq_iff, ofValEqZeroAux_prop,
      ← LinearMap.comp_apply, ← factorPow_comp_powSMulQuotInclusion I (by rfl)
      (show i + k + n = k + (i + n) by ring), LinearMap.comp_apply, ofValEqZeroAux_prop]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
⊢ (ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn) = x
have h : ∀ (i : ℕ),
  (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      i =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
i : ℕ
⊢ (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      i =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
have pos : ∀ (h : n ≤ i),
  (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      i =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
Tactic: by_cases! h : n ≤ i
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
i : ℕ
pos :
  ∀ (h : n ≤ i),
    (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
          (n : ℕ) → M ⧸ I ^ n • ⊤)
        i =
      (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
⊢ (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      i =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
have neg : ∀ (h : i < n),
  (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      i =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
Tactic: by_cases! h : n ≤ i
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
i : ℕ
h : n ≤ i
⊢ (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      i =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
have pos : ∀ (k : ℕ) (h : n ≤ k + n),
  (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      (k + n) =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n)
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
k : ℕ
h : n ≤ k + n
⊢ (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      (k + n) =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n)
have pos : (powSMulQuotInclusion I M sorry ⊤ : (a : ↥(I ^ n • ⊤) ⧸ I ^ k • ⊤) → M ⧸ I ^ (k + n) • ⊤)
    ((↑(ofValEqZero I hxn) : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) k) =
  (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n)
Tactic: rw [ofPowSMul_val_apply _ (by rfl), ofValEqZero, ofValEqZeroAux_prop]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
k : ℕ
h : n ≤ k + n
pos :
  (powSMulQuotInclusion I M ⋯ ⊤ : (a : ↥(I ^ n • ⊤) ⧸ I ^ k • ⊤) → M ⧸ I ^ (k + n) • ⊤)
      ((↑(ofValEqZero I hxn) : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) k) =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n)
⊢ (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      (k + n) =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n)
have pos₁ : (powSMulQuotInclusion I M sorry ⊤ : (a : ↥(I ^ n • ⊤) ⧸ I ^ k • ⊤) → M ⧸ I ^ (k + n) • ⊤)
    ((↑(Subtype.mk (p :=
            fun
              (f :
                (n_1 : ℕ) →
                  ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ⧸
                    HSMul.hSMul (β := Submodule R ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) (I ^ n_1) ⊤) ↦
            ∀ {m n_1 : ℕ} (hmn : m ≤ n_1),
              (transitionMap I (↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) hmn :
                    (a : ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) → ↥(I ^ n • ⊤) ⧸ I ^ m • ⊤)
                  (f n_1) =
                f m)
            (fun (i : ℕ) ↦ ofValEqZeroAux I sorry hxn) sorry) :
        (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤)
      k) =
  (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n)
Tactic: rw [ofPowSMul_val_apply _ (by rfl), ofValEqZero, ofValEqZeroAux_prop]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
k : ℕ
h : n ≤ k + n
pos :
  (powSMulQuotInclusion I M ⋯ ⊤ : (a : ↥(I ^ n • ⊤) ⧸ I ^ k • ⊤) → M ⧸ I ^ (k + n) • ⊤)
      ((↑(ofValEqZero I hxn) : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) k) =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n)
pos₁ :
  (powSMulQuotInclusion I M ⋯ ⊤ : (a : ↥(I ^ n • ⊤) ⧸ I ^ k • ⊤) → M ⧸ I ^ (k + n) • ⊤)
      ((↑(Subtype.mk (p :=
              fun
                (f :
                  (n_1 : ℕ) →
                    ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) ⧸
                      HSMul.hSMul (β := Submodule R ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) (I ^ n_1) ⊤) ↦
              ∀ {m n_1 : ℕ} (hmn : m ≤ n_1),
                (transitionMap I (↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)) hmn :
                      (a : ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) → ↥(I ^ n • ⊤) ⧸ I ^ m • ⊤)
                    (f n_1) =
                  f m)
              (fun (i : ℕ) ↦ ofValEqZeroAux I ⋯ hxn) ⋯) :
          (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤)
        k) =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n)
⊢ (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      (k + n) =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n)
have pos₂ : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n) = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n)
Tactic: rw [ofPowSMul_val_apply _ (by rfl), ofValEqZero, ofValEqZeroAux_prop]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
i : ℕ
h : i < n
⊢ (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      i =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
have neg : 0 = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
Tactic: rw [ofPowSMul_val_apply_eq_zero _ h.le, ← x.prop h.le, hxn, _root_.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdicCompletion.Completeness (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
x : AdicCompletion I M
hxn : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
i : ℕ
h : i < n
neg : 0 = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
⊢ (↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn)) :
        (n : ℕ) → M ⧸ I ^ n • ⊤)
      i =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) i
have neg₁ : Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤)
  ((transitionMap I M sorry : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ i • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
    M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤)
Tactic: rw [ofPowSMul_val_apply_eq_zero _ h.le, ← x.prop h.le, hxn, _root_.map_zero]