-- Mathlib/Algebra/FreeAlgebra.lean
theorem ι_ne_algebraMap [Nontrivial R] (x : X) (r : R) : ι R x ≠ algebraMap R _ r := fun h ↦ by
  let f0 : FreeAlgebra R X →ₐ[R] R := lift R 0
  let f1 : FreeAlgebra R X →ₐ[R] R := lift R 1
  have hf0 : f0 (ι R x) = 0 := lift_ι_apply _ _
  have hf1 : f1 (ι R x) = 1 := lift_ι_apply _ _
  rw [h, f0.commutes, Algebra.id.map_eq_self] at hf0
  rw [h, f1.commutes, Algebra.id.map_eq_self] at hf1
  exact zero_ne_one (hf0.symm.trans hf1)

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
⊢ False

Tactic:
have hf0 : f0 (ι R x) = 0 := lift_ι_apply _ _

Result:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : f0 (ι R x) = 0
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
⊢ False

Tactic:
let f0 : FreeAlgebra R X →ₐ[R] R := lift R 0

Result:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
⊢ False

Tactic:
let f1 : FreeAlgebra R X →ₐ[R] R := lift R 1

Result:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : r = 0
hf1 : f1 (ι R x) = 1
⊢ False

Tactic:
rw [h, f1.commutes, Algebra.id.map_eq_self] at hf1

Result:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : r = 0
hf1 : r = 1
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : f0 (ι R x) = 0
hf1 : f1 (ι R x) = 1
⊢ False

Tactic:
rw [h, f0.commutes, Algebra.id.map_eq_self] at hf0

Result:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : r = 0
hf1 : f1 (ι R x) = 1
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : r = 0
hf1 : r = 1
⊢ False

Tactic:
exact zero_ne_one (hf0.symm.trans hf1)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : f0 (ι R x) = 0
⊢ False

Tactic:
have hf1 : f1 (ι R x) = 1 := lift_ι_apply _ _

Result:
R : Type u_1
inst✝¹ : CommSemiring R
X : Type u_2
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : f0 (ι R x) = 0
hf1 : f1 (ι R x) = 1
⊢ False