no goals
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.688668
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x y : X
hoxy : ι R x = ι R y
⊢ ¬x = y → False
classical exact fun hxy : x ≠ y ↦
    let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
    have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
    have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
    have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
    one_ne_zero <| hfy1.symm.trans hfy0
no goals
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type ?u.688668
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x y : X
hoxy : ι R x = ι R y
⊢ ¬x = y → False
exact fun hxy : x ≠ y ↦
let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
one_ne_zero <| hfy1.symm.trans hfy0