awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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) ⊤)
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) ⊤)
⊢ 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

Tactic:
rw [map_val_apply]

Premises used: AdicCompletion.map_val_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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) ⊤)

Tactic:
Quotient.induction_on _ (x.val a) fun z ↦ ?_

Premises used: Submodule.Quotient.induction_on, HPow.hPow, HSMul.hSMul, Top.top, Subtype.val
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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) ⊤)
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) ⊤)
⊢ 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:
refine Quotient.induction_on _ (x.val a) fun z ↦ ?_
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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) ⊤)
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:
simpa using pow_smul_top_le _ _ h z.prop

Premises used: Submodule.pow_smul_top_le, Subtype.prop
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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 : ℕ
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
⊢ 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)

Tactic:
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']

Premises used: LinearMap.ker_eq_bot, LinearMap.ker_eq_bot'
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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)
h : ∀ (i : ℕ), (↑x : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i = (↑0 : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i
⊢ x = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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 : ℕ
⊢ ∀ (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

Premises used: AdicCompletion.ext_iff, Pi.zero_apply, AdicCompletion.val_zero
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
⊢ 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)

Premises used: HAdd.hAdd
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
rw rw₁ : n + i = n + i
⊢ i + n = i + n

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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

Tactic:
rw [ofPowSMul_val_apply I (by rw [add_comm]),
    LinearMap.map_eq_zero_iff _ (powSMulQuotInclusion_injective ..)] at hx

Premises used: Submodule.powSMulQuotInclusion_injective, AdicCompletion.ofPowSMul_val_apply, LinearMap.map_eq_zero_iff
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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 : (↑x : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i = 0
⊢ (↑x : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i = (↑0 : (n_1 : ℕ) → ↥(I ^ n • ⊤) ⧸ I ^ n_1 • ⊤) i

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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 : ℕ
x : AdicCompletion I M
h : c = b + a
ha : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) a = 0
⊢ a ≤ c

Tactic:
lia
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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 : ℕ
x : AdicCompletion I M
h : c = b + a
ha : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) a = 0
⊢ ∃ (t :
    ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤) ⧸
      HSMul.hSMul (β := Submodule R ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)) (I ^ b) ⊤),
    (powSMulQuotInclusion I M h ⊤ : (a : ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤) → M ⧸ I ^ c • ⊤) t = (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) c

Tactic:
simpa [← LinearMap.mem_range, range_powSMulQuotInclusion] using
    (val_apply_mem_smul_top_iff I (show a ≤ c by lia)).mpr ha

Premises used: Iff.mpr, AdicCompletion.val_apply_mem_smul_top_iff, Submodule.range_powSMulQuotInclusion, LinearMap.mem_range
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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 : ℕ
x : AdicCompletion I M
h : c = b + a
ha : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) a = 0
⊢ (powSMulQuotInclusion I M h ⊤ : (a : ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤) → M ⧸ I ^ c • ⊤) (ofValEqZeroAux I h ha) =
    (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) c

Tactic:
Exists.choose_spec (ofValEqZeroAux_exists I h ha)

Premises used: Exists.choose_spec, Set.Mem, AdicCompletion.ofValEqZeroAux, _private.0.AdicCompletion.ofValEqZeroAux_exists
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
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 ⋯ hxn) (i + k)))
      ((fun (i : ℕ) ↦ ofValEqZeroAux I ⋯ hxn) i)
⊢ 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)

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h

Premises used: Nat.exists_eq_add_of_le, rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
⊢ i + n = i + n

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
⊢ i + k + n = k + (i + n)

Tactic:
ring
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
rw :
  (factorPow I M ⋯ : (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)
⊢ 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)

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]

Premises used: Function.Injective.eq_iff, LinearMap.comp_apply, Submodule.factorPow_comp_powSMulQuotInclusion, Top.top, Submodule.powSMulQuotInclusion_injective, _private.0.AdicCompletion.ofValEqZeroAux_prop
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
⊢ i + n ≤ i + k + n

Tactic:
lia
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
⊢ (factorPow I M ⋯ : (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:
exact x.prop (by lia)

Premises used: Subtype.prop
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
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
⊢ (ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hxn) = x

Tactic:
ext i
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
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
⊢ (↑((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
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
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)
⊢ (↑((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:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le' h

Premises used: Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
⊢ k + n = k + n

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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)
pos₂ pos₃ : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) (k + n) = (↑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)

Tactic:
rw [ofPowSMul_val_apply _ (by rfl), ofValEqZero, ofValEqZeroAux_prop]

Premises used: AdicCompletion.ofValEqZero, AdicCompletion.ofPowSMul_val_apply, _private.0.AdicCompletion.ofValEqZeroAux_prop
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
neg₁ :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤)
    ((transitionMap I M ⋯ : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ i • ⊤) ((↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤)
neg₂ :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) 0
    ((transitionMap I M ⋯ : (a : M ⧸ I ^ n • ⊤) → M ⧸ I ^ i • ⊤) 0)
neg₃ neg₄ : Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) 0 0
⊢ (↑((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:
rw [ofPowSMul_val_apply_eq_zero _ h.le, ← x.prop h.le, hxn, _root_.map_zero]

Premises used: map_zero, LT.lt.le, AdicCompletion.ofPowSMul_val_apply_eq_zero, Subtype.prop
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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 : ℕ
⊢ Eq (α := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n)))
    (LinearMap.ker (eval I M n))

Tactic:
le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ ?_)

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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 : ℕ
refine_1 :
  ∀ (x : AdicCompletion I M)
    (hx :
      Membership.mem (γ := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n))) x),
    Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n)) x
refine_2 :
  ∀ (x : AdicCompletion I M)
    (hx : Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n)) x),
    Membership.mem (γ := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n))) x
⊢ Eq (α := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n)))
    (LinearMap.ker (eval I M n))

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ ?_)

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
hx : Membership.mem (γ := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n))) x
refine_1 :
  ∀ (y : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)),
    Membership.mem (α := AdicCompletion I M) (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n))
      ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y : AdicCompletion I M)
⊢ Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n)) x

Tactic:
rcases hx with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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 : ℕ
y : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
⊢ n ≤ n

Tactic:
rfl
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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 : ℕ
y : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
refine_1 :
  Eq (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((eval I M n : (a : AdicCompletion I M) → M ⧸ I ^ n • ⊤)
        ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    (0 : M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
refine_1₁ :
  Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤)
    ((↑((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y) : (n : ℕ) → M ⧸ I ^ n • ⊤) n) 0
refine_1₂ refine_1₃ : Eq.{u_2 + 1} (α := M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ n) ⊤) 0 0
⊢ Membership.mem (α := AdicCompletion I M) (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n))
    ((ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) y : AdicCompletion I M)

Tactic:
rw [LinearMap.mem_ker, eval_apply, ofPowSMul_val_apply_eq_zero _ (by rfl)]

Premises used: LinearMap.mem_ker, AdicCompletion.ofPowSMul_val_apply_eq_zero, AdicCompletion.eval_apply
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
hx : Membership.mem (γ := Submodule R (AdicCompletion I M)) (LinearMap.ker (eval I M n)) x
⊢ (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0

Tactic:
simp only [LinearMap.mem_ker, coe_eval] at hx

Premises used: AdicCompletion.coe_eval, LinearMap.mem_ker
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
hx : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
h : (ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hx) = x
⊢ Membership.mem (γ := Submodule R (AdicCompletion I M)) (restrictScalars R (LinearMap.range (ofPowSMul I M n))) x

Tactic:
use ofValEqZero I hx

Premises used: AdicCompletion.ofValEqZero
-- Module: Mathlib.RingTheory.AdicCompletion.Completeness
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
hx : (↑x : (n : ℕ) → M ⧸ I ^ n • ⊤) n = 0
⊢ (ofPowSMul I M n : (a : AdicCompletion I ↥(I ^ n • ⊤)) → AdicCompletion I M) (ofValEqZero I hx) = x

Tactic:
simp