awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
this_1 : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (R := Ideal A) (IsLocalRing.maximalIdeal A)
e : AlgEquiv.{u_1, u_1, u_2} K K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
  let __spread.0 : AlgHom.{u_1, u_1, u_2} K K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
    ofId K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A));
  let __spread.1 : Equiv.{u_1 + 1, u_2 + 1} K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
    Equiv.ofBijective
      (⇑(algebraMap K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) :
        (a : K) → A ⧸ IsLocalRing.maximalIdeal A)
      ⋯;
  {
    toFun :=
      (↑(↑__spread.0.toRingHom : K →* A ⧸ IsLocalRing.maximalIdeal A) :
          OneHom K (A ⧸ IsLocalRing.maximalIdeal A)).toFun,
    invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  AlgEquiv.trans (A₂ := A ⊗[K] K)
    (TensorProduct.congr AlgEquiv.refl e.symm :
      A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) ≃ₐ[A] A ⊗[K] K)
    (TensorProduct.rid K A A : A ⊗[K] K ≃ₐ[A] A)
f : HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) →ₗ[A] A :=
  e'.toLinearMap ∘ₗ sec K A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
hf :
  AlgHom.toLinearMap (ofId A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) ∘ₗ f = LinearMap.id
hf₁ :
  HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
    1
hf₂ :
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₃ : IsIdempotentElem (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₄ : Eq (α := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) (1 : A)
x : A
k : K
rw : ((algebraMap K A : (a : K) → A) k : A)
| (Function.comp (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      (⇑f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) (⇑e : (a : K) → A ⧸ IsLocalRing.maximalIdeal A) k :
    A)

Tactic:
rw [← mul_one k, ← smul_eq_mul, Function.comp_apply, map_smul,
      LinearMap.map_smul_of_tower, map_one, hf₄, ← algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, map_one, Function.comp_apply, LinearMap.map_smul_of_tower, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
this_1 : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (R := Ideal A) (IsLocalRing.maximalIdeal A)
e : AlgEquiv.{u_1, u_1, u_2} K K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
  let __spread.0 : AlgHom.{u_1, u_1, u_2} K K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
    ofId K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A));
  let __spread.1 : Equiv.{u_1 + 1, u_2 + 1} K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A)) :=
    Equiv.ofBijective
      (⇑(algebraMap K (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) :
        (a : K) → A ⧸ IsLocalRing.maximalIdeal A)
      ⋯;
  {
    toFun :=
      (↑(↑__spread.0.toRingHom : K →* A ⧸ IsLocalRing.maximalIdeal A) :
          OneHom K (A ⧸ IsLocalRing.maximalIdeal A)).toFun,
    invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  AlgEquiv.trans (A₂ := A ⊗[K] K)
    (TensorProduct.congr AlgEquiv.refl e.symm :
      A ⊗[K] HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) ≃ₐ[A] A ⊗[K] K)
    (TensorProduct.rid K A A : A ⊗[K] K ≃ₐ[A] A)
f : HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A) →ₗ[A] A :=
  e'.toLinearMap ∘ₗ sec K A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
hf :
  AlgHom.toLinearMap (ofId A (HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))) ∘ₗ f = LinearMap.id
hf₁ :
  HSMul.hSMul (α := A) (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) 1 =
    1
hf₂ :
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₃ : IsIdempotentElem (HSub.hSub (α := A) (β := A) (1 : A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A))
hf₄ : Eq (α := A) ((f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) 1 : A) (1 : A)
x : A
⊢ Eq (α := (a : K) → A) (⇑(algebraMap K A) : (a : K) → A)
    (Function.comp (β := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A))
      (⇑f : (a : A ⧸ IsLocalRing.maximalIdeal A) → A) (⇑e : (a : K) → A ⧸ IsLocalRing.maximalIdeal A))

Tactic:
have : ⇑(algebraMap K A) = ⇑f ∘ ⇑e := by
    ext k
    conv_rhs => rw [← mul_one k, ← smul_eq_mul, Function.comp_apply, map_smul,
      LinearMap.map_smul_of_tower, map_one, hf₄, ← algebraMap_eq_smul_one]
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
rw : LE.le (α := Ideal A) (IsLocalRing.maximalIdeal A) ⊥
⊢ IsField A

Tactic:
rw [IsLocalRing.isField_iff_maximalIdeal_eq, eq_bot_iff]

Premises used: IsLocalRing.isField_iff_maximalIdeal_eq, eq_bot_iff
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
x : A
hx : Membership.mem (γ := Submodule A A) (IsLocalRing.maximalIdeal A) x
obtain :
  ∀ (x : K)
    (hx :
      Membership.mem (α := A) (γ := Submodule A A) (IsLocalRing.maximalIdeal A) ((algebraMap K A : (a : K) → A) x : A)),
    Membership.mem.{u_2, u_2} (α := A) (γ := Submodule A A) ⊥ ((algebraMap K A : (a : K) → A) x : A)
⊢ Membership.mem (γ := Submodule A A) ⊥ x

Tactic:
obtain ⟨x, rfl⟩ := (bijective_of_isAlgClosed_of_isLocalRing K A).surjective x

Premises used: Algebra.FormallyUnramified.bijective_of_isAlgClosed_of_isLocalRing, Function.Bijective.surjective, rfl
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
x : K
hx : Membership.mem (α := A) (γ := Submodule A A) (IsLocalRing.maximalIdeal A) ((algebraMap K A : (a : K) → A) x : A)
rw : Eq.{u_2 + 1} (α := A) ((algebraMap K A : (a : K) → A) x : A) ((algebraMap K A : (a : K) → A) 0 : A)
⊢ Eq.{u_2 + 1} (α := A) ((algebraMap K A : (a : K) → A) x : A) (0 : A)

Tactic:
rw [← (algebraMap K A).map_zero]

Premises used: Algebra.algebraMap, RingHom.map_zero
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
x : K
hx : Membership.mem (α := A) (γ := Submodule A A) (IsLocalRing.maximalIdeal A) ((algebraMap K A : (a : K) → A) x : A)
by_contra :
  ∀ (hx' : ¬Eq.{u_2 + 1} (α := A) ((algebraMap K A : (a : K) → A) x : A) ((algebraMap K A : (a : K) → A) 0 : A)), False
⊢ Eq.{u_2 + 1} (α := A) ((algebraMap K A : (a : K) → A) x : A) ((algebraMap K A : (a : K) → A) 0 : A)

Tactic:
by_contra hx'
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
x : K
hx : Membership.mem (α := A) (γ := Submodule A A) (IsLocalRing.maximalIdeal A) ((algebraMap K A : (a : K) → A) x : A)
hx' : ¬Eq.{u_2 + 1} (α := A) ((algebraMap K A : (a : K) → A) x : A) ((algebraMap K A : (a : K) → A) 0 : A)
⊢ False

Tactic:
hx ((isUnit_iff_ne_zero.mpr
    (fun e ↦ hx' ((algebraMap K A).congr_arg e))).map (algebraMap K A))

Premises used: Iff.mpr, Algebra.algebraMap, isUnit_iff_ne_zero, IsUnit.map, RingHom.congr_arg
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
inst_5 : IsAlgClosed K
inst_6 : IsLocalRing A
x : K
hx : Membership.mem (α := A) (γ := Submodule A A) (IsLocalRing.maximalIdeal A) ((algebraMap K A : (a : K) → A) x : A)
hx' : ¬Eq.{u_2 + 1} (α := A) ((algebraMap K A : (a : K) → A) x : A) ((algebraMap K A : (a : K) → A) 0 : A)
⊢ False

Tactic:
exact hx ((isUnit_iff_ne_zero.mpr
    (fun e ↦ hx' ((algebraMap K A).congr_arg e))).map (algebraMap K A))

Premises used: Iff.mpr, Algebra.algebraMap, isUnit_iff_ne_zero, IsUnit.map, RingHom.congr_arg
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
eq_zero : ∀ (x : A), IsNilpotent x → x = 0
⊢ IsReduced A

Tactic:
constructor
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
h :
  ∀ (x : A),
    Eq (α := AlgebraicClosure K ⊗[K] A) ((f : (a : A) → AlgebraicClosure K ⊗[K] A) x : AlgebraicClosure K ⊗[K] A)
      ((LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
              AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A)) :
            (a : A) → AlgebraicClosure K ⊗[K] A)
          x :
        AlgebraicClosure K ⊗[K] A)
⊢ Eq (α := (a : A) → AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)

Tactic:
ext x
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x_1 : A
hx : IsNilpotent x_1
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
x : A
⊢ Eq (α := AlgebraicClosure K ⊗[K] A) ((f : (a : A) → AlgebraicClosure K ⊗[K] A) x : AlgebraicClosure K ⊗[K] A)
    ((LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
            AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A)) :
          (a : A) → AlgebraicClosure K ⊗[K] A)
        x :
      AlgebraicClosure K ⊗[K] A)

Tactic:
simp [f]
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
⊢ Eq (α := (a : A) → AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)

Tactic:
have : ⇑f = (LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap).comp
        (Algebra.TensorProduct.lid K A).symm.toLinearMap := by
      ext x; simp [f]
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this :
  Eq (α := (a : A) → AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)
rw :
  Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)
⊢ Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this_1 :
  Eq (α := (a : A) → AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)
this :
  Function.Injective (α := K ⊗[K] A) (β := AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K)))) :
      (a : K ⊗[K] A) → AlgebraicClosure K ⊗[K] A)
⊢ Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)

Tactic:
this.comp (Algebra.TensorProduct.lid K A).symm.injective

Premises used: AlgEquiv.symm, Quotient.liftOn', AddCon.liftOn, List.foldl, Algebra.TensorProduct.lid, Function.Injective.comp, AlgEquiv.injective, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this_1 :
  Eq (α := (a : A) → AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)
this :
  Function.Injective (α := K ⊗[K] A) (β := AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K)))) :
      (a : K ⊗[K] A) → AlgebraicClosure K ⊗[K] A)
⊢ Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)

Tactic:
exact this.comp (Algebra.TensorProduct.lid K A).symm.injective

Premises used: AlgEquiv.symm, Algebra.TensorProduct.lid, Function.Injective.comp, AlgEquiv.injective
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this :
  Eq (α := (a : A) → AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)
suffices :
  Function.Injective (α := K ⊗[K] A) (β := AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K)))) :
      (a : K ⊗[K] A) → AlgebraicClosure K ⊗[K] A)
⊢ Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)

Tactic:
suffices Function.Injective
        (LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap) by
      exact this.comp (Algebra.TensorProduct.lid K A).symm.injective
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this :
  Eq (α := (a : A) → AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)
hf :
  Function.Injective (α := K) (β := AlgebraicClosure K)
    (⇑(AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) : (a : K) → AlgebraicClosure K)
⊢ Function.Injective (α := K ⊗[K] A) (β := AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K)))) :
      (a : K ⊗[K] A) → AlgebraicClosure K ⊗[K] A)

Tactic:
apply Module.Flat.rTensor_preserves_injective_linearMap

Premises used: Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this :
  Eq (α := (a : A) → AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)
⊢ Function.Injective (α := K) (β := AlgebraicClosure K)
    (⇑(AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) : (a : K) → AlgebraicClosure K)

Tactic:
(algebraMap K _).injective

Premises used: Algebra.algebraMap, Submodule.Quotient.mk, RingHom.injective
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this :
  Eq (α := (a : A) → AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) ∘ₗ
          AlgEquiv.toLinearMap (AlgEquiv.symm (TensorProduct.lid K A))) :
      (a : A) → AlgebraicClosure K ⊗[K] A)
⊢ Function.Injective (α := K) (β := AlgebraicClosure K)
    (⇑(AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) : (a : K) → AlgebraicClosure K)

Tactic:
exact (algebraMap K _).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
⊢ Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)

Tactic:
have : Function.Injective f := by
    have : ⇑f = (LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap).comp
        (Algebra.TensorProduct.lid K A).symm.toLinearMap := by
      ext x; simp [f]
    rw [this]
    suffices Function.Injective
        (LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap) by
      exact this.comp (Algebra.TensorProduct.lid K A).symm.injective
    apply Module.Flat.rTensor_preserves_injective_linearMap
    exact (algebraMap K _).injective
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
eq_zero :
  Eq (α := AlgebraicClosure K ⊗[K] A) ((f : (a : A) → AlgebraicClosure K ⊗[K] A) x : AlgebraicClosure K ⊗[K] A)
    ((f : (a : A) → AlgebraicClosure K ⊗[K] A) 0 : AlgebraicClosure K ⊗[K] A)
⊢ x = 0

Tactic:
apply this
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
eq_zero :
  Eq (α := AlgebraicClosure K ⊗[K] A) ((f : (a : A) → AlgebraicClosure K ⊗[K] A) x : AlgebraicClosure K ⊗[K] A)
    (0 : AlgebraicClosure K ⊗[K] A)
⊢ Eq (α := AlgebraicClosure K ⊗[K] A) ((f : (a : A) → AlgebraicClosure K ⊗[K] A) x : AlgebraicClosure K ⊗[K] A)
    ((f : (a : A) → AlgebraicClosure K ⊗[K] A) 0 : AlgebraicClosure K ⊗[K] A)

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
eq_zero :
  ∀ (J : Ideal (AlgebraicClosure K ⊗[K] A)) (x_1 : J.IsMaximal),
    Eq (α := Localization.AtPrime J)
      ((algebraMap (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime J) :
            (a : AlgebraicClosure K ⊗[K] A) → Localization.AtPrime J)
          ((f : (a : A) → AlgebraicClosure K ⊗[K] A) x) :
        Localization.AtPrime J)
      (0 : Localization.AtPrime J)
⊢ Eq (α := AlgebraicClosure K ⊗[K] A) ((f : (a : A) → AlgebraicClosure K ⊗[K] A) x : AlgebraicClosure K ⊗[K] A)
    (0 : AlgebraicClosure K ⊗[K] A)

Tactic:
apply eq_zero_of_localization

Premises used: eq_zero_of_localization
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
A : Type u_2
inst : Field K
inst_1 : CommRing A
inst_2 : Algebra K A
inst_3 : FormallyUnramified K A
inst_4 : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
⊢ IsNilpotent (R := Localization.AtPrime M)
    ((algebraMap (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M) :
          (a : AlgebraicClosure K ⊗[K] A) → Localization.AtPrime M)
        ((f : (a : A) → AlgebraicClosure K ⊗[K] A) x) :
      Localization.AtPrime M)

Tactic:
have hy := (hx.map f).map (algebraMap _ (Localization.AtPrime M))