[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ a * a = 0 ↔
    ∀ (x y : R),
      ↑(↑(LinearEquiv.toEquiv (LinearEquiv.symm (LinearMap.ringLmapEquivSelf R ℕ A))) a) x *
          ↑(↑(LinearEquiv.toEquiv (LinearEquiv.symm (LinearMap.ringLmapEquivSelf R ℕ A))) a) y =
        0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ a * a = 0 ↔ ∀ (x y : R), x • a * y • a = 0
[PROOFSTEP]
simp_rw [smul_mul_smul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ a * a = 0 ↔ ∀ (x y : R), (x * y) • (a * a) = 0
[PROOFSTEP]
refine' ⟨fun h x y => h.symm ▸ smul_zero _, fun h => by simpa using h 1 1⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : ∀ (x y : R), (x * y) • (a * a) = 0
⊢ a * a = 0
[PROOFSTEP]
simpa using h 1 1
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
e : { e // e * e = 0 }
⊢ ↑(↑lift e) ε = ↑e
[PROOFSTEP]
simp only [lift_apply_apply, fst_eps, map_zero, snd_eps, one_smul, zero_add]
