-- Mathlib/RingTheory/Ideal/Quotient/Basic.lean
theorem exists_inv [hI : I.IsMaximal] :
    ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b : R ⧸ I, a * b = 1

Proof state:
case h.mk.intro.intro.intro
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ b * a - 1 ∈ I

Tactic:
rw [← eq_sub_iff_add_eq'] at abc

Result:
case h.mk.intro.intro.intro
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : c = 1 - b * a
⊢ b * a - 1 ∈ I

Proof state:
case h
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
⊢ ∀ (a : R ⧸ I), a ≠ 0 → ∃ b, b * a = 1

Tactic:
rintro ⟨a⟩ h

Result:
case h.mk
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
⊢ ∃ b, b * Quot.mk (⇑(Submodule.quotientRel I)) a = 1

Proof state:
case h.mk.intro.intro.intro
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ ∃ b, b * Quot.mk (⇑(Submodule.quotientRel I)) a = 1

Tactic:
refine ⟨mk _ b, Quot.sound ?_⟩

Result:
case h.mk.intro.intro.intro
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ (Quotient.ringCon I).toSetoid ((fun x1 x2 => x1 * x2) b a) 1

Proof state:
case h.mk
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
⊢ ∃ b, b * Quot.mk (⇑(Submodule.quotientRel I)) a = 1

Tactic:
rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩

Result:
case h.mk.intro.intro.intro
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ ∃ b, b * Quot.mk (⇑(Submodule.quotientRel I)) a = 1

Proof state:
case h.mk.intro.intro.intro
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ (Quotient.ringCon I).toSetoid ((fun x1 x2 => x1 * x2) b a) 1

Tactic:
simp only [Submodule.quotientRel_def]

Result:
case h.mk.intro.intro.intro
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ b * a - 1 ∈ I

Proof state:
case h.mk.intro.intro.intro
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
a✝ : R ⧸ I
a : R
h : Quot.mk (⇑(Submodule.quotientRel I)) a ≠ 0
b c : R
hc : c ∈ I
abc : c = 1 - b * a
⊢ b * a - 1 ∈ I

Tactic:
rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
⊢ ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b, a * b = 1

Tactic:
apply exists_right_inv_of_exists_left_inv

Result:
case h
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
hI : I.IsMaximal
⊢ ∀ (a : R ⧸ I), a ≠ 0 → ∃ b, b * a = 1