awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst_5 : IsAdicComplete I N
n : ℕ
h :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
      (((HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤).mkQ ∘ₗ lift I ha f ⋯ : (a_1 : M) → N ⧸ I ^ a n • ⊤) x :
        N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
      ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
⊢ (HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤).mkQ ∘ₗ lift I ha f ⋯ = f n

Tactic:
ext
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst_5 : IsAdicComplete I N
n : ℕ
x : M
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    (((HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤).mkQ ∘ₗ lift I ha f ⋯ : (a_1 : M) → N ⧸ I ^ a n • ⊤) x :
      N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    ((f n : (a_1 : M) → N ⧸ I ^ a n • ⊤) x : N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)

Tactic:
simp
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst_5 : IsAdicComplete I N
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤).mkQ ∘ₗ F = f n
a₁ :
  Eq (α := (a : M) → N) ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) F)
    ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) (lift I ha f ⋯))
⊢ F = lift I ha f ⋯

Tactic:
apply DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst_5 : IsAdicComplete I N
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤).mkQ ∘ₗ F = f n
a₁ :
  ∀ (n : ℕ) (m : M),
    Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
      (Submodule.Quotient.mk ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) F m))
      (Submodule.Quotient.mk ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) (lift I ha f ⋯) m))
⊢ Eq (α := (a : M) → N) ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) F)
    ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) (lift I ha f ⋯))

Tactic:
apply IsHausdorff.StrictMono.funext I ha

Premises used: IsHausdorff.StrictMono.funext
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
a : ℕ → ℕ
ha : StrictMono a
f : (n : ℕ) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) M (N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
hf : ∀ {m : ℕ}, Submodule.factorPow I N ⋯ ∘ₗ f (m + 1) = f m
inst_5 : IsAdicComplete I N
F : M →ₗ[R] N
hF : ∀ (n : ℕ), (HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤).mkQ ∘ₗ F = f n
n : ℕ
m : M
⊢ Eq.{u_5 + 1} (α := N ⧸ HSMul.hSMul (β := Submodule R N) (I ^ a n) ⊤)
    (Submodule.Quotient.mk ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) F m))
    (Submodule.Quotient.mk ((fun (f : M →ₗ[R] N) ↦ ((⇑f : (a : M) → N) : (a : M) → N)) (lift I ha f ⋯) m))

Tactic:
simp [← hF n]
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
M : Type u_4
inst_1 : AddCommGroup M
inst_2 : Module R M
h : IsAdicComplete.{u_1, u_4} (R := R) ⊤ M
⊢ Subsingleton M

Tactic:
h.1.subsingleton

Premises used: IsAdicComplete.toIsHausdorff, IsHausdorff.subsingleton
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
x : R
hx : x ∈ I
rw : ∀ (y : R), IsUnit (-x * y + 1)
⊢ Membership.mem (γ := Submodule R R) (jacobson ⊥) x

Tactic:
rw [← Ideal.neg_mem_iff, Ideal.mem_jacobson_bot]

Premises used: Ideal.neg_mem_iff, Ideal.mem_jacobson_bot
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
rw : IsUnit (1 + -x * y)
⊢ IsUnit (-x * y + 1)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
m n : ℕ
h : m ≤ n
simp : HSub.hSub (α := R) (∑ i ∈ range m, (x * y) ^ i) (∑ i ∈ range n, (x * y) ^ i) ∈ I ^ m
⊢ SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (f m) (f n)

Tactic:
simp only [f, smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]

Premises used: SModEq.sub_mem, smul_eq_mul, Ideal.mul_top
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
m n : ℕ
h : m ≤ n
rw : ∑ x_1 ∈ range (n - m), (x * y) ^ (m + x_1) ∈ I ^ m
⊢ HSub.hSub (α := R) (∑ i ∈ range m, (x * y) ^ i) (∑ i ∈ range n, (x * y) ^ i) ∈ I ^ m

Tactic:
rw [← add_tsub_cancel_of_le h, Finset.sum_range_add, ← sub_sub, sub_self, zero_sub,
      @neg_mem_iff]

Premises used: neg_mem_iff, sub_self, sub_sub, Finset.sum_range_add, add_tsub_cancel_of_le, zero_sub
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
m n : ℕ
h : m ≤ n
a : ∀ c ∈ range (n - m), (x * y) ^ (m + c) ∈ I ^ m
⊢ ∑ x_1 ∈ range (n - m), (x * y) ^ (m + x_1) ∈ I ^ m

Tactic:
apply Submodule.sum_mem

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
m n_1 : ℕ
h : m ≤ n_1
n : ℕ
a : n ∈ range (n_1 - m) → (x * y) ^ (m + n) ∈ I ^ m
⊢ n ∈ range (n_1 - m) → (x * y) ^ (m + n) ∈ I ^ m

Tactic:
_
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
m n_1 : ℕ
h : m ≤ n_1
n : ℕ
h_1 : n ∈ range (n_1 - m)
a : x ^ m * (x ^ n * y ^ (m + n)) ∈ I ^ m
⊢ (x * y) ^ (m + n) ∈ I ^ m

Tactic:
rw [mul_pow, pow_add, mul_assoc]

Premises used: mul_assoc, pow_add, mul_pow
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
m n_1 : ℕ
h : m ≤ n_1
n : ℕ
h_1 : n ∈ range (n_1 - m)
⊢ x ^ m * (x ^ n * y ^ (m + n)) ∈ I ^ m

Tactic:
Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)

Premises used: Set.Mem, HPow.hPow, Ideal.mul_mem_right, Ideal.pow_mem_pow
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
m n_1 : ℕ
h : m ≤ n_1
n : ℕ
h_1 : n ∈ range (n_1 - m)
⊢ x ^ m * (x ^ n * y ^ (m + n)) ∈ I ^ m

Tactic:
exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)

Premises used: HPow.hPow, Ideal.mul_mem_right, Ideal.pow_mem_pow
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
⊢ ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ m) ⊤) (f m) (f n)

Tactic:
have hf : ∀ m n, m ≤ n → f m ≡ f n [SMOD I ^ m • (⊤ : Submodule R R)] := by
    intro m n h
    simp only [f, smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]
    rw [← add_tsub_cancel_of_le h, Finset.sum_range_add, ← sub_sub, sub_self, zero_sub,
      @neg_mem_iff]
    apply Submodule.sum_mem
    intro n _
    rw [mul_pow, pow_add, mul_assoc]
    exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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)
obtain :
  ∀ (L : R) (hL : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (f n) L), IsUnit (1 + -x * y)
⊢ IsUnit (1 + -x * y)

Tactic:
obtain ⟨L, hL⟩ := IsPrecomplete.prec toIsPrecomplete @hf

Premises used: IsAdicComplete.toIsPrecomplete, IsPrecomplete.prec
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
hL : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (f n) L
rw : ∃ (b : R), (1 + -x * y) * b = 1
⊢ IsUnit (1 + -x * y)

Tactic:
rw [isUnit_iff_exists_inv]

Premises used: isUnit_iff_exists_inv
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
hL : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (f n) L
h : (1 + -x * y) * L = 1
⊢ ∃ (b : R), (1 + -x * y) * b = 1

Tactic:
use L
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
hL : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (f n) L
h : (1 + -(x * y)) * L - 1 = 0
⊢ (1 + -x * y) * L = 1

Tactic:
rw [← sub_eq_zero, neg_mul]

Premises used: sub_eq_zero, neg_mul
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
hL : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (f n) L
h : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) ((1 + -(x * y)) * L - 1) 0
⊢ (1 + -(x * y)) * L - 1 = 0

Tactic:
apply IsHausdorff.haus (toIsHausdorff : IsHausdorff I R)

Premises used: IsAdicComplete.toIsHausdorff, IsHausdorff.haus
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
hL : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (f n) L
n : ℕ
⊢ SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (f n) L

Tactic:
specialize hL n
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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 : SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (f n) L
h : ∀ (hL : f n - L ∈ I ^ n), (1 + -(x * y)) * L - 1 - 0 ∈ I ^ n
⊢ SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) ((1 + -(x * y)) * L - 1) 0

Tactic:
rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top] at hL ⊢

Premises used: SModEq.sub_mem, smul_eq_mul, Ideal.mul_top
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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 : (1 + -(x * y)) * L - 1 ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 - 0 ∈ I ^ n

Tactic:
rw [sub_zero]

Premises used: sub_zero
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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) * f n - 1 - (1 + -(x * y)) * (f n - L) ∈ I ^ n

Tactic:
Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL)

Premises used: HMul.hMul, HAdd.hAdd, Ideal.sub_mem, Ideal.mul_mem_left, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
h : (1 + -(x * y)) * L - 1 = (1 - x * y) * f n - 1 - (1 + -(x * y)) * (f n - L)
⊢ (1 + -(x * y)) * L - 1 ∈ I ^ n

Tactic:
convert! Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1

Premises used: HMul.hMul, HAdd.hAdd, Ideal.sub_mem, Ideal.mul_mem_left, OfNat.ofNat, Neg.neg
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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 = (1 - x * y) * f n - 1 - (1 + -(x * y)) * (f n - L)

Tactic:
ring
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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 : (1 - x * y) * f n - 1 ∈ I ^ n
⊢ (1 + -(x * y)) * L - 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
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
h₁ : ∀ (n : ℕ) (hL : f (n + 1) - L ∈ I ^ (n + 1)), (1 - x * y) * f (n + 1) - 1 ∈ I ^ (n + 1)
⊢ (1 - x * y) * f n - 1 ∈ I ^ n

Tactic:
cases n
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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
hL : f 0 - L ∈ HPow.hPow (β := ℕ) I 0
⊢ (1 - x * y) * f 0 - 1 ∈ HPow.hPow (β := ℕ) I 0

Tactic:
simp only [Ideal.one_eq_top, pow_zero, mem_top]

Premises used: Ideal.one_eq_top, pow_zero, Submodule.mem_top
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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)
h : x ^ (n + 1) * y ^ (n + 1) ∈ I ^ (n + 1)
⊢ (1 - x * y) * f (n + 1) - 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]

Premises used: neg_mem_iff, neg_sub, sub_self, add_comm, sub_sub, mul_geom_sum, HPow.hPow, neg_mul, OfNat.ofNat, mul_pow, zero_sub
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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)
⊢ x ^ (n + 1) * y ^ (n + 1) ∈ I ^ (n + 1)

Tactic:
Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _)

Premises used: Set.Mem, HPow.hPow, Ideal.mul_mem_right, Ideal.pow_mem_pow
-- Module: Mathlib.RingTheory.AdicCompletion.Basic
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)
⊢ x ^ (n + 1) * y ^ (n + 1) ∈ I ^ (n + 1)

Tactic:
exact Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _)

Premises used: HPow.hPow, Ideal.mul_mem_right, Ideal.pow_mem_pow
-- 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 : ℕ
h : c = b + a
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
⊢ b ≤ 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 : ℕ
h : c = b + a
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
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) ⊤) ⋯ :
            (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) ⊤)
⊢ 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) ⊤)

Tactic:
rw [← x.prop (show b ≤ c by lia), map_val_apply]

Premises used: AdicCompletion.map_val_apply, 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
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) ⊤)

Tactic:
Quotient.induction_on _ (x.val c) 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 c : ℕ
h : c = b + a
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
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) ⊤) ⋯ :
              (a_1 : ↥(I ^ a • ⊤) ⧸ I ^ c • ⊤) → ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤)
            (Submodule.Quotient.mk z)) :
        M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)
⊢ 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) ⊤)

Tactic:
refine Quotient.induction_on _ (x.val c) 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 c : ℕ
h : c = b + a
x : AdicCompletion I ↥(HSMul.hSMul (β := Submodule R M) (I ^ a) ⊤)
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) ⊤) ⋯ :
            (a_1 : ↥(I ^ a • ⊤) ⧸ I ^ c • ⊤) → ↥(I ^ a • ⊤) ⧸ I ^ b • ⊤)
          (Submodule.Quotient.mk z)) :
      M ⧸ HSMul.hSMul (β := Submodule R M) (I ^ c) ⊤)

Tactic:
simp [powSMulQuotInclusion]

Premises used: Submodule.powSMulQuotInclusion