awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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)
have inst : IsReduced.{u_3} (L ⊗[K] L)
Tactic: have inst : IsReduced (L ⊗[K] L) := isReduced_of_field 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
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
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have H : 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⟩)
-- 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_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)
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have pos : ∀ (h' : LinearIndependent K ![1, 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]
-- 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_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
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have neg : ∀ (h' : ¬LinearIndependent K ![1, 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]
-- 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_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]
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have h : LinearIndepOn K _root_.id (Set.range ![1, x])
Tactic: have h := h'.linearIndepOn_id
-- 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_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 ⋯
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have ha : Eq (α := L) ((Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend sorry) : Type u_3)) → L) a : L) (1 : L)
Tactic: have ha : Basis.extend h a = 1 := by simp [a]
-- 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_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 ⋯
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have hb : (Basis.extend (s := Set.range ![1, x]) h : (a : (↑(h.extend sorry) : Type u_3)) → L) b = x
Tactic: have hb : Basis.extend h b = x := by simp [b]
-- 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 : 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
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have pos : ∀ (e : a = b), Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
Tactic: by_cases e : a = b
-- 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 : 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
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have neg : ∀ (e : ¬a = b), Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
Tactic: by_cases e : a = b
-- 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 : 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
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have pos : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain rfl : 1 = x := congr_arg Subtype.val e
Cleared hypotheses: x, h_1, hn, this, H, h', h, S, a, ha, b, hb, e
-- 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_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
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have this₁ : 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)
-- 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_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]
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have h'₁ : ¬∀ (s t : K), HSMul.hSMul (β := L) s 1 + t • x = 0 → s = 0 ∧ t = 0
Tactic: rw [LinearIndependent.pair_iff] at h'
Cleared hypotheses: h'
-- 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_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
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have h'₁ : ∃ (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'
Cleared hypotheses: h'
-- 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_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)
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have 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
Tactic: obtain ⟨a, b, e, hab⟩ := h'
Cleared hypotheses: h'
-- 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_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
have rw : b ≠ 0
Tactic: rw [isUnit_iff_ne_zero]
-- 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_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
⊢ False
have e₁ : a = 0
Tactic: rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
        (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e
Cleared hypotheses: e, hab
-- 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_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
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have this₁ : 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
-- 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_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
⊢ Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_3} (R := K) (algebraMap K L)) x
have h : ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
Tactic: use (-this.unit⁻¹ * a)
-- 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_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
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
have 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
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
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
have h₁ : HSMul.hSMul (β := L) (-(↑this.unit⁻¹ : K)) (((algebraMap K L : K →+* L) : (a : K) → L) a : L) = 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
⊢ ((algebraMap K L : K →+* L) : (a : K) → L) (-(↑this.unit⁻¹ : K) * a) = x
have h₂ : -(↑this.unit⁻¹ : K) • HSMul.hSMul (β := L) a 1 = 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]