awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ ∃ (y : ℕ × K), (i : (a : K) → L) y.2 = x ^ p ^ y.1
have 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
Tactic: obtain ⟨n, y, h⟩ := IsPRadical.pow_mem i p x
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ liftAux i i p x = x
have 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) sorry).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) sorry).2 : L) =
  x
Tactic: rw [liftAux, Classical.choose_spec (lift_aux i p x), ← iterateFrobenius_def,
    ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ liftAux i i p x = x
have 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) sorry).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) sorry).1) =
  x
Tactic: rw [liftAux, Classical.choose_spec (lift_aux i p x), ← iterateFrobenius_def,
    ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ liftAux i i p x = x
have 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) sorry).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) sorry).1 :
          (a : L) → L)
        x :
      L) =
  x
Tactic: rw [liftAux, Classical.choose_spec (lift_aux i p x), ← iterateFrobenius_def,
    ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ liftAux i i p x = x
have 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) sorry).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) sorry).1 :
          (a : L) → L)
        x :
      L) =
  x
Tactic: rw [liftAux, Classical.choose_spec (lift_aux i p x), ← iterateFrobenius_def,
    ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ liftAux i i p x = x
have rw₄ : x = x
Tactic: rw [liftAux, Classical.choose_spec (lift_aux i p x), ← iterateFrobenius_def,
    ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (hypothesis)
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
⊢ liftAux (RingHom.id K) j p x = (j : (a : K) → M) x
have this : (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) sorry).2 =
  x ^ p ^ (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (RingHom.id K : (a : K) → K) x_1.2 = x ^ p ^ x_1.1) sorry).1
Tactic: have := RingHom.id_apply _ ▸ Classical.choose_spec (lift_aux (RingHom.id K) p x)
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ liftAux (RingHom.id K) j p x = (j : (a : K) → M) x
have 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) sorry).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) sorry).2 :
        M) :
    M)
  ((j : (a : K) → M) x : M)
Tactic: rw [liftAux, this, map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply,
    RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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)
⊢ liftAux (RingHom.id K) j p x = (j : (a : K) → M) x
have 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) sorry).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) sorry).1) :
        M) :
    M)
  ((j : (a : K) → M) x : M)
Tactic: rw [liftAux, this, map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply,
    RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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)
⊢ liftAux (RingHom.id K) j p x = (j : (a : K) → M) x
have 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) sorry).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) sorry).1)) :
    M)
  ((j : (a : K) → M) x : M)
Tactic: rw [liftAux, this, map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply,
    RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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)
⊢ liftAux (RingHom.id K) j p x = (j : (a : K) → M) x
have 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) sorry).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) sorry).1 :
            (a : M) → M)
          ((j : (a : K) → M) x : M) :
        M) :
    M)
  ((j : (a : K) → M) x : M)
Tactic: rw [liftAux, this, map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply,
    RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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)
⊢ liftAux (RingHom.id K) j p x = (j : (a : K) → M) x
have 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) sorry).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) sorry).1 :
            (a : M) → M)
          ((j : (a : K) → M) x : M) :
        M) :
    M)
  ((j : (a : K) → M) x : M)
Tactic: rw [liftAux, this, map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply,
    RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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)
⊢ liftAux (RingHom.id K) j p x = (j : (a : K) → M) x
have rw₅ : Eq.{u_3 + 1} (α := M) ((j : (a : K) → M) x : M) ((j : (a : K) → M) x : M)
Tactic: rw [liftAux, this, map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply,
    RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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)
⊢ f = g
have a : ∀ (x : L), Eq.{u_3 + 1} (α := M) ((f : (a : L) → M) x : M) ((g : (a : L) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : L) → M) x : M) ((g : (a : L) → M) x : M)
have 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)
Tactic: obtain ⟨n, y, hx⟩ := IsPRadical.pow_mem i p x
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : L) → M) x : M) ((g : (a : L) → M) x : M)
have a : HPow.hPow (α := M) ((f : (a : L) → M) x : M) (p ^ n) = HPow.hPow (α := M) ((g : (a : L) → M) x : M) (p ^ n)
Tactic: apply_fun _ using pow_expChar_pow_inj_of_pNilradical_eq_bot M p h n
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
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
⊢ liftAux i j p x = (RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M)
have 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) sorry).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) sorry).2 :
        M) :
    M)
  ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M)
Tactic: rw [liftAux]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (hypothesis)
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
⊢ 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)
have h' : (i : (a : K) → L) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) sorry).2 =
  x ^ p ^ (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) sorry).1
Tactic: have h' := Classical.choose_spec (lift_aux i p x)