-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma isQuasiregular_iff {x : R} :
    IsQuasiregular x ↔ ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0

Proof state:
case mpr.intro.intro.refine_2
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv y * equiv x = 1

Tactic:
apply equiv.symm.injective

Result:
case mpr.intro.intro.refine_2.a
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv.symm (equiv y * equiv x) = equiv.symm 1

Proof state:
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ IsQuasiregular x ↔ ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ IsQuasiregular x → ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0

case mpr
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ (∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0) → IsQuasiregular x

Proof state:
case mpr.intro.intro.refine_1
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv x * equiv y = 1

case mpr.intro.intro.refine_2
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv y * equiv x = 1

Tactic:
all_goals
  apply equiv.symm.injective
  assumption

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ IsQuasiregular x

Tactic:
refine ⟨⟨equiv x, equiv y, ?_, ?_⟩, rfl⟩

Result:
case mpr.intro.intro.refine_1
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv x * equiv y = 1

case mpr.intro.intro.refine_2
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv y * equiv x = 1

Proof state:
case mpr.intro.intro.refine_2.a
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ equiv.symm (equiv y * equiv x) = equiv.symm 1

Tactic:
assumption

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ IsQuasiregular x → ∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0

Tactic:
rintro ⟨u, rfl⟩

Result:
case mp.intro
R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ ∃ y, y + equiv.symm ↑u + equiv.symm ↑u * y = 0 ∧ equiv.symm ↑u + y + y * equiv.symm ↑u = 0

Proof state:
case mp.intro
R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ ∃ y, y + equiv.symm ↑u + equiv.symm ↑u * y = 0 ∧ equiv.symm ↑u + y + y * equiv.symm ↑u = 0

Tactic:
exact ⟨equiv.symm u⁻¹.val, by simp⟩

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : NonUnitalSemiring R
x : R
⊢ (∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0) → IsQuasiregular x

Tactic:
rintro ⟨y, hy₁, hy₂⟩

Result:
case mpr.intro.intro
R : Type u_1
inst✝ : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ IsQuasiregular x

Proof state:
R : Type u_1
inst✝ : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ equiv.symm ↑u⁻¹ + equiv.symm ↑u + equiv.symm ↑u * equiv.symm ↑u⁻¹ = 0 ∧
    equiv.symm ↑u + equiv.symm ↑u⁻¹ + equiv.symm ↑u⁻¹ * equiv.symm ↑u = 0

Tactic:
simp

Result:
no goals