awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ HAdd.hAdd (α := R) (β := R) ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u⁻¹ : PreQuasiregular R) : R)
          ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u : PreQuasiregular R) : R) +
        HMul.hMul (α := R) (β := R) ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u : PreQuasiregular R) : R)
          ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u⁻¹ : PreQuasiregular R) : R) =
      0 ∧
    HAdd.hAdd (α := R) (β := R) ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u : PreQuasiregular R) : R)
          ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u⁻¹ : PreQuasiregular R) : R) +
        HMul.hMul (α := R) (β := R) ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u⁻¹ : PreQuasiregular R) : R)
          ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u : PreQuasiregular R) : R) =
      0

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ ∃ (y : R),
    HAdd.hAdd (β := R) y ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u : PreQuasiregular R) : R) +
          HMul.hMul (α := R) ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u : PreQuasiregular R) : R) y =
        0 ∧
      HAdd.hAdd (α := R) ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u : PreQuasiregular R) : R) y +
          HMul.hMul (β := R) y ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (↑u : PreQuasiregular R) : R) =
        0

Tactic:
exact ⟨equiv.symm u⁻¹.val, by simp⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
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:
⟨⟨equiv x, equiv y, ?_, ?_⟩, rfl⟩

Premises used: PreQuasiregular.equiv, IsQuasiregular, Units.mk, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
mpr :
  HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R) =
    1
mpr₁ :
  HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R) =
    1
⊢ IsQuasiregular x

Tactic:
refine ⟨⟨equiv x, equiv y, ?_, ?_⟩, rfl⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
mpr :
  Eq (α := R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R)
        (HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
          ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R)
          ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R)) :
      R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R) 1 : R)
⊢ HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R) =
    1

Tactic:
apply equiv.symm.injective

Premises used: PreQuasiregular.equiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ Eq (α := R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R)
        (HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
          ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R)
          ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R)) :
      R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R) 1 : R)

Tactic:
assumption
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
mpr :
  Eq (α := R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R)
        (HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
          ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R)
          ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R)) :
      R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R) 1 : R)
⊢ HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R) =
    1

Tactic:
apply equiv.symm.injective

Premises used: PreQuasiregular.equiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ Eq (α := R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R)
        (HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
          ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R)
          ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R)) :
      R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R) 1 : R)

Tactic:
assumption
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x : R
⊢ IsQuasiregular x ↔ IsUnit (M := PreQuasiregular R) ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R)

Tactic:
simp only [IsQuasiregular, IsUnit, Equiv.apply_symm_apply,
    ← PreQuasiregular.equiv (R := R).injective.eq_iff]

Premises used: PreQuasiregular.equiv, Equiv.apply_symm_apply, Function.Injective.eq_iff, IsUnit, IsQuasiregular, Equiv.injective
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : NonUnitalSemiring R
inst_1 : NonUnitalSemiring S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
x : R
hx : IsQuasiregular x
rw :
  ∀ (hx : ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0),
    ∃ (y : S),
      HAdd.hAdd (β := S) y ((f : (a : R) → S) x : S) + HMul.hMul (α := S) ((f : (a : R) → S) x : S) y = 0 ∧
        HAdd.hAdd (α := S) ((f : (a : R) → S) x : S) y + HMul.hMul (β := S) y ((f : (a : R) → S) x : S) = 0
⊢ IsQuasiregular.{u_3} (R := S) ((f : (a : R) → S) x : S)

Tactic:
rw [isQuasiregular_iff] at hx ⊢

Premises used: isQuasiregular_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : NonUnitalSemiring R
inst_1 : NonUnitalSemiring S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
x : R
hx : ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0
obtain :
  ∀ (y : R) (hy₁ : y + x + x * y = 0) (hy₂ : x + y + y * x = 0),
    ∃ (y : S),
      HAdd.hAdd (β := S) y ((f : (a : R) → S) x : S) + HMul.hMul (α := S) ((f : (a : R) → S) x : S) y = 0 ∧
        HAdd.hAdd (α := S) ((f : (a : R) → S) x : S) y + HMul.hMul (β := S) y ((f : (a : R) → S) x : S) = 0
⊢ ∃ (y : S),
    HAdd.hAdd (β := S) y ((f : (a : R) → S) x : S) + HMul.hMul (α := S) ((f : (a : R) → S) x : S) y = 0 ∧
      HAdd.hAdd (α := S) ((f : (a : R) → S) x : S) y + HMul.hMul (β := S) y ((f : (a : R) → S) x : S) = 0

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := hx
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : NonUnitalSemiring R
inst_1 : NonUnitalSemiring S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) y : S) ((f : (a : R) → S) x : S) +
        HMul.hMul (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) =
      0 ∧
    HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) +
        HMul.hMul (α := S) (β := S) ((f : (a : R) → S) y : S) ((f : (a : R) → S) x : S) =
      0

Tactic:
simpa using And.intro congr(f $(hy₁)) congr(f $(hy₂))

Premises used: congrArg, id, And.intro, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : NonUnitalSemiring R
inst_1 : NonUnitalSemiring S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ ∃ (y : S),
    HAdd.hAdd (β := S) y ((f : (a : R) → S) x : S) + HMul.hMul (α := S) ((f : (a : R) → S) x : S) y = 0 ∧
      HAdd.hAdd (α := S) ((f : (a : R) → S) x : S) y + HMul.hMul (β := S) y ((f : (a : R) → S) x : S) = 0

Tactic:
exact ⟨f y, by simpa using And.intro congr(f $(hy₁)) congr(f $(hy₂))⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
obtain : ∀ (y : R) (hy₁ : y + x + x * y = 0) (hy₂ : x + y + y * x = 0), IsUnit (1 + x)
⊢ IsUnit (1 + x)

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := isQuasiregular_iff.mp hx

Premises used: isQuasiregular_iff, Iff.mp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ IsUnit (1 + x)

Tactic:
⟨⟨1 + x, 1 + y, ?_, ?_⟩, rfl⟩

Premises used: IsUnit, HAdd.hAdd, Units.mk, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
refine_1 : (1 + x) * (1 + y) = 1
refine_2 : (1 + y) * (1 + x) = 1
⊢ IsUnit (1 + x)

Tactic:
refine ⟨⟨1 + x, 1 + y, ?_, ?_⟩, rfl⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ 1 + (y + x + x * y) = HAdd.hAdd (α := R) 1 0

Tactic:
congr(1 + $(hy₁))

Premises used: congrArg, id, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
h : (1 + x) * (1 + y) = 1 + (y + x + x * y)
h₁ : 1 = HAdd.hAdd (α := R) 1 0
⊢ (1 + x) * (1 + y) = 1

Tactic:
convert! congr(1 + $(hy₁)) using 1
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
h h₁ h₂ h₃ : 1 + x + (y + x * y) = 1 + (y + x + x * y)
⊢ (1 + x) * (1 + y) = 1 + (y + x + x * y)

Tactic:
noncomm_ring
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ 1 = HAdd.hAdd (α := R) 1 0

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
h : (1 + x) * (1 + y) = 1 + (y + x + x * y)
h₁ : 1 = HAdd.hAdd (α := R) 1 0
h₂ : (1 + x) * (1 + y) = 1 + (y + x + x * y)
h₃ : 1 = HAdd.hAdd (α := R) 1 0
⊢ (1 + x) * (1 + y) = 1

Tactic:
convert! congr(1 + $(hy₁)) using 1 <;> [noncomm_ring; simp]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ 1 + (x + y + y * x) = HAdd.hAdd (α := R) 1 0

Tactic:
congr(1 + $(hy₂))

Premises used: congrArg, id, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
h : (1 + y) * (1 + x) = 1 + (x + y + y * x)
h₁ : 1 = HAdd.hAdd (α := R) 1 0
⊢ (1 + y) * (1 + x) = 1

Tactic:
convert! congr(1 + $(hy₂)) using 1
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
h h₁ h₂ h₃ : 1 + y + (x + y * x) = 1 + (x + y + y * x)
⊢ (1 + y) * (1 + x) = 1 + (x + y + y * x)

Tactic:
noncomm_ring
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
h : (1 + y) * (1 + x) = 1 + (x + y + y * x)
h₁ : 1 = HAdd.hAdd (α := R) 1 0
h₂ : (1 + y) * (1 + x) = 1 + (x + y + y * x)
h₃ : 1 = HAdd.hAdd (α := R) 1 0
⊢ (1 + y) * (1 + x) = 1

Tactic:
convert! congr(1 + $(hy₂)) using 1 <;> [noncomm_ring; simp]
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
⊢ IsQuasiregular x ↔ IsUnit (1 + x)

Tactic:
⟨IsQuasiregular.isUnit_one_add, fun hx ↦ ?_⟩

Premises used: Iff.intro, IsQuasiregular.isUnit_one_add
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
refine : ∀ (hx : IsUnit (1 + x)), IsQuasiregular x
⊢ IsQuasiregular x ↔ IsUnit (1 + x)

Tactic:
refine ⟨IsQuasiregular.isUnit_one_add, fun hx ↦ ?_⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
rw : ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0
⊢ IsQuasiregular x

Tactic:
rw [isQuasiregular_iff]

Premises used: isQuasiregular_iff
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
h :
  (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0 ∧
    x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0
⊢ ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0

Tactic:
use hx.unit⁻¹ - 1

Premises used: IsUnit.unit
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
h : (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0
h₁ : x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0
⊢ (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0 ∧
    x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ (1 + x) * (↑hx.unit⁻¹ : R) - 1 = HSub.hSub (α := R) 1 1

Tactic:
have := congr($(hx.mul_val_inv) - 1)
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ (1 + x) * (↑hx.unit⁻¹ : R) - 1 = HSub.hSub (α := R) 1 1

Tactic:
case' h.left => have := congr($(hx.mul_val_inv) - 1)
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ (↑hx.unit⁻¹ : R) * (1 + x) - 1 = HSub.hSub (α := R) 1 1

Tactic:
have := congr($(hx.val_inv_mul) - 1)
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ (↑hx.unit⁻¹ : R) * (1 + x) - 1 = HSub.hSub (α := R) 1 1

Tactic:
case' h.right => have := congr($(hx.val_inv_mul) - 1)
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : (↑hx.unit⁻¹ : R) * (1 + x) - 1 = HSub.hSub (α := R) 1 1
⊢ ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1 = 0

Tactic:
rw [← sub_add_cancel (↑hx.unit⁻¹ : R) 1, sub_self] at this

Premises used: Units.val, sub_self, Inv.inv, IsUnit.unit, OfNat.ofNat, sub_add_cancel
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1 = 0
⊢ ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1 = 0

Tactic:
this
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1 = 0
h : x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1
⊢ x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0

Tactic:
convert! this using 1
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1 = 0
h h₁ h₂ h₃ :
  x + ((↑hx.unit⁻¹ : R) + -1) + ((↑hx.unit⁻¹ : R) * x + -x) =
    (↑hx.unit⁻¹ : R) + -1 + 1 + ((↑hx.unit⁻¹ : R) * x + -x + x) + -1
⊢ x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1

Tactic:
noncomm_ring
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : (1 + x) * (↑hx.unit⁻¹ : R) - 1 = HSub.hSub (α := R) 1 1
⊢ (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1 = 0

Tactic:
rw [← sub_add_cancel (↑hx.unit⁻¹ : R) 1, sub_self] at this

Premises used: Units.val, sub_self, Inv.inv, IsUnit.unit, OfNat.ofNat, sub_add_cancel
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1 = 0
⊢ (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1 = 0

Tactic:
this
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1 = 0
h : (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1
⊢ (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0

Tactic:
convert! this using 1
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1 = 0
h h₁ h₂ h₃ :
  (↑hx.unit⁻¹ : R) + -1 + x + (x * (↑hx.unit⁻¹ : R) + -x) =
    (↑hx.unit⁻¹ : R) + x * (↑hx.unit⁻¹ : R) + -(1 + x) + (1 + x) + -1
⊢ (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1

Tactic:
noncomm_ring
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
⊢ IsQuasiregular x ↔ IsUnit (HAdd.hAdd (α := Unitization R A) 1 (↑x : Unitization R A))

Tactic:
⟨?_, fun hx ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
refine_1 : IsQuasiregular x → IsUnit (HAdd.hAdd (α := Unitization R A) 1 (↑x : Unitization R A))
refine_2 : ∀ (hx : IsUnit (HAdd.hAdd (α := Unitization R A) 1 (↑x : Unitization R A))), IsQuasiregular x
⊢ IsQuasiregular x ↔ IsUnit (HAdd.hAdd (α := Unitization R A) 1 (↑x : Unitization R A))

Tactic:
refine ⟨?_, fun hx ↦ ?_⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
u : (PreQuasiregular A)ˣ
⊢ IsUnit
    (HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
      ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑u : PreQuasiregular A)) :
          Unitization R A) :
        Unitization R A))

Tactic:
(Unitization.unitsFstOne_mulEquiv_quasiregular R).symm u |>.val.isUnit

Premises used: Unitization.unitsFstOne_mulEquiv_quasiregular, Units.isUnit, MulEquiv.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
u : (PreQuasiregular A)ˣ
⊢ IsUnit
    (HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
      ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑u : PreQuasiregular A)) :
          Unitization R A) :
        Unitization R A))

Tactic:
exact (Unitization.unitsFstOne_mulEquiv_quasiregular R).symm u |>.val.isUnit

Premises used: Unitization.unitsFstOne_mulEquiv_quasiregular, Units.isUnit, MulEquiv.symm, Subtype.val, DFunLike.coe
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
hx : IsUnit (HAdd.hAdd (α := Unitization R A) 1 (↑x : Unitization R A))
⊢ Membership.mem (γ := Subgroup (Unitization R A)ˣ) (Unitization.unitsFstOne R A) hx.unit

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
hx : IsUnit (HAdd.hAdd (α := Unitization R A) 1 (↑x : Unitization R A))
⊢ (Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A)
      (↑((Unitization.unitsFstOne_mulEquiv_quasiregular R : (a : ↥(Unitization.unitsFstOne R A)) → (PreQuasiregular A)ˣ)
            (Subtype.mk (p := fun (x : (Unitization R A)ˣ) ↦
              Membership.mem (γ := Subgroup (Unitization R A)ˣ) (Unitization.unitsFstOne R A) x) hx.unit ⋯)) :
        PreQuasiregular A) =
    x

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
x : A
hx : IsUnit (HAdd.hAdd (α := Unitization R A) 1 (↑x : Unitization R A))
⊢ IsQuasiregular x

Tactic:
exact ⟨(Unitization.unitsFstOne_mulEquiv_quasiregular R) ⟨hx.unit, by simp⟩, by simp⟩
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
a : A
r : R
hr : ¬IsUnit r
⊢ r ∈ quasispectrum R a

Tactic:
fun hr' ↦ (hr hr').elim

Premises used: Set.Mem, False.elim, setOf, quasispectrum
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Nontrivial R
a : A
⊢ ¬IsUnit.{u_1} (M := R) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalRing A
inst_2 : Module R A
inst_3 : Nontrivial R
a : A
⊢ (quasispectrum R a).Nonempty

Tactic:
Set.nonempty_of_mem <| quasispectrum.zero_mem R a

Premises used: quasispectrum.zero_mem, Set.nonempty_of_mem
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : NonUnitalRing A
inst_3 : NonUnitalRing B
inst_4 : Module R S
inst_5 : Module S A
inst_6 : Module R A
inst_7 : Module S B
inst_8 : Module R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
inst_11 : FunLike F A B
inst_12 : NonUnitalAlgHomClass F S A B
φ : F
a : A
⊢ quasispectrum.{u_4, u_7} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a

Tactic:
Set.compl_subset_compl.mp fun x ↦ ?_

Premises used: Set.compl_subset_compl, Iff.mp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
F : Type u_3
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : NonUnitalRing A
inst_3 : NonUnitalRing B
inst_4 : Module R S
inst_5 : Module S A
inst_6 : Module R A
inst_7 : Module S B
inst_8 : Module R B
inst_9 : IsScalarTower R S A
inst_10 : IsScalarTower R S B
inst_11 : FunLike F A B
inst_12 : NonUnitalAlgHomClass F S A B
φ : F
a : A
refine : ∀ x ∈ (quasispectrum R a)ᶜ, x ∈ (quasispectrum.{u_4, u_7} R (A := B) ((φ : (a : A) → B) a : B))ᶜ
⊢ quasispectrum.{u_4, u_7} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a

Tactic:
refine Set.compl_subset_compl.mp fun x ↦ ?_

Premises used: Set.compl_subset_compl, Iff.mp