awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
a : F
rw : HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F F) : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
⊢ normalizedTraceAux F F a = a
have rw₁ : HSMul.hSMul (α := F) (β := F) (↑1 : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
Tactic: rw [normalizedTraceAux_eq_of_finiteDimensional F a, Module.finrank_self F,
    Nat.cast_one, inv_one, one_smul, trace_self_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
a : F
rw : HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F F) : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₁ : HSMul.hSMul (α := F) (β := F) (↑1 : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
⊢ normalizedTraceAux F F a = a
have rw₂ : HSMul.hSMul (α := F) (β := F) 1⁻¹ ((trace F F : (a : F) → F) a : F) = a
Tactic: rw [normalizedTraceAux_eq_of_finiteDimensional F a, Module.finrank_self F,
    Nat.cast_one, inv_one, one_smul, trace_self_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
a : F
rw : HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F F) : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₁ : HSMul.hSMul (α := F) (β := F) (↑1 : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₂ : HSMul.hSMul (α := F) (β := F) 1⁻¹ ((trace F F : (a : F) → F) a : F) = a
⊢ normalizedTraceAux F F a = a
have rw₃ : HSMul.hSMul (α := F) (β := F) 1 ((trace F F : (a : F) → F) a : F) = a
Tactic: rw [normalizedTraceAux_eq_of_finiteDimensional F a, Module.finrank_self F,
    Nat.cast_one, inv_one, one_smul, trace_self_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
a : F
rw : HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F F) : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₁ : HSMul.hSMul (α := F) (β := F) (↑1 : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₂ : HSMul.hSMul (α := F) (β := F) 1⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₃ : HSMul.hSMul (α := F) (β := F) 1 ((trace F F : (a : F) → F) a : F) = a
⊢ normalizedTraceAux F F a = a
have rw₄ : (trace F F : (a : F) → F) a = a
Tactic: rw [normalizedTraceAux_eq_of_finiteDimensional F a, Module.finrank_self F,
    Nat.cast_one, inv_one, one_smul, trace_self_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
a : F
rw : HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F F) : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₁ : HSMul.hSMul (α := F) (β := F) (↑1 : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₂ : HSMul.hSMul (α := F) (β := F) 1⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₃ : HSMul.hSMul (α := F) (β := F) 1 ((trace F F : (a : F) → F) a : F) = a
rw₄ : (trace F F : (a : F) → F) a = a
⊢ normalizedTraceAux F F a = a
have rw₅ : a = a
Tactic: rw [normalizedTraceAux_eq_of_finiteDimensional F a, Module.finrank_self F,
    Nat.cast_one, inv_one, one_smul, trace_self_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (hypothesis)
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F K
inst_8 : CharZero F
inst_9 : CharZero E
inst_10 : Algebra.IsIntegral E K
a : K
h : Membership.mem (γ := Subsemiring (Polynomial E)) (Polynomial.lifts (algebraMap F E)) (minpoly E a)
⊢ Eq.{u_4 + 1} (α := E) ((algebraMap F E : (a : F) → E) ((normalizedTrace F K : (a : K) → F) a : F) : E)
    ((normalizedTrace E K : (a : K) → E) a : E)
have ha : IsIntegral F a
Tactic: have ha : IsIntegral F a := IsIntegral.isIntegral a
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (hypothesis)
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
⊢ Eq.{u_3 + 1} (α := F) ((normalizedTrace F E : (a : E) → F) ((normalizedTrace E K : (a : K) → E) a : E) : F)
    ((normalizedTrace F K : (a : K) → F) a : F)
have this : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
Tactic: have : FiniteDimensional E E⟮a⟯ :=
    IntermediateField.adjoin.finiteDimensional (IsIntegral.isIntegral a)
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
⊢ Eq.{u_3 + 1} (α := F) ((normalizedTrace F E : (a : E) → F) ((normalizedTrace E K : (a : K) → E) a : E) : F)
    ((normalizedTrace F K : (a : K) → F) a : F)
have rw : (normalizedTrace F K : (a : K) → F) a =
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_3, u_5} F ↥E⟮a⟯) : F)⁻¹
    ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
Tactic: rw [normalizedTrace_def E K, inv_natCast_smul_eq (R := E) (S := F), map_smul,
    normalizedTrace_eq_of_finiteDimensional F E, LinearMap.smul_apply, ← smul_assoc,
    smul_eq_mul (a := _⁻¹), ← mul_inv, trace_trace, mul_comm,
    ← Nat.cast_mul, Module.finrank_mul_finrank, eq_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (hypothesis)
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
⊢ (normalizedTrace F K : (a : K) → F) a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_3, u_5} F ↥E⟮a⟯) : F)⁻¹
      ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
have this₁ : FiniteDimensional.{u_3, u_5} F ↥E'
Tactic: have : FiniteDimensional F E' := Module.Finite.trans E E⟮a⟯
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (hypothesis)
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this_1 : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
this : FiniteDimensional.{u_3, u_5} F ↥E'
⊢ (normalizedTrace F K : (a : K) → F) a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_3, u_5} F ↥E⟮a⟯) : F)⁻¹
      ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
have h_finrank_eq : Module.finrank.{u_3, u_5} F ↥E⟮a⟯ = Module.finrank.{u_3, u_5} F ↥E'
Tactic: have h_finrank_eq : Module.finrank F E⟮a⟯ = Module.finrank F E' := rfl
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (hypothesis)
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this_1 : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
this : FiniteDimensional.{u_3, u_5} F ↥E'
h_finrank_eq : Module.finrank.{u_3, u_5} F ↥E⟮a⟯ = Module.finrank.{u_3, u_5} F ↥E'
⊢ (normalizedTrace F K : (a : K) → F) a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_3, u_5} F ↥E⟮a⟯) : F)⁻¹
      ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
have h_trace_eq : Eq.{u_3 + 1} (α := F) ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
  ((trace F ↥E' : (a : ↥E') → F) (AdjoinSimple.gen E a) : F)
Tactic: have h_trace_eq : trace F E⟮a⟯ (AdjoinSimple.gen E a) = trace F E' (AdjoinSimple.gen E a : E') :=
    rfl
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this_1 : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
this : FiniteDimensional.{u_3, u_5} F ↥E'
h_finrank_eq : Module.finrank.{u_3, u_5} F ↥E⟮a⟯ = Module.finrank.{u_3, u_5} F ↥E'
h_trace_eq :
  Eq.{u_3 + 1} (α := F) ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
    ((trace F ↥E' : (a : ↥E') → F) (AdjoinSimple.gen E a) : F)
a' : ↥E' := AdjoinSimple.gen E a
⊢ (normalizedTrace F K : (a : K) → F) a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_3, u_5} F ↥E⟮a⟯) : F)⁻¹
      ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
have rw : Eq.{u_3 + 1} (α := F) ((normalizedTrace F K : (a : K) → F) a : F) ((normalizedTrace F K : (a : K) → F) (↑a' : K) : F)
Tactic: rw [h_finrank_eq, h_trace_eq, ← normalizedTrace_eq_of_finiteDimensional_apply F,
    ← normalizedTrace_intermediateField F K a']
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
M : Type u_1
p q : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
inst_2 : PerfectRing M q
⊢ Bijective (β := M) fun (x : M) ↦ x ^ (p * q)
have simp_rw : Bijective (β := M) fun (x : M) ↦ (x ^ p) ^ q
Tactic: simp_rw [pow_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
M : Type u_1
p : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
n_1 n : ℕ
ih : powMulEquiv M (p ^ n) = HPow.hPow (α := M ≃* M) (powMulEquiv M p) n
⊢ powMulEquiv M (p ^ n.succ) = HPow.hPow (α := M ≃* M) (powMulEquiv M p) n.succ
have rw : Eq (α := M ≃* M) (powMulEquiv M (p ^ n.succ)) (powMulEquiv M (p * p ^ n))
Tactic: rw [pow_succ (powMulEquiv M p), ← ih, MulAut.mul_def, ← powMulEquiv_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
M : Type u_1
p : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
n_1 n : ℕ
ih : powMulEquiv M (p ^ n) = HPow.hPow (α := M ≃* M) (powMulEquiv M p) n
⊢ Eq (α := M ≃* M) (powMulEquiv M (p ^ n.succ)) (powMulEquiv M (p * p ^ n))
have e_p : p ^ n.succ = p * p ^ n
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
M : Type u_1
p : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
n_1 n : ℕ
ih : powMulEquiv M (p ^ n) = HPow.hPow (α := M ≃* M) (powMulEquiv M p) n
⊢ p ^ n.succ = p * p ^ n
have e_p : p * p ^ n = p * p ^ n
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p m n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ Eq (α := R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p (m + n)) : (a : R) → R) x : R) :
      R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
            ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
          R) :
      R)
have rw : x =
  (iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
    ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
      R)
Tactic: rw [RingEquiv.apply_symm_apply, add_comm,
    iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p m n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
rw :
  x =
    (iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
      ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
        R)
⊢ Eq (α := R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p (m + n)) : (a : R) → R) x : R) :
      R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
            ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
          R) :
      R)
have rw₁ : x =
  (iterateFrobeniusEquiv R p (n + m) : (a : R) → R)
    ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
      R)
Tactic: rw [RingEquiv.apply_symm_apply, add_comm,
    iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p m n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
rw :
  x =
    (iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
      ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
        R)
rw₁ :
  x =
    (iterateFrobeniusEquiv R p (n + m) : (a : R) → R)
      ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
        R)
⊢ Eq (α := R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p (m + n)) : (a : R) → R) x : R) :
      R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
            ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
          R) :
      R)
have rw₂ : x =
  (iterateFrobeniusEquiv R p n : (a : R) → R)
    ((iterateFrobeniusEquiv R p m : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
            ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
          R) :
      R)
Tactic: rw [RingEquiv.apply_symm_apply, add_comm,
    iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p m n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
rw :
  x =
    (iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
      ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
        R)
rw₁ :
  x =
    (iterateFrobeniusEquiv R p (n + m) : (a : R) → R)
      ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
        R)
rw₂ :
  x =
    (iterateFrobeniusEquiv R p n : (a : R) → R)
      ((iterateFrobeniusEquiv R p m : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
              ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
            R) :
        R)
⊢ Eq (α := R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p (m + n)) : (a : R) → R) x : R) :
      R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
            ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
          R) :
      R)
have rw₃ : x = (iterateFrobeniusEquiv R p n : (a : R) → R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R)
Tactic: rw [RingEquiv.apply_symm_apply, add_comm,
    iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p m n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
rw :
  x =
    (iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
      ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
        R)
rw₁ :
  x =
    (iterateFrobeniusEquiv R p (n + m) : (a : R) → R)
      ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
        R)
rw₂ :
  x =
    (iterateFrobeniusEquiv R p n : (a : R) → R)
      ((iterateFrobeniusEquiv R p m : (a : R) → R)
          ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
              ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
            R) :
        R)
rw₃ :
  x = (iterateFrobeniusEquiv R p n : (a : R) → R) ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R)
⊢ Eq (α := R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p (m + n)) : (a : R) → R) x : R) :
      R)
    ((iterateFrobeniusEquiv R p (m + n) : (a : R) → R)
        ((RingEquiv.symm (iterateFrobeniusEquiv R p m) : (a : R) → R)
            ((RingEquiv.symm (iterateFrobeniusEquiv R p n) : (a : R) → R) x : R) :
          R) :
      R)
have rw₄ : x = x
Tactic: rw [RingEquiv.apply_symm_apply, add_comm,
    iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ (iterateFrobeniusEquiv R p 0 : (a : R) → R) x = x
have rw : x ^ HPow.hPow (β := ℕ) p 0 = x
Tactic: rw [iterateFrobeniusEquiv_def, pow_zero, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
rw : x ^ HPow.hPow (β := ℕ) p 0 = x
⊢ (iterateFrobeniusEquiv R p 0 : (a : R) → R) x = x
have rw₁ : HPow.hPow (β := ℕ) x 1 = x
Tactic: rw [iterateFrobeniusEquiv_def, pow_zero, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
rw : x ^ HPow.hPow (β := ℕ) p 0 = x
rw₁ : HPow.hPow (β := ℕ) x 1 = x
⊢ (iterateFrobeniusEquiv R p 0 : (a : R) → R) x = x
have rw₂ : x = x
Tactic: rw [iterateFrobeniusEquiv_def, pow_zero, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
⊢ (iterateFrobeniusEquiv R p 1 : (a : R) → R) x = x ^ p
have rw : x ^ HPow.hPow (β := ℕ) p 1 = x ^ p
Tactic: rw [iterateFrobeniusEquiv_def, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
rw : x ^ HPow.hPow (β := ℕ) p 1 = x ^ p
⊢ (iterateFrobeniusEquiv R p 1 : (a : R) → R) x = x ^ p
have rw₁ : x ^ p = x ^ p
Tactic: rw [iterateFrobeniusEquiv_def, pow_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := (a : R) → R) (⇑(iterateFrobeniusEquiv R p n) : (a : R) → R)
    (⇑((RingAut.toPerm R : (a : RingAut R) → Equiv.Perm R) (HPow.hPow (α := R ≃+* R) (frobeniusEquiv R p) n) :
          Equiv.Perm R) :
      (a : R) → R)
have rw : Eq (α := (a : R) → R) (⇑(iterateFrobeniusEquiv R p n) : (a : R) → R)
  (⇑((RingAut.toPerm R : (a : RingAut R) → Equiv.Perm R) (frobeniusEquiv R p) : Equiv.Perm R) : (a : R) → R)^[n]
Tactic: rw [map_pow, Equiv.Perm.coe_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p n : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ RingEquiv.symm (iterateFrobeniusEquiv R p n) = HPow.hPow (α := R ≃+* R) (RingEquiv.symm (frobeniusEquiv R p)) n
have rw : (HPow.hPow (α := R ≃+* R) (frobeniusEquiv R p) n).symm =
  HPow.hPow (α := R ≃+* R) (RingEquiv.symm (frobeniusEquiv R p)) n
Tactic: rw [iterateFrobeniusEquiv_eq_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := R →+* R) (RingHom.comp (frobenius R p) (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R)) (RingHom.id R)
have a : ∀ (x : R),
  Eq (α := R) ((RingHom.comp (frobenius R p) (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) : (a : R) → R) x : R)
    ((RingHom.id R : (a : R) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := R →+* R) (RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) (frobenius R p)) (RingHom.id R)
have a : ∀ (x : R),
  Eq (α := R) ((RingHom.comp (↑(RingEquiv.symm (frobeniusEquiv R p)) : R →+* R) (frobenius R p) : (a : R) → R) x : R)
    ((RingHom.id R : (a : R) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := R → R)
    (Function.comp (β := R) (⇑(frobenius R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)) id
have h : ∀ (x : R),
  Function.comp (β := R) (⇑(frobenius R p) : (a : R) → R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R) x =
    id x
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
⊢ Eq (α := R → R)
    (Function.comp (β := R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R) (⇑(frobenius R p) : (a : R) → R)) id
have h : ∀ (x : R),
  Function.comp (β := R) (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R) (⇑(frobenius R p) : (a : R) → R) x =
    id x
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
n : ℕ
⊢ (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x ^ p ^ n = x
have zero : ∀ (x : R), (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[0] x ^ HPow.hPow (β := ℕ) p 0 = x
Tactic: induction n generalizing x with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih]
Cleared hypotheses: x, n
-- Lean 4 proof step from Mathlib.FieldTheory.Perfect (goal)
Goal:
R : Type u_1
p : ℕ
inst : CommSemiring R
inst_1 : ExpChar R p
inst_2 : PerfectRing R p
x : R
n : ℕ
zero : ∀ (x : R), (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[0] x ^ HPow.hPow (β := ℕ) p 0 = x
⊢ (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x ^ p ^ n = x
have succ : ∀ (n : ℕ) (ih : ∀ (x : R), (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] x ^ p ^ n = x) (x : R),
  (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n + 1] x ^ p ^ (n + 1) = x
Tactic: induction n generalizing x with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih]
Cleared hypotheses: x, n