F : Type u_2
R : Type u_1
A : Type u_3
B : Type ?u.1475208
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
h : ↑↑ₐ (↑φ a) - a ∈ RingHom.ker ↑φ
⊢ ↑φ a ∈ σ a
F : Type u_2
R : Type u_1
A : Type u_3
B : Type ?u.1475208
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ ↑φ a ∈ σ a
have h : ↑ₐ (φ a) - a ∈ RingHom.ker (φ : A →+* R) := by
  simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes,
    Algebra.id.map_eq_id, RingHom.id_apply, sub_self]
no goals
F : Type u_2
R : Type u_1
A : Type u_3
B : Type ?u.1475208
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
h : ↑↑ₐ (↑φ a) - a ∈ RingHom.ker ↑φ
⊢ ↑φ a ∈ σ a
simp only [spectrum.mem_iff, ← mem_nonunits_iff,
  coe_subset_nonunits (RingHom.ker_ne_top (φ : A →+* R)) h]
no goals
F : Type u_2
R : Type u_1
A : Type u_3
B : Type ?u.1475208
inst✝⁶ : CommRing R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : AlgHomClass F R A R
inst✝ : Nontrivial R
φ : F
a : A
⊢ ↑↑ₐ (↑φ a) - a ∈ RingHom.ker ↑φ
simp only [RingHom.mem_ker, map_sub, RingHom.coe_coe, AlgHomClass.commutes,
  Algebra.id.map_eq_id, RingHom.id_apply, sub_self]