awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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 (α := A) (β := AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
have 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)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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 (α := 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)
have 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)
Tactic: suffices Function.Injective
        (LinearMap.rTensor A (Algebra.ofId K (AlgebraicClosure K)).toLinearMap) by
      exact this.comp (Algebra.TensorProduct.lid K A).symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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 ⊗[K] A) (β := AlgebraicClosure K ⊗[K] A)
    (⇑(LinearMap.rTensor A (AlgHom.toLinearMap (ofId K (AlgebraicClosure K)))) :
      (a : K ⊗[K] A) → AlgebraicClosure K ⊗[K] A)
have hf : Function.Injective (α := K) (β := AlgebraicClosure K)
  (⇑(AlgHom.toLinearMap (ofId K (AlgebraicClosure K))) : (a : K) → AlgebraicClosure K)
Tactic: apply Module.Flat.rTensor_preserves_injective_linearMap
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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
⊢ x = 0
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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)
⊢ x = 0
have 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)
Tactic: apply this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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 (α := 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)
have eq_zero : Eq (α := AlgebraicClosure K ⊗[K] A) ((f : (a : A) → AlgebraicClosure K ⊗[K] A) x : AlgebraicClosure K ⊗[K] A)
  (0 : AlgebraicClosure K ⊗[K] A)
Tactic: rw [map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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 (α := AlgebraicClosure K ⊗[K] A) ((f : (a : A) → AlgebraicClosure K ⊗[K] A) x : AlgebraicClosure K ⊗[K] A)
    (0 : AlgebraicClosure K ⊗[K] A)
have 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)
Tactic: apply eq_zero_of_localization
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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
⊢ Eq (α := 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)
    (0 : Localization.AtPrime M)
have hy : 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))
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
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
hy :
  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)
⊢ Eq (α := 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)
    (0 : Localization.AtPrime M)
have eq_zero : ∀ (y : Localization.AtPrime M) (hy : IsNilpotent y), y = 0
Tactic: generalize algebraMap _ (Localization.AtPrime M) (f x) = y at *
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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
y : Localization.AtPrime M
hy : IsNilpotent y
⊢ y = 0
have this₁ : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
Tactic: have := EssFiniteType.of_isLocalization (Localization.AtPrime M) M.primeCompl
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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 : Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
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
have this₁ : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
Tactic: have := of_isLocalization (Rₘ := Localization.AtPrime M) M.primeCompl
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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 : Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this_2 : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
⊢ y = 0
have this₁ : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
Tactic: have := EssFiniteType.comp (AlgebraicClosure K) (AlgebraicClosure K ⊗[K] A)
    (Localization.AtPrime M)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
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 : Function.Injective (α := A) (β := AlgebraicClosure K ⊗[K] A) (⇑f : (a : A) → AlgebraicClosure K ⊗[K] A)
M : Ideal (AlgebraicClosure K ⊗[K] A)
hM : M.IsMaximal
y : Localization.AtPrime M
hy : IsNilpotent y
this_2 : EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this_3 : FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)
this : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
⊢ y = 0
have this₁ : FormallyUnramified (AlgebraicClosure K) (Localization.AtPrime M)
Tactic: have := comp (AlgebraicClosure K) (AlgebraicClosure K ⊗[K] A)
    (Localization.AtPrime M)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
A : Type u_2
inst : CommRing A
B : Type u_4
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : EssFiniteType A B
inst_4 : FormallyUnramified A B
p : Ideal A
inst_5 : p.IsMaximal
this : Field (A ⧸ p) := Ideal.Quotient.field p
⊢ Ideal.IsRadical.{u_4} (R := B) (Ideal.map (F := A →+* B) (algebraMap A B) p)
have rw : IsReduced.{u_4} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
Tactic: rw [Ideal.isRadical_iff_quotient_reduced]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
⊢ Nontrivial.{u_3} (L ⊗[K] L)
have rw : Nontrivial L
Tactic: rw [← not_subsingleton_iff_nontrivial, ← rank_zero_iff (R := K), rank_tensorProduct',
      mul_eq_zero, or_self, rank_zero_iff, not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
⊢ Eq.{u_3 + 1} (α := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) ⊤
have this : Nontrivial.{u_3} (L ⊗[K] L)
Tactic: have : Nontrivial (L ⊗[K] L) := by
    rw [← not_subsingleton_iff_nontrivial, ← rank_zero_iff (R := K), rank_tensorProduct',
      mul_eq_zero, or_self, rank_zero_iff, not_subsingleton_iff_nontrivial]
    infer_instance
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
this : Nontrivial.{u_3} (L ⊗[K] L)
⊢ Eq.{u_3 + 1} (α := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) ⊤
have rw : LE.le.{u_3} (α := Subring L) ⊤ (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L))
Tactic: rw [← top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
this : Nontrivial.{u_3} (L ⊗[K] L)
x : L
h : Membership.mem (γ := Subring L) ⊤ x
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have obtain : ∀ (n : ℕ)
  (hn : Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) (x ^ ringExpChar K ^ n)),
  Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
Tactic: obtain ⟨n, hn⟩ := IsPurelyInseparable.pow_mem K (ringExpChar K) x
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
this : Nontrivial.{u_3} (L ⊗[K] L)
x : L
h : Membership.mem (γ := Subring L) ⊤ x
n : ℕ
hn : Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) (x ^ ringExpChar K ^ n)
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have this₁ : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
Tactic: have : ExpChar (L ⊗[K] L) (ringExpChar K) := by
    refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
this_1 : Nontrivial.{u_3} (L ⊗[K] L)
x : L
h : Membership.mem (γ := Subring L) ⊤ x
n : ℕ
hn : Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) (x ^ ringExpChar K ^ n)
this : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
⊢ HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
have rw : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] (x ^ ringExpChar K ^ n)) ((x ^ ringExpChar K ^ n) ⊗ₜ[K] 1) = 0
Tactic: rw [sub_pow_expChar_pow, TensorProduct.tmul_pow, one_pow, TensorProduct.tmul_pow, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
this_1 : Nontrivial.{u_3} (L ⊗[K] L)
x : L
h : Membership.mem (γ := Subring L) ⊤ x
n : ℕ
hn : Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) (x ^ ringExpChar K ^ n)
this : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
⊢ HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] (x ^ ringExpChar K ^ n)) ((x ^ ringExpChar K ^ n) ⊗ₜ[K] 1) = 0
have obtain : ∀ (r : K) (hr : ((algebraMap K L : K →+* L) : (a : K) → L) r = x ^ ringExpChar K ^ n),
  HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] (x ^ ringExpChar K ^ n)) ((x ^ ringExpChar K ^ n) ⊗ₜ[K] 1) = 0
Tactic: obtain ⟨r, hr⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
this_1 : Nontrivial.{u_3} (L ⊗[K] L)
x : L
h : Membership.mem (γ := Subring L) ⊤ x
n : ℕ
this : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
r : K
hr : ((algebraMap K L : K →+* L) : (a : K) → L) r = x ^ ringExpChar K ^ n
⊢ HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] (x ^ ringExpChar K ^ n)) ((x ^ ringExpChar K ^ n) ⊗ₜ[K] 1) = 0
have rw : HSub.hSub (α := L ⊗[K] L) (β := L ⊗[K] L) (1 ⊗ₜ[K] ((algebraMap K L : K →+* L) : (a : K) → L) r : L ⊗[K] L)
    (((algebraMap K L : K →+* L) : (a : K) → L) r ⊗ₜ[K] 1 : L ⊗[K] L) =
  0
Tactic: rw [← hr, algebraMap_eq_smul_one, TensorProduct.smul_tmul, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
this_1 : Nontrivial.{u_3} (L ⊗[K] L)
x : L
h : Membership.mem (γ := Subring L) ⊤ x
n : ℕ
this : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
r : K
hr : ((algebraMap K L : K →+* L) : (a : K) → L) r = x ^ ringExpChar K ^ n
rw :
  HSub.hSub (α := L ⊗[K] L) (β := L ⊗[K] L) (1 ⊗ₜ[K] ((algebraMap K L : K →+* L) : (a : K) → L) r : L ⊗[K] L)
      (((algebraMap K L : K →+* L) : (a : K) → L) r ⊗ₜ[K] 1 : L ⊗[K] L) =
    0
⊢ HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] (x ^ ringExpChar K ^ n)) ((x ^ ringExpChar K ^ n) ⊗ₜ[K] 1) = 0
have rw₁ : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] HSMul.hSMul (β := L) r 1) (HSMul.hSMul (β := L) r 1 ⊗ₜ[K] 1) = 0
Tactic: rw [← hr, algebraMap_eq_smul_one, TensorProduct.smul_tmul, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
this_1 : Nontrivial.{u_3} (L ⊗[K] L)
x : L
h : Membership.mem (γ := Subring L) ⊤ x
n : ℕ
this : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
r : K
hr : ((algebraMap K L : K →+* L) : (a : K) → L) r = x ^ ringExpChar K ^ n
rw :
  HSub.hSub (α := L ⊗[K] L) (β := L ⊗[K] L) (1 ⊗ₜ[K] ((algebraMap K L : K →+* L) : (a : K) → L) r : L ⊗[K] L)
      (((algebraMap K L : K →+* L) : (a : K) → L) r ⊗ₜ[K] 1 : L ⊗[K] L) =
    0
rw₁ : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] HSMul.hSMul (β := L) r 1) (HSMul.hSMul (β := L) r 1 ⊗ₜ[K] 1) = 0
⊢ HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] (x ^ ringExpChar K ^ n)) ((x ^ ringExpChar K ^ n) ⊗ₜ[K] 1) = 0
have rw₂ : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] HSMul.hSMul (β := L) r 1) (1 ⊗ₜ[K] HSMul.hSMul (β := L) r 1) = 0
Tactic: rw [← hr, algebraMap_eq_smul_one, TensorProduct.smul_tmul, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (goal)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
this_1 : Nontrivial.{u_3} (L ⊗[K] L)
x : L
h : Membership.mem (γ := Subring L) ⊤ x
n : ℕ
this : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
r : K
hr : ((algebraMap K L : K →+* L) : (a : K) → L) r = x ^ ringExpChar K ^ n
rw :
  HSub.hSub (α := L ⊗[K] L) (β := L ⊗[K] L) (1 ⊗ₜ[K] ((algebraMap K L : K →+* L) : (a : K) → L) r : L ⊗[K] L)
      (((algebraMap K L : K →+* L) : (a : K) → L) r ⊗ₜ[K] 1 : L ⊗[K] L) =
    0
rw₁ : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] HSMul.hSMul (β := L) r 1) (HSMul.hSMul (β := L) r 1 ⊗ₜ[K] 1) = 0
rw₂ : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] HSMul.hSMul (β := L) r 1) (1 ⊗ₜ[K] HSMul.hSMul (β := L) r 1) = 0
⊢ HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] (x ^ ringExpChar K ^ n)) ((x ^ ringExpChar K ^ n) ⊗ₜ[K] 1) = 0
have rw₃ : Eq.{u_3 + 1} (α := L ⊗[K] L) 0 0
Tactic: rw [← hr, algebraMap_eq_smul_one, TensorProduct.smul_tmul, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Field (hypothesis)
Goal:
K : Type u_1
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FormallyUnramified K L
inst_4 : EssFiniteType K L
inst_5 : IsPurelyInseparable K L
this_1 : Nontrivial.{u_3} (L ⊗[K] L)
x : L
h : Membership.mem (γ := Subring L) ⊤ x
n : ℕ
hn : Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) (x ^ ringExpChar K ^ n)
this : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have this₁ : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
Tactic: have : (1 ⊗ₜ x - x ⊗ₜ 1 : L ⊗[K] L) ^ (ringExpChar K) ^ n = 0 := by
    rw [sub_pow_expChar_pow, TensorProduct.tmul_pow, one_pow, TensorProduct.tmul_pow, one_pow]
    obtain ⟨r, hr⟩ := hn
    rw [← hr, algebraMap_eq_smul_one, TensorProduct.smul_tmul, sub_self]