awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
inst_8 : Algebra.IsSeparable E K
x : K
h : Membership.mem (γ := IntermediateField E K) ⊤ x
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E (↑S : Set K)
this_1 : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x_1 : Algebra ↥S ↥L := i.toAlgebra
x_2 : SMul ↥S ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring S) DivisionSemiring.toSemiring _
this_2 : IsScalarTower (↥S) (↥L) K
this_3 : Algebra.IsAlgebraic F K
this_4 : IsPurelyInseparable (↥S) K
this : IsPurelyInseparable (↥L) K
obtain :
  ∀ (y : ↥L),
    Membership.mem (α := K) (γ := IntermediateField E K) ⊤ ((algebraMap (↥L) K : (a : ↥L) → K) y : K) →
      Membership.mem (α := K) L ((algebraMap (↥L) K : (a : ↥L) → K) y : K)
⊢ x ∈ L

Tactic:
obtain ⟨y, rfl⟩ := IsPurelyInseparable.surjective_algebraMap_of_isSeparable L K x

Premises used: Membership.mem, IsPurelyInseparable.surjective_algebraMap_of_isSeparable, Subtype, rfl
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
inst_8 : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E (↑S : Set K)
this_1 : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x : Algebra ↥S ↥L := i.toAlgebra
x_1 : SMul ↥S ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring S) DivisionSemiring.toSemiring _
this_2 : IsScalarTower (↥S) (↥L) K
this_3 : Algebra.IsAlgebraic F K
this_4 : IsPurelyInseparable (↥S) K
this : IsPurelyInseparable (↥L) K
y : ↥L
h : Membership.mem (α := K) (γ := IntermediateField E K) ⊤ ((algebraMap (↥L) K : (a : ↥L) → K) y : K)
⊢ Membership.mem (α := K) L ((algebraMap (↥L) K : (a : ↥L) → K) y : K)

Tactic:
y.2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
inst_8 : Algebra.IsSeparable E K
S : IntermediateField F K := separableClosure F K
L : IntermediateField E K := adjoin E (↑S : Set K)
this_1 : Algebra.IsSeparable (↥L) K
i : ↥S →+* ↥L := Subsemiring.inclusion ⋯
x : Algebra ↥S ↥L := i.toAlgebra
x_1 : SMul ↥S ↥L := @Algebra.toSMul _ _ (SubsemiringClass.toCommSemiring S) DivisionSemiring.toSemiring _
this_2 : IsScalarTower (↥S) (↥L) K
this_3 : Algebra.IsAlgebraic F K
this_4 : IsPurelyInseparable (↥S) K
this : IsPurelyInseparable (↥L) K
y : ↥L
h : Membership.mem (α := K) (γ := IntermediateField E K) ⊤ ((algebraMap (↥L) K : (a : ↥L) → K) y : K)
⊢ Membership.mem (α := K) L ((algebraMap (↥L) K : (a : ↥L) → K) y : K)

Tactic:
exact y.2

Premises used: Subtype.property
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
set :
  let S : IntermediateField E K := separableClosure E K;
  adjoin E (↑(separableClosure F K) : Set K) = S
⊢ Eq (α := IntermediateField E K) (adjoin E (↑(separableClosure F K) : Set K)) (separableClosure E K)

Tactic:
set S := separableClosure E K

Premises used: separableClosure
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
S : IntermediateField E K := separableClosure E K
⊢ lift (adjoin E (↑(separableClosure F ↥S) : Set ↥S)) = lift (F := S) ⊤

Tactic:
have h := congr_arg lift (adjoin_eq_of_isAlgebraic_of_isSeparable (F := F) S)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
S : IntermediateField E K := separableClosure E K
h : lift (adjoin E (↑(separableClosure F ↥S) : Set ↥S)) = lift (F := S) ⊤
⊢ adjoin E (Subtype.val (p := fun (x : K) ↦ x ∈ S) '' (↑(separableClosure F ↥S) : Set ↥S)) = S

Tactic:
rw [lift_top, lift_adjoin] at h

Premises used: IntermediateField.lift_top, IntermediateField.lift_adjoin
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
S : IntermediateField E K := separableClosure E K
h : adjoin E (Subtype.val (p := fun (x : K) ↦ x ∈ S) '' (↑(separableClosure F ↥S) : Set ↥S)) = S
⊢ IsScalarTower F (↥S) K

Tactic:
haveI : IsScalarTower F S K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
S : IntermediateField E K := separableClosure E K
h : adjoin E (Subtype.val (p := fun (x : K) ↦ x ∈ S) '' (↑(separableClosure F ↥S) : Set ↥S)) = S
this : IsScalarTower F (↥S) K
rw :
  Eq (α := IntermediateField E K)
    (adjoin E
      (↑(IntermediateField.map (L := ↥(separableClosure E K)) (IsScalarTower.toAlgHom F (↥(separableClosure E K)) K)
            (separableClosure F ↥(separableClosure E K))) :
        Set K))
    (adjoin E (Subtype.val (p := fun (x : K) ↦ x ∈ S) '' (↑(separableClosure F ↥S) : Set ↥S)))
⊢ adjoin E (↑(separableClosure F K) : Set K) = S

Tactic:
rw [← h, ← map_eq_of_separableClosure_eq_bot F (separableClosure_eq_bot E K)]

Premises used: separableClosure.map_eq_of_separableClosure_eq_bot, separableClosure.separableClosure_eq_bot
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsAlgebraic F E
S : IntermediateField E K := separableClosure E K
h : adjoin E (Subtype.val (p := fun (x : K) ↦ x ∈ S) '' (↑(separableClosure F ↥S) : Set ↥S)) = S
this : IsScalarTower F (↥S) K
⊢ Eq (α := IntermediateField E K)
    (adjoin E
      (↑(IntermediateField.map (L := ↥(separableClosure E K)) (IsScalarTower.toAlgHom F (↥(separableClosure E K)) K)
            (separableClosure F ↥(separableClosure E K))) :
        Set K))
    (adjoin E (Subtype.val (p := fun (x : K) ↦ x ∈ S) '' (↑(separableClosure F ↥S) : Set ↥S)))

Tactic:
simp only [S, coe_map, IsScalarTower.coe_toAlgHom', IntermediateField.algebraMap_apply]

Premises used: IsScalarTower.coe_toAlgHom', IntermediateField.algebraMap_apply, IntermediateField.coe_map
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x y : A
n : ℕ
hx : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)
m : ℕ
hy : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (y ^ p ^ m)
h : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x * y) ^ p ^ (n + m))
⊢ Membership.mem (γ := Set A)
    {x : A | ∃ (n : ℕ), Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)} (x * y)

Tactic:
use n + m
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x y : A
n : ℕ
hx : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)
m : ℕ
hy : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (y ^ p ^ m)
h : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x ^ p ^ n) ^ p ^ m * (y ^ p ^ m) ^ p ^ n)
⊢ Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x * y) ^ p ^ (n + m))

Tactic:
rw [mul_pow, pow_add, pow_mul, mul_comm (_ ^ n), pow_mul]

Premises used: pow_add, pow_mul, HPow.hPow, mul_comm, mul_pow
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x y : A
n : ℕ
hx : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)
m : ℕ
hy : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (y ^ p ^ m)
⊢ Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x ^ p ^ n) ^ p ^ m * (y ^ p ^ m) ^ p ^ n)

Tactic:
mul_mem (pow_mem hx _) (pow_mem hy _)

Premises used: pow_mem, MulMemClass.mul_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x y : A
n : ℕ
hx : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)
m : ℕ
hy : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (y ^ p ^ m)
⊢ Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x ^ p ^ n) ^ p ^ m * (y ^ p ^ m) ^ p ^ n)

Tactic:
exact mul_mem (pow_mem hx _) (pow_mem hy _)

Premises used: pow_mem, MulMemClass.mul_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x y : A
n : ℕ
hx : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)
m : ℕ
hy : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (y ^ p ^ m)
h : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x + y) ^ p ^ (n + m))
⊢ Membership.mem (γ := Set A)
    {x : A | ∃ (n : ℕ), Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)} (x + y)

Tactic:
use n + m
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x y : A
n : ℕ
hx : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)
m : ℕ
hy : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (y ^ p ^ m)
h : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x ^ p ^ n) ^ p ^ m + (y ^ p ^ m) ^ p ^ n)
⊢ Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x + y) ^ p ^ (n + m))

Tactic:
rw [add_pow_expChar_pow, pow_add, pow_mul, mul_comm (_ ^ n), pow_mul]

Premises used: add_pow_expChar_pow, pow_add, pow_mul, HPow.hPow, mul_comm
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x y : A
n : ℕ
hx : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)
m : ℕ
hy : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (y ^ p ^ m)
⊢ Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x ^ p ^ n) ^ p ^ m + (y ^ p ^ m) ^ p ^ n)

Tactic:
add_mem (pow_mem hx _) (pow_mem hy _)

Premises used: pow_mem, AddMemClass.add_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x y : A
n : ℕ
hx : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)
m : ℕ
hy : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (y ^ p ^ m)
⊢ Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x ^ p ^ n) ^ p ^ m + (y ^ p ^ m) ^ p ^ n)

Tactic:
exact add_mem (pow_mem hx _) (pow_mem hy _)

Premises used: pow_mem, AddMemClass.add_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x : R
rw :
  Membership.mem (α := A) (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((algebraMap R A : (a : R) → A) x : A)
⊢ Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A))
    (HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) x : A) (HPow.hPow (β := ℕ) p 0))

Tactic:
rw [pow_zero, pow_one]

Premises used: pow_zero, pow_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x : R
⊢ Membership.mem (α := A) (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((algebraMap R A : (a : R) → A) x : A)

Tactic:
⟨x, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type w
inst_3 : Field K
inst_4 : Algebra F K
R : Type u_1
A : Type u_2
inst_5 : CommSemiring R
inst_6 : CommSemiring A
inst_7 : Algebra R A
p : ℕ
inst_8 : ExpChar A p
x : R
⊢ Membership.mem (α := A) (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((algebraMap R A : (a : R) → A) x : A)

Tactic:
exact ⟨x, rfl⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
p : ℕ
inst_3 : ExpChar A p
x : A
⊢ Membership.mem (γ := Subalgebra R A) (perfectClosure R A p) x ↔
    ∃ (n : ℕ), Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
x : R ⊗[k] K
⊢ Nontrivial (R ⊗[k] K)

Tactic:
nontriviality (R ⊗[k] K)

Premises used: TensorProduct
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
x : R ⊗[k] K
h : Nontrivial (R ⊗[k] K)
inl :
  ∀ (hq : Nat.Prime q),
    ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
inr :
  ∀ (hq : q = 1),
    ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)

Tactic:
obtain (hq | hq) := expChar_is_prime_or_one k q

Premises used: expChar_is_prime_or_one
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
⊢ ((algebraMap R (R ⊗[k] K) : R →+* R ⊗[k] K) : (a : R) → R ⊗[k] K) 0 =
    HPow.hPow (α := R ⊗[k] K) 0 (HPow.hPow (β := ℕ) q 0)

Tactic:
simp
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
      (HPow.hPow (α := R ⊗[k] K) 0 (q ^ n))

Tactic:
exact ⟨0, 0, by simp⟩
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h_1 : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x y : R ⊗[k] K
h : ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
h' : ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (y ^ q ^ n)
⊢ ExpChar (R ⊗[k] K) q

Tactic:
have : ExpChar (R ⊗[k] K) q := expChar_of_injective_ringHom (algebraMap k _).injective q
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h_1 : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x y : R ⊗[k] K
h : ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
h' : ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (y ^ q ^ n)
this : ExpChar (R ⊗[k] K) q
inl :
  ∀
    (h :
      Membership.mem (γ := Subalgebra R (R ⊗[k] K)) (Subalgebra.perfectClosure R (R ⊗[k] K) q : Subalgebra R (R ⊗[k] K))
        x)
    (h' :
      Membership.mem (γ := Subalgebra R (R ⊗[k] K)) (Subalgebra.perfectClosure R (R ⊗[k] K) q : Subalgebra R (R ⊗[k] K))
        y),
    Membership.mem (γ := Subalgebra R (R ⊗[k] K)) (Subalgebra.perfectClosure R (R ⊗[k] K) q : Subalgebra R (R ⊗[k] K))
      (x + y)
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) ((x + y) ^ q ^ n)

Tactic:
simp_rw [RingHom.mem_range, ← RingHom.mem_rangeS, ← Subalgebra.mem_perfectClosure_iff] at h h' ⊢

Premises used: RingHom.mem_range, RingHom.mem_rangeS, Subalgebra.mem_perfectClosure_iff
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h_1 : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x y : R ⊗[k] K
this : ExpChar (R ⊗[k] K) q
h : Membership.mem (γ := Subalgebra R (R ⊗[k] K)) (Subalgebra.perfectClosure R (R ⊗[k] K) q : Subalgebra R (R ⊗[k] K)) x
h' :
  Membership.mem (γ := Subalgebra R (R ⊗[k] K)) (Subalgebra.perfectClosure R (R ⊗[k] K) q : Subalgebra R (R ⊗[k] K)) y
⊢ Membership.mem (γ := Subalgebra R (R ⊗[k] K)) (Subalgebra.perfectClosure R (R ⊗[k] K) q : Subalgebra R (R ⊗[k] K))
    (x + y)

Tactic:
add_mem h h'

Premises used: Set.Mem, setOf, AddMemClass.add_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h_1 : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x y : R ⊗[k] K
this : ExpChar (R ⊗[k] K) q
h : Membership.mem (γ := Subalgebra R (R ⊗[k] K)) (Subalgebra.perfectClosure R (R ⊗[k] K) q : Subalgebra R (R ⊗[k] K)) x
h' :
  Membership.mem (γ := Subalgebra R (R ⊗[k] K)) (Subalgebra.perfectClosure R (R ⊗[k] K) q : Subalgebra R (R ⊗[k] K)) y
⊢ Membership.mem (γ := Subalgebra R (R ⊗[k] K)) (Subalgebra.perfectClosure R (R ⊗[k] K) q : Subalgebra R (R ⊗[k] K))
    (x + y)

Tactic:
exact add_mem h h'

Premises used: AddMemClass.add_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
inl :
  ∀ (n : ℕ) (a : k) (ha : ((algebraMap k K : k →+* K) : (a : k) → K) a = y ^ q ^ n),
    ∃ (n : ℕ),
      Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
        (HPow.hPow (α := R ⊗[k] K) (x ⊗ₜ[k] y) (q ^ n))
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
      (HPow.hPow (α := R ⊗[k] K) (x ⊗ₜ[k] y) (q ^ n))

Tactic:
obtain ⟨n, a, ha⟩ := IsPurelyInseparable.pow_mem k q y

Premises used: IsPurelyInseparable.pow_mem
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h_1 : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : ((algebraMap k K : k →+* K) : (a : k) → K) a = y ^ q ^ n
h :
  Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
    (HPow.hPow (α := R ⊗[k] K) (x ⊗ₜ[k] y) (q ^ n))
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
      (HPow.hPow (α := R ⊗[k] K) (x ⊗ₜ[k] y) (q ^ n))

Tactic:
use n
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : ((algebraMap k K : k →+* K) : (a : k) → K) a = y ^ q ^ n
rw : Eq (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n)) ((x ^ q ^ n * 1) ⊗ₜ[k] (1 * y ^ q ^ n))
rw₁ : Eq (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n)) ((x ^ q ^ n) ⊗ₜ[k] (1 * y ^ q ^ n))
rw₂ rw₃ : Eq (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n)) ((x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n))
⊢ (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))

Tactic:
rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]

Premises used: Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul
-- Module: Mathlib.FieldTheory.PurelyInseparable.Basic
Goal:
k : Type u_1
K : Type u_2
R : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : CommRing R
inst_4 : Algebra k R
inst_5 : IsPurelyInseparable k K
q : ℕ
inst_6 : ExpChar k q
h : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : ((algebraMap k K : k →+* K) : (a : k) → K) a = y ^ q ^ n
⊢ (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))

Tactic:
have : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) =
        (x ^ q ^ n) ⊗ₜ[k] (1 : K) * (1 : R) ⊗ₜ[k] (y ^ q ^ n) := by
      rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]