R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I✝ : Ideal S
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
x : R
⊢ IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I✝ : Ideal S
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
x : R
⊢ IsUnit (↑(Ideal.Quotient.mk I) x) ↔ IsUnit x
refine' ⟨_, fun h => h.map <| Ideal.Quotient.mk I⟩
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I✝ : Ideal S
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ {x : R}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I✝ : Ideal S
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
x : R
⊢ IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
revert x
case h₁
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_1
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x

case h₂
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_1
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk J) x) → IsUnit x
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I✝ : Ideal S
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : IsNilpotent I
⊢ ∀ {x : R}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
apply Ideal.IsNilpotent.induction_on (R := R) (S := R) I hI <;> clear hI I
case h₂
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_1
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk J) x) → IsUnit x

case h₁
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_1
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
case h₁
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_1
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x

case h₂
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_1
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk J) x) → IsUnit x
swap
case h₂
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit (↑(Ideal.Quotient.mk J) x)
⊢ IsUnit x
case h₂
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_1
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x) →
        (∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) →
          ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk J) x) → IsUnit x
introv e h₁ h₂ h₃
case h₂.a
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit (↑(Ideal.Quotient.mk J) x)
⊢ IsUnit (↑(Ideal.Quotient.mk I) x)
case h₂
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit (↑(Ideal.Quotient.mk J) x)
⊢ IsUnit x
apply h₁
case h₂.a.a
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit (↑(Ideal.Quotient.mk J) x)
⊢ IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) (↑(Ideal.Quotient.mk I) x))
case h₂.a
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit (↑(Ideal.Quotient.mk J) x)
⊢ IsUnit (↑(Ideal.Quotient.mk I) x)
apply h₂
no goals
case h₂.a.a
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I J : Ideal S
e : I ≤ J
h₁ : ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
h₂ : ∀ {x : S ⧸ I}, IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x
x : S
h₃ : IsUnit (↑(Ideal.Quotient.mk J) x)
⊢ IsUnit (↑(Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) (↑(Ideal.Quotient.mk I) x))
exact
  h₃.map
    ((DoubleQuot.quotQuotEquivQuotSup I J).trans
          (Ideal.quotEquivOfEq (sup_eq_right.mpr e))).symm.toRingHom
case h₁
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
⊢ IsUnit x
case h₁
R✝ : Type ?u.10312
S : Type ?u.10315
inst✝³ : CommSemiring R✝
inst✝² : CommRing S
inst✝¹ : Algebra R✝ S
I : Ideal S
R : Type u_1
inst✝ : CommRing R
⊢ ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ {x : S}, IsUnit (↑(Ideal.Quotient.mk I) x) → IsUnit x
introv e H
case h₁
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
⊢ IsUnit x
case h₁
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
⊢ IsUnit x
skip
case h₁.intro
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
⊢ IsUnit x
case h₁
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
⊢ IsUnit x
obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (↑H.unit⁻¹ : S ⧸ I)
case h₁.intro
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : ↑(Ideal.Quotient.mk I) (x * y) = ↑(Ideal.Quotient.mk I) 1
⊢ IsUnit x
case h₁.intro
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
⊢ IsUnit x
have : Ideal.Quotient.mk I (x * y) = Ideal.Quotient.mk I 1 := by
  rw [map_one, _root_.map_mul, hy, IsUnit.mul_val_inv]
case h₁.intro
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : x * y - 1 ∈ I
⊢ IsUnit x
case h₁.intro
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : ↑(Ideal.Quotient.mk I) (x * y) = ↑(Ideal.Quotient.mk I) 1
⊢ IsUnit x
rw [Ideal.Quotient.eq] at this
case h₁.intro
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝ : x * y - 1 ∈ I
this : (x * y - 1) ^ 2 = 0
⊢ IsUnit x
case h₁.intro
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : x * y - 1 ∈ I
⊢ IsUnit x
have : (x * y - 1) ^ 2 = 0 := by
  rw [← Ideal.mem_bot, ← e]
  exact Ideal.pow_mem_pow this _
case h₁.intro
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝¹ : x * y - 1 ∈ I
this✝ : (x * y - 1) ^ 2 = 0
this : x * (y * (2 - x * y)) = 1
⊢ IsUnit x
case h₁.intro
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝ : x * y - 1 ∈ I
this : (x * y - 1) ^ 2 = 0
⊢ IsUnit x
have : x * (y * (2 - x * y)) = 1 := by
  rw [eq_comm, ← sub_eq_zero, ← this]
  ring
no goals
case h₁.intro
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝¹ : x * y - 1 ∈ I
this✝ : (x * y - 1) ^ 2 = 0
this : x * (y * (2 - x * y)) = 1
⊢ IsUnit x
exact isUnit_of_mul_eq_one _ _ this
no goals
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
⊢ ↑(Ideal.Quotient.mk I) (x * y) = ↑(Ideal.Quotient.mk I) 1
rw [map_one, _root_.map_mul, hy, IsUnit.mul_val_inv]
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : x * y - 1 ∈ I
⊢ (x * y - 1) ^ 2 ∈ I ^ 2
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : x * y - 1 ∈ I
⊢ (x * y - 1) ^ 2 = 0
rw [← Ideal.mem_bot, ← e]
no goals
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this : x * y - 1 ∈ I
⊢ (x * y - 1) ^ 2 ∈ I ^ 2
exact Ideal.pow_mem_pow this _
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝ : x * y - 1 ∈ I
this : (x * y - 1) ^ 2 = 0
⊢ 1 - x * (y * (2 - x * y)) = (x * y - 1) ^ 2
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝ : x * y - 1 ∈ I
this : (x * y - 1) ^ 2 = 0
⊢ x * (y * (2 - x * y)) = 1
rw [eq_comm, ← sub_eq_zero, ← this]
no goals
R✝ : Type ?u.10312
S✝ : Type ?u.10315
inst✝⁴ : CommSemiring R✝
inst✝³ : CommRing S✝
inst✝² : Algebra R✝ S✝
I✝ : Ideal S✝
R : Type u_1
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
I : Ideal S
e : I ^ 2 = ⊥
x : S
H : IsUnit (↑(Ideal.Quotient.mk I) x)
y : S
hy : ↑(Ideal.Quotient.mk I) y = ↑(IsUnit.unit H)⁻¹
this✝ : x * y - 1 ∈ I
this : (x * y - 1) ^ 2 = 0
⊢ 1 - x * (y * (2 - x * y)) = (x * y - 1) ^ 2
ring