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
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_zero : ∀ (y : Localization.AtPrime M) (hy : IsNilpotent y), y = 0
⊢ 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)

Tactic:
generalize algebraMap _ (Localization.AtPrime M) (f x) = y at *

Premises used: Algebra.algebraMap, Localization.AtPrime, DFunLike.coe
-- 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
y : Localization.AtPrime M
hy : IsNilpotent y
⊢ EssFiniteType (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)

Tactic:
have := EssFiniteType.of_isLocalization (Localization.AtPrime M) M.primeCompl
-- 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 : 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)
⊢ FormallyUnramified (AlgebraicClosure K ⊗[K] A) (Localization.AtPrime M)

Tactic:
have := of_isLocalization (Rₘ := Localization.AtPrime M) M.primeCompl
-- 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 : 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)
⊢ EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)

Tactic:
have := EssFiniteType.comp (AlgebraicClosure K) (AlgebraicClosure K ⊗[K] A)
    (Localization.AtPrime M)
-- 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 : 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)
⊢ FormallyUnramified (AlgebraicClosure K) (Localization.AtPrime M)

Tactic:
have := comp (AlgebraicClosure K) (AlgebraicClosure K ⊗[K] A)
    (Localization.AtPrime M)
-- 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 : 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_4 : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
this_5 : FormallyUnramified (AlgebraicClosure K) (Localization.AtPrime M)
this : Field (Localization.AtPrime M) := IsField.toField ⋯
⊢ y = 0

Tactic:
hy.eq_zero

Premises used: IsNilpotent.eq_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_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_4 : EssFiniteType (AlgebraicClosure K) (Localization.AtPrime M)
this_5 : FormallyUnramified (AlgebraicClosure K) (Localization.AtPrime M)
this : Field (Localization.AtPrime M) := IsField.toField ⋯
⊢ y = 0

Tactic:
exact hy.eq_zero

Premises used: IsNilpotent.eq_zero
-- Module: Mathlib.RingTheory.Unramified.Field
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
rw : IsReduced.{u_4} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))
⊢ Ideal.IsRadical.{u_4} (R := B) (Ideal.map (F := A →+* B) (algebraMap A B) p)

Tactic:
rw [Ideal.isRadical_iff_quotient_reduced]

Premises used: Ideal.isRadical_iff_quotient_reduced
-- Module: Mathlib.RingTheory.Unramified.Field
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
⊢ IsReduced.{u_4} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))

Tactic:
Algebra.FormallyUnramified.isReduced_of_field (A ⧸ p) (B ⧸ p.map (algebraMap A B))

Premises used: Algebra.algebraMap, Ideal.map, Algebra.FormallyUnramified.isReduced_of_field, HasQuotient.Quotient
-- Module: Mathlib.RingTheory.Unramified.Field
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
⊢ IsReduced.{u_4} (HasQuotient.Quotient B (B := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p))

Tactic:
exact Algebra.FormallyUnramified.isReduced_of_field (A ⧸ p) (B ⧸ p.map (algebraMap A B))

Premises used: Algebra.algebraMap, Ideal.map, Algebra.FormallyUnramified.isReduced_of_field, HasQuotient.Quotient
-- Module: Mathlib.RingTheory.Unramified.Field
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
rw : Nontrivial L
⊢ Nontrivial.{u_3} (L ⊗[K] 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]

Premises used: mul_eq_zero, or_self, rank_zero_iff, not_subsingleton_iff_nontrivial, rank_tensorProduct'
-- Module: Mathlib.RingTheory.Unramified.Field
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 L

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Unramified.Field
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)

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
-- Module: Mathlib.RingTheory.Unramified.Field
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)
rw : LE.le.{u_3} (α := Subring L) ⊤ (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L))
⊢ Eq.{u_3 + 1} (α := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.RingTheory.Unramified.Field
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
_ :
  Membership.mem (γ := Subring L) ⊤ x →
    Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
⊢ Membership.mem (γ := Subring L) ⊤ x →
    Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Field
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
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
⊢ 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

Premises used: ringExpChar, IsPurelyInseparable.pow_mem
-- Module: Mathlib.RingTheory.Unramified.Field
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)
⊢ ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)

Tactic:
expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)

Premises used: Algebra.algebraMap, ringExpChar, expChar_of_injective_ringHom, RingHom.injective
-- Module: Mathlib.RingTheory.Unramified.Field
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)
⊢ ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)

Tactic:
refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)

Premises used: Algebra.algebraMap, ringExpChar, expChar_of_injective_ringHom, RingHom.injective
-- Module: Mathlib.RingTheory.Unramified.Field
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)
⊢ 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)
-- Module: Mathlib.RingTheory.Unramified.Field
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)
rw : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] (x ^ ringExpChar K ^ n)) ((x ^ ringExpChar K ^ n) ⊗ₜ[K] 1) = 0
⊢ HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0

Tactic:
rw [sub_pow_expChar_pow, TensorProduct.tmul_pow, one_pow, TensorProduct.tmul_pow, one_pow]

Premises used: one_pow, Algebra.TensorProduct.tmul_pow, sub_pow_expChar_pow
-- Module: Mathlib.RingTheory.Unramified.Field
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)
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
⊢ HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] (x ^ ringExpChar K ^ n)) ((x ^ ringExpChar K ^ n) ⊗ₜ[K] 1) = 0

Tactic:
obtain ⟨r, hr⟩ := hn
-- Module: Mathlib.RingTheory.Unramified.Field
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
rw₃ rw₄ : Eq.{u_3 + 1} (α := L ⊗[K] L) 0 0
⊢ HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] (x ^ ringExpChar K ^ n)) ((x ^ ringExpChar K ^ n) ⊗ₜ[K] 1) = 0

Tactic:
rw [← hr, algebraMap_eq_smul_one, TensorProduct.smul_tmul, sub_self]

Premises used: TensorProduct.smul_tmul, sub_self, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.Unramified.Field
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

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]
-- Module: Mathlib.RingTheory.Unramified.Field
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_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
⊢ IsReduced.{u_3} (L ⊗[K] L)

Tactic:
have inst : IsReduced (L ⊗[K] L) := isReduced_of_field L _
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FormallyUnramified K L
inst_5 : EssFiniteType K L
inst_6 : 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_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
inst : IsReduced.{u_3} (L ⊗[K] L)
⊢ Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)

Tactic:
sub_eq_zero.mp (IsNilpotent.eq_zero ⟨_, this⟩)

Premises used: sub_eq_zero, Exists.intro, Iff.mp, IsNilpotent.eq_zero
-- Module: Mathlib.RingTheory.Unramified.Field
Goal:
K : Type u_1
L : Type u_3
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FormallyUnramified K L
inst_5 : EssFiniteType K L
inst_6 : 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_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
inst : IsReduced.{u_3} (L ⊗[K] L)
⊢ Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)

Tactic:
exact sub_eq_zero.mp (IsNilpotent.eq_zero ⟨_, this⟩)

Premises used: sub_eq_zero, Exists.intro, Iff.mp, IsNilpotent.eq_zero
-- Module: Mathlib.RingTheory.Unramified.Field
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_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
⊢ Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)

Tactic:
have H : (1 ⊗ₜ x : L ⊗[K] L) = x ⊗ₜ 1 := by
    have inst : IsReduced (L ⊗[K] L) := isReduced_of_field L _
    exact sub_eq_zero.mp (IsNilpotent.eq_zero ⟨_, this⟩)
-- Module: Mathlib.RingTheory.Unramified.Field
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_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)
pos :
  ∀ (h' : LinearIndependent K ![1, x]),
    Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
neg :
  ∀ (h' : ¬LinearIndependent K ![1, x]),
    Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x

Tactic:
by_cases h' : LinearIndependent K ![1, x]

Premises used: LinearIndependent, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- Module: Mathlib.RingTheory.Unramified.Field
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_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)
h' : LinearIndependent K ![1, x]
⊢ LinearIndepOn K _root_.id (Set.range ![1, x])

Tactic:
have h := h'.linearIndepOn_id
-- Module: Mathlib.RingTheory.Unramified.Field
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_1 : 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_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L :=
  LinearIndepOn.extend.{u_3, u_3, u_1} (K := K) (V := L) (v := _root_.id) (s := Set.range ![1, x]) (t := Set.univ) h ⋯
⊢ 1 ∈ Set.range ![1, x]

Tactic:
simp
-- Module: Mathlib.RingTheory.Unramified.Field
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_1 : 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_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L :=
  LinearIndepOn.extend.{u_3, u_3, u_1} (K := K) (V := L) (v := _root_.id) (s := Set.range ![1, x]) (t := Set.univ) h ⋯
a : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) 1 ⋯
⊢ Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)

Tactic:
simp [a]
-- Module: Mathlib.RingTheory.Unramified.Field
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_1 : 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_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L :=
  LinearIndepOn.extend.{u_3, u_3, u_1} (K := K) (V := L) (v := _root_.id) (s := Set.range ![1, x]) (t := Set.univ) h ⋯
a : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) 1 ⋯
⊢ Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)

Tactic:
have ha : Basis.extend h a = 1 := by simp [a]