awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : MonoidHom.{u_2, u_3} M (Perfection N p)
⊢ (fun (f : M →* N) ↦
        ({
            toFun := fun (r : M) ↦
              Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                (fun (n : ℕ) ↦ (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M)) ⋯,
            map_one' := ⋯, map_mul' := ⋯ } :
          MonoidHom.{u_2, u_3} M (Perfection N p)))
      (MonoidHom.comp (coeffMonoidHom N p 0) f) =
    f
have h : ∀ (m : M) (n : ℕ),
  Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        ((((fun (f : M →* N) ↦
                    ({
                        toFun := fun (r : M) ↦
                          Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                            (fun (n : ℕ) ↦
                              (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M))
                            sorry,
                        map_one' := sorry, map_mul' := sorry } :
                      MonoidHom.{u_2, u_3} M (Perfection N p)))
                  (MonoidHom.comp (coeffMonoidHom N p 0) f) :
                MonoidHom.{u_2, u_3} M (Perfection N p)) :
              (a : M) → Perfection N p)
            m :
          Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
Tactic: ext m n
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : MonoidHom.{u_2, u_3} M (Perfection N p)
m : M
n : ℕ
⊢ Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        ((((fun (f : M →* N) ↦
                    ({
                        toFun := fun (r : M) ↦
                          Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                            (fun (n : ℕ) ↦
                              (f : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M))
                            ⋯,
                        map_one' := ⋯, map_mul' := ⋯ } :
                      MonoidHom.{u_2, u_3} M (Perfection N p)))
                  (MonoidHom.comp (coeffMonoidHom N p 0) f) :
                MonoidHom.{u_2, u_3} M (Perfection N p)) :
              (a : M) → Perfection N p)
            m :
          Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
have h : Eq (α := N)
  ((coeffMonoidHom N p 0 : (a : Perfection N p) → N)
      ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p) :
    N)
  ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
Tactic: simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.coe_mk, OneHom.coe_mk,
      coeffMonoidHom_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : MonoidHom.{u_2, u_3} M (Perfection N p)
m : M
n : ℕ
⊢ Eq (α := N)
    ((coeffMonoidHom N p 0 : (a : Perfection N p) → N)
        ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
have h : Eq (α := N)
  ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N)
      (HPow.hPow (α := Perfection N p)
        ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p)
        (p ^ n)) :
    N)
  ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
Tactic: rw [← coeffMonoidHom_pow_p_pow _ 0 n, ← map_pow, powMulEquiv_symm_pow_p, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : MonoidHom.{u_2, u_3} M (Perfection N p)
m : M
n : ℕ
h :
  Eq (α := N)
    ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N)
        (HPow.hPow (α := Perfection N p)
          ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p)
          (p ^ n)) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
⊢ Eq (α := N)
    ((coeffMonoidHom N p 0 : (a : Perfection N p) → N)
        ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
have h₁ : Eq (α := N)
  ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N)
      ((f : (a : M) → Perfection N p)
          (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m : M) (p ^ n)) :
        Perfection N p) :
    N)
  ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
Tactic: rw [← coeffMonoidHom_pow_p_pow _ 0 n, ← map_pow, powMulEquiv_symm_pow_p, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : MonoidHom.{u_2, u_3} M (Perfection N p)
m : M
n : ℕ
h :
  Eq (α := N)
    ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N)
        (HPow.hPow (α := Perfection N p)
          ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p)
          (p ^ n)) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
h₁ :
  Eq (α := N)
    ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N)
        ((f : (a : M) → Perfection N p)
            (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m : M) (p ^ n)) :
          Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
⊢ Eq (α := N)
    ((coeffMonoidHom N p 0 : (a : Perfection N p) → N)
        ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
have h₂ : Eq (α := N)
  ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
  ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
Tactic: rw [← coeffMonoidHom_pow_p_pow _ 0 n, ← map_pow, powMulEquiv_symm_pow_p, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
f : MonoidHom.{u_2, u_3} M (Perfection N p)
m : M
n : ℕ
h :
  Eq (α := N)
    ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N)
        (HPow.hPow (α := Perfection N p)
          ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p)
          (p ^ n)) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
h₁ :
  Eq (α := N)
    ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N)
        ((f : (a : M) → Perfection N p)
            (HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m : M) (p ^ n)) :
          Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
h₂ :
  Eq (α := N)
    ((coeffMonoidHom N p (0 + n) : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
⊢ Eq (α := N)
    ((coeffMonoidHom N p 0 : (a : Perfection N p) → N)
        ((f : (a : M) → Perfection N p) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) m) : Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
have h₃ : Eq (α := N) ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
  ((coeffMonoidHom N p n : (a : Perfection N p) → N) ((f : (a : M) → Perfection N p) m : Perfection N p) : N)
Tactic: rw [← coeffMonoidHom_pow_p_pow _ 0 n, ← map_pow, powMulEquiv_symm_pow_p, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
inst_1 : CommMonoid M
inst_2 : PerfectRing M p
N : Type u_3
inst_3 : CommMonoid N
x x_1 : M →* N
⊢ {
      toFun := fun (r : M) ↦
        Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
          (fun (n : ℕ) ↦ (x * x_1 : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M)) ⋯,
      map_one' := ⋯, map_mul' := ⋯ } =
    HMul.hMul (α := MonoidHom.{u_2, u_3} M (Perfection N p))
      {
        toFun := fun (r : M) ↦
          Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (x : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M)) ⋯,
        map_one' := ⋯, map_mul' := ⋯ : MonoidHom.{u_2, u_3} M (Perfection N p) }
      {
        toFun := fun (r : M) ↦
          Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (x_1 : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M)) ⋯,
        map_one' := ⋯, map_mul' := ⋯ : MonoidHom.{u_2, u_3} M (Perfection N p) }
have h : ∀ (x_2 : M) (n : ℕ),
  Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        (({
                toFun := fun (r : M) ↦
                  Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                    (fun (n : ℕ) ↦
                      (x * x_1 : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M))
                    sorry,
                map_one' := sorry, map_mul' := sorry } :
              (a : M) → Perfection N p)
            x_2 :
          Perfection N p) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        ((HMul.hMul (α := MonoidHom.{u_2, u_3} M (Perfection N p))
                {
                  toFun := fun (r : M) ↦
                    Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                      (fun (n : ℕ) ↦ (x : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M)) sorry,
                  map_one' := sorry, map_mul' := sorry : MonoidHom.{u_2, u_3} M (Perfection N p) }
                {
                  toFun := fun (r : M) ↦
                    Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
                      (fun (n : ℕ) ↦ (x_1 : (a : M) → N) ((MulEquiv.symm (powMulEquiv M (p ^ n)) : (a : M) → M) r : M))
                      sorry,
                  map_one' := sorry, map_mul' := sorry : MonoidHom.{u_2, u_3} M (Perfection N p) } :
              (a : M) → Perfection N p)
            x_2 :
          Perfection N p) :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
N : Type u_3
inst_1 : CommMonoid M
inst_2 : CommMonoid N
φ : M →* N
f : Perfection M p
n : ℕ
⊢ HPow.hPow (α := N)
      ((fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) (n + 1)) p =
    (fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) n
have rw : Eq.{u_3 + 1} (α := N)
  ((φ : (a : M) → N) (HPow.hPow (α := M) ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M) p) : N)
  ((fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) n : N)
Tactic: rw [← map_pow, coeffMonoidHom_pow_p']
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
N : Type u_3
inst_1 : CommMonoid M
inst_2 : CommMonoid N
φ : M →* N
f : Perfection M p
n : ℕ
rw :
  Eq.{u_3 + 1} (α := N)
    ((φ : (a : M) → N) (HPow.hPow (α := M) ((coeffMonoidHom M p (n + 1) : (a : Perfection M p) → M) f : M) p) : N)
    ((fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) n : N)
⊢ HPow.hPow (α := N)
      ((fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) (n + 1)) p =
    (fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) n
have rw₁ : Eq.{u_3 + 1} (α := N) ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)
  ((fun (n : ℕ) ↦ ((φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) f : M) : N)) n : N)
Tactic: rw [← map_pow, coeffMonoidHom_pow_p']
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
N : Type u_3
inst_1 : CommMonoid M
inst_2 : CommMonoid N
φ : M →* N
⊢ Eq.{u_3 + 1} (α := Perfection N p)
    (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
      (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) 1 : M)) ⋯)
    1
have h : ∀ (n : ℕ),
  Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
          (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) 1 : M)) sorry) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N) 1 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
M_1 : Type u_1
inst : CommMonoid M_1
p_1 p : ℕ
M : Type u_2
N : Type u_3
inst_1 : CommMonoid M
inst_2 : CommMonoid N
φ : M →* N
x x_1 : Perfection M p
⊢ Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
      (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) (x * x_1) : M)) ⋯ =
    HMul.hMul (α := Perfection N p)
      (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
        (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)) ⋯)
      (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
        (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x_1 : M)) ⋯)
have h : ∀ (n : ℕ),
  Eq (α := N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
          (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) (x * x_1) : M)) sorry) :
      N)
    ((coeffMonoidHom N p n : (a : Perfection N p) → N)
        (HMul.hMul (α := Perfection N p)
          (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x : M)) sorry)
          (Subtype.mk (p := fun (f : ℕ → N) ↦ ∀ (n : ℕ), f (n + 1) ^ p = f n)
            (fun (n : ℕ) ↦ (φ : (a : M) → N) ((coeffMonoidHom M p n : (a : Perfection M p) → M) x_1 : M)) sorry)) :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ Eq (α := Perfection R p →+* Perfection R p) (pthRoot R p)
    (↑(RingEquiv.symm (frobeniusEquiv (Perfection R p) p)) : Perfection R p →+* Perfection R p)
have a : ∀ (x : Perfection R p),
  Eq (α := Perfection R p) ((pthRoot R p : (a : Perfection R p) → Perfection R p) x : Perfection R p)
    (((↑(RingEquiv.symm (frobeniusEquiv (Perfection R p) p)) : Perfection R p →+* Perfection R p) :
          (a : Perfection R p) → Perfection R p)
        x :
      Perfection R p)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ Eq (α := Perfection R p →+* Perfection R p) (RingHom.comp (pthRoot R p) (frobenius (Perfection R p) p))
    (RingHom.id (Perfection R p))
have a : ∀ (x : Perfection R p) (n : ℕ),
  Eq (α := R)
    ((coeff R p n : (a : Perfection R p) → R)
        ((RingHom.comp (pthRoot R p) (frobenius (Perfection R p) p) : (a : Perfection R p) → Perfection R p) x :
          Perfection R p) :
      R)
    ((coeff R p n : (a : Perfection R p) → R)
        ((RingHom.id (Perfection R p) : (a : Perfection R p) → Perfection R p) x : Perfection R p) :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
hfn : Ne (α := R) ((coeff R p n : (a : Perfection R p) → R) f : R) (0 : R)
k_1 k : ℕ
ih : Ne (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
h : Eq (α := R) ((coeff R p (n + k.succ) : (a : Perfection R p) → R) f : R) (0 : R)
⊢ Eq (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
have h₁ : Eq (α := R) ((coeff R p (n + k).succ : (a : Perfection R p) → R) f : R) (0 : R)
Tactic: rw [Nat.add_succ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
hfn : Ne (α := R) ((coeff R p n : (a : Perfection R p) → R) f : R) (0 : R)
k_1 k : ℕ
ih : Ne (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
h : Eq (α := R) ((coeff R p (n + k).succ : (a : Perfection R p) → R) f : R) (0 : R)
⊢ Eq (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
have rw : Eq (α := R) ((coeff R p (n + k + 1) : (a : Perfection R p) → R) (f ^ p) : R) (0 : R)
Tactic: rw [← coeff_pow_p, map_pow, h, zero_pow hp.1.ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
hfn : Ne (α := R) ((coeff R p n : (a : Perfection R p) → R) f : R) (0 : R)
k_1 k : ℕ
ih : Ne (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
h : Eq (α := R) ((coeff R p (n + k).succ : (a : Perfection R p) → R) f : R) (0 : R)
rw : Eq (α := R) ((coeff R p (n + k + 1) : (a : Perfection R p) → R) (f ^ p) : R) (0 : R)
⊢ Eq (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
have rw₁ : HPow.hPow (α := R) ((coeff R p (n + k + 1) : (a : Perfection R p) → R) f : R) p = 0
Tactic: rw [← coeff_pow_p, map_pow, h, zero_pow hp.1.ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
hfn : Ne (α := R) ((coeff R p n : (a : Perfection R p) → R) f : R) (0 : R)
k_1 k : ℕ
ih : Ne (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
h : Eq (α := R) ((coeff R p (n + k).succ : (a : Perfection R p) → R) f : R) (0 : R)
rw : Eq (α := R) ((coeff R p (n + k + 1) : (a : Perfection R p) → R) (f ^ p) : R) (0 : R)
rw₁ : HPow.hPow (α := R) ((coeff R p (n + k + 1) : (a : Perfection R p) → R) f : R) p = 0
⊢ Eq (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
have rw₂ : HPow.hPow (α := R) 0 p = 0
Tactic: rw [← coeff_pow_p, map_pow, h, zero_pow hp.1.ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
f : Perfection R p
n : ℕ
hfn : Ne (α := R) ((coeff R p n : (a : Perfection R p) → R) f : R) (0 : R)
k_1 k : ℕ
ih : Ne (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
h : Eq (α := R) ((coeff R p (n + k).succ : (a : Perfection R p) → R) f : R) (0 : R)
rw : Eq (α := R) ((coeff R p (n + k + 1) : (a : Perfection R p) → R) (f ^ p) : R) (0 : R)
rw₁ : HPow.hPow (α := R) ((coeff R p (n + k + 1) : (a : Perfection R p) → R) f : R) p = 0
rw₂ : HPow.hPow (α := R) 0 p = 0
⊢ Eq (α := R) ((coeff R p (n + k) : (a : Perfection R p) → R) f : R) (0 : R)
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← coeff_pow_p, map_pow, h, zero_pow hp.1.ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h : Function.Surjective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
n : ℕ
x : R
⊢ ∃ (a : Perfection R p), (coeff R p n : (a : Perfection R p) → R) a = x
have refine_1 : (m : ℕ) → (h : n ≤ m) → R
Tactic: refine ⟨⟨fun m ↦ if h : n ≤ m then ?_ else x ^ p ^ (n - m), ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h : Function.Surjective (α := R) (β := R) (⇑(frobenius R p) : (a : R) → R)
n : ℕ
x : R
refine_1 : (m : ℕ) → (h : n ≤ m) → R
⊢ ∃ (a : Perfection R p), (coeff R p n : (a : Perfection R p) → R) a = x
have refine_2 : ∀ (n_1 : ℕ),
  HPow.hPow (α := R)
      ((fun (m : ℕ) ↦
          (if h_1 : n ≤ m then
              Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
                (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                  (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                    (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) sorry) sorry)
                h_1
            else x ^ p ^ (n - m) :
            R))
        (n_1 + 1))
      p =
    (fun (m : ℕ) ↦
        (if h_1 : n ≤ m then
            Nat.leRec (motive := fun (m : ℕ) (h : n ≤ m) ↦ R) x
              (fun ⦃k : ℕ⦄ (hle : n ≤ k) (xk : R) ↦
                (fun (x : R) (hx : (frobenius R p : (a : R) → R) x = xk) ↦ x)
                  (Classical.choose (p := fun (a : R) ↦ (frobenius R p : (a : R) → R) a = xk) sorry) sorry)
              h_1
          else x ^ p ^ (n - m) :
          R))
      n_1
Tactic: refine ⟨⟨fun m ↦ if h : n ≤ m then ?_ else x ^ p ^ (n - m), ?_⟩, ?_⟩