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
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)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw₃ : (x1 ^ p ^ n1) ^ 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]
-- 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)
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)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw₄ : (x1 ^ p ^ n1) ^ p ^ n2 * (x2 ^ p ^ n2) ^ 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]
-- 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)
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)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw₅ : x1 ^ (p ^ n1 * p ^ n2) * (x2 ^ p ^ n2) ^ 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]
-- 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)
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)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw₆ : x1 ^ p ^ (n1 + n2) * (x2 ^ p ^ n2) ^ 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]
-- 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)
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)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw₇ : x1 ^ p ^ (n1 + n2) * x2 ^ (p ^ n2 * 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]
-- 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)
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)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw₈ : x1 ^ p ^ (n1 + n2) * x2 ^ p ^ (n2 + 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]
-- 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)
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)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw₉ : x1 ^ p ^ (n1 + n2) * x2 ^ p ^ (n1 + n2) = (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)
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)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 * y2 ^ p ^ n1) = (x1 * x2) ^ p ^ (n1 + n2)
have rw₁₀ : x1 ^ p ^ (n1 + n2) * x2 ^ p ^ (n1 + n2) = x1 ^ p ^ (n1 + n2) * 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
⊢ liftAux i j p (x1 * x2) = liftAux i j p x1 * liftAux i j p x2
have 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)
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]
-- 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
⊢ 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)
have 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)
Tactic: nth_rw 1 [iterateFrobeniusEquiv_symm_add_apply]
-- 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
⊢ 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)
have rw : 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 (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: rw [RingEquiv.symm_apply_apply, add_comm n1, iterateFrobeniusEquiv_symm_add_apply,
      ← iterateFrobeniusEquiv_def, 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
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) : (a : M) → M) ((j : (a : K) → M) y1 : 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) : (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)
have rw₁ : 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 + n1)) : (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: rw [RingEquiv.symm_apply_apply, add_comm n1, iterateFrobeniusEquiv_symm_add_apply,
      ← iterateFrobeniusEquiv_def, 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
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) : (a : M) → M) ((j : (a : K) → M) y1 : 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)
rw₁ :
  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 + n1)) : (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) : (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)
have rw₂ : 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)
        ((RingEquiv.symm (iterateFrobeniusEquiv M p n1) : (a : M) → M)
            (HPow.hPow (α := M) ((j : (a : K) → M) y2 : M) (p ^ n1)) :
          M) :
      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: rw [RingEquiv.symm_apply_apply, add_comm n1, iterateFrobeniusEquiv_symm_add_apply,
      ← iterateFrobeniusEquiv_def, 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
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) 0 = HPow.hPow (α := L) 0 (HPow.hPow (β := ℕ) p 0)
have rw : (i : (a : K) → L) 0 = HPow.hPow (α := L) (β := ℕ) 0 1
Tactic: rw [pow_zero, pow_one, 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
rw : (i : (a : K) → L) 0 = HPow.hPow (α := L) (β := ℕ) 0 1
⊢ (i : (a : K) → L) 0 = HPow.hPow (α := L) 0 (HPow.hPow (β := ℕ) p 0)
have rw₁ : Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) 0 : L) (0 : L)
Tactic: rw [pow_zero, pow_one, map_zero]