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 :
  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)
⊢ 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 (n2 + n1)) : (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]
-- 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 (α := 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)
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 (n2 + n1)) : (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)
⊢ 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 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) =
  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]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
x : K
⊢ (i : (a : K) → L) x = HPow.hPow (α := L) ((i : (a : K) → L) x : L) (HPow.hPow (β := ℕ) p 0)
have rw : (i : (a : K) → L) x = HPow.hPow (α := L) (β := ℕ) ((i : (a : K) → L) x : L) 1
Tactic: rw [pow_zero, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
x : K
rw : (i : (a : K) → L) x = HPow.hPow (α := L) (β := ℕ) ((i : (a : K) → L) x : L) 1
⊢ (i : (a : K) → L) x = HPow.hPow (α := L) ((i : (a : K) → L) x : L) (HPow.hPow (β := ℕ) p 0)
have rw₁ : Eq.{u_2 + 1} (α := L) ((i : (a : K) → L) x : L) ((i : (a : K) → L) x : L)
Tactic: rw [pow_zero, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
x : K
⊢ Eq.{u_3 + 1} (α := M) ((lift i j p : (a : L) → M) ((i : (a : K) → L) x : L) : M) ((j : (a : K) → M) x : M)
have rw : Eq (α := M) ((RingEquiv.symm (RingEquiv.refl M) : (a : M) → M) ((j : (a : K) → M) x : M) : M) ((j : (a : K) → M) x : M)
Tactic: rw [lift_apply i j p _ 0 x (by rw [pow_zero, pow_one]), iterateFrobeniusEquiv_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
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
inst_9 : ExpChar N p
inst_10 : PerfectRing N p
inst_11 : IsPRadical j p
⊢ Eq (α := K →+* N) ((fun (f : L →+* N) ↦ f.comp i) ((lift j k p).comp (lift i j p)))
    ((fun (f : L →+* N) ↦ f.comp i) (lift i k p))
have a : ∀ (x : K),
  Eq.{u_4 + 1} (α := N) (((fun (f : L →+* N) ↦ f.comp i) ((lift j k p).comp (lift i j p)) : (a : K) → N) x : N)
    (((fun (f : L →+* N) ↦ f.comp i) (lift i k p) : (a : K) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
inst_8 : IsPRadical j p
inst_9 : PerfectRing L p
x : L
⊢ (lift j i p : (a : M) → L) ((lift i j p : (a : L) → M) x : M) = x
have rw : (lift i i p : (a : L) → L) x = x
Tactic: rw [lift_comp_lift_apply, lift_self_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : PerfectRing M p
inst_6 : IsPRadical i p
inst_7 : ExpChar L p
inst_8 : IsPRadical j p
inst_9 : PerfectRing L p
x : L
rw : (lift i i p : (a : L) → L) x = x
⊢ (lift j i p : (a : M) → L) ((lift i j p : (a : L) → M) x : M) = x
have rw₁ : x = x
Tactic: rw [lift_comp_lift_apply, lift_self_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
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
inst_9 : ExpChar N p
inst_10 : IsPRadical g p
inst_11 : IsPRadical (g.comp i) p
⊢ lift g (lift i j p) p = lift (g.comp i) j p
have refine : Eq (α := K →+* M) ((fun (f : N →+* M) ↦ f.comp (g.comp i)) (lift g (lift i j p) p))
  ((fun (f : N →+* M) ↦ f.comp (g.comp i)) (lift (g.comp i) j p))
Tactic: refine IsPRadical.injective_comp_of_perfect _ (g.comp i) p ?_
-- 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
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
inst_9 : ExpChar N p
inst_10 : IsPRadical g p
inst_11 : IsPRadical (g.comp i) p
simp_rw simp_rw₁ : (lift g (lift i j p) p).comp (g.comp i) = (lift (g.comp i) j p).comp (g.comp i)
⊢ Eq (α := K →+* M) ((fun (f : N →+* M) ↦ f.comp (g.comp i)) (lift g (lift i j p) p))
    ((fun (f : N →+* M) ↦ f.comp (g.comp i)) (lift (g.comp i) j p))
have simp_rw₂ : ((lift g (lift i j p) p).comp g).comp i = (lift (g.comp i) j p).comp (g.comp i)
Tactic: simp_rw [← RingHom.comp_assoc _ _ (lift g _ p), lift_comp]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
x : M
n : ℕ
y : K
h : (j : (a : K) → M) y = x ^ p ^ n
⊢ Eq.{u_2 + 1} (α := L) (((equiv i j p).symm : (a : M) → L) x : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) y : L) : L)
have rw : Eq.{u_2 + 1} (α := L) ((equiv j i p : (a : M) → L) x : L)
  ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) y : L) : L)
Tactic: rw [equiv_symm, equiv_apply j i p _ _ _ h]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
x : M
n : ℕ
y : K
h : (j : (a : K) → M) y = x ^ p ^ n
rw :
  Eq.{u_2 + 1} (α := L) ((equiv j i p : (a : M) → L) x : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) y : L) : L)
⊢ Eq.{u_2 + 1} (α := L) (((equiv i j p).symm : (a : M) → L) x : L)
    ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) y : L) : L)
have rw₁ : Eq (α := L) ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) y : L) : L)
  ((RingEquiv.symm (iterateFrobeniusEquiv L p n) : (a : L) → L) ((i : (a : K) → L) y : L) : L)
Tactic: rw [equiv_symm, equiv_apply j i p _ _ _ h]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
x : L
⊢ (equiv j i p : (a : M) → L) ((equiv i j p : (a : L) → M) x : M) = x
have rw : (equiv i i p : (a : L) → L) x = x
Tactic: rw [equiv_comp_equiv_apply, equiv_self_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing K
inst_1 : CommRing L
inst_2 : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst_3 : ExpChar M p
inst_4 : ExpChar K p
inst_5 : ExpChar L p
inst_6 : PerfectRing L p
inst_7 : IsPerfectClosure i p
inst_8 : PerfectRing M p
inst_9 : IsPerfectClosure j p
x : L
rw : (equiv i i p : (a : L) → L) x = x
⊢ (equiv j i p : (a : M) → L) ((equiv i j p : (a : L) → M) x : M) = x
have rw₁ : x = x
Tactic: rw [equiv_comp_equiv_apply, equiv_self_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
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
⊢ (of K p : (a : K) → PerfectClosure K p) x.2 = HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ x.1)
have rw : Eq (α := PerfectClosure K p) ((of K p : (a : K) → PerfectClosure K p) x.2 : PerfectClosure K p)
  ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[x.1] (mk K p x) :
    PerfectClosure K p)
Tactic: rw [← iterate_frobenius, iterate_frobenius_mk K p x.1 x.2]
-- 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
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x_1 : PerfectClosure K p
x : ℕ × K
rw :
  Eq (α := PerfectClosure K p) ((of K p : (a : K) → PerfectClosure K p) x.2 : PerfectClosure K p)
    ((⇑(frobenius (PerfectClosure K p) p) : (a : PerfectClosure K p) → PerfectClosure K p)^[x.1] (mk K p x) :
      PerfectClosure K p)
⊢ (of K p : (a : K) → PerfectClosure K p) x.2 = HPow.hPow (α := PerfectClosure K p) (mk K p x) (p ^ x.1)
have rw₁ : Eq (α := PerfectClosure K p) ((of K p : (a : K) → PerfectClosure K p) x.2 : PerfectClosure K p)
  ((of K p : (a : K) → PerfectClosure K p) x.2 : PerfectClosure K p)
Tactic: rw [← iterate_frobenius, iterate_frobenius_mk K p x.1 x.2]
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (hypothesis)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
h : Membership.mem (γ := Submodule K K) (RingHom.ker (F := K →+* PerfectClosure K p) (of K p)) x
⊢ Membership.mem (γ := Submodule K K) (pNilradical K p) x
have h₁ : ∃ (z : ℕ),
  (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1 + z] (0, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(0, x).1 + z] (0, 0).2
Tactic: rw [RingHom.mem_ker, of_apply, zero_def, mk_eq_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (goal)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
h :
  ∃ (z : ℕ),
    (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1 + z] (0, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(0, x).1 + z] (0, 0).2
⊢ Membership.mem (γ := Submodule K K) (pNilradical K p) x
have obtain : ∀ (n : ℕ)
  (h :
    (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1 + n] (0, x).2 =
      (⇑(frobenius K p) : (a : K) → K)^[(0, x).1 + n] (0, 0).2),
  Membership.mem (γ := Submodule K K) (pNilradical K p) x
Tactic: obtain ⟨n, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsPerfectClosure (hypothesis)
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing K
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP K p
x : K
n : ℕ
h : (⇑(frobenius K p) : (a : K) → K)^[(0, 0).1 + n] (0, x).2 = (⇑(frobenius K p) : (a : K) → K)^[(0, x).1 + n] (0, 0).2
⊢ Membership.mem (γ := Submodule K K) (pNilradical K p) x
have h₁ : Eq (α := K) ((iterateFrobenius K p n : (a : K) → K) x : K) (0 : K)
Tactic: simp_rw [zero_add, ← coe_iterateFrobenius, map_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x
exists_isRoot_of_odd_natDegree : ∀ {f : R[X]}, Odd f.natDegree → ∃ (x : R), f.IsRoot x
x : R
⊢ IsSquare x ∨ IsSquare (-x)
have inl : ∀ (neg : x ≤ 0), IsSquare x ∨ IsSquare (-x)
Tactic: rcases le_total x 0 with (neg | pos)
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
isSquare_of_nonneg : ∀ {x : R}, 0 ≤ x → IsSquare x
exists_isRoot_of_odd_natDegree : ∀ {f : R[X]}, Odd f.natDegree → ∃ (x : R), f.IsRoot x
x : R
inl : ∀ (neg : x ≤ 0), IsSquare x ∨ IsSquare (-x)
⊢ IsSquare x ∨ IsSquare (-x)
have inr : ∀ (pos : 0 ≤ x), IsSquare x ∨ IsSquare (-x)
Tactic: rcases le_total x 0 with (neg | pos)
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hn : Odd n
⊢ ∃ (r : R), x = r ^ n
have rcases : ∀ (r : R) (hr : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])).IsRoot r),
  ∃ (r : R), x = r ^ n
Tactic: rcases exists_isRoot_of_odd_natDegree (f := X ^ n - C x) (by simp [hn]) with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])).IsRoot r
⊢ x = r ^ n
have linear_combination : r ^ n - x = 0
Tactic: linear_combination - (by simpa using hr : r ^ n - x = 0)
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
k : ℤ
hk : Odd k
⊢ ∃ (r : R), x = r ^ k
have inl : ∀ (n : ℕ) (hk : Odd (α := ℤ) (↑n : ℤ)), ∃ (r : R), x = HPow.hPow (β := ℤ) r (↑n : ℤ)
Tactic: rcases k.eq_nat_or_neg with ⟨n, rfl | rfl⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
k : ℤ
hk : Odd k
inl : ∀ (n : ℕ) (hk : Odd (α := ℤ) (↑n : ℤ)), ∃ (r : R), x = HPow.hPow (β := ℤ) r (↑n : ℤ)
⊢ ∃ (r : R), x = r ^ k
have inr : ∀ (n : ℕ) (hk : Odd (α := ℤ) (-(↑n : ℤ))), ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))
Tactic: rcases k.eq_nat_or_neg with ⟨n, rfl | rfl⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
n : ℕ
hk : Odd (α := ℤ) (-(↑n : ℤ))
⊢ ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))
have inr : ∀ (r : R) (hr : x = r ^ n), ∃ (r : R), x = HPow.hPow (β := ℤ) r (-(↑n : ℤ))
Tactic: rcases exists_eq_pow_of_odd x (by simpa using hk) with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
⊢ ∃ (r : R), x = r ^ n
have h : ∀ (even : Even n), ∃ (r : R), x = r ^ n
Tactic: rcases Nat.even_or_odd n with (even | odd)
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
h : ∀ (even : Even n), ∃ (r : R), x = r ^ n
⊢ ∃ (r : R), x = r ^ n
have h₁ : ∀ (odd : Odd n), ∃ (r : R), x = r ^ n
Tactic: rcases Nat.even_or_odd n with (even | odd)
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
even : Even n
⊢ ∃ (r : R), x = r ^ n
have h : ∀ (m : ℕ) (hm : n = m + m), ∃ (r : R), x = r ^ n
Tactic: rcases even with ⟨m, hm⟩
Cleared hypotheses: even
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hx : IsSquare x
hn : n ≠ 0
m : ℕ
hm : n = m + m
⊢ ∃ (r : R), x = r ^ n
have h : ∀ (s : R) (hs : x = s * s), ∃ (r : R), x = r ^ n
Tactic: rcases hx with ⟨s, hs⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
⊢ ∃ (r : R), x = r ^ n
have h : ∀ (h : IsSquare s), ∃ (r : R), x = r ^ n
Tactic: rcases isSquare_or_isSquare_neg s with (h | h)
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : ∀ (h : IsSquare s), ∃ (r : R), x = r ^ n
⊢ ∃ (r : R), x = r ^ n
have h₁ : ∀ (h : IsSquare (-s)), ∃ (r : R), x = r ^ n
Tactic: rcases isSquare_or_isSquare_neg s with (h | h)
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare s
⊢ ∃ (r : R), x = r ^ n
have h₁ : ∀ (r : R) (hr : s = r ^ m), ∃ (r : R), x = r ^ n
Tactic: rcases ih m (by lia) h (by lia) with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
n : ℕ
ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m
x : R
hn : n ≠ 0
m : ℕ
hm : n = m + m
s : R
hs : x = s * s
h : IsSquare (-s)
⊢ ∃ (r : R), x = r ^ n
have h₁ : ∀ (r : R) (hr : -s = r ^ m), ∃ (r : R), x = r ^ n
Tactic: rcases ih m (by lia) h (by lia) with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hn : n ≠ 0
⊢ ∃ (r : R), x = r ^ n
have h : ∀ (n : ℕ) (ih : ∀ m < n, ∀ {x : R} (hx : IsSquare x) (hn : m ≠ 0), ∃ (r : R), x = r ^ m) {x : R} (hx : IsSquare x)
  (hn : n ≠ 0), ∃ (r : R), x = r ^ n
Tactic: induction n using Nat.strong_induction_on generalizing x with
  | h n ih =>
    rcases Nat.even_or_odd n with (even | odd)
    · rcases even with ⟨m, hm⟩
      rcases hx with ⟨s, hs⟩
      rcases isSquare_or_isSquare_neg s with (h | h) <;>
        rcases ih m (by lia) h (by lia) with ⟨r, hr⟩ <;>
        exact ⟨r, by simp [hm, pow_add, ← hr, hs]⟩
    · exact exists_eq_pow_of_odd x odd
Cleared hypotheses: x, hx, n, hn
-- Lean 4 proof step from Mathlib.FieldTheory.IsRealClosed.Basic (goal)
Goal:
R : Type u
inst : Field R
inst_1 : IsRealClosed R
x : R
hx : IsSquare x
k : ℤ
hk : k ≠ 0
⊢ ∃ (r : R), x = r ^ k
have inl : ∀ (n : ℕ) (hk : Ne (α := ℤ) (↑n : ℤ) 0), ∃ (r : R), x = HPow.hPow (β := ℤ) r (↑n : ℤ)
Tactic: rcases k.eq_nat_or_neg with ⟨n, rfl | rfl⟩
Cleared hypotheses: k, hk