awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp_1 : ¬1 < p
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 1
neg : ∀ (h : x ^ HPow.hPow (α := ℕ) 1 n = 0) (hp : p = 1), x = 0
⊢ x = 0
have neg₁ : ∀ (h : HPow.hPow (β := ℕ) x 1 = 0) (hp : p = 1), x = 0
Tactic: rwa [hp, one_pow, pow_one] at h
Cleared hypotheses: h, hp
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
x : R
hp_1 : ¬1 < p
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h : x ^ p ^ n = 0
hp : p = 1
neg : ∀ (h : x ^ HPow.hPow (α := ℕ) 1 n = 0) (hp : p = 1), x = 0
neg₁ : ∀ (h : HPow.hPow (β := ℕ) x 1 = 0) (hp : p = 1), x = 0
⊢ x = 0
have neg₂ : ∀ (h : x = 0) (hp : p = 1), x = 0
Tactic: rwa [hp, one_pow, pow_one] at h
Cleared hypotheses: h, hp
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : ExpChar R p
x y : R
⊢ Membership.mem (γ := Ideal R) (pNilradical R p) (x - y) ↔ ∃ (n : ℕ), x ^ p ^ n = y ^ p ^ n
have simp_rw : (∃ (n : ℕ), (x - y) ^ p ^ n = 0) ↔ ∃ (n : ℕ), x ^ p ^ n = y ^ p ^ n
Tactic: simp_rw [mem_pNilradical, sub_pow_expChar_pow, sub_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
inst_1 : ExpChar R p
x y : R
simp_rw : (∃ (n : ℕ), (x - y) ^ p ^ n = 0) ↔ ∃ (n : ℕ), x ^ p ^ n = y ^ p ^ n
⊢ Membership.mem (γ := Ideal R) (pNilradical R p) (x - y) ↔ ∃ (n : ℕ), x ^ p ^ n = y ^ p ^ n
have simp_rw₁ : (∃ (n : ℕ), x ^ p ^ n - y ^ p ^ n = 0) ↔ ∃ (n : ℕ), x ^ p ^ n = y ^ p ^ n
Tactic: simp_rw [mem_pNilradical, sub_pow_expChar_pow, sub_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
h : Function.Injective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
x : R
⊢ Membership.mem (γ := Submodule R R) (pNilradical R p) x → Membership.mem (γ := Submodule R R) ⊥ x
have rw : (∃ (n : ℕ), x ^ p ^ n = 0) → x = 0
Tactic: rw [mem_pNilradical, Ideal.mem_bot]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
h : Function.Injective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
x : R
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h_2 : x ^ p ^ n = 0
⊢ (⇑(frobenius R p) : (a : R) → R)^[n] x = (⇑(frobenius R p) : (a : R) → R)^[n] 0
have rwa : Eq (α := R) ((iterateFrobenius R p n : (a : R) → R) x : R) ((iterateFrobenius R p n : (a : R) → R) 0 : R)
Tactic: rwa [← coe_iterateFrobenius, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
h : Function.Injective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
x : R
h_1 : ∃ (n : ℕ), x ^ p ^ n = 0
n : ℕ
h_2 : x ^ p ^ n = 0
rwa : Eq (α := R) ((iterateFrobenius R p n : (a : R) → R) x : R) ((iterateFrobenius R p n : (a : R) → R) 0 : R)
⊢ (⇑(frobenius R p) : (a : R) → R)^[n] x = (⇑(frobenius R p) : (a : R) → R)^[n] 0
have rwa₁ : Eq (α := R) ((iterateFrobenius R p n : (a : R) → R) x : R) (0 : R)
Tactic: rwa [← coe_iterateFrobenius, map_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
⊢ Eq (α := Ideal K) (Ideal.comap i (pNilradical L p)) (pNilradical K p)
have refine_1 : ∀ (x : K) (h : Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x), ∃ (n : ℕ), x ^ p ^ n = 0
Tactic: refine le_antisymm (fun x h ↦ mem_pNilradical.2 ?_) (fun x h ↦ ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
refine_1 :
  ∀ (x : K) (h : Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x), ∃ (n : ℕ), x ^ p ^ n = 0
⊢ Eq (α := Ideal K) (Ideal.comap i (pNilradical L p)) (pNilradical K p)
have refine_2 : ∀ (x : K) (h : Membership.mem (γ := Submodule K K) (pNilradical K p) x),
  Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x
Tactic: refine le_antisymm (fun x h ↦ mem_pNilradical.2 ?_) (fun x h ↦ ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h : Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x
⊢ ∃ (n : ℕ), x ^ p ^ n = 0
have refine_1 : ∀ (n : ℕ) (h : HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0), ∃ (n : ℕ), x ^ p ^ n = 0
Tactic: obtain ⟨n, h⟩ := mem_pNilradical.1 <| Ideal.mem_comap.1 h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h_1 : Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x
n : ℕ
h : HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0
⊢ ∃ (n : ℕ), x ^ p ^ n = 0
have refine_1 : ∀ (m : ℕ) (h : (x ^ p ^ n) ^ p ^ m = 0), ∃ (n : ℕ), x ^ p ^ n = 0
Tactic: obtain ⟨m, h⟩ := mem_pNilradical.1 <| ker_le i p ((map_pow i x _).symm ▸ h)
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h_1 : Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x
n : ℕ
h_2 : HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0
m : ℕ
h : (x ^ p ^ n) ^ p ^ m = 0
⊢ x ^ p ^ (n + m) = 0
have rwa : x ^ (p ^ n * p ^ m) = 0
Tactic: rwa [pow_add, pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h : Membership.mem (γ := Submodule K K) (pNilradical K p) x
⊢ Membership.mem (γ := Submodule K K) (Ideal.comap i (pNilradical L p)) x
have refine_2 : ∀ (h : ∃ (n : ℕ), x ^ p ^ n = 0), ∃ (n : ℕ), HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0
Tactic: simp only [Ideal.mem_comap, mem_pNilradical] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : IsPRadical i p
x : K
h : ∃ (n : ℕ), x ^ p ^ n = 0
⊢ ∃ (n : ℕ), HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0
have refine_2 : ∀ (n : ℕ) (h : x ^ p ^ n = 0), ∃ (n : ℕ), HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n) = 0
Tactic: obtain ⟨n, h⟩ := 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 : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
⊢ ∃ (n : ℕ) (y : K), (f.comp i : (a : K) → M) y = x ^ p ^ n
have obtain : ∀ (n : ℕ) (y : L) (hy : (f : (a : L) → M) y = x ^ p ^ n), ∃ (n : ℕ) (y : K), (f.comp i : (a : K) → M) y = x ^ p ^ n
Tactic: obtain ⟨n, y, hy⟩ := pow_mem f p x
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
n : ℕ
y : L
hy : (f : (a : L) → M) y = x ^ p ^ n
⊢ ∃ (n : ℕ) (y : K), (f.comp i : (a : K) → M) y = x ^ p ^ n
have obtain : ∀ (m : ℕ) (z : K) (hz : (i : (a : K) → L) z = y ^ p ^ m), ∃ (n : ℕ) (y : K), (f.comp i : (a : K) → M) y = x ^ p ^ n
Tactic: obtain ⟨m, z, hz⟩ := pow_mem i p y
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
n : ℕ
y : L
hy : (f : (a : L) → M) y = x ^ p ^ n
m : ℕ
z : K
hz : (i : (a : K) → L) z = y ^ p ^ m
⊢ (f.comp i : (a : K) → M) z = x ^ p ^ (n + m)
have rw : (f : (a : L) → M) ((i : (a : K) → L) z : L) = x ^ p ^ (n + m)
Tactic: rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
n : ℕ
y : L
hy : (f : (a : L) → M) y = x ^ p ^ n
m : ℕ
z : K
hz : (i : (a : K) → L) z = y ^ p ^ m
rw : (f : (a : L) → M) ((i : (a : K) → L) z : L) = x ^ p ^ (n + m)
⊢ (f.comp i : (a : K) → M) z = x ^ p ^ (n + m)
have rw₁ : (f : (a : L) → M) (y ^ p ^ m) = x ^ p ^ (n + m)
Tactic: rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
n : ℕ
y : L
hy : (f : (a : L) → M) y = x ^ p ^ n
m : ℕ
z : K
hz : (i : (a : K) → L) z = y ^ p ^ m
rw : (f : (a : L) → M) ((i : (a : K) → L) z : L) = x ^ p ^ (n + m)
rw₁ : (f : (a : L) → M) (y ^ p ^ m) = x ^ p ^ (n + m)
⊢ (f.comp i : (a : K) → M) z = x ^ p ^ (n + m)
have rw₂ : HPow.hPow (α := M) ((f : (a : L) → M) y : M) (p ^ m) = x ^ p ^ (n + m)
Tactic: rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
n : ℕ
y : L
hy : (f : (a : L) → M) y = x ^ p ^ n
m : ℕ
z : K
hz : (i : (a : K) → L) z = y ^ p ^ m
rw : (f : (a : L) → M) ((i : (a : K) → L) z : L) = x ^ p ^ (n + m)
rw₁ : (f : (a : L) → M) (y ^ p ^ m) = x ^ p ^ (n + m)
rw₂ : HPow.hPow (α := M) ((f : (a : L) → M) y : M) (p ^ m) = x ^ p ^ (n + m)
⊢ (f.comp i : (a : K) → M) z = x ^ p ^ (n + m)
have rw₃ : (x ^ p ^ n) ^ p ^ m = x ^ p ^ (n + m)
Tactic: rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
n : ℕ
y : L
hy : (f : (a : L) → M) y = x ^ p ^ n
m : ℕ
z : K
hz : (i : (a : K) → L) z = y ^ p ^ m
rw : (f : (a : L) → M) ((i : (a : K) → L) z : L) = x ^ p ^ (n + m)
rw₁ : (f : (a : L) → M) (y ^ p ^ m) = x ^ p ^ (n + m)
rw₂ : HPow.hPow (α := M) ((f : (a : L) → M) y : M) (p ^ m) = x ^ p ^ (n + m)
rw₃ : (x ^ p ^ n) ^ p ^ m = x ^ p ^ (n + m)
⊢ (f.comp i : (a : K) → M) z = x ^ p ^ (n + m)
have rw₄ : (x ^ p ^ n) ^ p ^ m = x ^ (p ^ n * p ^ m)
Tactic: rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : M
n : ℕ
y : L
hy : (f : (a : L) → M) y = x ^ p ^ n
m : ℕ
z : K
hz : (i : (a : K) → L) z = y ^ p ^ m
rw : (f : (a : L) → M) ((i : (a : K) → L) z : L) = x ^ p ^ (n + m)
rw₁ : (f : (a : L) → M) (y ^ p ^ m) = x ^ p ^ (n + m)
rw₂ : HPow.hPow (α := M) ((f : (a : L) → M) y : M) (p ^ m) = x ^ p ^ (n + m)
rw₃ : (x ^ p ^ n) ^ p ^ m = x ^ p ^ (n + m)
rw₄ : (x ^ p ^ n) ^ p ^ m = x ^ (p ^ n * p ^ m)
⊢ (f.comp i : (a : K) → M) z = x ^ p ^ (n + m)
have rw₅ : (x ^ p ^ n) ^ p ^ m = (x ^ p ^ n) ^ p ^ m
Tactic: rw [RingHom.comp_apply, hz, map_pow, hy, pow_add, pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (hypothesis)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : CommSemiring M
i : K →+* L
f : L →+* M
p : ℕ
inst_3 : IsPRadical i p
inst_4 : IsPRadical f p
x : K
h : Membership.mem (γ := Submodule K K) (RingHom.ker (f.comp i)) x
⊢ Membership.mem (γ := Submodule K K) (pNilradical K p) x
have h₁ : Membership.mem (α := L) (γ := Ideal L) (RingHom.ker f) ((i : (a : K) → L) x : L)
Tactic: rw [RingHom.mem_ker, RingHom.comp_apply, ← 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
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h : Membership.mem (γ := Submodule K K) (pNilradical K p) x
⊢ Membership.mem (γ := Submodule K K) (ker i) x
have obtain : ∀ (n : ℕ) (h : x ^ p ^ n = 0), Membership.mem (γ := Submodule K K) (ker i) x
Tactic: obtain ⟨n, h⟩ := mem_pNilradical.1 h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h_1 : Membership.mem (γ := Submodule K K) (pNilradical K p) x
n : ℕ
h : x ^ p ^ n = 0
⊢ Membership.mem (γ := Submodule K K) (ker i) x
have h₁ : Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) (x ^ p ^ n) : L) : L)
  ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)
Tactic: replace h := congr((iterateFrobeniusEquiv L p n).symm (i $h))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h_1 : Membership.mem (γ := Submodule K K) (pNilradical K p) x
n : ℕ
h :
  Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) (x ^ p ^ n) : L) : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)
⊢ Membership.mem (γ := Submodule K K) (ker i) x
have rwa : ∀
  (h :
    Eq (α := L)
      ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
          (HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n)) :
        L)
      ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
  Membership.mem (γ := Submodule K K) (ker i) x
Tactic: rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply,
    map_zero, map_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h_1 : Membership.mem (γ := Submodule K K) (pNilradical K p) x
n : ℕ
h :
  Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) (x ^ p ^ n) : L) : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)
rwa :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            (HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n)) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
⊢ Membership.mem (γ := Submodule K K) (ker i) x
have rwa₁ : ∀
  (h :
    Eq (α := L)
      ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
          ((iterateFrobenius L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
        L)
      ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
  Membership.mem (γ := Submodule K K) (ker i) x
Tactic: rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply,
    map_zero, map_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h_1 : Membership.mem (γ := Submodule K K) (pNilradical K p) x
n : ℕ
h :
  Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) (x ^ p ^ n) : L) : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)
rwa :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            (HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n)) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₁ :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            ((iterateFrobenius L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
⊢ Membership.mem (γ := Submodule K K) (ker i) x
have rwa₂ : ∀
  (h :
    Eq (α := L)
      ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
          ((iterateFrobeniusEquiv L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
        L)
      ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
  Membership.mem (γ := Submodule K K) (ker i) x
Tactic: rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply,
    map_zero, map_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h_1 : Membership.mem (γ := Submodule K K) (pNilradical K p) x
n : ℕ
h :
  Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) (x ^ p ^ n) : L) : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)
rwa :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            (HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n)) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₁ :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            ((iterateFrobenius L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₂ :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            ((iterateFrobeniusEquiv L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
⊢ Membership.mem (γ := Submodule K K) (ker i) x
have rwa₃ : ∀
  (h :
    Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L)
      ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
  Membership.mem (γ := Submodule K K) (ker i) x
Tactic: rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply,
    map_zero, map_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h_1 : Membership.mem (γ := Submodule K K) (pNilradical K p) x
n : ℕ
h :
  Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) (x ^ p ^ n) : L) : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)
rwa :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            (HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n)) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₁ :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            ((iterateFrobenius L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₂ :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            ((iterateFrobeniusEquiv L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₃ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
⊢ Membership.mem (γ := Submodule K K) (ker i) x
have rwa₄ : ∀
  (h :
    Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L)
      ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) 0 : L)),
  Membership.mem (γ := Submodule K K) (ker i) x
Tactic: rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply,
    map_zero, map_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
i : K →+* L
p : ℕ
inst_2 : ExpChar L p
inst_3 : PerfectRing L p
x : K
h_1 : Membership.mem (γ := Submodule K K) (pNilradical K p) x
n : ℕ
h :
  Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) (x ^ p ^ n) : L) : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)
rwa :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            (HPow.hPow (α := L) ((i : (a : K) → L) x : L) (p ^ n)) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₁ :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            ((iterateFrobenius L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₂ :
  ∀
    (h :
      Eq (α := L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L)
            ((iterateFrobeniusEquiv L p n : (a : L) → L) ((i : (a : K) → L) x : L) : L) :
          L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₃ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) 0 : L) : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
rwa₄ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L)
        ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) 0 : L)),
    Membership.mem (γ := Submodule K K) (ker i) x
⊢ Membership.mem (γ := Submodule K K) (ker i) x
have rwa₅ : ∀ (h : Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L) (0 : L)), Membership.mem (γ := Submodule K K) (ker i) x
Tactic: rwa [map_pow, ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply, RingEquiv.symm_apply_apply,
    map_zero, map_zero] at h
Cleared hypotheses: h