case mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
⊢ ∃ b, Quot.mk Setoid.r a * b = 1
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
⊢ ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b, a * b = 1
rintro ⟨a⟩ h
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ ∃ b, Quot.mk Setoid.r a * b = 1
case mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
⊢ ∃ b, Quot.mk Setoid.r a * b = 1
rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : a * b + c = 1
⊢ ∃ b, Quot.mk Setoid.r a * b = 1
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ ∃ b, Quot.mk Setoid.r a * b = 1
rw [mul_comm] at abc
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : a * b + c = 1
⊢ Setoid.r ((fun x x_1 => x * x_1) a b) 1
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : a * b + c = 1
⊢ ∃ b, Quot.mk Setoid.r a * b = 1
refine' ⟨mk _ b, Quot.sound _⟩
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : a * b + c = 1
⊢ a * b - 1 ∈ I
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : a * b + c = 1
⊢ Setoid.r ((fun x x_1 => x * x_1) a b) 1
simp only [Submodule.quotientRel_r_def]
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : c = 1 - a * b
⊢ a * b - 1 ∈ I
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : a * b + c = 1
⊢ a * b - 1 ∈ I
rw [← eq_sub_iff_add_eq'] at abc
no goals
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : c = 1 - a * b
⊢ a * b - 1 ∈ I
rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc