mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
X✝ Y✝ : ModuleCat R
f✝ : X✝ ⟶ Y✝
⊢ (ModuleCat.toMatrixModCat R ι ⋙ toModuleCat R i).map f✝ ≫
      (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑Y✝) i ≪≫ₗ
            fromModuleCatToModuleCatLinearEquiv R (↑Y✝) i).toModuleIso.hom =
    (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X✝) i ≪≫ₗ
            fromModuleCatToModuleCatLinearEquiv R (↑X✝) i).toModuleIso.hom ≫
      (𝟭 (ModuleCat R)).map f✝

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
X✝ Y✝ : ModuleCat R
f✝ : X✝ ⟶ Y✝
x✝ : ↑((ModuleCat.toMatrixModCat R ι ⋙ toModuleCat R i).obj X✝)
⊢ (ModuleCat.Hom.hom
        ((ModuleCat.toMatrixModCat R ι ⋙ toModuleCat R i).map f✝ ≫
          (fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑Y✝) i ≪≫ₗ
                fromModuleCatToModuleCatLinearEquiv R (↑Y✝) i).toModuleIso.hom))
      x✝ =
    (ModuleCat.Hom.hom
        ((fromModuleCatToModuleCatLinearEquivtoModuleCatObj R (↑X✝) i ≪≫ₗ
                fromModuleCatToModuleCatLinearEquiv R (↑X✝) i).toModuleIso.hom ≫
          (𝟭 (ModuleCat R)).map f✝))
      x✝
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x✝¹ x✝ : ↑M
⊢ (fun i ↦ ⟨single j i 1 • (x✝¹ + x✝), ⋯⟩) = (fun i ↦ ⟨single j i 1 • x✝¹, ⋯⟩) + fun i ↦ ⟨single j i 1 • x✝, ⋯⟩

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x✝² x✝¹ : ↑M
x✝ : ι
⊢ ↑⟨single j x✝ 1 • (x✝² + x✝¹), ⋯⟩ = ↑(((fun i ↦ ⟨single j i 1 • x✝², ⋯⟩) + fun i ↦ ⟨single j i 1 • x✝¹, ⋯⟩) x✝)
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
⊢ (expand p hp) ↑φ = ↑((MvPolynomial.expand p) φ)

Tactic:
by
  ext n
  simp only [MvPolynomial.coeff_coe]
  by_cases! h : ∀ i, p ∣ n i
  · obtain ⟨m, hm⟩ : ∃ m, p • m = n := ⟨n.mapRange (fun a ↦ a / p) (by simp),
      by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
    rw [← hm, coeff_expand_smul p hp _ _, φ.coeff_expand_smul _ hp, φ.coeff_coe]
  · obtain ⟨i, hi⟩ := h
    rw [coeff_expand_of_not_dvd p hp _ hi, MvPolynomial.coeff_expand_of_not_dvd _ hi]

Goal state after:
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
X✝ Y✝ : ModuleCat (Matrix ι ι R)
f✝ : X✝ ⟶ Y✝
⊢ (toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι).map f✝ ≫
      (toModuleCatFromModuleCatLinearEquiv R Y✝ i).symm.toModuleIso.hom =
    (toModuleCatFromModuleCatLinearEquiv R X✝ i).symm.toModuleIso.hom ≫ (𝟭 (ModuleCat (Matrix ι ι R))).map f✝

Tactic:
ext

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
X✝ Y✝ : ModuleCat (Matrix ι ι R)
f✝ : X✝ ⟶ Y✝
x✝ : ↑((toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι).obj X✝)
⊢ (ModuleCat.Hom.hom
        ((toModuleCat R i ⋙ ModuleCat.toMatrixModCat R ι).map f✝ ≫
          (toModuleCatFromModuleCatLinearEquiv R Y✝ i).symm.toModuleIso.hom))
      x✝ =
    (ModuleCat.Hom.hom
        ((toModuleCatFromModuleCatLinearEquiv R X✝ i).symm.toModuleIso.hom ≫ (𝟭 (ModuleCat (Matrix ι ι R))).map f✝))
      x✝
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
⊢ Valued.v x ≤ 1

Tactic:
← mem_adicCompletionIntegers

Goal state after:
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
hx : x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K) x
hf : f = (ratfuncAdicComplRingEquiv K) x
⊢ x ∈ adicCompletionIntegers K⟮X⟯ (idealX K)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ∑ x ∈ range (n + 1), (map f) ((monomial (single x (p ^ (n - x)))) (↑p ^ x)) = W_ S n

Tactic:
wittPolynomial

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ∑ x ∈ range (n + 1), (map f) ((monomial (single x (p ^ (n - x)))) (↑p ^ x)) =
    ∑ i ∈ range (n + 1), (monomial (single i (p ^ (n - i)))) (↑p ^ i)
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✝
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_2
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
⊢ (liftMonoidHom p (Perfection R p) R).symm
      (((liftMonoidHom p (Perfection (R ⧸ I) p) R) (teichmuller p I)).comp (mapMonoidHom p ↑(Ideal.Quotient.mk I))) =
    (liftMonoidHom p (Perfection R p) R).symm (MonoidHom.id (Perfection R p))

Tactic:
ext

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✝
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_2
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x✝ : Perfection R p
⊢ ((liftMonoidHom p (Perfection R p) R).symm
        (((liftMonoidHom p (Perfection (R ⧸ I) p) R) (teichmuller p I)).comp (mapMonoidHom p ↑(Ideal.Quotient.mk I))))
      x✝ =
    ((liftMonoidHom p (Perfection R p) R).symm (MonoidHom.id (Perfection R p))) x✝
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✝
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_2
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
⊢ (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)).symm
      ((mapMonoidHom p ↑(Ideal.Quotient.mk I)).comp ((liftMonoidHom p (Perfection (R ⧸ I) p) R) (teichmuller p I))) =
    (liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)).symm (MonoidHom.id (Perfection (R ⧸ I) p))

Tactic:
ext

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✝
p : ℕ
inst✝³ : Fact (Nat.Prime p)
R : Type u_2
inst✝² : CommRing R
I : Ideal R
inst✝¹ : CharP (R ⧸ I) p
inst✝ : IsAdicComplete I R
x✝ : Perfection (R ⧸ I) p
⊢ ((liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)).symm
        ((mapMonoidHom p ↑(Ideal.Quotient.mk I)).comp ((liftMonoidHom p (Perfection (R ⧸ I) p) R) (teichmuller p I))))
      x✝ =
    ((liftMonoidHom p (Perfection (R ⧸ I) p) (R ⧸ I)).symm (MonoidHom.id (Perfection (R ⧸ I) p))) x✝
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: case refine_2
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 : ℕ
⊢ φ n = wittStructureRat p Φ n

Tactic:
show φ n = bind₁ φ (bind₁ (W_ ℚ) (xInTermsOfW p ℚ n)) by
        rw [bind₁_wittPolynomial_xInTermsOfW p, bind₁_X_right]

Goal state after:
case refine_2
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₁ φ) ((bind₁ (W_ ℚ)) (xInTermsOfW p ℚ n)) = wittStructureRat p Φ n
Module: Mathlib.RingTheory.NoetherNormalization

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin n) k)
hi : I ≠ ⊤
⊢ ∃ s ≤ n, ∃ g, Function.Injective ⇑g ∧ g.IsIntegral

Tactic:
induction n with
  | zero =>
    refine ⟨0, le_rfl, Quotient.mkₐ k I, fun a b hab ↦ ?_,
      isIntegral_of_surjective _ (Quotient.mkₐ_surjective k I)⟩
    rw [Quotient.mkₐ_eq_mk, Ideal.Quotient.eq] at hab
    by_contra ne
    have eq := eq_C_of_isEmpty (a - b)
    have ne : coeff 0 (a - b) ≠ 0 := fun h ↦ h ▸ eq ▸ sub_ne_zero_of_ne ne <| map_zero _
    obtain ⟨c, _, eqr⟩ := isUnit_iff_exists.mp ne.isUnit
    have one : c • (a - b) = 1 := by
      rw [MvPolynomial.smul_eq_C_mul, eq, ← map_mul, eqr, MvPolynomial.C_1]
    exact hi ((eq_top_iff_one I).mpr (one ▸ I.smul_of_tower_mem c hab))
  | succ d hd =>
    by_cases eqi : I = 0
    · have bij : Function.Bijective (Quotient.mkₐ k I) :=
        (Quotient.mk_bijective_iff_eq_bot I).mpr eqi
      exact ⟨d + 1, le_rfl, _, bij.1, isIntegral_of_surjective _ bij.2⟩
    · obtain ⟨f, fi, fne⟩ := Submodule.exists_mem_ne_zero_of_ne_bot eqi
      set ϕ := kerLiftAlg <| hom2 f I
      have := Quotient.nontrivial_iff.mpr hi
      obtain ⟨s, _, g, injg, intg⟩ := hd (ker <| hom2 f I) (ker_ne_top <| hom2 f I)
      have comp : (kerLiftAlg (hom2 f I)).comp (Quotient.mkₐ k <| ker <| hom2 f I) = (hom2 f I) :=
        AlgHom.ext fun a ↦ by
          simp only [AlgHom.coe_comp, Quotient.mkₐ_eq_mk, Function.comp_apply, kerLiftAlg_mk]
      exact ⟨s, by lia, ϕ.comp g, (ϕ.coe_comp  g) ▸ (kerLiftAlg_injective _).comp injg,
        intg.trans _ _ <| (comp ▸ hom2_isIntegral f I fne fi).tower_top _ _⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittAdd p 0 = X (0, 0) + X (1, 0)

Tactic:
by
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittAdd, wittStructureRat, map_add, rename_X, xInTermsOfW_zero, map_X,
    wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
⊢ map (RingHom.id R) = RingHom.id (𝕎 R)

Tactic:
ext

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x✝ : 𝕎 R
n✝ : ℕ
⊢ ((map (RingHom.id R)) x✝).coeff n✝ = ((RingHom.id (𝕎 R)) x✝).coeff n✝
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
x : Perfection M p
⊢ (pthRootMonoidHom M p) ((fun x ↦ x ^ p) x) = x

Tactic:
ext

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
x : Perfection M p
n✝ : ℕ
⊢ (coeffMonoidHom M p n✝) ((pthRootMonoidHom M p) ((fun x ↦ x ^ p) x)) = (coeffMonoidHom M p n✝) x
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
x : Perfection M p
⊢ (fun x ↦ x ^ p) ((pthRootMonoidHom M p) x) = x

Tactic:
ext

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
x : Perfection M p
n✝ : ℕ
⊢ (coeffMonoidHom M p n✝) ((fun x ↦ x ^ p) ((pthRootMonoidHom M p) x)) = (coeffMonoidHom M p n✝) x
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
x : Perfection M p
⊢ (powMulEquiv (Perfection M p) p) ((pthRootMonoidHom M p) x) = x

Tactic:
ext

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
x : Perfection M p
n✝ : ℕ
⊢ (coeffMonoidHom M p n✝) ((powMulEquiv (Perfection M p) p) ((pthRootMonoidHom M p) x)) = (coeffMonoidHom M p n✝) x
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
⊢ (coeffMonoidHom N p 0).comp
      ((fun f ↦ { toFun := fun r ↦ ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }) f) =
    f

Tactic:
ext

Goal state after:
M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
x✝ : M
⊢ ((coeffMonoidHom N p 0).comp
        ((fun f ↦ { toFun := fun r ↦ ⟨fun n ↦ f ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ })
          f))
      x✝ =
    f x✝
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
x✝¹ x✝ : M →* N
⊢ { toFun := fun r ↦ ⟨fun n ↦ (x✝¹ * x✝) ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ } =
    { toFun := fun r ↦ ⟨fun n ↦ x✝¹ ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ } *
      { toFun := fun r ↦ ⟨fun n ↦ x✝ ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

Tactic:
ext

Goal state after:
M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
x✝² x✝¹ : M →* N
x✝ : M
n✝ : ℕ
⊢ (coeffMonoidHom N p n✝)
      ({ toFun := fun r ↦ ⟨fun n ↦ (x✝² * x✝¹) ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
        x✝) =
    (coeffMonoidHom N p n✝)
      (({ toFun := fun r ↦ ⟨fun n ↦ x✝² ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ } *
          { toFun := fun r ↦ ⟨fun n ↦ x✝¹ ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ })
        x✝)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝² : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
N : Type u_3
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
φ : M →* N
⊢ ⟨fun n ↦ φ ((coeffMonoidHom M p n) 1), ⋯⟩ = 1

Tactic:
ext

Goal state after:
M✝ : Type u_1
inst✝² : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
N : Type u_3
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
φ : M →* N
n✝ : ℕ
⊢ (coeffMonoidHom N p n✝) ⟨fun n ↦ φ ((coeffMonoidHom M p n) 1), ⋯⟩ = (coeffMonoidHom N p n✝) 1
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝² : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
N : Type u_3
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
φ : M →* N
x✝¹ x✝ : Perfection M p
⊢ ⟨fun n ↦ φ ((coeffMonoidHom M p n) (x✝¹ * x✝)), ⋯⟩ =
    ⟨fun n ↦ φ ((coeffMonoidHom M p n) x✝¹), ⋯⟩ * ⟨fun n ↦ φ ((coeffMonoidHom M p n) x✝), ⋯⟩

Tactic:
ext

Goal state after:
M✝ : Type u_1
inst✝² : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
N : Type u_3
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
φ : M →* N
x✝¹ x✝ : Perfection M p
n✝ : ℕ
⊢ (coeffMonoidHom N p n✝) ⟨fun n ↦ φ ((coeffMonoidHom M p n) (x✝¹ * x✝)), ⋯⟩ =
    (coeffMonoidHom N p n✝) (⟨fun n ↦ φ ((coeffMonoidHom M p n) x✝¹), ⋯⟩ * ⟨fun n ↦ φ ((coeffMonoidHom M p n) x✝), ⋯⟩)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ (pthRoot R p).comp (frobenius (Perfection R p) p) = RingHom.id (Perfection R p)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x✝ : Perfection R p
n✝ : ℕ
⊢ (coeff R p n✝) (((pthRoot R p).comp (frobenius (Perfection R p) p)) x✝) =
    (coeff R p n✝) ((RingHom.id (Perfection R p)) x✝)
Module: Mathlib.RingTheory.WittVector.Frobenius

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

Tactic:
add_right_inj,

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ C ↑p * X (n + 1) +
      -(C ↑p *
          (MvPolynomial.map (Int.castRingHom ℚ))
            (∑ i ∈ range n,
              ∑ j ∈ range (p ^ (n - i)),
                (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
                  C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))))) =
    C ↑p * X (n + 1) +
      ((∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) -
        (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
          C (⅟↑p ^ n))

Tactic:
add_right_inj,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ -(C ↑p *
        (MvPolynomial.map (Int.castRingHom ℚ))
          (∑ i ∈ range n,
            ∑ j ∈ range (p ^ (n - i)),
              (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
                C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1))))) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (x✝ + y✝).coeff = fun n ↦ peval (wittAdd p n) ![x✝.coeff, y✝.coeff]

Tactic:
ext

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
x✝ : ℕ
⊢ (x✝¹ + y✝).coeff x✝ = peval (wittAdd p x✝) ![x✝¹.coeff, y✝.coeff]
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (x✝ * y✝).coeff = fun n ↦ peval (wittMul p n) ![x✝.coeff, y✝.coeff]

Tactic:
ext

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝¹ y✝ : 𝕎 R✝
x✝ : ℕ
⊢ (x✝¹ * y✝).coeff x✝ = peval (wittMul p x✝) ![x✝¹.coeff, y✝.coeff]
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case pos
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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : v ↑p = 0
⊢ v ↑p ≤ v ↑p ^ (1 / ↑p) * v ↑p ^ (1 / ↑p)

Tactic:
rw [hvp]

Goal state after:
case pos
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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
hvp : v ↑p = 0
⊢ 0 ≤ 0 ^ (1 / ↑p) * 0 ^ (1 / ↑p)
Module: Mathlib.RingTheory.WittVector.Domain

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
⊢ ∃ n x', x'.coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] x'

Tactic:
have hex : ∃ k : ℕ, x.coeff k ≠ 0 := by
    by_contra! hall
    apply hx
    ext i
    simp only [hall, zero_coeff]
  let n := Nat.find hex
  use n, x.shift n
  refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩
  exact Nat.find_min hex hi

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ teichmullerFun p 1 = 1

Tactic:
by
    ext ⟨⟩
    · rw [one_coeff_zero]; rfl
    · rw [one_coeff_eq_of_pos _ _ _ (Nat.succ_pos _)]; rfl

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
hx : x ∈ ⨅ i, RingHom.ker (WittVector.truncate i)
⊢ x = 0

Tactic:
ext

Goal state after:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
hx : x ∈ ⨅ i, RingHom.ker (WittVector.truncate i)
n✝ : ℕ
⊢ x.coeff n✝ = WittVector.coeff 0 n✝
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
⊢ RingHom.ker constantCoeff = Ideal.span {↑p}

Tactic:
ext

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x✝ : 𝕎 k
⊢ x✝ ∈ RingHom.ker constantCoeff ↔ x✝ ∈ Ideal.span {↑p}
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
hind :
  (∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}) →
    ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n✝ n : ℕ
b c : ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
⊢ b = c

Tactic:
ext

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝ : CommRing R
α : Type u_2
x : α → 𝕎 R
a : α
S' : Finset α
ha : a ∉ S'
hind :
  (∀ (n : ℕ), Subsingleton ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}) →
    ∀ (n : ℕ), (∑ s ∈ S', x s).coeff n = ∑ s ∈ S', (x s).coeff n
h : ∀ (n : ℕ), Subsingleton ↑{r | r ∈ insert a S' ∧ (x r).coeff n ≠ 0}
n✝ n : ℕ
b c : ↑{r | r ∈ S' ∧ (x r).coeff n ≠ 0}
⊢ ↑b = ↑c
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
hF : Function.Surjective ⇑(_root_.frobenius (ModP R p) p)
this : Ideal.map (fontaineTheta R p) (span {↑p}) = 𝔭
x✝ : IsHausdorff (Ideal.map (fontaineTheta R p) (span {↑p})) R
⊢ ⇑(Ideal.Quotient.mk 𝔭) ∘ ⇑(fontaineTheta R p) = (fun x ↦ (PreTilt.coeff 0) x) ∘ fun x ↦ x.coeff 0

Tactic:
ext

Goal state after:
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
hF : Function.Surjective ⇑(_root_.frobenius (ModP R p) p)
this : Ideal.map (fontaineTheta R p) (span {↑p}) = 𝔭
x✝¹ : IsHausdorff (Ideal.map (fontaineTheta R p) (span {↑p})) R
x✝ : 𝕎 R♭
⊢ (⇑(Ideal.Quotient.mk 𝔭) ∘ ⇑(fontaineTheta R p)) x✝ = ((fun x ↦ (PreTilt.coeff 0) x) ∘ fun x ↦ x.coeff 0) x✝
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n✝ i : ℕ
hi : i < n✝ + 1
n : ℕ
x✝¹ x✝ :
  ↑{r | r ∈ Finset.Iic n✝ ∧ ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ r) (x.coeff r)) * ↑p ^ r).coeff n ≠ 0}
a : ℕ
left✝¹ : a ∈ Finset.Iic n✝
ha : ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ a) (x.coeff a)) * ↑p ^ a).coeff n ≠ 0
b : ℕ
left✝ : b ∈ Finset.Iic n✝
hb : ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ b) (x.coeff b)) * ↑p ^ b).coeff n ≠ 0
⊢ ⟨a, ⋯⟩ = ⟨b, ⋯⟩

Tactic:
ext

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n✝ i : ℕ
hi : i < n✝ + 1
n : ℕ
x✝¹ x✝ :
  ↑{r | r ∈ Finset.Iic n✝ ∧ ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ r) (x.coeff r)) * ↑p ^ r).coeff n ≠ 0}
a : ℕ
left✝¹ : a ∈ Finset.Iic n✝
ha : ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ a) (x.coeff a)) * ↑p ^ a).coeff n ≠ 0
b : ℕ
left✝ : b ∈ Finset.Iic n✝
hb : ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ b) (x.coeff b)) * ↑p ^ b).coeff n ≠ 0
⊢ ↑⟨a, ⋯⟩ = ↑⟨b, ⋯⟩