awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y z : PreQuasiregular R
⊢ z.val + (y.val + x.val + x.val * y.val) + (y.val * z.val + x.val * z.val + x.val * (y.val * z.val)) =
    z.val + y.val + y.val * z.val + x.val + (x.val * z.val + x.val * y.val + x.val * (y.val * z.val))

Tactic:
abel
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x : PreQuasiregular R
⊢ Eq (α := R) ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (1 * x) : R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R) x : R)

Tactic:
simp [-EmbeddingLike.apply_eq_iff_eq]

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x : PreQuasiregular R
⊢ Eq (α := R) ((Equiv.symm equiv : (a : PreQuasiregular R) → R) (x * 1) : R)
    ((Equiv.symm equiv : (a : PreQuasiregular R) → R) x : R)

Tactic:
simp [-EmbeddingLike.apply_eq_iff_eq]

Premises used: EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ (↑u⁻¹ : PreQuasiregular R).val + (↑u : PreQuasiregular R).val +
      (↑u : PreQuasiregular R).val * (↑u⁻¹ : PreQuasiregular R).val =
    0

Tactic:
simpa [-Units.mul_inv] using congr($(u.mul_inv).val)

Premises used: Units.mul_inv
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
u : (PreQuasiregular R)ˣ
⊢ (↑u : PreQuasiregular R).val + (↑u⁻¹ : PreQuasiregular R).val +
      (↑u⁻¹ : PreQuasiregular R).val * (↑u : PreQuasiregular R).val =
    0

Tactic:
simpa [-Units.inv_mul] using congr($(u.inv_mul).val)

Premises used: Units.inv_mul
-- 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 y : (Unitization R A)ˣ
hx : (↑x : Unitization R A).toProd.1 = 1
hy : (↑y : Unitization R A).toProd.1 = 1
⊢ Membership.mem (γ := Set (Unitization R A)ˣ) {x : (Unitization R A)ˣ | (↑x : Unitization R A).toProd.1 = 1} (x * y)

Tactic:
simp [hx, hy]
-- 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 : (Unitization R A)ˣ
hx : (↑x : Unitization R A).toProd.1 = 1
⊢ Membership.mem (γ := Set (Unitization R A)ˣ) {x : (Unitization R A)ˣ | (↑x : Unitization R A).toProd.1 = 1} x⁻¹

Tactic:
simpa [-Units.mul_inv, hx] using congr(fstHom R A $(x.mul_inv))

Premises used: Units.mul_inv
-- 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 : (Unitization R A)ˣ
⊢ Membership.mem (γ := Subgroup (Unitization R A)ˣ) (unitsFstOne R A) x ↔ (↑x : Unitization R A).toProd.1 = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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 : ↥(unitsFstOne R A)
⊢ (↑(↑x : (Unitization R A)ˣ) : Unitization R A).toProd.1 = 1

Tactic:
mem_unitsFstOne.mp x.property

Premises used: Iff.mp, Unitization.mem_unitsFstOne, Subtype.property
-- 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 : ↥(unitsFstOne R A)
⊢ (↑(↑x : (Unitization R A)ˣ)⁻¹ : Unitization R A).toProd.1 = 1

Tactic:
mem_unitsFstOne.mp x⁻¹.property

Premises used: Inv.inv, Iff.mp, Unitization.mem_unitsFstOne, Subtype.property
-- 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 : ↥(unitsFstOne R A)
⊢ Eq (α := A)
    ((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A)
        (HMul.hMul (α := PreQuasiregular A) (β := PreQuasiregular A)
          ((PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
              (↑(↑x : (Unitization R A)ˣ) : Unitization R A).toProd.2 :
            PreQuasiregular A)
          ((PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
              (↑(↑x⁻¹ : (Unitization R A)ˣ) : Unitization R A).toProd.2 :
            PreQuasiregular A)) :
      A)
    ((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) 1 : A)

Tactic:
simpa [-Units.mul_inv] using congr($(x.val.mul_inv).snd)

Premises used: Units.mul_inv
-- 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 : ↥(unitsFstOne R A)
⊢ Eq (α := A)
    ((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A)
        (HMul.hMul (α := PreQuasiregular A) (β := PreQuasiregular A)
          ((PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
              (↑(↑x⁻¹ : (Unitization R A)ˣ) : Unitization R A).toProd.2 :
            PreQuasiregular A)
          ((PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
              (↑(↑x : (Unitization R A)ˣ) : Unitization R A).toProd.2 :
            PreQuasiregular A)) :
      A)
    ((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) 1 : A)

Tactic:
simpa [-Units.inv_mul] using congr($(x.val.inv_mul).snd)

Premises used: Units.inv_mul
-- 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 : (PreQuasiregular A)ˣ
⊢ HAdd.hAdd (α := Unitization R A) 1
      (↑((↑x⁻¹ : PreQuasiregular A).val + (↑x : PreQuasiregular A).val +
            (↑x : PreQuasiregular A).val * (↑x⁻¹ : PreQuasiregular A).val) :
        Unitization R A) =
    HAdd.hAdd (α := Unitization R A) 1 (↑0 : Unitization R A)

Tactic:
congr((1 + $(inv_add_add_mul_eq_zero x) : Unitization R A))

Premises used: congrArg, PreQuasiregular.inv_add_add_mul_eq_zero, Unitization.inr, id, HAdd.hAdd, OfNat.ofNat
-- 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 : (PreQuasiregular A)ˣ
h :
  HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) *
      HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x⁻¹ : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) =
    HAdd.hAdd (α := Unitization R A) 1
      (↑((↑x⁻¹ : PreQuasiregular A).val + (↑x : PreQuasiregular A).val +
            (↑x : PreQuasiregular A).val * (↑x⁻¹ : PreQuasiregular A).val) :
        Unitization R A)
h₁ : 1 = HAdd.hAdd (α := Unitization R A) 1 (↑0 : Unitization R A)
⊢ HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) *
      HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x⁻¹ : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) =
    1

Tactic:
convert! congr((1 + $(inv_add_add_mul_eq_zero x) : Unitization R A)) using 1
-- 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 : (PreQuasiregular A)ˣ
h :
  HAdd.hAdd (α := Unitization R A) 1 (↑(↑x : PreQuasiregular A).val : Unitization R A) +
      ((↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A) +
        HMul.hMul (α := Unitization R A) (↑(↑x : PreQuasiregular A).val : Unitization R A)
          (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A)) =
    1 +
      (HAdd.hAdd (α := Unitization R A) (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A)
          (↑(↑x : PreQuasiregular A).val : Unitization R A) +
        HMul.hMul (α := Unitization R A) (↑(↑x : PreQuasiregular A).val : Unitization R A)
          (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A))
⊢ HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) *
      HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x⁻¹ : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) =
    HAdd.hAdd (α := Unitization R A) 1
      (↑((↑x⁻¹ : PreQuasiregular A).val + (↑x : PreQuasiregular A).val +
            (↑x : PreQuasiregular A).val * (↑x⁻¹ : PreQuasiregular A).val) :
        Unitization R A)

Tactic:
simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
              add_mul, inr_add, inr_mul]

Premises used: add_mul, PreQuasiregular.equiv_symm_apply, Unitization.inr_mul, Unitization.inr_add, mul_add, mul_one, one_mul
-- 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 : (PreQuasiregular A)ˣ
⊢ HAdd.hAdd (α := Unitization R A) 1 (↑(↑x : PreQuasiregular A).val : Unitization R A) +
      ((↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A) +
        HMul.hMul (α := Unitization R A) (↑(↑x : PreQuasiregular A).val : Unitization R A)
          (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A)) =
    1 +
      (HAdd.hAdd (α := Unitization R A) (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A)
          (↑(↑x : PreQuasiregular A).val : Unitization R A) +
        HMul.hMul (α := Unitization R A) (↑(↑x : PreQuasiregular A).val : Unitization R A)
          (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A))

Tactic:
abel
-- 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 : (PreQuasiregular A)ˣ
⊢ 1 = HAdd.hAdd (α := Unitization R A) 1 (↑0 : Unitization R A)

Tactic:
simp only [inr_zero, add_zero]

Premises used: Unitization.inr_zero, add_zero
-- 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 : (PreQuasiregular A)ˣ
⊢ HAdd.hAdd (α := Unitization R A) 1
      (↑((↑x : PreQuasiregular A).val + (↑x⁻¹ : PreQuasiregular A).val +
            (↑x⁻¹ : PreQuasiregular A).val * (↑x : PreQuasiregular A).val) :
        Unitization R A) =
    HAdd.hAdd (α := Unitization R A) 1 (↑0 : Unitization R A)

Tactic:
congr((1 + $(add_inv_add_mul_eq_zero x) : Unitization R A))

Premises used: PreQuasiregular.add_inv_add_mul_eq_zero, congrArg, Unitization.inr, id, HAdd.hAdd, OfNat.ofNat
-- 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 : (PreQuasiregular A)ˣ
h :
  HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x⁻¹ : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) *
      HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) =
    HAdd.hAdd (α := Unitization R A) 1
      (↑((↑x : PreQuasiregular A).val + (↑x⁻¹ : PreQuasiregular A).val +
            (↑x⁻¹ : PreQuasiregular A).val * (↑x : PreQuasiregular A).val) :
        Unitization R A)
h₁ : 1 = HAdd.hAdd (α := Unitization R A) 1 (↑0 : Unitization R A)
⊢ HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x⁻¹ : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) *
      HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) =
    1

Tactic:
convert! congr((1 + $(add_inv_add_mul_eq_zero x) : Unitization R A)) using 1
-- 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 : (PreQuasiregular A)ˣ
h :
  HAdd.hAdd (α := Unitization R A) 1 (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A) +
      ((↑(↑x : PreQuasiregular A).val : Unitization R A) +
        HMul.hMul (α := Unitization R A) (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A)
          (↑(↑x : PreQuasiregular A).val : Unitization R A)) =
    1 +
      (HAdd.hAdd (α := Unitization R A) (↑(↑x : PreQuasiregular A).val : Unitization R A)
          (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A) +
        HMul.hMul (α := Unitization R A) (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A)
          (↑(↑x : PreQuasiregular A).val : Unitization R A))
⊢ HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x⁻¹ : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) *
      HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x : PreQuasiregular A)) :
            Unitization R A) :
          Unitization R A) =
    HAdd.hAdd (α := Unitization R A) 1
      (↑((↑x : PreQuasiregular A).val + (↑x⁻¹ : PreQuasiregular A).val +
            (↑x⁻¹ : PreQuasiregular A).val * (↑x : PreQuasiregular A).val) :
        Unitization R A)

Tactic:
simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
              add_mul, inr_add, inr_mul]

Premises used: add_mul, PreQuasiregular.equiv_symm_apply, Unitization.inr_mul, Unitization.inr_add, mul_add, mul_one, one_mul
-- 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 : (PreQuasiregular A)ˣ
⊢ HAdd.hAdd (α := Unitization R A) 1 (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A) +
      ((↑(↑x : PreQuasiregular A).val : Unitization R A) +
        HMul.hMul (α := Unitization R A) (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A)
          (↑(↑x : PreQuasiregular A).val : Unitization R A)) =
    1 +
      (HAdd.hAdd (α := Unitization R A) (↑(↑x : PreQuasiregular A).val : Unitization R A)
          (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A) +
        HMul.hMul (α := Unitization R A) (↑(↑x⁻¹ : PreQuasiregular A).val : Unitization R A)
          (↑(↑x : PreQuasiregular A).val : Unitization R A))

Tactic:
abel
-- 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 : (PreQuasiregular A)ˣ
⊢ Membership.mem (γ := Subgroup (Unitization R A)ˣ) (unitsFstOne R A)
    {
      val :=
        HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
          ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x : PreQuasiregular A)) :
              Unitization R A) :
            Unitization R A),
      inv :=
        HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
          ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x⁻¹ : PreQuasiregular A)) :
              Unitization R A) :
            Unitization R A),
      val_inv := ⋯, inv_val := ⋯ }

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 : ↥(unitsFstOne R A)
⊢ (↑(↑((fun (x : (PreQuasiregular A)ˣ) ↦
                (Subtype.mk (p := fun (x : (Unitization R A)ˣ) ↦
                    Membership.mem (γ := Subgroup (Unitization R A)ˣ) (unitsFstOne R A) x)
                    {
                      val :=
                        HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
                          ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A)
                                  (↑x : PreQuasiregular A)) :
                              Unitization R A) :
                            Unitization R A),
                      inv :=
                        HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
                          ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A)
                                  (↑x⁻¹ : PreQuasiregular A)) :
                              Unitization R A) :
                            Unitization R A),
                      val_inv := ⋯, inv_val := ⋯ }
                    ⋯ :
                  ↥(unitsFstOne R A)))
              ((fun (x : ↥(unitsFstOne R A)) ↦
                  ({
                      val :=
                        (PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
                          (↑(↑x : (Unitization R A)ˣ) : Unitization R A).toProd.2,
                      inv :=
                        (PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
                          (↑(↑x⁻¹ : (Unitization R A)ˣ) : Unitization R A).toProd.2,
                      val_inv := ⋯, inv_val := ⋯ } :
                    (PreQuasiregular A)ˣ))
                x)) :
          (Unitization R A)ˣ) :
      Unitization R A) =
    (↑(↑x : (Unitization R A)ˣ) : Unitization R A)

Tactic:
simpa using x.val.val.inl_fst_add_inr_snd_eq

Premises used: Units.val, Subtype.val, Unitization.inl_fst_add_inr_snd_eq
-- 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 : (PreQuasiregular A)ˣ
⊢ (↑((fun (x : ↥(unitsFstOne R A)) ↦
            ({
                val :=
                  (PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
                    (↑(↑x : (Unitization R A)ˣ) : Unitization R A).toProd.2,
                inv :=
                  (PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
                    (↑(↑x⁻¹ : (Unitization R A)ˣ) : Unitization R A).toProd.2,
                val_inv := ⋯, inv_val := ⋯ } :
              (PreQuasiregular A)ˣ))
          ((fun (x : (PreQuasiregular A)ˣ) ↦
              (Subtype.mk (p := fun (x : (Unitization R A)ˣ) ↦
                  Membership.mem (γ := Subgroup (Unitization R A)ˣ) (unitsFstOne R A) x)
                  {
                    val :=
                      HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
                        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A) (↑x : PreQuasiregular A)) :
                            Unitization R A) :
                          Unitization R A),
                    inv :=
                      HAdd.hAdd (α := Unitization R A) (β := Unitization R A) (1 : Unitization R A)
                        ((↑((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A)
                                (↑x⁻¹ : PreQuasiregular A)) :
                            Unitization R A) :
                          Unitization R A),
                    val_inv := ⋯, inv_val := ⋯ }
                  ⋯ :
                ↥(unitsFstOne R A)))
            x)) :
      PreQuasiregular A) =
    (↑x : PreQuasiregular A)

Tactic:
simp [-PreQuasiregular.equiv_symm_apply]

Premises used: PreQuasiregular.equiv_symm_apply
-- 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 y : ↥(unitsFstOne R A)
⊢ Eq (α := A)
    ((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A)
        ((↑{
                val :=
                  (PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
                    (↑(↑(x * y) : (Unitization R A)ˣ) : Unitization R A).toProd.2,
                inv :=
                  (PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
                    (↑(↑(x * y)⁻¹ : (Unitization R A)ˣ) : Unitization R A).toProd.2,
                val_inv := ⋯, inv_val := ⋯ } :
            PreQuasiregular A) :
          PreQuasiregular A) :
      A)
    ((Equiv.symm PreQuasiregular.equiv : (a : PreQuasiregular A) → A)
        (↑(HMul.hMul (α := (PreQuasiregular A)ˣ) (β := (PreQuasiregular A)ˣ)
              ({
                  val :=
                    (PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
                      (↑(↑x : (Unitization R A)ˣ) : Unitization R A).toProd.2,
                  inv :=
                    (PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
                      (↑(↑x⁻¹ : (Unitization R A)ˣ) : Unitization R A).toProd.2,
                  val_inv := ⋯, inv_val := ⋯ } :
                (PreQuasiregular A)ˣ)
              ({
                  val :=
                    (PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
                      (↑(↑y : (Unitization R A)ˣ) : Unitization R A).toProd.2,
                  inv :=
                    (PreQuasiregular.equiv : (a : A) → PreQuasiregular A)
                      (↑(↑y⁻¹ : (Unitization R A)ˣ) : Unitization R A).toProd.2,
                  val_inv := ⋯, inv_val := ⋯ } :
                (PreQuasiregular A)ˣ)) :
          PreQuasiregular A) :
      A)

Tactic:
simp
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
⊢ IsQuasiregular (R := ℕ) 0

Tactic:
⟨1, rfl⟩

Premises used: IsQuasiregular, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x : R
mp : IsQuasiregular x → ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0
mpr : (∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0) → IsQuasiregular x
⊢ IsQuasiregular x ↔ ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0

Tactic:
constructor