awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : f.coeff (n + 1) = 0 ∨ HAdd.hAdd (α := R) (↑n : R) 1 = 0
neg : ∀ (h' : f.coeff (n + 1) = 0), 0 = f.coeff (n + 1)
⊢ 0 = f.coeff (n + 1)
have neg₁ : HAdd.hAdd (α := R) (↑n : R) 1 = 0 → 0 = f.coeff (n + 1)
Tactic: rcases this with h' | _
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : f.coeff (n + 1) = 0
⊢ 0 = f.coeff (n + 1)
have neg : Eq.{u + 1} (α := R) 0 0
Tactic: rw [h']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
h' : HAdd.hAdd (α := R) (↑n : R) 1 = 0
⊢ 0 = f.coeff (n + 1)
have h'₁ : p ∣ n.succ
Tactic: rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
⊢ (expand R p : (a : R[X]) → R[X]) (contract p f) = f
have zero : ∀ [CharZero R] [ExpChar R 1], (expand R 1 : (a : R[X]) → R[X]) (contract 1 f) = f
Tactic: obtain _ | @⟨_, hprime, hchar⟩ := ‹ExpChar R p›
Cleared hypotheses: p, inst_1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
zero : ∀ [CharZero R] [ExpChar R 1], (expand R 1 : (a : R[X]) → R[X]) (contract 1 f) = f
⊢ (expand R p : (a : R[X]) → R[X]) (contract p f) = f
have prime : ∀ (hprime : Nat.Prime p) [hchar : CharP R p], (expand R p : (a : R[X]) → R[X]) (contract p f) = f
Tactic: obtain _ | @⟨_, hprime, hchar⟩ := ‹ExpChar R p›
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
inst_2 : CharZero R
inst_3 : ExpChar R 1
⊢ (expand R 1 : (a : R[X]) → R[X]) (contract 1 f) = f
have zero : contract 1 f = f
Tactic: rw [expand_one, contract_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
inst_2 : CharZero R
inst_3 : ExpChar R 1
zero : contract 1 f = f
⊢ (expand R 1 : (a : R[X]) → R[X]) (contract 1 f) = f
have zero₁ : f = f
Tactic: rw [expand_one, contract_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hprime : Nat.Prime p
hchar : CharP R p
⊢ (expand R p : (a : R[X]) → R[X]) (contract p f) = f
have this : Fact (CharP R p)
Tactic: haveI := Fact.mk hchar
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) f) = f ^ p
have refine_1 : ∀ (a b : R[X]) (ha : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a) = a ^ p)
  (hb : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = b ^ p),
  map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (a + b)) = (a + b) ^ p
Tactic: refine f.induction_on' (fun a b ha hb => ?_) fun n a => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
refine_1 :
  ∀ (a b : R[X]) (ha : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a) = a ^ p)
    (hb : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = b ^ p),
    map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (a + b)) = (a + b) ^ p
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) f) = f ^ p
have refine_2 : ∀ (n : ℕ) (a : R),
  map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a)) =
    HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) p
Tactic: refine f.induction_on' (fun a b ha hb => ?_) fun n a => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a) = a ^ p
hb : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = b ^ p
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (a + b)) = (a + b) ^ p
have refine_1 : map (frobenius R p)
    (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) a : R[X])
      ((expand R p : (a : R[X]) → R[X]) b : R[X])) =
  (a + b) ^ p
Tactic: rw [map_add, Polynomial.map_add, ha, hb, add_pow_expChar]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a) = a ^ p
hb : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = b ^ p
refine_1 :
  map (frobenius R p)
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) a : R[X])
        ((expand R p : (a : R[X]) → R[X]) b : R[X])) =
    (a + b) ^ p
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (a + b)) = (a + b) ^ p
have refine_1₁ : HAdd.hAdd (α := R[X]) (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a))
    (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b)) =
  (a + b) ^ p
Tactic: rw [map_add, Polynomial.map_add, ha, hb, add_pow_expChar]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a) = a ^ p
hb : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = b ^ p
refine_1 :
  map (frobenius R p)
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) a : R[X])
        ((expand R p : (a : R[X]) → R[X]) b : R[X])) =
    (a + b) ^ p
refine_1₁ :
  HAdd.hAdd (α := R[X]) (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a))
      (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b)) =
    (a + b) ^ p
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (a + b)) = (a + b) ^ p
have refine_1₂ : a ^ p + map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = (a + b) ^ p
Tactic: rw [map_add, Polynomial.map_add, ha, hb, add_pow_expChar]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a) = a ^ p
hb : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = b ^ p
refine_1 :
  map (frobenius R p)
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) a : R[X])
        ((expand R p : (a : R[X]) → R[X]) b : R[X])) =
    (a + b) ^ p
refine_1₁ :
  HAdd.hAdd (α := R[X]) (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a))
      (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b)) =
    (a + b) ^ p
refine_1₂ : a ^ p + map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = (a + b) ^ p
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (a + b)) = (a + b) ^ p
have refine_1₃ : a ^ p + b ^ p = (a + b) ^ p
Tactic: rw [map_add, Polynomial.map_add, ha, hb, add_pow_expChar]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a) = a ^ p
hb : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = b ^ p
refine_1 :
  map (frobenius R p)
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) a : R[X])
        ((expand R p : (a : R[X]) → R[X]) b : R[X])) =
    (a + b) ^ p
refine_1₁ :
  HAdd.hAdd (α := R[X]) (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a))
      (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b)) =
    (a + b) ^ p
refine_1₂ : a ^ p + map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = (a + b) ^ p
refine_1₃ : a ^ p + b ^ p = (a + b) ^ p
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (a + b)) = (a + b) ^ p
have refine_1₄ : a ^ p + b ^ p = a ^ p + b ^ p
Tactic: rw [map_add, Polynomial.map_add, ha, hb, add_pow_expChar]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a)) =
    HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) p
have refine_2 : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a ^ p) : R[X]) (HPow.hPow (α := R[X]) X (n * p)) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a ^ p) : R[X]) (HPow.hPow (α := R[X]) X n ^ p)
Tactic: rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
      mul_pow, ← C.map_pow, frobenius_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
⊢ map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f) = f ^ p ^ (k + 1)
have succ : f ^ p ^ (k + 1) = map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
| f ^ p ^ (k + 1)
have rw : HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p
Tactic: rw [pow_succ, pow_mul, ← n_ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
⊢ f ^ p ^ (k + 1) = map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
have succ : HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p =
  map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
Tactic: conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
⊢ HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
have succ : Eq (α := R[X])
  (map (frobenius R p)
    ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
  (map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f))
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
succ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f))
⊢ HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
have succ₁ : Eq (α := R[X])
  (map (frobenius R p)
    ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
  (map (iterateFrobenius R p (k + 1)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
succ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f))
succ₁ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
⊢ HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
have succ₂ : Eq (α := R[X])
  (map (frobenius R p)
    ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
  (map (iterateFrobenius R p (1 + k)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
succ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f))
succ₁ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₂ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (1 + k)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
⊢ HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
have succ₃ : Eq (α := R[X])
  (map (frobenius R p)
    ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
  (map (RingHom.comp (iterateFrobenius R p 1) (iterateFrobenius R p k)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
succ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f))
succ₁ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₂ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (1 + k)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₃ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (RingHom.comp (iterateFrobenius R p 1) (iterateFrobenius R p k))
      ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
⊢ HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
have succ₄ : Eq (α := R[X])
  (map (frobenius R p)
    ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
  (map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
succ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f))
succ₁ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₂ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (1 + k)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₃ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (RingHom.comp (iterateFrobenius R p 1) (iterateFrobenius R p k))
      ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₄ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
⊢ HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
have succ₅ : Eq (α := R[X])
  (map (frobenius R p)
    (map (iterateFrobenius R p k) ((expand R p : (a : R[X]) → R[X]) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
  (map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
succ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f))
succ₁ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₂ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (1 + k)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₃ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (RingHom.comp (iterateFrobenius R p 1) (iterateFrobenius R p k))
      ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₄ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
succ₅ :
  Eq (α := R[X])
    (map (frobenius R p)
      (map (iterateFrobenius R p k) ((expand R p : (a : R[X]) → R[X]) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
⊢ HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
have succ₆ : Eq (α := R[X]) (map (frobenius R p) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
  (map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
Tactic: simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
n : ℕ
⊢ map (iterateFrobenius R p n) ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = f ^ p ^ n
have zero : map (iterateFrobenius R p 0) ((expand R (HPow.hPow (β := ℕ) p 0) : (a : R[X]) → R[X]) f) = f ^ HPow.hPow (β := ℕ) p 0
Tactic: induction n with
  | zero => simp
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
n : ℕ
zero :
  map (iterateFrobenius R p 0) ((expand R (HPow.hPow (β := ℕ) p 0) : (a : R[X]) → R[X]) f) = f ^ HPow.hPow (β := ℕ) p 0
⊢ map (iterateFrobenius R p n) ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = f ^ p ^ n
have succ : ∀ (k : ℕ) (n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k),
  map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f) = f ^ p ^ (k + 1)
Tactic: induction n with
  | zero => simp
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]
Cleared hypotheses: n