awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ 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
have h₁ : 1 = HAdd.hAdd (α := Unitization R A) 1 (↑0 : Unitization R A)
Tactic: convert! congr((1 + $(inv_add_add_mul_eq_zero x) : Unitization R A)) using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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) (β := 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)
have 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))
Tactic: simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
              add_mul, inr_add, inr_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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) (β := 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
have 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)
Tactic: convert! congr((1 + $(add_inv_add_mul_eq_zero x) : Unitization R A)) using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ 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
have h₁ : 1 = HAdd.hAdd (α := Unitization R A) 1 (↑0 : Unitization R A)
Tactic: convert! congr((1 + $(add_inv_add_mul_eq_zero x) : Unitization R A)) using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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) (β := 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)
have 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))
Tactic: simp only [mul_one, PreQuasiregular.equiv_symm_apply, one_mul, mul_add,
              add_mul, inr_add, inr_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x : R
⊢ IsQuasiregular x ↔ ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0
have mp : IsQuasiregular x → ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ IsQuasiregular x ↔ ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0
have mpr : (∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0) → IsQuasiregular x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
have mpr : HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
    ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R)
    ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R) =
  1
Tactic: refine ⟨⟨equiv x, equiv y, ?_, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ IsQuasiregular x
have mpr₁ : HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
    ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R)
    ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R) =
  1
Tactic: refine ⟨⟨equiv x, equiv y, ?_, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R) =
    1
have 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)
Tactic: apply equiv.symm.injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : NonUnitalSemiring R
x y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ HMul.hMul (α := PreQuasiregular R) (β := PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) y : PreQuasiregular R)
      ((equiv : (a : R) → PreQuasiregular R) x : PreQuasiregular R) =
    1
have 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)
Tactic: apply equiv.symm.injective
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ IsQuasiregular.{u_3} (R := S) ((f : (a : R) → S) x : S)
have 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
Tactic: rw [isQuasiregular_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨y, hy₁, hy₂⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : IsQuasiregular x
⊢ IsUnit (1 + x)
have obtain : ∀ (y : R) (hy₁ : y + x + x * y = 0) (hy₂ : x + y + y * x = 0), IsUnit (1 + x)
Tactic: obtain ⟨y, hy₁, hy₂⟩ := isQuasiregular_iff.mp hx
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
have refine_1 : (1 + x) * (1 + y) = 1
Tactic: refine ⟨⟨1 + x, 1 + y, ?_, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ IsUnit (1 + x)
have refine_2 : (1 + y) * (1 + x) = 1
Tactic: refine ⟨⟨1 + x, 1 + y, ?_, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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) * (1 + y) = 1
have h : (1 + x) * (1 + y) = 1 + (y + x + x * y)
Tactic: convert! congr(1 + $(hy₁)) using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ (1 + x) * (1 + y) = 1
have h₁ : 1 = HAdd.hAdd (α := R) 1 0
Tactic: convert! congr(1 + $(hy₁)) using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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) * (1 + y) = 1 + (y + x + x * y)
have h : 1 + x + (y + x * y) = 1 + (y + x + x * y)
Tactic: noncomm_ring
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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) * (1 + y) = 1
have h : (1 + x) * (1 + y) = 1 + (y + x + x * y)
Tactic: convert! congr(1 + $(hy₁)) using 1 <;> [noncomm_ring; simp]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ (1 + x) * (1 + y) = 1
have h₁ : 1 = HAdd.hAdd (α := R) 1 0
Tactic: convert! congr(1 + $(hy₁)) using 1 <;> [noncomm_ring; simp]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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) * (1 + x) = 1
have h : (1 + y) * (1 + x) = 1 + (x + y + y * x)
Tactic: convert! congr(1 + $(hy₂)) using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ (1 + y) * (1 + x) = 1
have h₁ : 1 = HAdd.hAdd (α := R) 1 0
Tactic: convert! congr(1 + $(hy₂)) using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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) * (1 + x) = 1 + (x + y + y * x)
have h : 1 + y + (x + y * x) = 1 + (x + y + y * x)
Tactic: noncomm_ring
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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) * (1 + x) = 1
have h : (1 + y) * (1 + x) = 1 + (x + y + y * x)
Tactic: convert! congr(1 + $(hy₂)) using 1 <;> [noncomm_ring; simp]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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)
⊢ (1 + y) * (1 + x) = 1
have h₁ : 1 = HAdd.hAdd (α := R) 1 0
Tactic: convert! congr(1 + $(hy₂)) using 1 <;> [noncomm_ring; simp]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
⊢ IsQuasiregular x ↔ IsUnit (1 + x)
have refine : ∀ (hx : IsUnit (1 + x)), IsQuasiregular x
Tactic: refine ⟨IsQuasiregular.isUnit_one_add, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ IsQuasiregular x
have rw : ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0
Tactic: rw [isQuasiregular_iff]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0
have h : (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0 ∧ x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0
Tactic: use hx.unit⁻¹ - 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0 ∧
    x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0
have h : (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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
⊢ (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0 ∧
    x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0
have h₁ : x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0
have this : (1 + x) * (↑hx.unit⁻¹ : R) - 1 = HSub.hSub (α := R) 1 1
Tactic: have := congr($(hx.mul_val_inv) - 1)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0
have this : (1 + x) * (↑hx.unit⁻¹ : R) - 1 = HSub.hSub (α := R) 1 1
Tactic: case' h.left => have := congr($(hx.mul_val_inv) - 1)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0
have this : (↑hx.unit⁻¹ : R) * (1 + x) - 1 = HSub.hSub (α := R) 1 1
Tactic: have := congr($(hx.val_inv_mul) - 1)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
⊢ x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0
have this : (↑hx.unit⁻¹ : R) * (1 + x) - 1 = HSub.hSub (α := R) 1 1
Tactic: case' h.right => have := congr($(hx.val_inv_mul) - 1)
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (hypothesis)
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
⊢ x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0
have this₁ : ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1 = 0
Tactic: rw [← sub_add_cancel (↑hx.unit⁻¹ : R) 1, sub_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1 = 0
⊢ x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = 0
have h : x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1 = 0
⊢ x + ((↑hx.unit⁻¹ : R) - 1) + ((↑hx.unit⁻¹ : R) - 1) * x = ((↑hx.unit⁻¹ : R) - 1 + 1) * (1 + x) - 1
have h : x + ((↑hx.unit⁻¹ : R) + -1) + ((↑hx.unit⁻¹ : R) * x + -x) =
  (↑hx.unit⁻¹ : R) + -1 + 1 + ((↑hx.unit⁻¹ : R) * x + -x + x) + -1
Tactic: noncomm_ring
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (hypothesis)
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
⊢ (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0
have this₁ : (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1 = 0
Tactic: rw [← sub_add_cancel (↑hx.unit⁻¹ : R) 1, sub_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1 = 0
⊢ (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = 0
have h : (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
hx : IsUnit (1 + x)
this : (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1 = 0
⊢ (↑hx.unit⁻¹ : R) - 1 + x + x * ((↑hx.unit⁻¹ : R) - 1) = (1 + x) * ((↑hx.unit⁻¹ : R) - 1 + 1) - 1
have h : (↑hx.unit⁻¹ : R) + -1 + x + (x * (↑hx.unit⁻¹ : R) + -x) =
  (↑hx.unit⁻¹ : R) + x * (↑hx.unit⁻¹ : R) + -(1 + x) + (1 + x) + -1
Tactic: noncomm_ring
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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))
have refine_1 : IsQuasiregular x → IsUnit (HAdd.hAdd (α := Unitization R A) 1 (↑x : Unitization R A))
Tactic: refine ⟨?_, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Spectrum.Quasispectrum (goal)
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))
⊢ IsQuasiregular x ↔ IsUnit (HAdd.hAdd (α := Unitization R A) 1 (↑x : Unitization R A))
have refine_2 : ∀ (hx : IsUnit (HAdd.hAdd (α := Unitization R A) 1 (↑x : Unitization R A))), IsQuasiregular x
Tactic: refine ⟨?_, fun hx ↦ ?_⟩