mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
i : σ
hi : m i > n i
⊢ ¬p • m ≤ p • n

Tactic:
have : ¬ p • m i ≤ p • n i := by
          simp [Nat.mul_lt_mul_of_pos_left hi (p.ne_zero_iff_zero_lt.mp hp)]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ∀ (i : σ), p ∣ d i
m : σ →₀ ℕ
hm : p • m = d
h_le : ¬m ≤ n
i : σ
hi : m i > n i
this : ¬p • m i ≤ p • n i
⊢ ¬p • m ≤ p • n
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
⊢ ∀ (a : σ →₀ ℕ), ∃ b, a ≤ b ∧ (trunc' R b) ((map (frobenius R p)) ((expand p hp) f)) = (trunc' R b) (f ^ p)

Tactic:
intro n

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∃ b, n ≤ b ∧ (trunc' R b) ((map (frobenius R p)) ((expand p hp) f)) = (trunc' R b) (f ^ p)
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ (T1 f c).comp (T1 f (-c)) = AlgHom.id k (MvPolynomial (Fin (n + 1)) k)

Tactic:
rw [comp_aeval, ← MvPolynomial.aeval_X_left]

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
c : k
⊢ (MvPolynomial.aeval fun i ↦
      (T1 f c) (if i = 0 then MvPolynomial.X 0 else MvPolynomial.X i + -c • MvPolynomial.X 0 ^ r i)) =
    MvPolynomial.aeval MvPolynomial.X
Module: Mathlib.RingTheory.NormTrace

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
a : A
x : B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Tactic:
let ι := Module.Free.ChooseBasisIndex A B

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2 := Free.ChooseBasisIndex A B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
⊢ ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X j))).leadingCoeff = 1

Tactic:
by_cases h : j = 0
      · simp [h, finSuccEquiv_apply]
      · simp only [aeval_eq_bind₁, bind₁_X_right, if_neg h, one_smul, map_add, map_pow]
        obtain ⟨i, rfl⟩ := Fin.exists_succ_eq.mpr h
        simp [finSuccEquiv_X_succ, finSuccEquiv_X_zero, add_comm]

Goal state after:
Module: Mathlib.RingTheory.Teichmuller

Goal state before:
pp: p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ (Quotient.out ((coeff (R ⧸ I) p n) x) * Quotient.out ((coeff (R ⧸ I) p n) y)) ^ p ^ n ≡
    x.teichmullerFun * y.teichmullerFun [SMOD I ^ (n + 1)]

Tactic:
mul_pow

Goal state after:
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x y : Perfection (R ⧸ I) p
n : ℕ
⊢ Quotient.out ((coeff (R ⧸ I) p n) x) ^ p ^ n * Quotient.out ((coeff (R ⧸ I) p n) y) ^ p ^ n ≡
    x.teichmullerFun * y.teichmullerFun [SMOD I ^ (n + 1)]
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ (wittStructureRat p Φ)) (W_ ℚ n) =
    (bind₁ fun i ↦ (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ i)) (W_ ℚ n)

Tactic:
exact eval₂Hom_congr (RingHom.ext_rat _ _) rfl rfl

Goal state after:
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case refine_1
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ (fun φ ↦ ∀ (n : ℕ), (bind₁ φ) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ) (wittStructureRat p Φ)

Tactic:
intro n

Goal state after:
case refine_1
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
⊢ (bind₁ (wittStructureRat p Φ)) (W_ ℚ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) Φ
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ i ∈ range n

Tactic:
rw [vars_C_mul] at H

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ i ∈ range n

case ind.ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ ↑p ^ j ≠ 0
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False

Tactic:
rw [vars_C_mul] at H

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False

case ind.hpq.ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ ↑p ^ j ≠ 0
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ n)

Tactic:
refine Nat.strong_induction_on n ?_

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ m < n,
        X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
          (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)) →
      X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
        (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ n)
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ),
    (∀ m < n,
        X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
          (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)) →
      X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
        (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ n)

Tactic:
intro n

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∀ m < n,
      X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
        (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)) →
    X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ n)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case py₁
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (n : ℕ),
    (bind₁ fun k ↦ (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
      (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Tactic:
intro n

Goal state after:
case py₁
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
n : ℕ
⊢ (bind₁ fun k ↦ (map (Int.castRingHom ℚ)) (φ k)) (W_ ℚ n) =
    (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case py₂
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
⊢ ∀ (n : ℕ),
    (bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
      (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)

Tactic:
intro n

Goal state after:
case py₂
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
φ : ℕ → MvPolynomial (idx × ℕ) ℤ
h : ∀ (n : ℕ), (bind₁ φ) (W_ ℤ n) = (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℤ n)) Φ
n : ℕ
⊢ (bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
    (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ n.succ)) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ (n.succ - 1))

Tactic:
rw [Nat.succ_eq_add_one, add_tsub_cancel_right]

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (MvPolynomial.eval x) ((bind₁ verschiebungPoly) (wittPolynomial p ℤ (n + 1))) =
    (MvPolynomial.eval x) (↑p * wittPolynomial p ℤ n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r * s)) =
    v ((algebraMap O K) r) * preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s)

Tactic:
preVal_mk hv hy0,

Goal state after:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r * s)) = v ((algebraMap O K) r) * v ((algebraMap O K) s)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r + s)) ≤
    max (v ((algebraMap O K) r)) (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s))

Tactic:
preVal_mk hv hy0,

Goal state after:
case neg
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
r : O
hx0 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ≠ 0
s : O
hy0 : (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0
hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r + s)) ≤ max (v ((algebraMap O K) r)) (v ((algebraMap O K) s))
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ C ↑p ^ i *
        ((C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i)) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1))) *
      C ⅟↑p ^ n =
    C ↑p *
      ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))))

Tactic:
mul_pow

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
h1 : ↑p ^ n * ⅟↑p ^ n = 1
i : ℕ
hi : i < n
j : ℕ
hj : j < p ^ (n - i)
⊢ C ↑p ^ i *
        (C ↑p ^ (j + 1) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) *
          ↑((p ^ (n - i)).choose (j + 1))) *
      C ⅟↑p ^ n =
    C ↑p *
      ((X i ^ p) ^ (p ^ (n - i) - (j + 1)) * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p i) ^ (j + 1) *
        C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))))
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case e'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i ↦
        ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)

pp: case e'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i ↦
        ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)

Tactic:
all_goals
    simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    ext1
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    ext ⟨b, _⟩
    fin_cases b <;> simp only [coeff_mk, uncurry] <;> rfl

Goal state after:
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
⊢ ∀ (n : ℕ), (ghostComponent n) (select P x + select (fun i ↦ ¬P i) x) = (ghostComponent n) x

Tactic:
intro n

Goal state after:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ (ghostComponent n) (select P x + select (fun i ↦ ¬P i) x) = (ghostComponent n) x
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case inr.inr
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
hfg : (coeff (max m n + 1)) f * (coeff (max m n + 1)) g ≠ 0
⊢ (ModP.preVal K v O p ((coeff (max m n + 1)) f) * ModP.preVal K v O p ((coeff (max m n + 1)) g)) ^ p ^ (max m n + 1) =
    ModP.preVal K v O p ((coeff (max m n + 1)) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O p ((coeff (max m n + 1)) g) ^ p ^ (max m n + 1)

Tactic:
mul_pow

Goal state after:
case inr.inr
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
hfg : (coeff (max m n + 1)) f * (coeff (max m n + 1)) g ≠ 0
⊢ ModP.preVal K v O p ((coeff (max m n + 1)) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O p ((coeff (max m n + 1)) g) ^ p ^ (max m n + 1) =
    ModP.preVal K v O p ((coeff (max m n + 1)) f) ^ p ^ (max m n + 1) *
      ModP.preVal K v O p ((coeff (max m n + 1)) g) ^ p ^ (max m n + 1)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
⊢ valAux K v O p (f * g) = valAux K v O p f * valAux K v O p g

Tactic:
by
  obtain rfl | hf := eq_or_ne f 0
  · simp
  obtain rfl | hg := eq_or_ne g 0
  · simp
  obtain ⟨m, hm⟩ : ∃ n, coeff n f ≠ 0 := not_forall.1 fun h => hf <| Perfection.ext h
  obtain ⟨n, hn⟩ : ∃ n, coeff n g ≠ 0 := not_forall.1 fun h => hg <| Perfection.ext h
  replace hm := coeff_ne_zero_of_le hm (le_max_left m n)
  replace hn := coeff_ne_zero_of_le hn (le_max_right m n)
  have hfg : coeff (max m n + 1) (f * g) ≠ 0 := by
    rw [map_mul]
    refine ModP.mul_ne_zero_of_pow_p_ne_zero (hv := hv) ?_ ?_
    · rw [coeff_pow_p f]; assumption
    · rw [coeff_pow_p g]; assumption
  rw [valAux_eq hv (coeff_add_ne_zero hm 1),
      valAux_eq hv (coeff_add_ne_zero hn 1), valAux_eq hv hfg]
  rw [map_mul] at hfg ⊢; rw [ModP.preVal_mul hv hfg, mul_pow]

Goal state after:
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
⊢ (x + y).coeff n = x.coeff n + y.coeff n

Tactic:
have hy : select (fun i => ¬P i) z = y := by
    ext1 n; rw [select, coeff_mk, coeff_mk]
    split_ifs with hn
    · exact hn.symm
    · rfl

Goal state after:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = 0 ∨ y.coeff n = 0
P : ℕ → Prop := fun n ↦ y.coeff n = 0
this : DecidablePred P
z : 𝕎 R := mk p fun n ↦ if P n then x.coeff n else y.coeff n
hx : select P z = x
hy : select (fun i ↦ ¬P i) z = y
⊢ (x + y).coeff n = x.coeff n + y.coeff n
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : ℕ → 𝕎 k
h : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD Ideal.span {↑p} ^ m • ⊤]
⊢ ∀ (n : ℕ), x n ≡ mk p fun n ↦ (x (n + 1)).coeff n [SMOD Ideal.span {↑p} ^ n • ⊤]

Tactic:
intro n

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : ℕ → 𝕎 k
h : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD Ideal.span {↑p} ^ m • ⊤]
n : ℕ
⊢ x n ≡ mk p fun n ↦ (x (n + 1)).coeff n [SMOD Ideal.span {↑p} ^ n • ⊤]
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
x : R♭
⊢ ∀ (n : ℕ), (fontaineTheta R p) ((teichmuller p) x) ≡ untilt x [SMOD 𝔭 ^ n]

Tactic:
intro n

Goal state after:
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
x : R♭
n : ℕ
⊢ (fontaineTheta R p) ((teichmuller p) x) ≡ untilt x [SMOD 𝔭 ^ n]
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ map (Int.castRingHom ℚ) (dickson 1 1 (m * n)) = map (Int.castRingHom ℚ) ((dickson 1 1 m).comp (dickson 1 1 n))

Tactic:
simp only [map_dickson, map_comp, eq_intCast, Int.cast_one, dickson_one_one_eq_chebyshev_T,
    Nat.cast_mul, Chebyshev.T_mul, two_mul, ← add_comp]

Goal state after:
case e_a
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ ((Chebyshev.T ℚ ↑m + Chebyshev.T ℚ ↑m).comp (Chebyshev.T ℚ ↑n)).comp (C ⅟2 * X) =
    ((Chebyshev.T ℚ ↑m + Chebyshev.T ℚ ↑m).comp (C ⅟2 * X)).comp ((Chebyshev.T ℚ ↑n + Chebyshev.T ℚ ↑n).comp (C ⅟2 * X))
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
⊢ ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)

Tactic:
intro n

Goal state after:
n✝ k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n : ℕ
⊢ ∀ (k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case e_a.e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n + 1) * (2 * n + 1 + (k + 1) + 1).choose (k + 1) =
    (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 2) * (k + 2)

Tactic:
Nat.choose,

Goal state after:
case e_a.e_a.e_a
n✝ k✝ : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
n k : ℕ
⊢ (2 * n + 1) * ((2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 1)) =
    (2 * n + 1) * (2 * n + 1 + (k + 1)).choose k + (2 * n + 1 + (k + 1)).choose (k + 2) * (k + 2)
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ n > (p * (1 - X)).natDegree,
    (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))

Tactic:
intro n

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
⊢ n > (p * (1 - X)).natDegree →
    (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) ((p * (1 - X)).hilbertPoly (d + 1))
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case e_a.a
n m : ℕ
hm : m ∈ range (n + 1)
⊢ (-1) ^ m * (X ^ 2) ^ m * X ^ (n - m) * ↑(n.choose m) = n.choose m • (-1) ^ m * X ^ (n + m)

Tactic:
pow_two,

Goal state after:
case e_a.a
n m : ℕ
hm : m ∈ range (n + 1)
⊢ (-1) ^ m * (X * X) ^ m * X ^ (n - m) * ↑(n.choose m) = n.choose m • (-1) ^ m * X ^ (n + m)