awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n j : ℕ
hj : j < p ^ n
⊢ (↑(n - v p (j + 1)) : ℕ∞) ≤ emultiplicity p ((p ^ n).choose (j + 1))
have hk : LE.le (α := ℕ∞) (↑(n - v p (j + 1)) : ℕ∞) (↑(n - v p (j + 1)) : ℕ∞)
Tactic: rw [hp.out.emultiplicity_choose_prime_pow hj j.succ_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
⊢ j - v p (j + 1) + n = i + j + (n - i - v p (j + 1))
have generalize : ∀ (m : ℕ) (h : v p (j + 1) = m), j - m + n = i + j + (n - i - m)
Tactic: generalize h : v p (j + 1) = m
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
⊢ j - m + n = i + j + (n - i - m)
have rsuffices : ∀ (h₁ : m ≤ n - i) (h₂ : m ≤ j), j - m + n = i + j + (n - i - m)
Tactic: rsuffices ⟨h₁, h₂⟩ : m ≤ n - i ∧ m ≤ j
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
rsuffices : ∀ (h₁ : m ≤ n - i) (h₂ : m ≤ j), j - m + n = i + j + (n - i - m)
⊢ j - m + n = i + j + (n - i - m)
have rsuffices₁ : m ≤ n - i ∧ m ≤ j
Tactic: rsuffices ⟨h₁, h₂⟩ : m ≤ n - i ∧ m ≤ j
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
⊢ j - m + n = i + j + (n - i - m)
have rw : j + n - m = i + j + (n - i - m)
Tactic: rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)),
      add_assoc, tsub_right_comm, add_comm i,
      tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
rw : j + n - m = i + j + (n - i - m)
⊢ j - m + n = i + j + (n - i - m)
have rw₁ : j + n - m = j + i + (n - i - m)
Tactic: rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)),
      add_assoc, tsub_right_comm, add_comm i,
      tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
rw : j + n - m = i + j + (n - i - m)
rw₁ : j + n - m = j + i + (n - i - m)
⊢ j - m + n = i + j + (n - i - m)
have rw₂ : j + (n - m) = j + i + (n - i - m)
Tactic: rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)),
      add_assoc, tsub_right_comm, add_comm i,
      tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
rw : j + n - m = i + j + (n - i - m)
rw₁ : j + n - m = j + i + (n - i - m)
rw₂ : j + (n - m) = j + i + (n - i - m)
⊢ j - m + n = i + j + (n - i - m)
have rw₃ : j + (n - m) = j + (i + (n - i - m))
Tactic: rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)),
      add_assoc, tsub_right_comm, add_comm i,
      tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
rw : j + n - m = i + j + (n - i - m)
rw₁ : j + n - m = j + i + (n - i - m)
rw₂ : j + (n - m) = j + i + (n - i - m)
rw₃ : j + (n - m) = j + (i + (n - i - m))
⊢ j - m + n = i + j + (n - i - m)
have rw₄ : j + (n - m) = j + (i + (n - m - i))
Tactic: rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)),
      add_assoc, tsub_right_comm, add_comm i,
      tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
rw : j + n - m = i + j + (n - i - m)
rw₁ : j + n - m = j + i + (n - i - m)
rw₂ : j + (n - m) = j + i + (n - i - m)
rw₃ : j + (n - m) = j + (i + (n - i - m))
rw₄ : j + (n - m) = j + (i + (n - m - i))
⊢ j - m + n = i + j + (n - i - m)
have rw₅ : j + (n - m) = j + (n - m - i + i)
Tactic: rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)),
      add_assoc, tsub_right_comm, add_comm i,
      tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
h₁ : m ≤ n - i
h₂ : m ≤ j
rw : j + n - m = i + j + (n - i - m)
rw₁ : j + n - m = j + i + (n - i - m)
rw₂ : j + (n - m) = j + i + (n - i - m)
rw₃ : j + (n - m) = j + (i + (n - i - m))
rw₄ : j + (n - m) = j + (i + (n - m - i))
rw₅ : j + (n - m) = j + (n - m - i + i)
⊢ j - m + n = i + j + (n - i - m)
have rw₆ : j + (n - m) = j + (n - m)
Tactic: rw [tsub_add_eq_add_tsub h₂, add_comm i j, add_tsub_assoc_of_le (h₁.trans (Nat.sub_le n i)),
      add_assoc, tsub_right_comm, add_comm i,
      tsub_add_cancel_of_le (le_tsub_of_add_le_right ((le_tsub_iff_left hi).mp h₁))]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n i j : ℕ
hi : i ≤ n
hj : j < p ^ (n - i)
m : ℕ
h : v p (j + 1) = m
⊢ m ≤ n - i ∧ m ≤ j
have hle : p ^ m ≤ j + 1
Tactic: have hle : p ^ m ≤ j + 1 := h ▸ Nat.le_of_dvd j.succ_pos (pow_multiplicity_dvd _ _)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPoly p n) =
    frobeniusPolyRat p n
have rw : HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
    HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
      ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
        MvPolynomial ℕ ℚ) =
  (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
Tactic: rw [frobeniusPoly, map_add, map_mul, map_pow, map_C, map_X, eq_intCast, Int.cast_natCast,
    frobeniusPolyRat]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
have refine : ∀ (n : ℕ),
  (∀ m < n,
      HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
          HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
            ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
              MvPolynomial ℕ ℚ) =
        (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
          (xInTermsOfW p ℚ m)) →
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
Tactic: refine Nat.strong_induction_on n ?_
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ n)
have rw : HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
    HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
      ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
        MvPolynomial ℕ ℚ) =
  (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
    (HMul.hMul (β := MvPolynomial ℕ ℚ)
      (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
        (∑ i ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
          (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
        MvPolynomial ℕ ℚ))
Tactic: rw [xInTermsOfW_eq]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
      (HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HSub.hSub (α := MvPolynomial ℕ ℚ) (X n)
          (∑ i ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ i) (p ^ (n - i)))))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ))
have simp : HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
    HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
      ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
        MvPolynomial ℕ ℚ) =
  HMul.hMul (β := MvPolynomial ℕ ℚ)
    (HSub.hSub (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
      ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (X n) :
        MvPolynomial ℕ ℚ)
      (∑ x ∈ range n,
          HMul.hMul (α := MvPolynomial ℕ ℚ)
            ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) x) : MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℚ)
              ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
                  (xInTermsOfW p ℚ x) :
                MvPolynomial ℕ ℚ)
              (p ^ (n - x))) :
        MvPolynomial ℕ ℚ))
    ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
        (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
      MvPolynomial ℕ ℚ)
Tactic: simp only [map_sum, map_sub, map_mul, map_pow (bind₁ _), bind₁_C_right]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
have rw : HMul.hMul (α := ℚ) (↑p : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) ^ n = 1
Tactic: rw [← mul_pow, mul_invOf_self, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
rw : HMul.hMul (α := ℚ) (↑p : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) ^ n = 1
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
have rw₁ : HPow.hPow (α := ℚ) 1 n = 1
Tactic: rw [← mul_pow, mul_invOf_self, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
rw : HMul.hMul (α := ℚ) (↑p : ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) ^ n = 1
rw₁ : HPow.hPow (α := ℚ) 1 n = 1
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
have rw₂ : Eq (α := ℚ) 1 1
Tactic: rw [← mul_pow, mul_invOf_self, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
⊢ HPow.hPow (α := MvPolynomial ℕ ℚ) (X n) p +
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p n) :
          MvPolynomial ℕ ℚ) =
    HMul.hMul (β := MvPolynomial ℕ ℚ)
      (HSub.hSub (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (X n) :
          MvPolynomial ℕ ℚ)
        (∑ x ∈ range n,
            HMul.hMul (α := MvPolynomial ℕ ℚ)
              ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) x) : MvPolynomial ℕ ℚ)
              (HPow.hPow (α := MvPolynomial ℕ ℚ)
                ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
                    (xInTermsOfW p ℚ x) :
                  MvPolynomial ℕ ℚ)
                (p ^ (n - x))) :
          MvPolynomial ℕ ℚ))
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
          (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
        MvPolynomial ℕ ℚ)
have h1 : HPow.hPow (α := ℚ) (↑p : ℚ) n *
    HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
  1
Tactic: have h1 : (p : ℚ) ^ n * ⅟(p : ℚ) ^ n = 1 := by rw [← mul_pow, mul_invOf_self, one_pow]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    HPow.hPow (α := MvPolynomial ℕ ℚ) (X m) p +
        HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
          ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ) (frobeniusPolyAux p m) :
            MvPolynomial ℕ ℚ) =
      (bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ) (xInTermsOfW p ℚ m)
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i ∈ range n
⊢ HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ)
            ((bind₁ (wittPolynomial p ℚ ∘ fun (n : ℕ) ↦ n + 1) : (a : MvPolynomial ℕ ℚ) → MvPolynomial ℕ ℚ)
                (xInTermsOfW p ℚ i) :
              MvPolynomial ℕ ℚ)
            (p ^ (n - i))))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ) -
      HMul.hMul (β := MvPolynomial ℕ ℚ)
        (HMul.hMul (α := MvPolynomial ℕ ℚ)
          ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) (p ^ (n + 1 - i))))
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
          MvPolynomial ℕ ℚ) =
    ∑ i_1 ∈ range (p ^ (n - i)),
      HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
        ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
            (HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (i_1 + 1)) * frobeniusPolyAux p i ^ (i_1 + 1) *
              (C : (a : ℤ) → MvPolynomial ℕ ℤ)
                (↑((p ^ (n - i)).choose (i_1 + 1) / p ^ (n - i - v p (i_1 + 1)) * p ^ (i_1 - v p (i_1 + 1))) : ℤ)) :
          MvPolynomial ℕ ℚ)
have hi₁ : i < n
Tactic: rw [mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Frobenius (hypothesis)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 :
  HPow.hPow (α := ℚ) (↑p : ℚ) n *
      HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n =
    1
i : ℕ
hi : i < n
j : ℕ
hj : j ∈ range (p ^ (n - i))
⊢ HMul.hMul (β := MvPolynomial ℕ ℚ)
      (HMul.hMul (α := MvPolynomial ℕ ℚ)
        ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (HPow.hPow (α := ℚ) (↑p : ℚ) i) : MvPolynomial ℕ ℚ)
        (HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
                ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
                ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
                    (frobeniusPolyAux p i) :
                  MvPolynomial ℕ ℚ) ^
              (j + 1) *
            HPow.hPow (α := MvPolynomial ℕ ℚ) (X i) p ^ (p ^ (n - i) - (j + 1)) *
          (↑((p ^ (n - i)).choose (j + 1)) : MvPolynomial ℕ ℚ)))
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ)
          (HPow.hPow (α := ℚ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (↑p : ℚ) _) n) :
        MvPolynomial ℕ ℚ) =
    HMul.hMul (α := MvPolynomial ℕ ℚ) (β := MvPolynomial ℕ ℚ)
      ((C : (a : ℚ) → MvPolynomial ℕ ℚ) (↑p : ℚ) : MvPolynomial ℕ ℚ)
      ((MvPolynomial.map (Int.castRingHom ℚ) : (a : MvPolynomial ℕ ℤ) → MvPolynomial ℕ ℚ)
          (HPow.hPow (α := MvPolynomial ℕ ℤ) (X i) p ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
            (C : (a : ℤ) → MvPolynomial ℕ ℤ)
              (↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))) : ℤ)) :
        MvPolynomial ℕ ℚ)
have hj₁ : j < p ^ (n - i)
Tactic: rw [mem_range] at hj
Cleared hypotheses: hj