[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : (n : ℕ) → M ⧸ I ^ n • ⊤
m n : ℕ
h : m ≤ n
⊢ I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤))
[PROOFSTEP]
rw [ker_mkQ]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : (n : ℕ) → M ⧸ I ^ n • ⊤
m n : ℕ
h : m ≤ n
⊢ I ^ n • ⊤ ≤ I ^ m • ⊤
[PROOFSTEP]
exact smul_mono (Ideal.pow_le_pow h) le_rfl
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a✝ b✝ : (n : ℕ) → M ⧸ I ^ n • ⊤
hf :
  a✝ ∈
    {f |
      ∀ {m n : ℕ} (h : m ≤ n),
        ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤)))) (f n) = f m}
hg :
  b✝ ∈
    {f |
      ∀ {m n : ℕ} (h : m ≤ n),
        ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤)))) (f n) = f m}
m n : ℕ
hmn : m ≤ n
⊢ ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤)))) ((a✝ + b✝) n) = (a✝ + b✝) m
[PROOFSTEP]
rw [Pi.add_apply, Pi.add_apply, LinearMap.map_add, hf hmn, hg hmn]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m✝ n✝ : ℕ
hmn : m✝ ≤ n✝
⊢ ↑(liftQ (I ^ n✝ • ⊤) (mkQ (I ^ m✝ • ⊤)) (_ : I ^ n✝ • ⊤ ≤ LinearMap.ker (mkQ (I ^ m✝ • ⊤)))) (OfNat.ofNat 0 n✝) =
    OfNat.ofNat 0 m✝
[PROOFSTEP]
rw [Pi.zero_apply, Pi.zero_apply, LinearMap.map_zero]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
c : R
f : (n : ℕ) → M ⧸ I ^ n • ⊤
hf :
  f ∈
    {
          toAddSubsemigroup :=
            {
              carrier :=
                {f |
                  ∀ {m n : ℕ} (h : m ≤ n),
                    ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤)))) (f n) =
                      f m},
              add_mem' :=
                (_ :
                  ∀ {a b : (n : ℕ) → M ⧸ I ^ n • ⊤},
                    a ∈
                        {f |
                          ∀ {m n : ℕ} (h : m ≤ n),
                            ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤))))
                                (f n) =
                              f m} →
                      b ∈
                          {f |
                            ∀ {m n : ℕ} (h : m ≤ n),
                              ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤))))
                                  (f n) =
                                f m} →
                        ∀ (m n : ℕ) (hmn : m ≤ n),
                          ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤))))
                              ((a + b) n) =
                            (a + b) m) },
          zero_mem' :=
            (_ :
              ∀ {m n : ℕ} (hmn : m ≤ n),
                ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤))))
                    (OfNat.ofNat 0 n) =
                  OfNat.ofNat 0 m) }.toAddSubsemigroup.carrier
m n : ℕ
hmn : m ≤ n
⊢ ↑(liftQ (I ^ n • ⊤) (mkQ (I ^ m • ⊤)) (_ : I ^ n • ⊤ ≤ LinearMap.ker (mkQ (I ^ m • ⊤)))) ((c • f) n) = (c • f) m
[PROOFSTEP]
rw [Pi.smul_apply, Pi.smul_apply, LinearMap.map_smul, hf hmn]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD ⊥ ^ n • ⊤]
⊢ x = 0
[PROOFSTEP]
simpa only [pow_one ⊥, bot_smul, SModEq.bot] using hx 1
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff ⊤ M
x y : M
n : ℕ
⊢ x - y ≡ 0 [SMOD ⊤ ^ n • ⊤]
[PROOFSTEP]
rw [Ideal.top_pow, top_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff ⊤ M
x y : M
n : ℕ
⊢ x - y ≡ 0 [SMOD ⊤]
[PROOFSTEP]
exact SModEq.top
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
⊢ x ∈ I ^ n • ⊤
[PROOFSTEP]
have := comap_map_mkQ (⨅ n : ℕ, I ^ n • ⊤ : Submodule R M) (I ^ n • ⊤)
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
this :
  comap (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (map (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (I ^ n • ⊤)) = (⨅ (n : ℕ), I ^ n • ⊤) ⊔ I ^ n • ⊤
⊢ x ∈ I ^ n • ⊤
[PROOFSTEP]
simp only [sup_of_le_right (iInf_le (fun n => (I ^ n • ⊤ : Submodule R M)) n)] at this 
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
this : comap (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (map (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (I ^ n • ⊤)) = I ^ n • ⊤
⊢ x ∈ I ^ n • ⊤
[PROOFSTEP]
rw [← this, map_smul'', mem_comap, Submodule.map_top, range_mkQ, ← SModEq.zero]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x✝ : Hausdorffification I M
x : M
hx : ∀ (n : ℕ), Quotient.mk'' x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
this : comap (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (map (mkQ (⨅ (n : ℕ), I ^ n • ⊤)) (I ^ n • ⊤)) = I ^ n • ⊤
⊢ ↑(mkQ (⨅ (n : ℕ), I ^ n • ⊤)) x ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
exact hx n
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff I N
f : M →ₗ[R] N
n : ℕ
⊢ map f (I ^ n • ⊤) ≤ I ^ n • ⊤
[PROOFSTEP]
rw [map_smul'']
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff I N
f : M →ₗ[R] N
n : ℕ
⊢ I ^ n • map f ⊤ ≤ I ^ n • ⊤
[PROOFSTEP]
exact smul_mono le_rfl le_top
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff I N
f : M →ₗ[R] N
g : Hausdorffification I M →ₗ[R] N
hg : LinearMap.comp g (of I M) = f
x✝ : Hausdorffification I M
x : M
⊢ ↑g (↑(of I M) x) = ↑(lift I f) (↑(of I M) x)
[PROOFSTEP]
rw [lift_of, ← hg, LinearMap.comp_apply]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsPrecomplete ⊥ M
[PROOFSTEP]
refine' ⟨fun f hf => ⟨f 1, fun n => _⟩⟩
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
n : ℕ
⊢ f n ≡ f 1 [SMOD ⊥ ^ n • ⊤]
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
⊢ f Nat.zero ≡ f 1 [SMOD ⊥ ^ Nat.zero • ⊤]
[PROOFSTEP]
rw [pow_zero, Ideal.one_eq_top, top_smul]
[GOAL]
case zero
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
⊢ f Nat.zero ≡ f 1 [SMOD ⊤]
[PROOFSTEP]
exact SModEq.top
[GOAL]
case succ
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊥ ^ m • ⊤]
n : ℕ
⊢ f (Nat.succ n) ≡ f 1 [SMOD ⊥ ^ Nat.succ n • ⊤]
[PROOFSTEP]
specialize hf (Nat.le_add_left 1 n)
[GOAL]
case succ
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
n : ℕ
hf : f 1 ≡ f (n + 1) [SMOD ⊥ ^ 1 • ⊤]
⊢ f (Nat.succ n) ≡ f 1 [SMOD ⊥ ^ Nat.succ n • ⊤]
[PROOFSTEP]
rw [pow_one, bot_smul, SModEq.bot] at hf 
[GOAL]
case succ
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
n : ℕ
hf : f 1 = f (n + 1)
⊢ f (Nat.succ n) ≡ f 1 [SMOD ⊥ ^ Nat.succ n • ⊤]
[PROOFSTEP]
rw [hf]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊤ ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD ⊤ ^ n • ⊤]
[PROOFSTEP]
rw [Ideal.top_pow, top_smul]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD ⊤ ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD ⊤]
[PROOFSTEP]
exact SModEq.top
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Subsingleton M
f : ℕ → M
x✝ : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
n : ℕ
⊢ f n ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
rw [Subsingleton.elim (f n) 0]
[GOAL]
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
x : { x // x ∈ adicCompletion I M }
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
n : ℕ
x✝¹ x✝ : { x // x ∈ adicCompletion I M }
ih1 : ↑(eval I M n) x✝¹ = ↑(eval I M n) 0
ih2 : ↑(eval I M n) x✝ = ↑(eval I M n) 0
⊢ ↑(eval I M n) (x✝¹ + x✝) = ↑(eval I M n) 0
[PROOFSTEP]
rw [LinearMap.map_add, ih1, ih2, LinearMap.map_zero, add_zero]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
⊢ I ≤ Ideal.jacobson ⊥
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
⊢ x ∈ Ideal.jacobson ⊥
[PROOFSTEP]
rw [← Ideal.neg_mem_iff, Ideal.mem_jacobson_bot]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
⊢ ∀ (y : R), IsUnit (-x * y + 1)
[PROOFSTEP]
intro y
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
⊢ IsUnit (-x * y + 1)
[PROOFSTEP]
rw [add_comm]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
⊢ IsUnit (1 + -x * y)
[PROOFSTEP]
let f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
⊢ IsUnit (1 + -x * y)
[PROOFSTEP]
have hf : ∀ m n, m ≤ n → f m ≡ f n [SMOD I ^ m • (⊤ : Submodule R R)] :=
  by
  intro m n h
  simp only [Algebra.id.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)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
⊢ ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
[PROOFSTEP]
intro m n h
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ f m ≡ f n [SMOD I ^ m • ⊤]
[PROOFSTEP]
simp only [Algebra.id.smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ ∑ i in range m, (x * y) ^ i - ∑ i in range n, (x * y) ^ i ∈ I ^ m
[PROOFSTEP]
rw [← add_tsub_cancel_of_le h, Finset.sum_range_add, ← sub_sub, sub_self, zero_sub, @neg_mem_iff]
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ ∑ x_1 in range (n - m), (x * y) ^ (m + x_1) ∈ I ^ m
[PROOFSTEP]
apply Submodule.sum_mem
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n : ℕ
h : m ≤ n
⊢ ∀ (c : ℕ), c ∈ range (n - m) → (x * y) ^ (m + c) ∈ I ^ m
[PROOFSTEP]
intro n _
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n✝ : ℕ
h : m ≤ n✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ (x * y) ^ (m + n) ∈ I ^ m
[PROOFSTEP]
rw [mul_pow, pow_add, mul_assoc]
[GOAL]
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
m n✝ : ℕ
h : m ≤ n✝
n : ℕ
a✝ : n ∈ range (n✝ - m)
⊢ x ^ m * (x ^ n * y ^ (m + n)) ∈ I ^ m
[PROOFSTEP]
exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
⊢ IsUnit (1 + -x * y)
[PROOFSTEP]
obtain ⟨L, hL⟩ := IsPrecomplete.prec toIsPrecomplete @hf
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ IsUnit (1 + -x * y)
[PROOFSTEP]
rw [isUnit_iff_exists_inv]
[GOAL]
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ ∃ b, (1 + -x * y) * b = 1
[PROOFSTEP]
use L
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ (1 + -x * y) * L = 1
[PROOFSTEP]
rw [← sub_eq_zero, neg_mul]
[GOAL]
case h
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ (1 + -(x * y)) * L - 1 = 0
[PROOFSTEP]
apply IsHausdorff.haus (toIsHausdorff : IsHausdorff I R)
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
⊢ ∀ (n : ℕ), (1 + -(x * y)) * L - 1 ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
intro n
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]
n : ℕ
⊢ (1 + -(x * y)) * L - 1 ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
specialize hL n
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n ≡ L [SMOD I ^ n • ⊤]
⊢ (1 + -(x * y)) * L - 1 ≡ 0 [SMOD I ^ n • ⊤]
[PROOFSTEP]
rw [SModEq.sub_mem, Algebra.id.smul_eq_mul, Ideal.mul_top] at hL ⊢
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 - 0 ∈ I ^ n
[PROOFSTEP]
rw [sub_zero]
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 + -(x * y)) * L - 1 ∈ I ^ n
[PROOFSTEP]
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
[GOAL]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
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
[PROOFSTEP]
convert Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1
[GOAL]
case h.e'_4
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
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)
[PROOFSTEP]
ring
[GOAL]
case h.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n : ℕ
hL : f n - L ∈ I ^ n
⊢ (1 - x * y) * f n - 1 ∈ I ^ n
[PROOFSTEP]
cases n
[GOAL]
case h.a.zero
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
hL : f Nat.zero - L ∈ I ^ Nat.zero
⊢ (1 - x * y) * f Nat.zero - 1 ∈ I ^ Nat.zero
[PROOFSTEP]
simp only [Ideal.one_eq_top, pow_zero, Nat.zero_eq, mem_top]
[GOAL]
case h.a.succ
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (Nat.succ n✝) - L ∈ I ^ Nat.succ n✝
⊢ (1 - x * y) * f (Nat.succ n✝) - 1 ∈ I ^ Nat.succ n✝
[PROOFSTEP]
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]
[GOAL]
case h.a.succ
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
hf : ∀ (m n : ℕ), m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]
L : R
n✝ : ℕ
hL : f (Nat.succ n✝) - L ∈ I ^ Nat.succ n✝
⊢ x ^ Nat.succ n✝ * y ^ Nat.succ n✝ ∈ I ^ Nat.succ n✝
[PROOFSTEP]
exact Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _)
