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
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
h' :
  (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
⊢ 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 set : let n' := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) sorry).1;
∀
  (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 ^ n'),
  Eq (α := M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n') : (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: set n' := (Classical.choose (lift_aux i p x)).1
Cleared hypotheses: h'
-- 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
n' : ℕ := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1
h' :
  (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 ^ n'
⊢ Eq (α := M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n') : (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₁ : (x ^ p ^ n) ^ p ^ n' = HPow.hPow (α := L) ((i : (a : K) → L) y : L) (p ^ n')
Tactic: replace h := congr($(h.symm) ^ p ^ n')
Cleared hypotheses: h
-- 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
n' : ℕ := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1
h' :
  (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 ^ n'
h : (x ^ p ^ n) ^ p ^ n' = HPow.hPow (α := L) ((i : (a : K) → L) y : L) (p ^ n')
⊢ Eq (α := M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n') : (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₁ : Membership.mem (γ := Ideal K) (RingHom.ker i)
  ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) sorry).2 ^ p ^ n - y ^ p ^ n')
Tactic: rw [← pow_mul, mul_comm, pow_mul, ← h', ← map_pow, ← map_pow, ← sub_eq_zero, ← map_sub,
    ← RingHom.mem_ker] at h
Cleared hypotheses: h
-- 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
n' : ℕ := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1
h' :
  (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 ^ n'
h :
  Membership.mem (γ := Ideal K) (RingHom.ker i)
    ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n')
⊢ Eq (α := M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n') : (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 obtain : ∀ (m : ℕ)
  (h :
    ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) sorry).2 ^ p ^ n - y ^ p ^ n') ^
        p ^ m =
      0),
  Eq (α := M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n') : (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: obtain ⟨m, h⟩ := mem_pNilradical.1 (IsPRadical.ker_le i p h)
-- 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
n' : ℕ := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1
h' :
  (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 ^ n'
h_1 :
  Membership.mem (γ := Ideal K) (RingHom.ker i)
    ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n')
m : ℕ
h :
  ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n') ^
      p ^ m =
    0
⊢ Eq (α := M)
    ((RingEquiv.symm (iterateFrobeniusEquiv M p n') : (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 refine : Eq (α := M)
  ((iterateFrobeniusEquiv M p (m + n + n') : (a : M) → M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n') : (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) :
    M)
  ((iterateFrobeniusEquiv M p (m + n + n') : (a : M) → M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
    M)
Tactic: refine (iterateFrobeniusEquiv M p (m + n + n')).injective ?_
-- 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
n' : ℕ := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1
h' :
  (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 ^ n'
h_1 :
  Membership.mem (γ := Ideal K) (RingHom.ker i)
    ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n')
m : ℕ
h :
  ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n') ^
      p ^ m =
    0
| ((iterateFrobeniusEquiv M p (m + n + n') : (a : M) → M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n') : (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) :
    M)
have rw : ((iterateFrobeniusEquiv M p (m + n) : (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)
Tactic: rw [iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_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
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
n' : ℕ := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1
h' :
  (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 ^ n'
h_1 :
  Membership.mem (γ := Ideal K) (RingHom.ker i)
    ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n')
m : ℕ
h :
  ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n') ^
      p ^ m =
    0
⊢ Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n + n') : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n') : (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) :
      M)
    ((iterateFrobeniusEquiv M p (m + n + n') : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
have conv_lhs : Eq (α := M)
  ((iterateFrobeniusEquiv M p (m + n) : (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)
  ((iterateFrobeniusEquiv M p (m + n + n') : (a : M) → M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
    M)
Tactic: conv_lhs => rw [iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_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
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
n' : ℕ := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1
h' :
  (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 ^ n'
h_1 :
  Membership.mem (γ := Ideal K) (RingHom.ker i)
    ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n')
m : ℕ
h :
  ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n') ^
      p ^ m =
    0
⊢ Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (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)
    ((iterateFrobeniusEquiv M p (m + n + n') : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
have rw : Eq (α := M)
  ((iterateFrobeniusEquiv M p (m + n) : (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)
  ((iterateFrobeniusEquiv M p (m + (n + n')) : (a : M) → M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
    M)
Tactic: rw [add_assoc, add_comm n n', ← add_assoc,
    iterateFrobeniusEquiv_add_apply (m := m + n'), RingEquiv.apply_symm_apply,
    iterateFrobeniusEquiv_def, iterateFrobeniusEquiv_def,
    ← sub_eq_zero, ← map_pow, ← map_pow, ← map_sub,
    add_comm m, add_comm m, pow_add, pow_mul, pow_add, pow_mul, ← sub_pow_expChar_pow, h, map_zero]
-- 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
n' : ℕ := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1
h' :
  (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 ^ n'
h_1 :
  Membership.mem (γ := Ideal K) (RingHom.ker i)
    ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n')
m : ℕ
h :
  ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n') ^
      p ^ m =
    0
rw :
  Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (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)
    ((iterateFrobeniusEquiv M p (m + (n + n')) : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
⊢ Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (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)
    ((iterateFrobeniusEquiv M p (m + n + n') : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
have rw₁ : Eq (α := M)
  ((iterateFrobeniusEquiv M p (m + n) : (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)
  ((iterateFrobeniusEquiv M p (m + (n' + n)) : (a : M) → M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
    M)
Tactic: rw [add_assoc, add_comm n n', ← add_assoc,
    iterateFrobeniusEquiv_add_apply (m := m + n'), RingEquiv.apply_symm_apply,
    iterateFrobeniusEquiv_def, iterateFrobeniusEquiv_def,
    ← sub_eq_zero, ← map_pow, ← map_pow, ← map_sub,
    add_comm m, add_comm m, pow_add, pow_mul, pow_add, pow_mul, ← sub_pow_expChar_pow, h, map_zero]
-- 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
n' : ℕ := (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).1
h' :
  (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 ^ n'
h_1 :
  Membership.mem (γ := Ideal K) (RingHom.ker i)
    ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n')
m : ℕ
h :
  ((Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 ^ p ^ n - y ^ p ^ n') ^
      p ^ m =
    0
rw :
  Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (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)
    ((iterateFrobeniusEquiv M p (m + (n + n')) : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
rw₁ :
  Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (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)
    ((iterateFrobeniusEquiv M p (m + (n' + n)) : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
⊢ Eq (α := M)
    ((iterateFrobeniusEquiv M p (m + n) : (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)
    ((iterateFrobeniusEquiv M p (m + n + n') : (a : M) → M)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
      M)
have rw₂ : Eq (α := M)
  ((iterateFrobeniusEquiv M p (m + n) : (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)
  ((iterateFrobeniusEquiv M p (m + n' + n) : (a : M) → M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n) : (a : M) → M) ((j : (a : K) → M) y : M) : M) :
    M)
Tactic: rw [add_assoc, add_comm n n', ← add_assoc,
    iterateFrobeniusEquiv_add_apply (m := m + n'), RingEquiv.apply_symm_apply,
    iterateFrobeniusEquiv_def, iterateFrobeniusEquiv_def,
    ← sub_eq_zero, ← map_pow, ← map_pow, ← map_sub,
    add_comm m, add_comm m, pow_add, pow_mul, pow_add, pow_mul, ← sub_pow_expChar_pow, h, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
⊢ (i : (a : K) → L) 1 = HPow.hPow (α := L) 1 (HPow.hPow (β := ℕ) p 0)
have rw : Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) 1 : L) (1 : L)
Tactic: rw [one_pow, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
rw : Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) 1 : L) (1 : L)
⊢ (i : (a : K) → L) 1 = HPow.hPow (α := L) 1 (HPow.hPow (β := ℕ) p 0)
have rw₁ : Eq.{u_2 + 1} (α := L) 1 1
Tactic: rw [one_pow, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
x1 x2 : L
⊢ liftAux i j p (x1 * x2) = liftAux i j p x1 * liftAux i j p x2
have obtain : ∀ (n1 : ℕ) (y1 : K) (h1 : (i : (a : K) → L) y1 = x1 ^ p ^ n1),
  liftAux i j p (x1 * x2) = liftAux i j p x1 * liftAux i j p x2
Tactic: obtain ⟨n1, y1, h1⟩ := IsPRadical.pow_mem i p x1
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : (i : (a : K) → L) y1 = x1 ^ p ^ n1
⊢ liftAux i j p (x1 * x2) = liftAux i j p x1 * liftAux i j p x2
have obtain : ∀ (n2 : ℕ) (y2 : K) (h2 : (i : (a : K) → L) y2 = x2 ^ p ^ n2),
  liftAux i j p (x1 * x2) = liftAux i j p x1 * liftAux i j p x2
Tactic: obtain ⟨n2, y2, h2⟩ := IsPRadical.pow_mem i p x2
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : (i : (a : K) → L) y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : (i : (a : K) → L) y2 = x2 ^ p ^ n2
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw : HMul.hMul (α := L) (β := L) ((i : (a : K) → L) (y1 ^ p ^ n2) : L) ((i : (a : K) → L) (y2 ^ p ^ n1) : L) =
  (x1 * x2) ^ p ^ (n1 + n2)
Tactic: rw [map_mul,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, mul_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : (i : (a : K) → L) y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : (i : (a : K) → L) y2 = x2 ^ p ^ n2
rw :
  HMul.hMul (α := L) (β := L) ((i : (a : K) → L) (y1 ^ p ^ n2) : L) ((i : (a : K) → L) (y2 ^ p ^ n1) : L) =
    (x1 * x2) ^ p ^ (n1 + n2)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw₁ : HMul.hMul (β := L) (HPow.hPow (α := L) ((i : (a : K) → L) y1 : L) (p ^ n2)) ((i : (a : K) → L) (y2 ^ p ^ n1) : L) =
  (x1 * x2) ^ p ^ (n1 + n2)
Tactic: rw [map_mul,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, mul_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
inst_3 : CommRing N
i : K →+* L
j : K →+* M
k : K →+* N
f : L →+* M
g : L →+* N
p : ℕ
inst_4 : ExpChar M p
inst_5 : ExpChar K p
inst_6 : PerfectRing M p
inst_7 : IsPRadical i p
inst_8 : ExpChar L p
x1 x2 : L
n1 : ℕ
y1 : K
h1 : (i : (a : K) → L) y1 = x1 ^ p ^ n1
n2 : ℕ
y2 : K
h2 : (i : (a : K) → L) y2 = x2 ^ p ^ n2
rw :
  HMul.hMul (α := L) (β := L) ((i : (a : K) → L) (y1 ^ p ^ n2) : L) ((i : (a : K) → L) (y2 ^ p ^ n1) : L) =
    (x1 * x2) ^ p ^ (n1 + n2)
rw₁ :
  HMul.hMul (β := L) (HPow.hPow (α := L) ((i : (a : K) → L) y1 : L) (p ^ n2)) ((i : (a : K) → L) (y2 ^ p ^ n1) : L) =
    (x1 * x2) ^ p ^ (n1 + n2)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw₂ : HPow.hPow (α := L) ((i : (a : K) → L) y1 : L) (p ^ n2) * HPow.hPow (α := L) ((i : (a : K) → L) y2 : L) (p ^ n1) =
  (x1 * x2) ^ p ^ (n1 + n2)
Tactic: rw [map_mul,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, mul_pow]