awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
set :
  let 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)
⊢ 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)

Tactic:
set n' := (Classical.choose (lift_aux i p x)).1

Premises used: Prod.fst, Classical.choose, PerfectRing.lift_aux
-- 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
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'
⊢ (x ^ p ^ n) ^ p ^ n' = HPow.hPow (α := L) ((i : (a : K) → L) y : L) (p ^ n')

Tactic:
replace h := congr($(h.symm) ^ p ^ n')
-- 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
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')
⊢ 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')

Tactic:
rw [← pow_mul, mul_comm, pow_mul, ← h', ← map_pow, ← map_pow, ← sub_eq_zero, ← map_sub,
    ← RingHom.mem_ker] at h

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker, map_pow, pow_mul, mul_comm
-- 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
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')
obtain :
  ∀ (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)
⊢ 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)

Tactic:
obtain ⟨m, h⟩ := mem_pNilradical.1 (IsPRadical.ker_le i p h)

Premises used: IsPRadical.ker_le, mem_pNilradical, Iff.mp
-- 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
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)

Tactic:
(iterateFrobeniusEquiv M p (m + n + n')).injective ?_

Premises used: iterateFrobeniusEquiv, RingEquiv.injective, HAdd.hAdd
-- 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
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
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) ⋯).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)
⊢ 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)

Tactic:
refine (iterateFrobeniusEquiv M p (m + n + n')).injective ?_

Premises used: iterateFrobeniusEquiv, RingEquiv.injective, HAdd.hAdd
-- 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
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 :
  ((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) (Classical.choose (p := fun (x_1 : ℕ × K) ↦ (i : (a : K) → L) x_1.2 = x ^ p ^ x_1.1) ⋯).2 :
            M) :
        M) :
    M)

Tactic:
rw [iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply, iterateFrobeniusEquiv_add_apply
-- 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
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
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) ⋯).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 + 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)

Tactic:
conv_lhs => rw [iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply]

Premises used: RingEquiv.apply_symm_apply, iterateFrobeniusEquiv_add_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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)
rw₁ rw₂ : Eq.{u_2 + 1} (α := L) 1 1
⊢ (i : (a : K) → L) 1 = HPow.hPow (α := L) 1 (HPow.hPow (β := ℕ) p 0)

Tactic:
rw [one_pow, map_one]

Premises used: one_pow, map_one
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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
⊢ liftAux i j p 1 = 1

Tactic:
simp [liftAux_apply i j p 1 0 1 (by rw [one_pow, map_one])]

Premises used: OfNat.ofNat, PerfectRing.liftAux_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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
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
⊢ 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

Premises used: IsPRadical.pow_mem
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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
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
⊢ 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

Premises used: IsPRadical.pow_mem
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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)
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)
rw₃ : (x1 ^ p ^ n1) ^ p ^ n2 * HPow.hPow (α := L) ((i : (a : K) → L) y2 : L) (p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
rw₄ : (x1 ^ p ^ n1) ^ p ^ n2 * (x2 ^ p ^ n2) ^ p ^ n1 = (x1 * x2) ^ p ^ (n1 + n2)
rw₅ : x1 ^ (p ^ n1 * p ^ n2) * (x2 ^ p ^ n2) ^ p ^ n1 = (x1 * x2) ^ p ^ (n1 + n2)
rw₆ : x1 ^ p ^ (n1 + n2) * (x2 ^ p ^ n2) ^ p ^ n1 = (x1 * x2) ^ p ^ (n1 + n2)
rw₇ : x1 ^ p ^ (n1 + n2) * x2 ^ (p ^ n2 * p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
rw₈ : x1 ^ p ^ (n1 + n2) * x2 ^ p ^ (n2 + n1) = (x1 * x2) ^ p ^ (n1 + n2)
rw₉ : x1 ^ p ^ (n1 + n2) * x2 ^ p ^ (n1 + n2) = (x1 * x2) ^ p ^ (n1 + n2)
rw₁₀ rw₁₁ : x1 ^ p ^ (n1 + n2) * x2 ^ p ^ (n1 + n2) = x1 ^ p ^ (n1 + n2) * x2 ^ p ^ (n1 + n2)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ 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]

Premises used: pow_add, map_pow, add_comm, pow_mul, map_mul, mul_pow
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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 (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          ((iterateFrobeniusEquiv M p n2 : (a : M) → M) ((j : (a : K) → M) y1 : M) : M) :
        M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
        M) =
    HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)
⊢ liftAux i j p (x1 * x2) = liftAux i j p x1 * liftAux i j p x2

Tactic:
rw [liftAux_apply i j p _ _ _ h1, liftAux_apply i j p _ _ _ h2,
      liftAux_apply i j p (x1 * x2) (n1 + n2) (y1 ^ p ^ n2 * y2 ^ p ^ n1) (by rw [map_mul,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, mul_pow]),
      map_mul, map_pow, map_pow, map_mul, ← iterateFrobeniusEquiv_def]

Premises used: HMul.hMul, iterateFrobeniusEquiv_def, map_pow, map_mul, HPow.hPow, HAdd.hAdd, PerfectRing.liftAux_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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
nth_rw :
  HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M)
          ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M)
              ((iterateFrobeniusEquiv M p n2 : (a : M) → M) ((j : (a : K) → M) y1 : M) : M) :
            M) :
        M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
        M) =
    HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)
⊢ HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          ((iterateFrobeniusEquiv M p n2 : (a : M) → M) ((j : (a : K) → M) y1 : M) : M) :
        M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p (n1 + n2)) : (a : M) → M)
          (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
        M) =
    HMul.hMul (α := M) (β := M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M) ((j : (a : K) → M) y1 : M) : M)
      ((RingEquiv.symm (iterateFrobeniusEquiv M p n2) : (a : M) → M) ((j : (a : K) → M) y2 : M) : M)

Tactic:
nth_rw 1 [iterateFrobeniusEquiv_symm_add_apply]

Premises used: iterateFrobeniusEquiv_symm_add_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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 : (i : (a : K) → L) 0 = HPow.hPow (α := L) (β := ℕ) 0 1
rw₁ : Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) 0 : L) (0 : L)
rw₂ rw₃ : Eq.{u_2 + 1} (α := L) 0 0
⊢ (i : (a : K) → L) 0 = HPow.hPow (α := L) 0 (HPow.hPow (β := ℕ) p 0)

Tactic:
rw [pow_zero, pow_one, map_zero]

Premises used: map_zero, pow_zero, pow_one
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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
⊢ liftAux i j p 0 = 0

Tactic:
simp [liftAux_apply i j p 0 0 0 (by rw [pow_zero, pow_one, map_zero])]

Premises used: OfNat.ofNat, PerfectRing.liftAux_apply
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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
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
⊢ 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

Premises used: IsPRadical.pow_mem
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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
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
⊢ 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

Premises used: IsPRadical.pow_mem
-- Module: Mathlib.FieldTheory.IsPerfectClosure
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 :
  HAdd.hAdd (α := L) (β := L) ((i : (a : K) → L) (y1 ^ p ^ n2) : L) ((i : (a : K) → L) (y2 ^ p ^ n1) : L) =
    (x1 + x2) ^ p ^ (n1 + n2)
rw₁ :
  HAdd.hAdd (β := 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)
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)
rw₃ : (x1 ^ p ^ n1) ^ p ^ n2 + HPow.hPow (α := L) ((i : (a : K) → L) y2 : L) (p ^ n1) = (x1 + x2) ^ p ^ (n1 + n2)
rw₄ : (x1 ^ p ^ n1) ^ p ^ n2 + (x2 ^ p ^ n2) ^ p ^ n1 = (x1 + x2) ^ p ^ (n1 + n2)
rw₅ : x1 ^ (p ^ n1 * p ^ n2) + (x2 ^ p ^ n2) ^ p ^ n1 = (x1 + x2) ^ p ^ (n1 + n2)
rw₆ : x1 ^ p ^ (n1 + n2) + (x2 ^ p ^ n2) ^ p ^ n1 = (x1 + x2) ^ p ^ (n1 + n2)
rw₇ : x1 ^ p ^ (n1 + n2) + x2 ^ (p ^ n2 * p ^ n1) = (x1 + x2) ^ p ^ (n1 + n2)
rw₈ : x1 ^ p ^ (n1 + n2) + x2 ^ p ^ (n2 + n1) = (x1 + x2) ^ p ^ (n1 + n2)
rw₉ : x1 ^ p ^ (n1 + n2) + x2 ^ p ^ (n1 + n2) = (x1 + x2) ^ p ^ (n1 + n2)
rw₁₀ rw₁₁ : x1 ^ p ^ (n1 + n2) + x2 ^ p ^ (n1 + n2) = x1 ^ p ^ (n1 + n2) + x2 ^ p ^ (n1 + n2)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 + y2 ^ p ^ n1) = (x1 + x2) ^ p ^ (n1 + n2)

Tactic:
rw [map_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_pow]

Premises used: add_pow_expChar_pow, pow_add, map_add, map_pow, add_comm, pow_mul