awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h_1 : Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x
n : ℕ
h_2 : HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0
m : ℕ
h : (x ^ p ^ n) ^ p ^ m = 0
⊢ ∃ (n : ℕ), x ^ p ^ n = 0

Tactic:
exact ⟨n + m, by rwa [pow_add, pow_mul]⟩
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h : Membership.mem (γ := Submodule K K) (pNilradical K p) x
refine_2 : ∀ (h : ∃ (n : ℕ), x ^ p ^ n = 0), ∃ (n : ℕ), HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0
⊢ Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x

Tactic:
simp only [Ideal.mem_comap, mem_pNilradical] at h ⊢

Premises used: mem_pNilradical, Ideal.mem_comap
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h : ∃ (n : ℕ), x ^ p ^ n = 0
refine_2 : ∀ (n : ℕ) (h : x ^ p ^ n = 0), ∃ (n : ℕ), HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0
⊢ ∃ (n : ℕ), HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0

Tactic:
obtain ⟨n, h⟩ := h
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
n : ℕ
h : x ^ p ^ n = 0
⊢ HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0

Tactic:
simpa only [map_pow, map_zero] using congr(i $h)

Premises used: map_zero, map_pow
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
n : ℕ
h : x ^ p ^ n = 0
⊢ ∃ (n : ℕ), HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0

Tactic:
exact ⟨n, by simpa only [map_pow, map_zero] using congr(i $h)⟩
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
j : K →+* M
f : L →+* M
p : ℕ
x : K
⊢ (RingHom.id K : (a : K) → K) x = x ^ HPow.hPow (β := ℕ) p 0

Tactic:
simp
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
j : K →+* M
f : L →+* M
p : ℕ
x : K
h : Membership.mem (γ := Submodule K K) (RingHom.ker (F := K →+* K) (RingHom.id K)) x
⊢ Membership.mem (γ := Ideal K) (pNilradical K p) 0

Tactic:
Ideal.zero_mem _

Premises used: Ideal.zero_mem
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
j : K →+* M
f : L →+* M
p : ℕ
x : K
h : Membership.mem (γ := Submodule K K) (RingHom.ker (F := K →+* K) (RingHom.id K)) x
⊢ Membership.mem (γ := Submodule K K) (pNilradical K p) x

Tactic:
convert! Ideal.zero_mem _

Premises used: Ideal.zero_mem
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
obtain :
  ∀ (n : ℕ) (y : L) (hy : (f : (a : L) → M) y = x ^ p ^ n), ∃ (n : ℕ) (y : K), (f.comp i : (a : K) → M) y = x ^ p ^ n
⊢ ∃ (n : ℕ) (y : K), (f.comp i : (a : K) → M) y = x ^ p ^ n

Tactic:
obtain ⟨n, y, hy⟩ := pow_mem f p x

Premises used: IsPRadical.pow_mem
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
n : ℕ
y : L
hy : (f : (a : L) → M) y = x ^ p ^ n
obtain :
  ∀ (m : ℕ) (z : K) (hz : (i : (a : K) → L) z = y ^ p ^ m), ∃ (n : ℕ) (y : K), (f.comp i : (a : K) → M) y = x ^ p ^ n
⊢ ∃ (n : ℕ) (y : K), (f.comp i : (a : K) → M) y = x ^ p ^ n

Tactic:
obtain ⟨m, z, hz⟩ := pow_mem i p y

Premises used: IsPRadical.pow_mem
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
n : ℕ
y : L
hy : (f : (a : L) → M) y = x ^ p ^ n
m : ℕ
z : K
hz : (i : (a : K) → L) z = y ^ p ^ m
rw : (f : (a : L) → M) ((i : (a : K) → L) z : L) = x ^ p ^ (n + m)
rw₁ : (f : (a : L) → M) (y ^ p ^ m) = x ^ p ^ (n + m)
rw₂ : HPow.hPow (α := M) ((f : (a : L) → M) y : M) (p ^ m) = x ^ p ^ (n + m)
rw₃ : (x ^ p ^ n) ^ p ^ m = x ^ p ^ (n + m)
rw₄ : (x ^ p ^ n) ^ p ^ m = x ^ (p ^ n * p ^ m)
rw₅ rw₆ : (x ^ p ^ n) ^ p ^ m = (x ^ p ^ n) ^ p ^ m
⊢ (f.comp i : (a : K) → M) z = x ^ p ^ (n + m)

Tactic:
rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]

Premises used: pow_add, map_pow, pow_mul, RingHom.comp_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
n : ℕ
y : L
hy : (f : (a : L) → M) y = x ^ p ^ n
m : ℕ
z : K
hz : (i : (a : K) → L) z = y ^ p ^ m
⊢ ∃ (n : ℕ) (y : K), (f.comp i : (a : K) → M) y = x ^ p ^ n

Tactic:
exact ⟨n + m, z, by rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]⟩
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : K
h : Membership.mem (γ := Submodule K K) (RingHom.ker (f.comp i)) x
⊢ Membership.mem (α := L) (γ := Ideal L) (RingHom.ker f) ((i : (a : K) → L) x : L)

Tactic:
rw [RingHom.mem_ker, RingHom.comp_apply, ← RingHom.mem_ker] at h

Premises used: RingHom.mem_ker, RingHom.comp_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : K
h : Membership.mem (α := L) (γ := Ideal L) (RingHom.ker f) ((i : (a : K) → L) x : L)
⊢ Membership.mem (γ := Submodule K K) (pNilradical K p) x

Tactic:
simpa only [← Ideal.mem_comap, comap_pNilradical] using ker_le f p h

Premises used: IsPRadical.ker_le, IsPRadical.comap_pNilradical, Ideal.mem_comap
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h : Membership.mem (γ := Submodule K K) (pNilradical K p) x
obtain : ∀ (n : ℕ) (h : x ^ p ^ n = 0), Membership.mem (γ := Submodule K K) (ker i) x
⊢ Membership.mem (γ := Submodule K K) (ker i) x

Tactic:
obtain ⟨n, h⟩ := mem_pNilradical.1 h

Premises used: mem_pNilradical, Iff.mp
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h_1 : Membership.mem (γ := Submodule K K) (pNilradical K p) x
n : ℕ
h : x ^ p ^ n = 0
⊢ Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) (x ^ p ^ n) : L) : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)

Tactic:
replace h := congr((iterateFrobeniusEquiv L p n).symm (i $h))
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h_1 : Membership.mem (γ := Submodule K K) (pNilradical K p) x
n : ℕ
h :
  Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) (x ^ p ^ n) : L) : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)
rwa :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            (HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n)) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₁ :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            ((iterateFrobenius L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₂ :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            ((iterateFrobeniusEquiv L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₃ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₄ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) 0 : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (h : Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L) (0 : L)), Membership.mem (γ := Submodule K K) (ker i) x
⊢ Membership.mem (γ := Submodule K K) (ker i) x

Tactic:
rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply,
    map_zero, map_zero] at h

Premises used: RingEquiv.symm_apply_apply, map_zero, map_pow, iterateFrobenius_def, iterateFrobeniusEquiv_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
inst_4 : IsPerfectClosure i p
⊢ Eq (α := Ideal K) (RingHom.ker i) (pNilradical K p)

Tactic:
IsPRadical.ker_le'.antisymm (i.pNilradical_le_ker_of_perfectRing p)

Premises used: LE.le.antisymm, RingHom.pNilradical_le_ker_of_perfectRing, IsPRadical.ker_le'
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : L
obtain : ∀ (n : ℕ) (y : K) (h : (i : (a : K) → L) y = x ^ p ^ n), ∃ (y : ℕ × K), (i : (a : K) → L) y.2 = x ^ p ^ y.1
⊢ ∃ (y : ℕ × K), (i : (a : K) → L) y.2 = x ^ p ^ y.1

Tactic:
obtain ⟨n, y, h⟩ := IsPRadical.pow_mem i p x

Premises used: IsPRadical.pow_mem
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : L
n : ℕ
y : K
h : (i : (a : K) → L) y = x ^ p ^ n
⊢ ∃ (y : ℕ × K), (i : (a : K) → L) y.2 = x ^ p ^ y.1

Tactic:
⟨(n, y), h⟩

Premises used: Prod.mk, Exists.intro
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : L
n : ℕ
y : K
h : (i : (a : K) → L) y = x ^ p ^ n
⊢ ∃ (y : ℕ × K), (i : (a : K) → L) y.2 = x ^ p ^ y.1

Tactic:
exact ⟨(n, y), h⟩
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
inst_3 : ExpChar L p
inst_4 : PerfectRing L p
x : L
rw :
  (RingEquiv.symm
          (iterateFrobeniusEquiv L p
            (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
        (a : L) → L)
      ((i : (a : K) → L) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 :
        L) =
    x
rw₁ :
  (RingEquiv.symm
          (iterateFrobeniusEquiv L p
            (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
        (a : L) → L)
      (x ^ p ^ (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1) =
    x
rw₂ :
  (RingEquiv.symm
          (iterateFrobeniusEquiv L p
            (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
        (a : L) → L)
      ((iterateFrobenius L p (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1 :
            (a : L) → L)
          x :
        L) =
    x
rw₃ :
  (RingEquiv.symm
          (iterateFrobeniusEquiv L p
            (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
        (a : L) → L)
      ((iterateFrobeniusEquiv L p
              (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1 :
            (a : L) → L)
          x :
        L) =
    x
rw₄ rw₅ : x = x
⊢ liftAux i i p x = x

Tactic:
rw [liftAux, Classical.choose_spec (lift_aux i p x), ← iterateFrobenius_def,
    ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply]

Premises used: RingEquiv.symm_apply_apply, iterateFrobenius_def, Classical.choose_spec, iterateFrobeniusEquiv_apply, PerfectRing.liftAux, PerfectRing.lift_aux
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
inst_3 : ExpChar L p
inst_4 : PerfectRing L p
⊢ liftAux i i p = id

Tactic:
funext (liftAux_self_apply i p)

Premises used: PerfectRing.liftAux_self_apply, funext
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring M
j : K →+* M
p : ℕ
inst_2 : ExpChar M p
inst_3 : PerfectRing M p
x : K
⊢ (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).2 =
    x ^ p ^ (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1

Tactic:
have := RingHom.id_apply _ ▸ Classical.choose_spec (lift_aux (RingHom.id K) p x)
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring M
j : K →+* M
p : ℕ
inst_2 : ExpChar M p
inst_3 : PerfectRing M p
x : K
this :
  (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).2 =
    x ^ p ^ (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1
rw :
  Eq (α := M)
    ((RingEquiv.symm
            (iterateFrobeniusEquiv M p
              (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
          (a : M) → M)
        ((j : (a : K) → M)
            (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).2 :
          M) :
      M)
    ((j : (a : K) → M) x : M)
rw₁ :
  Eq (α := M)
    ((RingEquiv.symm
            (iterateFrobeniusEquiv M p
              (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
          (a : M) → M)
        ((j : (a : K) → M)
            (x ^
              p ^
                (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
          M) :
      M)
    ((j : (a : K) → M) x : M)
rw₂ :
  Eq (α := M)
    ((RingEquiv.symm
            (iterateFrobeniusEquiv M p
              (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
          (a : M) → M)
        (HPow.hPow (α := M) ((j : (a : K) → M) x : M)
          (p ^ (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1)) :
      M)
    ((j : (a : K) → M) x : M)
rw₃ :
  Eq (α := M)
    ((RingEquiv.symm
            (iterateFrobeniusEquiv M p
              (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
          (a : M) → M)
        ((iterateFrobenius M p
                (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1 :
              (a : M) → M)
            ((j : (a : K) → M) x : M) :
          M) :
      M)
    ((j : (a : K) → M) x : M)
rw₄ :
  Eq (α := M)
    ((RingEquiv.symm
            (iterateFrobeniusEquiv M p
              (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
          (a : M) → M)
        ((iterateFrobeniusEquiv M p
                (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) ⋯).1 :
              (a : M) → M)
            ((j : (a : K) → M) x : M) :
          M) :
      M)
    ((j : (a : K) → M) x : M)
rw₅ rw₆ : Eq.{u_3 + 1} (α := M) ((j : (a : K) → M) x : M) ((j : (a : K) → M) x : M)
⊢ liftAux (RingHom.id K) j p x = (j : (a : K) → M) x

Tactic:
rw [liftAux, this, map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply,
    RingEquiv.symm_apply_apply]

Premises used: RingEquiv.symm_apply_apply, map_pow, iterateFrobenius_def, iterateFrobeniusEquiv_apply, PerfectRing.liftAux
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring M
j : K →+* M
p : ℕ
inst_2 : ExpChar M p
inst_3 : PerfectRing M p
⊢ liftAux (RingHom.id K) j p = (⇑j : (a : K) → M)

Tactic:
funext (liftAux_id_apply j p)

Premises used: PerfectRing.liftAux_id_apply, funext
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
p : ℕ
inst_3 : ExpChar M p
inst_4 : IsPRadical i p
h : Eq (α := Ideal M) (pNilradical M p) ⊥
f g : L →+* M
heq : Eq (α := K →+* M) ((fun (f : L →+* M) ↦ f.comp i) f) ((fun (f : L →+* M) ↦ f.comp i) g)
a : ∀ (x : L), Eq.{u_3 + 1} (α := M) ((f : (a : L) → M) x : M) ((g : (a : L) → M) x : M)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
p : ℕ
inst_3 : ExpChar M p
inst_4 : IsPRadical i p
h : Eq (α := Ideal M) (pNilradical M p) ⊥
f g : L →+* M
heq : Eq (α := K →+* M) ((fun (f : L →+* M) ↦ f.comp i) f) ((fun (f : L →+* M) ↦ f.comp i) g)
x : L
a :
  ∀ (n : ℕ) (y : K) (hx : (i : (a : K) → L) y = x ^ p ^ n),
    Eq.{u_3 + 1} (α := M) ((f : (a : L) → M) x : M) ((g : (a : L) → M) x : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : L) → M) x : M) ((g : (a : L) → M) x : M)

Tactic:
obtain ⟨n, y, hx⟩ := IsPRadical.pow_mem i p x

Premises used: IsPRadical.pow_mem
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
p : ℕ
inst_3 : ExpChar M p
inst_4 : IsPRadical i p
h : Eq (α := Ideal M) (pNilradical M p) ⊥
f g : L →+* M
heq : Eq (α := K →+* M) ((fun (f : L →+* M) ↦ f.comp i) f) ((fun (f : L →+* M) ↦ f.comp i) g)
x : L
n : ℕ
y : K
hx : (i : (a : K) → L) y = x ^ p ^ n
⊢ Function.Injective (β := M) fun (x : M) ↦ x ^ p ^ n

Tactic:
pow_expChar_pow_inj_of_pNilradical_eq_bot M p h n

Premises used: pow_expChar_pow_inj_of_pNilradical_eq_bot
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
p : ℕ
inst_3 : ExpChar M p
inst_4 : IsPRadical i p
h : Eq (α := Ideal M) (pNilradical M p) ⊥
f g : L →+* M
heq : Eq (α := K →+* M) ((fun (f : L →+* M) ↦ f.comp i) f) ((fun (f : L →+* M) ↦ f.comp i) g)
x : L
n : ℕ
y : K
hx : (i : (a : K) → L) y = x ^ p ^ n
a : HPow.hPow (α := M) ((f : (a : L) → M) x : M) (p ^ n) = HPow.hPow (α := M) ((g : (a : L) → M) x : M) (p ^ n)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : L) → M) x : M) ((g : (a : L) → M) x : M)

Tactic:
apply_fun _ using pow_expChar_pow_inj_of_pNilradical_eq_bot M p h n

Premises used: pow_expChar_pow_inj_of_pNilradical_eq_bot
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
p : ℕ
inst_3 : ExpChar M p
inst_4 : IsPRadical i p
h : Eq (α := Ideal M) (pNilradical M p) ⊥
f g : L →+* M
heq : Eq (α := K →+* M) ((fun (f : L →+* M) ↦ f.comp i) f) ((fun (f : L →+* M) ↦ f.comp i) g)
x : L
n : ℕ
y : K
hx : (i : (a : K) → L) y = x ^ p ^ n
⊢ HPow.hPow (α := M) ((f : (a : L) → M) x : M) (p ^ n) = HPow.hPow (α := M) ((g : (a : L) → M) x : M) (p ^ n)

Tactic:
simpa only [← map_pow, ← hx] using congr($(heq) y)

Premises used: map_pow
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
p : ℕ
inst_3 : ExpChar M p
inst_4 : IsPRadical i p
inst_5 : IsReduced M
⊢ Function.Injective (β := K →+* M) fun (f : L →+* M) ↦ f.comp i

Tactic:
injective_comp_of_pNilradical_eq_bot i p <| bot_unique <|
    pNilradical_le_nilradical.trans (nilradical_eq_zero M).le

Premises used: nilradical_eq_zero, Eq.le, IsPRadical.injective_comp_of_pNilradical_eq_bot, bot_unique, LE.le.trans, pNilradical_le_nilradical
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
p : ℕ
inst_3 : ExpChar M p
inst_4 : IsPRadical i p
inst_5 : PerfectRing M p
⊢ Function.Injective (β := K →+* M) fun (f : L →+* M) ↦ f.comp i

Tactic:
injective_comp_of_pNilradical_eq_bot i p (PerfectRing.pNilradical_eq_bot M p)

Premises used: IsPRadical.injective_comp_of_pNilradical_eq_bot, PerfectRing.pNilradical_eq_bot
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
x : L
n : ℕ
y : K
h : (i : (a : K) → L) y = x ^ p ^ n
rw :
  Eq (α := M)
    ((RingEquiv.symm
            (iterateFrobeniusEquiv M p
              (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1) :
          (a : M) → M)
        ((j : (a : K) → M) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 :
          M) :
      M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M)
⊢ liftAux i j p x = (RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M)

Tactic:
rw [liftAux]

Premises used: PerfectRing.liftAux
-- Module: Mathlib.FieldTheory.IsPerfectClosure
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
x : L
n : ℕ
y : K
h : (i : (a : K) → L) y = x ^ p ^ n
⊢ (i : (a : K) → L) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 =
    x ^ p ^ (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1

Tactic:
have h' := Classical.choose_spec (lift_aux i p x)