awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⋯
ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)
⊢ x ∈ 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 ⋯
ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)
b : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) x ⋯
⊢ (Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) b = x

Tactic:
simp [b]
-- 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 ⋯
ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)
b : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) x ⋯
⊢ (Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) b = x

Tactic:
have hb : Basis.extend h b = x := by simp [b]
-- 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 ⋯
ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)
b : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) x ⋯
hb : (Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) b = x
pos : ∀ (e : a = b), Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
neg : ∀ (e : ¬a = b), 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 e : a = b
-- 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 ⋯
ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)
b : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) x ⋯
hb : (Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) b = x
e : a = b
⊢ 1 = x

Tactic:
congr_arg Subtype.val e

Premises used: congr_arg, Subtype.val
-- 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 ⋯
ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)
b : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) x ⋯
hb : (Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) b = x
e : a = b
pos : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x

Tactic:
obtain rfl : 1 = x := congr_arg Subtype.val e

Premises used: congr_arg, Subtype.val, rfl
-- 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)
n : ℕ
this_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
h_1 : Membership.mem (γ := Subring L) ⊤ 1
hn :
  Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L))
    (HPow.hPow (α := L) 1 (ringExpChar K ^ n))
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] 1) (1 ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : Eq.{u_3 + 1} (α := L ⊗[K] L) (1 ⊗ₜ[K] 1) (1 ⊗ₜ[K] 1)
h' : LinearIndependent.{0, u_1, u_3} K (M := L) ![1, 1]
h : LinearIndepOn.{u_3, u_1, u_3} (ι := L) K _root_.id (Set.range ![1, 1])
S : Set L :=
  LinearIndepOn.extend.{u_3, u_3, u_1} (K := K) (V := L) (v := _root_.id) (s := Set.range ![1, 1]) (t := Set.univ) h ⋯
a : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) 1 ⋯
ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, 1]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)
b : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) 1 ⋯
hb : Eq (α := L) ((Basis.extend (s := Set.range ![1, 1]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) b : L) (1 : L)
e : a = b
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) 1

Tactic:
⟨1, map_one _⟩

Premises used: Set.Mem, setOf, map_one, Exists.intro, Set.range, OfNat.ofNat
-- 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)
n : ℕ
this_2 : ExpChar.{u_3} (L ⊗[K] L) (ringExpChar K)
h_1 : Membership.mem (γ := Subring L) ⊤ 1
hn :
  Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L))
    (HPow.hPow (α := L) 1 (ringExpChar K ^ n))
this : HSub.hSub (α := L ⊗[K] L) (1 ⊗ₜ[K] 1) (1 ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : Eq.{u_3 + 1} (α := L ⊗[K] L) (1 ⊗ₜ[K] 1) (1 ⊗ₜ[K] 1)
h' : LinearIndependent.{0, u_1, u_3} K (M := L) ![1, 1]
h : LinearIndepOn.{u_3, u_1, u_3} (ι := L) K _root_.id (Set.range ![1, 1])
S : Set L :=
  LinearIndepOn.extend.{u_3, u_3, u_1} (K := K) (V := L) (v := _root_.id) (s := Set.range ![1, 1]) (t := Set.univ) h ⋯
a : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) 1 ⋯
ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, 1]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)
b : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) 1 ⋯
hb : Eq (α := L) ((Basis.extend (s := Set.range ![1, 1]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) b : L) (1 : L)
e : a = b
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) 1

Tactic:
exact ⟨1, map_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_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 ⋯
ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)
b : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) x ⋯
hb : (Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) b = x
e : ¬a = b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
have := DFunLike.congr_fun
      (DFunLike.congr_arg ((Basis.extend h).tensorProduct (Basis.extend h)).repr H) (a, b)
-- 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_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)
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 ⋯
ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) a : L) (1 : L)
b : (↑S : Type u_3) := Subtype.mk (p := fun (x : L) ↦ x ∈ S) x ⋯
hb : (Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend ⋯) : Type u_3)) → L) b = x
e : ¬a = b
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x

Tactic:
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

Premises used: Ne.symm, MulZeroClass.mul_zero, reduceIte, Finsupp.single_apply, smul_eq_mul, mul_one, one_ne_zero, Module.Basis.tensorProduct_repr_tmul_apply, Module.Basis.repr_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
H : Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)
h' : ¬LinearIndependent K ![1, x]
⊢ ¬∀ (s t : K), HSMul.hSMul (β := L) s 1 + t • x = 0 → s = 0 ∧ t = 0

Tactic:
rw [LinearIndependent.pair_iff] at h'

Premises used: LinearIndependent.pair_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_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' : ¬∀ (s t : K), HSMul.hSMul (β := L) s 1 + t • x = 0 → s = 0 ∧ t = 0
⊢ ∃ (x_1 : K) (x_2 : K), HSMul.hSMul (β := L) x_1 1 + x_2 • x = 0 ∧ (x_1 = 0 → ¬x_2 = 0)

Tactic:
simp only [not_forall, not_and, exists_prop] at h'

Premises used: exists_prop, not_and, Classical.not_forall
-- 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' : ∃ (x_1 : K) (x_2 : K), HSMul.hSMul (β := L) x_1 1 + x_2 • x = 0 ∧ (x_1 = 0 → ¬x_2 = 0)
neg :
  ∀ (a b : K) (e : HSMul.hSMul (β := L) a 1 + b • x = 0) (hab : a = 0 → ¬b = 0),
    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 ⟨a, b, e, hab⟩ := h'
-- 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)
a b : K
e : HSMul.hSMul (β := L) a 1 + b • x = 0
hab : a = 0 → ¬b = 0
rw : b ≠ 0
⊢ IsUnit b

Tactic:
rw [isUnit_iff_ne_zero]

Premises used: isUnit_iff_ne_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
H : Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)
a : K
e : HSMul.hSMul (β := L) a 1 + HSMul.hSMul.{u_1, u_3, u_3} (α := K) 0 x = 0
hab : a = 0 → ¬Eq.{u_1 + 1} (α := K) 0 0
⊢ a = 0

Tactic:
rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
        (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e

Premises used: Algebra.algebraMap, injective_iff_map_eq_zero', RingHom.injective, Algebra.algebraMap_eq_smul_one, zero_smul, Iff.mp, add_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
H : Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)
a : K
e : HSMul.hSMul (β := L) a 1 + HSMul.hSMul.{u_1, u_3, u_3} (α := K) 0 x = 0
hab : a = 0 → ¬Eq.{u_1 + 1} (α := K) 0 0
e₁ : a = 0
⊢ a = 0 → ¬Eq.{u_1 + 1} (α := K) 0 0

Tactic:
rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
        (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e

Premises used: Algebra.algebraMap, injective_iff_map_eq_zero', RingHom.injective, Algebra.algebraMap_eq_smul_one, zero_smul, Iff.mp, add_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
H : Eq (α := L ⊗[K] L) (1 ⊗ₜ[K] x) (x ⊗ₜ[K] 1)
a : K
e : a = 0
hab : a = 0 → ¬Eq.{u_1 + 1} (α := K) 0 0
⊢ False

Tactic:
cases hab e rfl

Premises used: rfl
-- 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)
a b : K
e : HSMul.hSMul (β := L) a 1 + b • x = 0
hab : a = 0 → ¬b = 0
⊢ IsUnit b

Tactic:
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
-- 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_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 : ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x

Tactic:
use (-this.unit⁻¹ * a)

Premises used: Units.val, HMul.hMul, Inv.inv, IsUnit.unit, Neg.neg
-- 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_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
h₉ h₁₀ : x = x
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = 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]

Premises used: Iff.mpr, neg_smul, smul_smul, neg_neg, smul_neg, one_smul, Algebra.algebraMap_eq_smul_one, map_mul, Algebra.smul_def, eq_neg_iff_add_eq_zero, IsUnit.val_inv_mul
-- 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
⊢ Module.Finite K L

Tactic:
have := finite_of_free (R := K) (S := L)
-- 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
this : Module.Finite K L
rw : Eq (α := IntermediateField K L) (separableClosure K L) ⊤
⊢ Algebra.IsSeparable K L

Tactic:
rw [← separableClosure.eq_top_iff]

Premises used: separableClosure.eq_top_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
this : Module.Finite K L
⊢ FormallyUnramified (↥(separableClosure K L)) L

Tactic:
have := of_restrictScalars K (separableClosure K L) L