-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma isQuasiregular_inr_iff (a : A) :
    IsQuasiregular (a : Unitization R A) ↔ IsQuasiregular a

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : ∃ y, y + ↑a + ↑a * y = 0 ∧ ↑a + y + y * ↑a = 0
⊢ ∃ y, y + a + a * y = 0 ∧ a + y + y * a = 0

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := ha

Result:
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
y : Unitization R A
hy₁ : y + ↑a + ↑a * y = 0
hy₂ : ↑a + y + y * ↑a = 0
⊢ ∃ y, y + a + a * y = 0 ∧ a + y + y * a = 0

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ ↑(a + y + y * a) = ↑0

Tactic:
simpa

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
y : Unitization R A
hy₁ : y + ↑a + ↑a * y = 0
hy₂ : ↑a + y + y * ↑a = 0
⊢ ∃ y, y + a + a * y = 0 ∧ a + y + y * a = 0

Tactic:
lift y to A using by simpa using congr(fstHom R A $(hy₁))

Result:
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ ∃ y, y + a + a * y = 0 ∧ a + y + y * a = 0

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
⊢ IsQuasiregular ↑a ↔ IsQuasiregular a

Tactic:
refine ⟨fun ha ↦ ?_, IsQuasiregular.map (inrNonUnitalAlgHom R A)⟩

Result:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : IsQuasiregular ↑a
⊢ IsQuasiregular a

Proof state:
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a y : A
hy₁ : ↑y + ↑a + ↑a * ↑y = 0
hy₂ : ↑a + ↑y + ↑y * ↑a = 0
⊢ ∃ y, y + a + a * y = 0 ∧ a + y + y * a = 0

Tactic:
refine ⟨y, ?_, ?_⟩ <;> exact inr_injective (R := R) <| by simpa

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : IsQuasiregular ↑a
⊢ IsQuasiregular a

Tactic:
rw [isQuasiregular_iff] at ha ⊢

Result:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
ha : ∃ y, y + ↑a + ↑a * y = 0 ∧ ↑a + y + y * ↑a = 0
⊢ ∃ y, y + a + a * y = 0 ∧ a + y + y * a = 0

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalRing A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
a : A
y : Unitization R A
hy₁ : y + ↑a + ↑a * y = 0
hy₂ : ↑a + y + y * ↑a = 0
⊢ y.fst = 0

Tactic:
simpa using congr(fstHom R A $(hy₁))

Result:
no goals