mathlib-initiative/mathlib-tactics huggingface dataset:
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 + (Ideal.Quotient.mk (Ideal.span {↑p})) s = 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r + (Ideal.Quotient.mk (Ideal.span {↑p})) s) ≤
    max (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r))
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s))

Tactic:
rw [← map_add (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢

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 (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) r))
      (preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) s))
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 : ℕ
x : ModP O p
⊢ v ↑p < preVal K v O p x ↔ x ≠ 0

Tactic:
refine ⟨by aesop, fun h => lt_of_not_ge fun hp => h ?_⟩
  obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
  rw [preVal_mk hv h, ← map_natCast (algebraMap O K) p, hv.le_iff_dvd] at hp
  · rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]; exact hp

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

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ ∃ c, x = c * ↑p

Tactic:
use (frobeniusEquiv p k).symm (x.shift 1)

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 : x.coeff 0 = 0
⊢ x = (frobeniusEquiv p k).symm (x.shift 1) * ↑p
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
x : 𝕎 k
h : x.coeff 0 = 0
⊢ ∀ i < 1, x.coeff i = 0

Tactic:
by simp [h]

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

Goal state before:
pp: 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
g : ℕ → R := fun x ↦ 0
⊢ x.coeff i =
    ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i).coeff i +
      ∑ x_1 ∈ Finset.Iic n \ {i},
        ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ x_1) (x.coeff x_1)) * ↑p ^ x_1).coeff i

Tactic:
Finset.sum_congr rfl (g := g)

Goal state after:
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
g : ℕ → R := fun x ↦ 0
⊢ x.coeff i =
    ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i).coeff i + (Finset.Iic n \ {i}).sum g

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
g : ℕ → R := fun x ↦ 0
⊢ ∀ x_1 ∈ Finset.Iic n \ {i},
    ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ x_1) (x.coeff x_1)) * ↑p ^ x_1).coeff i = g x_1
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * X ^ (n + 1) = X ^ (n + 2)

Tactic:
pow_add X (n + 1) 1,

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * X ^ (n + 1) = X ^ (n + 1) * X ^ 1
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝³ : CommRing R
inst✝² : CharP R p
inst✝¹ : PerfectRing R p
S : Type u_2
inst✝ : CommRing S
f g : 𝕎 R →+* S
h : ∀ (x : R), f ((teichmuller p) x) = g ((teichmuller p) x)
n : ℕ
hn : ↑p ^ n = 0
x c : 𝕎 R
hc : x - ∑ i ≤ n, (teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i)) * ↑p ^ i = ↑p ^ (n + 1) * c
⊢ ∑ i ≤ n, f ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i))) * ↑p ^ i =
    ∑ i ≤ n, g ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ i) (x.coeff i))) * ↑p ^ i

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
⊢ (⋃ x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}, {y | x = y + y⁻¹ ∨ y = 0}).Finite

Tactic:
refine h.biUnion fun x _ => ?_

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ {y | x = y + y⁻¹ ∨ y = 0}.Finite
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ (preHilbertPoly F d k).coeff d = (↑d !)⁻¹

Tactic:
delta preHilbertPoly

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k : ℕ
⊢ ((↑d !)⁻¹ • (ascPochhammer F d).comp (X - C ↑k + 1)).coeff d = (↑d !)⁻¹
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : 0 < x
⊢ (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder = (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
simp_all only [mul_eq_mul_right_iff]

Goal state after:
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h : 0 < x
⊢ (coeff x) (X * largeSchroderSeries) = (x - 1).largeSchroder ∨ (n - x).largeSchroder = 0
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
⊢ (rTensor N P₁.subtype) u₁ = (rTensor N P₁.subtype) u'₁

Tactic:
hu₁,

Goal state after:
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t t' : ↥A ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A.val.toLinearMap) t'
P : Submodule R ↥A
hP : P.FG
u : ↥P ⊗[R] N
hu : (rTensor N P.subtype) u = t
P' : Submodule R ↥A
hP' : P'.FG
u' : ↥P' ⊗[R] N
hu' : (rTensor N P'.subtype) u' = t'
P₁ : Submodule R S := Submodule.map (Subalgebra.toSubmodule A).subtype (P ⊔ P')
hP₁ : P₁.FG
j : ↥P →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
j' : ↥P' →ₗ[R] ↥P₁ := (Subalgebra.toSubmodule A).subtype.restrict ⋯
u₁ : ↥P₁ ⊗[R] N := (rTensor N j) u
hu₁ : u₁ = (rTensor N j) u
u'₁ : ↥P₁ ⊗[R] N := (rTensor N j') u'
hu'₁ : u'₁ = (rTensor N j') u'
⊢ (rTensor N P₁.subtype) ((rTensor N j) u) = (rTensor N P₁.subtype) u'₁
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ 1 < ↑(radical z.natAbs) ↔ 1 < z.natAbs

Tactic:
Nat.one_lt_cast

Goal state after:
z : ℤ
⊢ 1 < radical z.natAbs ↔ 1 < z.natAbs
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := ⋯
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) := ⋯
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := ⋯
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ⋯
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
⊢ Function.Surjective ⇑((Ideal.span {x} • ⊤).mkQ ∘ₗ g)

Tactic:
rwa [Submodule.ideal_span_singleton_smul x ⊤, hg]

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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (rTensor M (Subalgebra.inclusion hA'B').toLinearMap) u' =
    (rTensor M (Subalgebra.inclusion ⋯).toLinearMap) ((rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u')

Tactic:
simp only [← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap]

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (rTensor M (Subalgebra.inclusion hA'B').toLinearMap) u' =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hA'B)).toLinearMap) u'
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
this : ∀ (k i : ℕ), (coeff i) q ∈ I ^ k
i k : ℕ
⊢ (coeff i) q ∈ I ^ k

Tactic:
exact this _ _

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsAdicComplete I A
r : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ H.div ↑r = 0

Tactic:
by
  obtain ⟨h1, h2⟩ := H.isWeierstrassDivisionAt_div_mod r
  exact (H.eq_of_mul_add_eq_mul_add (q := H.div r) (q' := 0) h1 hr (by simpa using h2.symm)).1

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0

Tactic:
rw [coeff_of_lt_order p.1 ?_]

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ 0 * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0

A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ ↑p.1 < ((map (IsLocalRing.residue A)) g).order
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g g' : A⟦X⟧
f : A[X]
h✝ : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
h : (map (IsLocalRing.residue A)) g = 0
⊢ (map (IsLocalRing.residue A)) (g * g') = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g g' : A⟦X⟧
f : A[X]
h✝ : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
h : (map (IsLocalRing.residue A)) g' = 0
⊢ (map (IsLocalRing.residue A)) (g * g') = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
h : (map (IsLocalRing.residue A)) g = 0
⊢ (map (IsLocalRing.residue A)) (g * g') = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
h : (map (IsLocalRing.residue A)) g' = 0
⊢ (map (IsLocalRing.residue A)) (g * g') = 0

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
⊢ (g * g').weierstrassDistinguished hg = g.weierstrassDistinguished ⋯ * g'.weierstrassDistinguished ⋯

Tactic:
have H'' := (g * g').isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
H'' : (g * g').IsWeierstrassFactorization ((g * g').weierstrassDistinguished hg) ((g * g').weierstrassUnit hg)
⊢ (g * g').weierstrassDistinguished hg = g.weierstrassDistinguished ⋯ * g'.weierstrassDistinguished ⋯
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯

Tactic:
have H'' := (g * g').isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
H'' : (g * g').IsWeierstrassFactorization ((g * g').weierstrassDistinguished hg) ((g * g').weierstrassUnit hg)
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ ((fromPadicInt p).comp (toPadicInt p)) x = (RingHom.id (𝕎 (ZMod p))) x

Tactic:
rw [fromPadicInt_comp_toPadicInt]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * r' = q' * b
h : q' = 0
⊢ q'.coeff 0 = 0

Tactic:
by simp [h]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
hq0 : q ≠ 0
h : r = 0
⊢ Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = 0

Tactic:
by simp [h]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (polyOfInterest p n).vars =
    (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars

Tactic:
polyOfInterest,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
this : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
          X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
        X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))).vars =
    (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this : Nontrivial V
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
obtain ⟨x, hx⟩ : ∃ x : V, x ≠ 0 := exists_ne 0

Goal state after:
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y ↦
    f₀ fun a ↦
      Subtype.casesOn a fun a ha ↦
        Function.uncurry ![x, y]
          (let S := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
⊢ (fun a ↦ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑a).1 ⟨(↑a).2, ⋯⟩) =
    Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] ∘ Subtype.val

Tactic:
ext a

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
  fun x y ↦
    f₀ fun a ↦
      Subtype.casesOn a fun a ha ↦
        Function.uncurry ![x, y]
          (let S := {a | a.2 = n ∨ a.2 < n};
          have ha' := ⋯;
          (a.1, ⟨a.2, ⋯⟩))
x y : 𝕎 k
a : ↥(univ ×ˢ range (n + 1))
⊢ ![truncateFun (n + 1) x, truncateFun (n + 1) y] (↑a).1 ⟨(↑a).2, ⋯⟩ =
    (Function.uncurry ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] ∘ Subtype.val) a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : cof α < ℵ₀
⊢ IsClub (⋂₀ s)

pp: case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
⊢ IsClub (⋂₀ s)

Tactic:
· exact .sInter_of_cof_le_one (cof_lt_aleph0_iff.1 hα) hs

Goal state after:
case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
⊢ IsClub (⋂₀ s)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hs : ∀ x ∈ s, IsClub x
hα : ℵ₀ < cof α
⊢ #↑s ≤ ℵ₀

Tactic:
le_aleph0_iff_set_countable

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hs : ∀ x ∈ s, IsClub x
hα : ℵ₀ < cof α
⊢ s.Countable
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: ⊢ (∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α) ↔ univ.{v, u + 1} < univ.{u, v + 1}

Tactic:
refine ⟨fun ⟨α, le⟩ ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
x✝ : ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
α : Type u
le : univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
⊢ univ.{v, u + 1} < univ.{u, v + 1}

case refine_2
h : univ.{v, u + 1} < univ.{u, v + 1}
⊢ ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α