R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
⊢ x ∈ Ideal.jacobson ⊥
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
⊢ I ≤ Ideal.jacobson ⊥
intro x hx
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
⊢ ∀ (y : R), IsUnit (-x * y + 1)
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
⊢ x ∈ Ideal.jacobson ⊥
rw [← Ideal.neg_mem_iff, Ideal.mem_jacobson_bot]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
⊢ IsUnit (-x * y + 1)
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
⊢ ∀ (y : R), IsUnit (-x * y + 1)
intro y
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
⊢ IsUnit (1 + -x * y)
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
⊢ IsUnit (-x * y + 1)
rw [add_comm]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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)
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsAdicComplete I R
x : R
hx : x ∈ I
y : R
⊢ IsUnit (1 + -x * y)
let f : ℕ → R := fun n => ∑ i in range n, (x * y) ^ i
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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)
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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)
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)
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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)
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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)
obtain ⟨L, hL⟩ := IsPrecomplete.prec toIsPrecomplete @hf
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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 • ⊤]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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 • ⊤]
intro m n h
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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 • ⊤]
simp only [Algebra.id.smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
rw [← add_tsub_cancel_of_le h, Finset.sum_range_add, ← sub_sub, sub_self, zero_sub,
  @neg_mem_iff]
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
apply Submodule.sum_mem
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
intro n _
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
rw [mul_pow, pow_add, mul_assoc]
no goals
case a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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)
rw [isUnit_iff_exists_inv]
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
use L
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
rw [← sub_eq_zero, neg_mul]
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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 • ⊤]
case intro
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
apply IsHausdorff.haus (toIsHausdorff : IsHausdorff I R)
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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 • ⊤]
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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 • ⊤]
intro n
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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 • ⊤]
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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 • ⊤]
specialize hL n
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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 • ⊤]
rw [SModEq.sub_mem, Algebra.id.smul_eq_mul, Ideal.mul_top] at hL⊢
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
rw [sub_zero]
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
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
case intro.a.zero
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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

case intro.a.succ
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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✝
case intro.a
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
cases n
case h.e'_4
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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)
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
convert Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1
no goals
case h.e'_4
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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)
ring
no goals
case intro.a.zero
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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
simp only [Ideal.one_eq_top, pow_zero, Nat.zero_eq, mem_top]
case intro.a.succ
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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✝
case intro.a.succ
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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✝
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]
no goals
case intro.a.succ
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type ?u.289904
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type ?u.290446
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✝
exact Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _)