mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic ⟨i, him⟩)
⊢ supDegree (⇑toLex) ((monomial (∑ j ∈ t, fun₀ | j => 1)) 1) <
    supDegree (⇑toLex) ((monomial (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1)) 1)

Tactic:
← single_eq_monomial,

Goal state after:
case refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
hne : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic ⟨i, him⟩)
⊢ supDegree (⇑toLex) (single (∑ j ∈ t, fun₀ | j => 1) 1) < supDegree (⇑toLex) (single (∑ j ≤ ⟨i, him⟩, fun₀ | j => 1) 1)
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case hp'
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
⊢ ∀ (x : R), (∀ (i : n →₀ ℕ), x ∣ coeff i (sumSMulX c)) → IsUnit x

Tactic:
intro r

Goal state after:
case hp'
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc_nonempty : c.support.Nonempty
hc_gcd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
r : R
⊢ (∀ (i : n →₀ ℕ), r ∣ coeff i (sumSMulX c)) → IsUnit r
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ 0 < 1

Tactic:
;

Goal state after:
case refine_2.refine_2
R : Type u_3
m : ℕ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : t ∈ powersetCard (i + 1) univ
ht' : #t = #(Iic ⟨i, him⟩)
hne : ∃ x, x ∈ Iic ⟨i, him⟩ \ t
hkm : (Iic ⟨i, him⟩ \ t).min' hne ∈ Iic ⟨i, him⟩ ∧ (Iic ⟨i, him⟩ \ t).min' hne ∉ t
⊢ 0 < 1
Module: Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Goal state before:
pp: case isPrimitive
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := ⋯
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
⊢ ∀ (r : R), (∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d (sumSMulXSMulY c)) → IsUnit r

Tactic:
intro r

Goal state after:
case isPrimitive
n : Type u_1
R : Type u_2
inst✝¹ : CommRing R
c : n →₀ R
inst✝ : IsDomain R
hc : c.support.Nontrivial
h_dvd : ∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r
ι : n ↪ n ⊕ n →₀ ℕ := { toFun := fun i ↦ Finsupp.single (Sum.inl i) 1 + Finsupp.single (Sum.inr i) 1, inj' := ⋯ }
aux : sumSMulXSMulY c = AddMonoidAlgebra.ofCoeff (Finsupp.embDomain ι c)
hcoeff : ∀ (i : n), coeff (ι i) (sumSMulXSMulY c) = c i
hsupp : (sumSMulXSMulY c).support = Finset.map ι c.support
a : n
ha : a ∈ c.support
r : R
⊢ (∀ (d : n ⊕ n →₀ ℕ), r ∣ coeff d (sumSMulXSMulY c)) → IsUnit r
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
ht : (t.1.erase t.2, t.2) = t
⊢ False

Tactic:
;

Goal state after:
case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
ht : (t.1.erase t.2, t.2) = t
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
ht : (t.1.erase t.2, t.2) = t
⊢ False

Tactic:
;

Goal state after:
case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
ht : (t.1.erase t.2, t.2) = t
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
ht : (cons t.2 t.1 h1, t.2) = t
⊢ False

Tactic:
;

Goal state after:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
ht : (cons t.2 t.1 h1, t.2) = t
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1✝ : t.2 ∉ t.1
h1 : (cons t.2 t.1 h1✝, t.2).2 ∉ (cons t.2 t.1 h1✝, t.2).1
ht : (cons t.2 t.1 h1✝, t.2) = t
⊢ False

Tactic:
;

Goal state after:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1✝ : t.2 ∉ t.1
h1 : (cons t.2 t.1 h1✝, t.2).2 ∉ (cons t.2 t.1 h1✝, t.2).1
ht : (cons t.2 t.1 h1✝, t.2) = t
⊢ False
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case inr.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
k : σ
hk : (fun x1 x2 ↦ x1 < x2) k i
⊢ (ofLex (p.support.sup ⇑toLex)) k = (ofLex (p.coeff.support.sup ⇑toLex)) k

Tactic:
;

Goal state after:
case inr.refine_1
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
p : MvPolynomial σ R
hp : p.IsSymmetric
h0 : p ≠ 0
i j : σ
hle : i ≤ j
hlt : (ofLex (supDegree (⇑toLex) p)) i < (ofLex (supDegree (⇑toLex) p)) j
k : σ
hk : (fun x1 x2 ↦ x1 < x2) k i
⊢ (ofLex (p.support.sup ⇑toLex)) k = (ofLex (p.coeff.support.sup ⇑toLex)) k
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x : K⟮X⟯
hx : Valued.v x = embedding ↑d
⊢ ¬(MonoidWithZeroHom.ofClass Valued.v) x = 0

Tactic:
;

Goal state after:
K : Type u_2
inst✝ : Field K
S : Set (K⟮X⟯ × K⟮X⟯)
T : Set (K⸨X⸩ × K⸨X⸩)
pre_T : (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' T ⊆ S
R : Set K⸨X⸩
hR : R ∈ nhds 0
pre_R : (fun x ↦ x.2 - x.1) ⁻¹' R ⊆ T
d : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
hd : {y | Valued.v.restrict (y - 0) < ↑d} ⊆ R
x : K⟮X⟯
hx : Valued.v x = embedding ↑d
⊢ ¬(MonoidWithZeroHom.ofClass Valued.v) x = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ antidiagonal k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
p : Finset σ × σ
hp : #p.1 = a.1
⊢ #p.1 < k

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : ℕ × ℕ
ha : a ∈ {a ∈ antidiagonal k | a.1 < k}
f : Finset σ × σ → MvPolynomial σ R
p : Finset σ × σ
hp : #p.1 = a.1
⊢ #p.1 < k
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a✝ : Finset σ × σ
⊢ a✝ ∈
      {x ∈ pairs σ k |
        match x with
        | (s, snd) => #s < k} ↔
    a✝ ∈ (range k).disjiUnion (fun x ↦ powersetCard x univ) ⋯ ×ˢ univ

Tactic:
;

Goal state after:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a✝ : Finset σ × σ
⊢ a✝ ∈
      {x ∈ pairs σ k |
        match x with
        | (s, snd) => #s < k} ↔
    a✝ ∈ (range k).disjiUnion (fun x ↦ powersetCard x univ) ⋯ ×ˢ univ
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case C
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
r : R
⊢ (algebraMap R ↥(symmetricSubalgebra (Fin m) R)) r ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
;

Goal state after:
case C
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
r : R
⊢ (algebraMap R ↥(symmetricSubalgebra (Fin m) R)) r ∈ (esymmAlgHom (Fin m) R n).range
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case add
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p q : MvPolynomial (Fin m) R
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
hq : (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) p + (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
;

Goal state after:
case add
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p q : MvPolynomial (Fin m) R
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
hq : (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) p + (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range
Module: Mathlib.RingTheory.Morita.Matrix

Goal state before:
pp: R : Type u
ι : Type v
inst✝⁶ : Ring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
i✝ j✝ : ι
⊢ ((diagonal fun x ↦ r) * single i i 1) i✝ j✝ = (single i i 1 * diagonal fun x ↦ r) i✝ j✝

Tactic:
;

Goal state after:
R : Type u
ι : Type v
inst✝⁶ : Ring R
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module (Matrix ι ι R) M
inst✝¹ : Module R M
inst✝ : IsScalarTower R (Matrix ι ι R) M
i : ι
r : R
x : M
i✝ j✝ : ι
⊢ ((diagonal fun x ↦ r) * single i i 1) i✝ j✝ = (single i i 1 * diagonal fun x ↦ r) i✝ j✝
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)
this : Module R ↑M := Module.compHom (↑M) (Matrix.scalar ι)
r : R
m : Matrix ι ι R
x : ↑M
⊢ (r • m) • x = (Matrix.scalar ι) r • m • x

Tactic:
← mul_smul,

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
this : Module R ↑M := Module.compHom (↑M) (Matrix.scalar ι)
r : R
m : Matrix ι ι R
x : ↑M
⊢ (r • m) • x = ((Matrix.scalar ι) r * m) • x
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
i : σ
⊢ (p • Finsupp.mapRange (fun a ↦ a / p) ⋯ d) i = d i

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPowerSeries σ R
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : ↑(Finsupp.degree d) < p • φ.order
h : ∀ (i : σ), p ∣ d i
i : σ
⊢ (p • Finsupp.mapRange (fun a ↦ a / p) ⋯ d) i = d i
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
⊢ (0, k).1 + (0, k).2 = k ∧ (0, k).1 < k ∧ ¬0 < (0, k).1

Tactic:
;

Goal state after:
σ : Type u_1
inst✝¹ : Fintype σ
R : Type u_2
inst✝ : CommRing R
k : ℕ
h : 0 < k
hesymm :
  ↑k * esymm σ R k =
    (-1) ^ (k + 1) *
      (∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2 +
        ∑ x ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < x.1, (-1) ^ x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides✝ :
  ↑k * esymm σ R k -
      (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    (-1) ^ (k + 1) * ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  (-1) ^ (k + 1) * ↑k * esymm σ R k -
      ∑ a ∈ {a ∈ antidiagonal k | a.1 < k} with 0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ antidiagonal k with a.1 < k ∧ ¬0 < a.1, (-1) ^ a.1 * esymm σ R a.1 * psum σ R a.2
⊢ (0, k).1 + (0, k).2 = k ∧ (0, k).1 < k ∧ ¬0 < (0, k).1
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
x✝ : ι
⊢ ↑⟨single j x✝ 1 • (x✝² + x✝¹), ⋯⟩ = ↑(((fun i ↦ ⟨single j i 1 • x✝², ⋯⟩) + fun i ↦ ⟨single j i 1 • x✝¹, ⋯⟩) x✝)

Tactic:
;

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.Morita.Matrix

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

Tactic:
have := MatrixModCat.isScalarTower_toModuleCat R M

Goal state after:
R : Type u
ι : Type v
inst✝² : Ring R
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : ModuleCat (Matrix ι ι R)
j : ι
x : Matrix ι ι R
m : ↑M
i : ι
this✝ : Module R ↑M := Module.compHom (↑M) (scalar ι)
this : IsScalarTower R (Matrix ι ι R) ↑M
⊢ ↑⟨single j i 1 • x • m, ⋯⟩ = ↑(((RingHom.id (Matrix ι ι R)) x • fun i ↦ ⟨single j i 1 • m, ⋯⟩) i)
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
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
i : σ
⊢ (p • Finsupp.mapRange (fun a ↦ a / p) ⋯ n) i = n i

Tactic:
;

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : MvPolynomial σ R
n : σ →₀ ℕ
h : ∀ (i : σ), p ∣ n i
i : σ
⊢ (p • Finsupp.mapRange (fun a ↦ a / p) ⋯ n) i = n i
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
i : σ
⊢ (p • Finsupp.mapRange (fun a ↦ a / p) ⋯ d) i = d i

Tactic:
;

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
i : σ
⊢ (p • Finsupp.mapRange (fun a ↦ a / p) ⋯ d) i = d i
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, m i > n i

Tactic:
by
          by_contra! hc
          exact h_le (Finsupp.coe_le_coe.mp hc)

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ 0 ≤ ‖(coeff n) (f + g)‖ * ∏ a ∈ n.support, |c a| ^ n a

Tactic:
;

Goal state after:
case refine_1
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ 0 ≤ ‖(coeff n) (f + g)‖ * ∏ a ∈ n.support, |c a| ^ n a
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ 0 ≤ ∏ a ∈ n.support, |c a| ^ n a

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : NormedRing R
σ : Type u_2
c : σ → ℝ
f g : MvPowerSeries σ R
hf : Tendsto (fun t ↦ ‖(coeff t) f‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
hg : Tendsto (fun t ↦ ‖(coeff t) g‖ * t.prod fun x1 x2 ↦ |c| x1 ^ x2) cofinite (𝓝 0)
n : σ →₀ ℕ
⊢ 0 ≤ ∏ a ∈ n.support, |c a| ^ n a
Module: Mathlib.RingTheory.MvPowerSeries.Expand

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((expand p hp) ((map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f))) =
    (map (iterateFrobenius R p (1 + k))) ((expand (p * p ^ k) ⋯) f)

Tactic:
iterateFrobenius_add,

Goal state after:
case succ
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p : ℕ
hp : p ≠ 0
inst✝ : ExpChar R p
f : MvPowerSeries σ R
k : ℕ
n_ih : (map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f) = f ^ p ^ k
⊢ (map (frobenius R p)) ((expand p hp) ((map (iterateFrobenius R p k)) ((expand (p ^ k) ⋯) f))) =
    (map ((iterateFrobenius R p 1).comp (iterateFrobenius R p k))) ((expand (p * p ^ k) ⋯) f)
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case h
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
hp : NeZero p
inst✝ : CharZero R
n : ℕ
this : ∀ (i : ℕ), ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars = {i}
⊢ Pairwise (Function.onFun Disjoint fun i ↦ ((monomial (single i (p ^ (n - i)))) (↑p ^ i)).vars)

Tactic:
simp only [this]
    intro a b h
    apply disjoint_singleton_left.mpr
    rwa [mem_singleton]

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✝
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✝

Tactic:
;

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
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✝

Tactic:
;

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: 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:
;

Goal state after:
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)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: 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)) Φ

Tactic:
;

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.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * C (↑p ^ n) =
    (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    (bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)

Tactic:
;

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
n : ℕ
this :
  (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n) * C (↑p ^ n) =
    (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i))
⊢ (bind₁ fun k ↦ (bind₁ fun i ↦ (rename (Prod.mk i)) (W_ ℚ k)) Φ)
      (X n - ∑ i ∈ Finset.range n, C (↑p ^ i) * xInTermsOfW p ℚ i ^ p ^ (n - i)) =
    (bind₁ fun b ↦ (rename fun i ↦ (b, i)) (W_ ℚ n)) Φ -
      ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
Module: Mathlib.RingTheory.WittVector.StructurePolynomial

Goal state before:
pp: p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun i ↦ (expand p) ((rename (Prod.mk i)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) =
    (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    (bind₁ fun i ↦ (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)

Tactic:
;

Goal state after:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
IH :
  ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m
key :
  (bind₁ fun i ↦ (expand p) ((rename (Prod.mk i)) (W_ ℚ n))) ((map (Int.castRingHom ℚ)) Φ) =
    (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n)
⊢ (bind₁ fun i ↦ (expand p) (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i)) (W_ ℚ n) =
    (bind₁ fun i ↦ (expand p) ((map (Int.castRingHom ℚ)) (wittStructureInt p Φ i))) (W_ ℚ n)