awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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_3 : 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)
a b : K
e : HSMul.hSMul (β := L) a 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
h :
  HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K)) : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) a : L) =
    x
h₁ : HSMul.hSMul (β := L) (-(↑this.unit⁻¹ : K)) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = x
h₂ : -(↑this.unit⁻¹ : K) • HSMul.hSMul (β := L) a 1 = x
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
have h₃ : -(↑this.unit⁻¹ : K) • -(b • x) = x
Tactic: rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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_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_3 : 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)
a b : K
e : HSMul.hSMul (β := L) a 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
h :
  HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K)) : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) a : L) =
    x
h₁ : HSMul.hSMul (β := L) (-(↑this.unit⁻¹ : K)) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = x
h₂ : -(↑this.unit⁻¹ : K) • HSMul.hSMul (β := L) a 1 = x
h₃ : -(↑this.unit⁻¹ : K) • -(b • x) = x
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
have h₄ : -(-(↑this.unit⁻¹ : K) • b • x) = x
Tactic: rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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_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_3 : 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)
a b : K
e : HSMul.hSMul (β := L) a 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
h :
  HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K)) : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) a : L) =
    x
h₁ : HSMul.hSMul (β := L) (-(↑this.unit⁻¹ : K)) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = x
h₂ : -(↑this.unit⁻¹ : K) • HSMul.hSMul (β := L) a 1 = x
h₃ : -(↑this.unit⁻¹ : K) • -(b • x) = x
h₄ : -(-(↑this.unit⁻¹ : K) • b • x) = x
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
have h₅ : - -((↑this.unit⁻¹ : K) • b • x) = x
Tactic: rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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_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_3 : 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)
a b : K
e : HSMul.hSMul (β := L) a 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
h :
  HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K)) : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) a : L) =
    x
h₁ : HSMul.hSMul (β := L) (-(↑this.unit⁻¹ : K)) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = x
h₂ : -(↑this.unit⁻¹ : K) • HSMul.hSMul (β := L) a 1 = x
h₃ : -(↑this.unit⁻¹ : K) • -(b • x) = x
h₄ : -(-(↑this.unit⁻¹ : K) • b • x) = x
h₅ : - -((↑this.unit⁻¹ : K) • b • x) = x
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
have h₆ : (↑this.unit⁻¹ : K) • b • x = x
Tactic: rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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_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_3 : 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)
a b : K
e : HSMul.hSMul (β := L) a 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
h :
  HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K)) : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) a : L) =
    x
h₁ : HSMul.hSMul (β := L) (-(↑this.unit⁻¹ : K)) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = x
h₂ : -(↑this.unit⁻¹ : K) • HSMul.hSMul (β := L) a 1 = x
h₃ : -(↑this.unit⁻¹ : K) • -(b • x) = x
h₄ : -(-(↑this.unit⁻¹ : K) • b • x) = x
h₅ : - -((↑this.unit⁻¹ : K) • b • x) = x
h₆ : (↑this.unit⁻¹ : K) • b • x = x
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
have h₇ : ((↑this.unit⁻¹ : K) * b) • x = x
Tactic: rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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_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_3 : 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)
a b : K
e : HSMul.hSMul (β := L) a 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
h :
  HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K)) : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) a : L) =
    x
h₁ : HSMul.hSMul (β := L) (-(↑this.unit⁻¹ : K)) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = x
h₂ : -(↑this.unit⁻¹ : K) • HSMul.hSMul (β := L) a 1 = x
h₃ : -(↑this.unit⁻¹ : K) • -(b • x) = x
h₄ : -(-(↑this.unit⁻¹ : K) • b • x) = x
h₅ : - -((↑this.unit⁻¹ : K) • b • x) = x
h₆ : (↑this.unit⁻¹ : K) • b • x = x
h₇ : ((↑this.unit⁻¹ : K) * b) • x = x
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
have h₈ : HSMul.hSMul.{u_1, u_3, u_3} (α := K) 1 x = x
Tactic: rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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_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_3 : 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)
a b : K
e : HSMul.hSMul (β := L) a 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
h :
  HMul.hMul (α := L) (β := L) (((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K)) : L)
      (((algebraMap K L : K →+* L) : (a : K) → L) a : L) =
    x
h₁ : HSMul.hSMul (β := L) (-(↑this.unit⁻¹ : K)) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = x
h₂ : -(↑this.unit⁻¹ : K) • HSMul.hSMul (β := L) a 1 = x
h₃ : -(↑this.unit⁻¹ : K) • -(b • x) = x
h₄ : -(-(↑this.unit⁻¹ : K) • b • x) = x
h₅ : - -((↑this.unit⁻¹ : K) • b • x) = x
h₆ : (↑this.unit⁻¹ : K) • b • x = x
h₇ : ((↑this.unit⁻¹ : K) * b) • x = x
h₈ : HSMul.hSMul.{u_1, u_3, u_3} (α := K) 1 x = x
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
have h₉ : x = x
Tactic: rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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
⊢ Eq.{u_3 + 1} (α := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) ⊤
have have : Nontrivial.{u_3} (L ⊗[K] L)
Tactic: classical
  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
  rw [← top_le_iff]
  intro x _
  obtain ⟨n, hn⟩ := IsPurelyInseparable.pow_mem K (ringExpChar K) x
  have : ExpChar (L ⊗[K] L) (ringExpChar K) := by
    refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)
  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]
  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⟩)
  by_cases h' : LinearIndependent K ![1, x]
  · have h := h'.linearIndepOn_id
    let S := h.extend (Set.subset_univ _)
    let a : S := ⟨1, h.subset_extend _ (by simp)⟩
    have ha : Basis.extend h a = 1 := by simp [a]
    let b : S := ⟨x, h.subset_extend _ (by simp)⟩
    have hb : Basis.extend h b = x := by simp [b]
    by_cases e : a = b
    · obtain rfl : 1 = x := congr_arg Subtype.val e
      exact ⟨1, map_one _⟩
    have := DFunLike.congr_fun
      (DFunLike.congr_arg ((Basis.extend h).tensorProduct (Basis.extend h)).repr H) (a, b)
    simp only [Basis.tensorProduct_repr_tmul_apply, ← ha, ← hb, Basis.repr_self, smul_eq_mul,
      Finsupp.single_apply, e, Ne.symm e, ↓reduceIte, mul_one, mul_zero, one_ne_zero] at this
  · rw [LinearIndependent.pair_iff] at h'
    simp only [not_forall, not_and, exists_prop] at h'
    obtain ⟨a, b, e, hab⟩ := h'
    have : IsUnit b := by
      rw [isUnit_iff_ne_zero]
      rintro rfl
      rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
        (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e
      cases hab e rfl
    use (-this.unit⁻¹ * a)
    rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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
have : Nontrivial.{u_3} (L ⊗[K] L)
⊢ Eq.{u_3 + 1} (α := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) ⊤
have have₁ : ∀ (this : Nontrivial.{u_3} (L ⊗[K] L)),
  Eq.{u_3 + 1} (α := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) ⊤
Tactic: classical
  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
  rw [← top_le_iff]
  intro x _
  obtain ⟨n, hn⟩ := IsPurelyInseparable.pow_mem K (ringExpChar K) x
  have : ExpChar (L ⊗[K] L) (ringExpChar K) := by
    refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)
  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]
  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⟩)
  by_cases h' : LinearIndependent K ![1, x]
  · have h := h'.linearIndepOn_id
    let S := h.extend (Set.subset_univ _)
    let a : S := ⟨1, h.subset_extend _ (by simp)⟩
    have ha : Basis.extend h a = 1 := by simp [a]
    let b : S := ⟨x, h.subset_extend _ (by simp)⟩
    have hb : Basis.extend h b = x := by simp [b]
    by_cases e : a = b
    · obtain rfl : 1 = x := congr_arg Subtype.val e
      exact ⟨1, map_one _⟩
    have := DFunLike.congr_fun
      (DFunLike.congr_arg ((Basis.extend h).tensorProduct (Basis.extend h)).repr H) (a, b)
    simp only [Basis.tensorProduct_repr_tmul_apply, ← ha, ← hb, Basis.repr_self, smul_eq_mul,
      Finsupp.single_apply, e, Ne.symm e, ↓reduceIte, mul_one, mul_zero, one_ne_zero] at this
  · rw [LinearIndependent.pair_iff] at h'
    simp only [not_forall, not_and, exists_prop] at h'
    obtain ⟨a, b, e, hab⟩ := h'
    have : IsUnit b := by
      rw [isUnit_iff_ne_zero]
      rintro rfl
      rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
        (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e
      cases hab e rfl
    use (-this.unit⁻¹ * a)
    rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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
have : Nontrivial.{u_3} (L ⊗[K] L)
have₁ :
  ∀ (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₂ : Nontrivial.{u_3} (L ⊗[K] L)
have₃ have₄ :
  ∀ (this : Nontrivial.{u_3} (L ⊗[K] L)),
    Eq.{u_3 + 1} (α := 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)) ⊤
have have₅ : ∀ (this : Nontrivial.{u_3} (L ⊗[K] L)),
  LE.le.{u_3} (α := Subring L) ⊤ (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L))
Tactic: classical
  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
  rw [← top_le_iff]
  intro x _
  obtain ⟨n, hn⟩ := IsPurelyInseparable.pow_mem K (ringExpChar K) x
  have : ExpChar (L ⊗[K] L) (ringExpChar K) := by
    refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)
  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]
  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⟩)
  by_cases h' : LinearIndependent K ![1, x]
  · have h := h'.linearIndepOn_id
    let S := h.extend (Set.subset_univ _)
    let a : S := ⟨1, h.subset_extend _ (by simp)⟩
    have ha : Basis.extend h a = 1 := by simp [a]
    let b : S := ⟨x, h.subset_extend _ (by simp)⟩
    have hb : Basis.extend h b = x := by simp [b]
    by_cases e : a = b
    · obtain rfl : 1 = x := congr_arg Subtype.val e
      exact ⟨1, map_one _⟩
    have := DFunLike.congr_fun
      (DFunLike.congr_arg ((Basis.extend h).tensorProduct (Basis.extend h)).repr H) (a, b)
    simp only [Basis.tensorProduct_repr_tmul_apply, ← ha, ← hb, Basis.repr_self, smul_eq_mul,
      Finsupp.single_apply, e, Ne.symm e, ↓reduceIte, mul_one, mul_zero, one_ne_zero] at this
  · rw [LinearIndependent.pair_iff] at h'
    simp only [not_forall, not_and, exists_prop] at h'
    obtain ⟨a, b, e, hab⟩ := h'
    have : IsUnit b := by
      rw [isUnit_iff_ne_zero]
      rintro rfl
      rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
        (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e
      cases hab e rfl
    use (-this.unit⁻¹ * a)
    rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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
have : Nontrivial.{u_3} (L ⊗[K] L)
have₁ :
  ∀ (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₂ : Nontrivial.{u_3} (L ⊗[K] L)
have₃ have₄ :
  ∀ (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₅ :
  ∀ (this : Nontrivial.{u_3} (L ⊗[K] L)),
    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)) ⊤
have have₆ : ∀ (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
Tactic: classical
  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
  rw [← top_le_iff]
  intro x _
  obtain ⟨n, hn⟩ := IsPurelyInseparable.pow_mem K (ringExpChar K) x
  have : ExpChar (L ⊗[K] L) (ringExpChar K) := by
    refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)
  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]
  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⟩)
  by_cases h' : LinearIndependent K ![1, x]
  · have h := h'.linearIndepOn_id
    let S := h.extend (Set.subset_univ _)
    let a : S := ⟨1, h.subset_extend _ (by simp)⟩
    have ha : Basis.extend h a = 1 := by simp [a]
    let b : S := ⟨x, h.subset_extend _ (by simp)⟩
    have hb : Basis.extend h b = x := by simp [b]
    by_cases e : a = b
    · obtain rfl : 1 = x := congr_arg Subtype.val e
      exact ⟨1, map_one _⟩
    have := DFunLike.congr_fun
      (DFunLike.congr_arg ((Basis.extend h).tensorProduct (Basis.extend h)).repr H) (a, b)
    simp only [Basis.tensorProduct_repr_tmul_apply, ← ha, ← hb, Basis.repr_self, smul_eq_mul,
      Finsupp.single_apply, e, Ne.symm e, ↓reduceIte, mul_one, mul_zero, one_ne_zero] at this
  · rw [LinearIndependent.pair_iff] at h'
    simp only [not_forall, not_and, exists_prop] at h'
    obtain ⟨a, b, e, hab⟩ := h'
    have : IsUnit b := by
      rw [isUnit_iff_ne_zero]
      rintro rfl
      rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
        (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e
      cases hab e rfl
    use (-this.unit⁻¹ * a)
    rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]
-- 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
⊢ Algebra.IsSeparable K L
have this : Module.Finite K L
Tactic: have := finite_of_free (R := K) (S := L)
-- 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
this : Module.Finite K L
⊢ Algebra.IsSeparable K L
have rw : Eq (α := IntermediateField K L) (separableClosure K L) ⊤
Tactic: rw [← separableClosure.eq_top_iff]
-- 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
this : Module.Finite K L
⊢ Eq (α := IntermediateField K L) (separableClosure K L) ⊤
have this₁ : FormallyUnramified (↥(separableClosure K L)) L
Tactic: have := of_restrictScalars K (separableClosure K L) L
-- 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
this_1 : Module.Finite K L
this : FormallyUnramified (↥(separableClosure K L)) L
⊢ Eq (α := IntermediateField K L) (separableClosure K L) ⊤
have this₁ : EssFiniteType (↥(separableClosure K L)) L
Tactic: have := EssFiniteType.of_comp K (separableClosure K L) L
-- 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
this_1 : Module.Finite K L
this_2 : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
⊢ Eq (α := IntermediateField K L) (separableClosure K L) ⊤
have h : ∀ (x : L),
  Membership.mem (γ := IntermediateField K L) (separableClosure K L) x ↔ Membership.mem (γ := IntermediateField K L) ⊤ x
Tactic: ext