-- Mathlib/RingTheory/Unramified/Field.lean
theorem isReduced_of_field :
    IsReduced A

Proof state:
case eq_zero.a.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this✝³ : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this✝² : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝¹ : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝ : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
this : FormallyUnramified (AlgebraicClosure K) (Localization.AtPrime M)
⊢ y = 0

Tactic:
letI := (isField_of_isAlgClosed_of_isLocalRing (AlgebraicClosure K)
  (A := Localization.AtPrime M)).toField

Result:
case eq_zero.a.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this✝⁴ : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this✝³ : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝² : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝¹ : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
this✝ : FormallyUnramified (AlgebraicClosure K) (Localization.AtPrime M)
this : Field (Localization.AtPrime M) := ⋯.toField
⊢ y = 0

Proof state:
case hf
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : ⇑f = ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap)
⊢ Function.Injective ⇑(ofId K (AlgebraicClosure K)).toLinearMap

Tactic:
exact (algebraMap K _).injective

Result:
no goals

Proof state:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : ⇑f = ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap)
⊢ Function.Injective
    ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap)

Tactic:
suffices Function.Injective
    (LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap) by
  exact this.comp (Algebra.TensorProduct.lid K A).symm.injective

Result:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : ⇑f = ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap)
⊢ Function.Injective ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap)

Proof state:
case eq_zero
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
⊢ ∀ (x : A), IsNilpotent x → x = 0

Tactic:
intro x hx

Result:
case eq_zero
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
⊢ x = 0

Proof state:
case eq_zero.a
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective ⇑f
⊢ f x = f 0

Tactic:
rw [map_zero]

Result:
case eq_zero.a
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective ⇑f
⊢ f x = 0

Proof state:
case eq_zero.a
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective ⇑f
⊢ f x = 0

Tactic:
apply eq_zero_of_localization

Result:
case eq_zero.a.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective ⇑f
⊢ ∀ (J : Ideal (AlgebraicClosure K ⊗[K] A)) (x_1 : J.IsMaximal),
    (algebraMap (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime J)) (f x) = 0

Proof state:
case eq_zero.a.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this✝¹ : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this✝ : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
⊢ y = 0

Tactic:
have := EssFiniteType.comp (AlgebraicClosure K) (AlgebraicClosure K ⊗[K] A)
  (Localization.AtPrime M)

Result:
case eq_zero.a.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this✝² : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this✝¹ : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this✝ : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
⊢ y = 0

Proof state:
case eq_zero.a.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this✝ : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
⊢ y = 0

Tactic:
have := of_isLocalization (Rₘ := Localization.AtPrime M) M.primeCompl

Result:
case eq_zero.a.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this✝¹ : Function.Injective ⇑f
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this✝ : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
⊢ y = 0