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
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)
⊢ (i : (a : K) → L) 0 = HPow.hPow (α := L) 0 (HPow.hPow (β := ℕ) p 0)
have rw₂ : Eq.{u_2 + 1} (α := L) 0 0
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
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 : 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)
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]
-- 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 :
  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)
⊢ (i : (a : K) → L) (y1 ^ p ^ n2 + y2 ^ p ^ n1) = (x1 + x2) ^ p ^ (n1 + n2)
have 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)
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]
-- 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 :
  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)
⊢ (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_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_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 :
  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)
⊢ (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_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_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 :
  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)
⊢ (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_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_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 :
  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)
⊢ (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_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_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 :
  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)
⊢ (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_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_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 :
  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)
⊢ (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_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_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 :
  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)
⊢ (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_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_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 :
  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)
⊢ (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_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_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 :
  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)
⊢ (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_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_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 : HAdd.hAdd (α := 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) =
  HAdd.hAdd (α := 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_add,
        map_pow, map_pow, h1, h2, ← pow_mul, ← pow_add, ← pow_mul, ← pow_add,
        add_comm n2, add_pow_expChar_pow]),
      map_add, map_pow, map_pow, map_add, ← 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
⊢ HAdd.hAdd (α := 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) =
    HAdd.hAdd (α := 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 : HAdd.hAdd (α := 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) =
  HAdd.hAdd (α := 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
⊢ HAdd.hAdd (α := 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) =
    HAdd.hAdd (α := 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 : HAdd.hAdd (α := 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) =
  HAdd.hAdd (α := 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]