awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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 (γ := Set A)
    {x : A | ∃ (n : ℕ), Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) (x ^ p ^ n)} (x + y)
have h : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x + y) ^ p ^ (n + m))
Tactic: use n + m
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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 + y) ^ p ^ (n + m))
have h : Membership.mem (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((x ^ p ^ n) ^ p ^ m + (y ^ p ^ m) ^ p ^ n)
Tactic: rw [add_pow_expChar_pow, pow_add, pow_mul, mul_comm (_ ^ n), pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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 (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A))
    (HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) x : A) (HPow.hPow (β := ℕ) p 0))
have rw : Membership.mem (α := A) (γ := Subsemiring A) (RingHom.rangeS (algebraMap R A)) ((algebraMap R A : (a : R) → A) x : A)
Tactic: rw [pow_zero, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
have a : Nontrivial (R ⊗[k] K)
Tactic: nontriviality (R ⊗[k] K)
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
have inl : ∀ (hq : Nat.Prime q),
  ∃ (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
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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)
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
have inr : ∀ (hq : q = 1),
  ∃ (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
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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)
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) ((x + y) ^ q ^ n)
have this : ExpChar (R ⊗[k] K) q
Tactic: have : ExpChar (R ⊗[k] K) q := expChar_of_injective_ringHom (algebraMap k _).injective q
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) ((x + y) ^ q ^ n)
have 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)
Tactic: simp_rw [RingHom.mem_range, ← RingHom.mem_rangeS, ← Subalgebra.mem_perfectClosure_iff] at h h' ⊢
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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 : ℕ),
    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))
have 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))
Tactic: obtain ⟨n, a, ha⟩ := IsPurelyInseparable.pow_mem k q y
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
⊢ ∃ (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))
have 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))
Tactic: use n
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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))
have rw : Eq (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n)) ((x ^ q ^ n * 1) ⊗ₜ[k] (1 * y ^ q ^ n))
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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))
⊢ (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
have rw₁ : Eq (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n)) ((x ^ q ^ n) ⊗ₜ[k] (1 * y ^ q ^ n))
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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))
⊢ (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
have rw₂ : Eq (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n)) ((x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n))
Tactic: rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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
⊢ 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))
have this : (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]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ 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))
have h : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
  (HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n)))
Tactic: rw [Algebra.TensorProduct.tmul_pow, this]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
⊢ Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
    (HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n)))
have h : Eq (α := R ⊗[k] K)
  (((algebraMap R (R ⊗[k] K) : R →+* R ⊗[k] K) : (a : R) → R ⊗[k] K) ((algebraMap k R : (a : k) → R) a) : R ⊗[k] K)
  (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
Tactic: refine Subring.mul_mem _ ⟨x ^ q ^ n, rfl⟩ ⟨algebraMap k R a, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
⊢ Eq (α := R ⊗[k] K)
    (((algebraMap R (R ⊗[k] K) : R →+* R ⊗[k] K) : (a : R) → R ⊗[k] K) ((algebraMap k R : (a : k) → R) a) : R ⊗[k] K)
    (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
have h : Eq (α := R ⊗[k] K) ((algebraMap k (R ⊗[k] K) : (a : k) → R ⊗[k] K) a : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
Tactic: rw [← IsScalarTower.algebraMap_apply, Algebra.TensorProduct.algebraMap_apply,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, ha]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
h : Eq (α := R ⊗[k] K) ((algebraMap k (R ⊗[k] K) : (a : k) → R ⊗[k] K) a : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
⊢ Eq (α := R ⊗[k] K)
    (((algebraMap R (R ⊗[k] K) : R →+* R ⊗[k] K) : (a : R) → R ⊗[k] K) ((algebraMap k R : (a : k) → R) a) : R ⊗[k] K)
    (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
have h₁ : Eq (α := R ⊗[k] K) ((algebraMap k R : (a : k) → R) a ⊗ₜ[k] 1 : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
Tactic: rw [← IsScalarTower.algebraMap_apply, Algebra.TensorProduct.algebraMap_apply,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, ha]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
h : Eq (α := R ⊗[k] K) ((algebraMap k (R ⊗[k] K) : (a : k) → R ⊗[k] K) a : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
h₁ : Eq (α := R ⊗[k] K) ((algebraMap k R : (a : k) → R) a ⊗ₜ[k] 1 : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
⊢ Eq (α := R ⊗[k] K)
    (((algebraMap R (R ⊗[k] K) : R →+* R ⊗[k] K) : (a : R) → R ⊗[k] K) ((algebraMap k R : (a : k) → R) a) : R ⊗[k] K)
    (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
have h₂ : Eq (α := R ⊗[k] K) (1 ⊗ₜ[k] (algebraMap k K : (a : k) → K) a : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
Tactic: rw [← IsScalarTower.algebraMap_apply, Algebra.TensorProduct.algebraMap_apply,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, ha]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = HMul.hMul (α := R ⊗[k] K) ((x ^ q ^ n) ⊗ₜ[k] 1) (1 ⊗ₜ[k] (y ^ q ^ n))
h : Eq (α := R ⊗[k] K) ((algebraMap k (R ⊗[k] K) : (a : k) → R ⊗[k] K) a : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
h₁ : Eq (α := R ⊗[k] K) ((algebraMap k R : (a : k) → R) a ⊗ₜ[k] 1 : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
h₂ : Eq (α := R ⊗[k] K) (1 ⊗ₜ[k] (algebraMap k K : (a : k) → K) a : R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
⊢ Eq (α := R ⊗[k] K)
    (((algebraMap R (R ⊗[k] K) : R →+* R ⊗[k] K) : (a : R) → R ⊗[k] K) ((algebraMap k R : (a : k) → R) a) : R ⊗[k] K)
    (1 ⊗ₜ[k] (y ^ q ^ n) : R ⊗[k] K)
have h₃ : Eq (α := R ⊗[k] K) (1 ⊗ₜ[k] (y ^ q ^ n)) (1 ⊗ₜ[k] (y ^ q ^ n))
Tactic: rw [← IsScalarTower.algebraMap_apply, Algebra.TensorProduct.algebraMap_apply,
      Algebra.TensorProduct.tmul_one_eq_one_tmul, ha]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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)
hq : q = 1
⊢ ∃ (n : ℕ), Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
have inr : ∀ [ExpChar k 1],
  ∃ (n : ℕ),
    Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
      (x ^ HPow.hPow (α := ℕ) 1 n)
Tactic: subst hq
Cleared hypotheses: q, inst_6, hq
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (hypothesis)
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
x : R ⊗[k] K
h : Nontrivial (R ⊗[k] K)
inst_6 : ExpChar k 1
⊢ ∃ (n : ℕ),
    Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K)))
      (x ^ HPow.hPow (α := ℕ) 1 n)
have this : CharZero k
Tactic: have : CharZero k := charZero_of_expChar_one' k
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
x : R ⊗[k] K
q : ℕ := ringExpChar k
⊢ ∃ n > 0, Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ n)
have obtain : ∀ (n : ℕ)
  (hr : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)),
  ∃ n > 0, Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ n)
Tactic: obtain ⟨n, hr⟩ := exists_pow_pow_mem_range_tensorProduct_of_expChar q x
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
⊢ ∃ n > 0, Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ n)
have refine : 0 < q
Tactic: refine ⟨q ^ n, pow_pos ?_ _, hr⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
⊢ 0 < q
have inl : ∀ (hq : Nat.Prime q), 0 < q
Tactic: obtain (hq | hq) := expChar_is_prime_or_one k q
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Basic (goal)
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
x : R ⊗[k] K
q : ℕ := ringExpChar k
n : ℕ
hr : Membership.mem (γ := Subring (R ⊗[k] K)) (RingHom.range (R := R) (algebraMap R (R ⊗[k] K))) (x ^ q ^ n)
inl : ∀ (hq : Nat.Prime q), 0 < q
⊢ 0 < q
have inr : ∀ (hq : q = 1), 0 < q
Tactic: obtain (hq | hq) := expChar_is_prime_or_one k q
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) a
⊢ elemExponent K a = 0
have apply : ∃ (y : K),
  minpoly K a =
    HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (HPow.hPow (β := ℕ) (ringExpChar K) 0))
      ((C : (a : K) → K[X]) y : K[X])
Tactic: apply (Nat.find_eq_zero _).mpr
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) a
⊢ ∃ (y : K),
    minpoly K a =
      HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (HPow.hPow (β := ℕ) (ringExpChar K) 0))
        ((C : (a : K) → K[X]) y : K[X])
have rw : ∃ (y : K), minpoly K a = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X])
Tactic: rw [pow_zero, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
h : Membership.mem (γ := Subring L) (RingHom.range.{u_2, u_3} (R := K) (algebraMap K L)) a
⊢ ∃ (y : K), minpoly K a = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X])
have obtain : ∀ (y : K) (hy : ((algebraMap K L : K →+* L) : (a : K) → L) y = a),
  ∃ (y : K), minpoly K a = HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X])
Tactic: obtain ⟨y, hy⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
⊢ natDegree (minpoly K a) = ringExpChar K ^ elemExponent K a
have rw : (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
      ((C : (a : K) → K[X]) (elemReduct K a) : K[X])).natDegree =
  ringExpChar K ^ elemExponent K a
Tactic: rw [minpoly_eq K a, natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.PurelyInseparable.Exponent (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsPurelyInseparable K L
a : L
rw :
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a))
        ((C : (a : K) → K[X]) (elemReduct K a) : K[X])).natDegree =
    ringExpChar K ^ elemExponent K a
⊢ natDegree (minpoly K a) = ringExpChar K ^ elemExponent K a
have rw₁ : (HPow.hPow (α := K[X]) X (ringExpChar K ^ elemExponent K a)).natDegree = ringExpChar K ^ elemExponent K a
Tactic: rw [minpoly_eq K a, natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]