mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Etale R S
⊢ (TensorProduct.lmul' R).Flat

Tactic:
algebraize [Algebra.TensorProduct.lmul' R (S := S) |>.toRingHom]
    have : Etale R (S ⊗[R] S) := .comp _ S _
    have : Etale (S ⊗[R] S) S := .of_restrictScalars R _ _
    exact Smooth.flat (S ⊗[R] S) S

Goal state after:
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ h1Cotangentι ∘ₗ H1Cotangent.map (P.toExtendScalars.comp (defaultHom R S P)) =
    h1Cotangentι ∘ₗ
      H1Cotangent.map
        ((defaultHom P.Ring S P.extendScalars).comp
          ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom)

Tactic:
H1Cotangent.map_eq

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ h1Cotangentι ∘ₗ H1Cotangent.map ?g =
    h1Cotangentι ∘ₗ
      H1Cotangent.map
        ((defaultHom P.Ring S P.extendScalars).comp
          ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom)

case g
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (Generators.self R S).toExtension.Hom P.extendScalars
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (hI.dpow m✝ a * hI.dpow n✝ a) = ↑((m✝ + n✝).choose m✝) * f (hI.dpow (m✝ + n✝) a)

Tactic:
hI.mul_dpow ha,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (↑((m✝ + n✝).choose m✝) * hI.dpow (m✝ + n✝) a) = ↑((m✝ + n✝).choose m✝) * f (hI.dpow (m✝ + n✝) a)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers J
hm : hI.IsDPMorphism hquot f
n : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ hquot.dpow n (f a) = (dividedPowers hI hf hIJ hIf).dpow n (f a)

Tactic:
hm.2 a ha,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers J
hm : hI.IsDPMorphism hquot f
n : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (hI.dpow n a) = (dividedPowers hI hf hIJ hIf).dpow n (f a)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers J
hm : hI.IsDPMorphism hquot f
n : ℕ
x : B
hx : x ∈ J
⊢ hquot.dpow n x = (dividedPowers hI hf hIJ hIf).dpow n x

Tactic:
by
    obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
    rw [hm.2 a ha, dpow_apply hI hf hIJ hIf ha]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : 0 < x.orderTop
g : Γ
x✝¹ : ℕ × ℕ
x✝ : x✝¹ ∈ ⋯.toFinset
⊢ (PowerSeries.coeff x✝¹.2) b • (PowerSeries.coeff x✝¹.1) a • (x ^ x✝¹.1 * x ^ x✝¹.2).coeff g =
    ((PowerSeries.coeff ⟨x✝¹.1 + x✝¹.2, x✝¹⟩.snd.1) a * (PowerSeries.coeff ⟨x✝¹.1 + x✝¹.2, x✝¹⟩.snd.2) b) •
      (x ^ ⟨x✝¹.1 + x✝¹.2, x✝¹⟩.fst).coeff g

Tactic:
simp [smul_smul, mul_comm, pow_add]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x y : SummableFamily Γ R α
g : Γ
a : α
ha : (x a).coeff g + (y a).coeff g ≠ 0
⊢ (x a).coeff g ≠ 0 ∨ a ∈ Function.support fun a ↦ (y a).coeff g

Tactic:
Function.mem_support

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x y : SummableFamily Γ R α
g : Γ
a : α
ha : (x a).coeff g + (y a).coeff g ≠ 0
⊢ (x a).coeff g ≠ 0 ∨ (y a).coeff g ≠ 0
Module: Mathlib.RingTheory.HopfAlgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
ha : IsGroupLikeElem R a
⊢ a * (antipode R) a = 1

Tactic:
simpa [ha, -mul_antipode_lTensor_comul_apply] using mul_antipode_lTensor_comul_apply (R := R) a

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ -(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ) ∈ I

Tactic:
Ideal.neg_mem_iff

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
n : ℕ
ih : c n ≡ a₀ [SMOD I]
⊢ Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ ∈ I
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ -(Polynomial.eval (c (m + k)) f * (Polynomial.eval (c (m + k)) f')⁻¹ʳ) ∈ I ^ m

Tactic:
Ideal.neg_mem_iff

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ Polynomial.eval (c (m + k)) f * (Polynomial.eval (c (m + k)) f')⁻¹ʳ ∈ I ^ m
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 + -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ) ∈ I

Tactic:
Ideal.neg_mem_iff

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : c 0 + -(Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ) ≡ a [SMOD I]
⊢ Polynomial.eval (c 0) f * (Polynomial.eval (c 0) f')⁻¹ʳ ∈ I
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
⊢ F.IsUniform ∧ F • F = F → F.IsGabriel

Tactic:
· rintro ⟨h₁, h₂⟩
    refine { toIsUniform := h₁, gabriel_closed := ?_ }
    rintro I ⟨J, hJ, hcolon⟩
    exact h₂.le ⟨J, hJ, fun x hx ↦ ⟨I.colon {x}, hcolon x hx, by simp⟩⟩

Goal state after:
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
U : Set G
UOpen : IsOpen U
einU : 1 ∈ U
⊢ ∃ H, ↑H ⊆ U

Tactic:
by
  rcases ((Filter.HasBasis.mem_iff' ((nhds_basis_clopen (1 : G))) U).mp <|
    mem_nhds_iff.mpr (by use U)) with ⟨W, hW, h⟩
  rcases IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one hW.2 hW.1 with ⟨H, hH⟩
  exact ⟨H, fun _ a ↦ h (hH a)⟩

Goal state after:
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: case a
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
⊢ ↑H ≤ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}

Tactic:
exact le_sInf fun N hN ↦ hN.2

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
r : Ideal R
hrI : r ∈ N.associatedPrimes
hrs : ⟨r, hrI⟩ ∈ s₀
hy2 : y ∈ r
⊢ y ∈ ⋃ r ∈ s₀, ↑↑r

Tactic:
exact Set.mem_biUnion hrs hy2

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
hi : ¬m i = 0
⊢ IsWeightedHomogeneous w ((monomial (m - single i 1)) ↑(m i)) n'

Tactic:
convert! isWeightedHomogeneous_monomial ..

Goal state after:
case neg.convert_10
R : Type u_1
σ : Type u_2
M : Type u_3
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : AddCancelCommMonoid M
w : σ → M
n n' : M
i : σ
h : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h' : n' + w i = n
m : σ →₀ ℕ
hm : m ∈ {d | (weight w) d = n}
hi : ¬m i = 0
⊢ (weight w) (m - single i 1) = n'
Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity

Goal state before:
pp: case refine_4
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
φ : MvPolynomial σ R
inst✝ : Fintype σ
n : ℕ
w : σ → ℕ
h✝ : φ ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
r : R
p : MvPolynomial σ R
x✝ : p ∈ Submodule.span R ((fun m ↦ AddMonoidAlgebra.single m 1) '' {d | (weight w) d = n})
h : ∑ i, w i • (X i * (pderiv i) p) = n • p
⊢ ∑ i, w i • (X i * (pderiv i) (r • p)) = n • r • p

Tactic:
simp_rw [(pderiv _).map_smul, nsmul_eq_mul, mul_smul_comm, ← Finset.smul_sum, ← nsmul_eq_mul, h]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: case refine_1
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝¹ : Fin m
i✝ : ℕ
this : i✝ ≤ m - 1
i : ℕ
hi : i < m - 1
x✝ : i✝ ≤ i
ih : ∀ (hi : i + 1 < m), (accumulate n m) (invAccumulate n m s) ⟨i + 1, hi⟩ = s ⟨i + 1, hi⟩
him : i < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨i, him⟩ = s ⟨i, him⟩

Tactic:
← Nat.pred_eq_sub_one,

Goal state after:
case refine_1
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x✝¹ : Fin m
i✝ : ℕ
this : i✝ ≤ m - 1
i : ℕ
hi : i < m.pred
x✝ : i✝ ≤ i
ih : ∀ (hi : i + 1 < m), (accumulate n m) (invAccumulate n m s) ⟨i + 1, hi⟩ = s ⟨i + 1, hi⟩
him : i < m
⊢ (accumulate n m) (invAccumulate n m s) ⟨i, him⟩ = s ⟨i, him⟩
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem

Goal state before:
pp: σ : 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
⊢ ?m.112 ∈ p.support

Tactic:
rw [← hp (Equiv.swap i j), mem_support_iff, coeff_rename_mapDomain _ (Equiv.injective _)]

Goal state after:
σ : 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
⊢ coeff ?d p ≠ 0

case d
σ : 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
⊢ σ →₀ ℕ
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
⊢ IsUniformInducing ⇑(algebraMap K⟮X⟯ K⸨X⸩)

Tactic:
rw [isUniformInducing_iff, Filter.comap]

Goal state after:
K : Type u_2
inst✝ : Field K
⊢ { sets := {s | ∃ t ∈ uniformity K⸨X⸩, (fun x ↦ ((algebraMap K⟮X⟯ K⸨X⸩) x.1, (algebraMap K⟮X⟯ K⸨X⸩) x.2)) ⁻¹' t ⊆ s},
      univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } =
    uniformity K⟮X⟯
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * ∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i = (-1) ^ k * ∑ x ∈ powersetCard k univ, ↑k * (-1) ^ k * ∏ i ∈ x, X i

Tactic:
mul_comm (k : MvPolynomial σ R) ((-1) ^ k),

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
k : ℕ
⊢ ↑k * ∑ t ∈ powersetCard k univ, ∏ i ∈ t, X i = (-1) ^ k * ∑ x ∈ powersetCard k univ, (-1) ^ k * ↑k * ∏ i ∈ x, X i
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
⊢ Tendsto (⇑Valued.v)
    (Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a))
    (𝓝 (Valued.v a))

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : a = 0
⊢ Tendsto (⇑Valued.v)
    (Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a))
    (𝓝 (Valued.v a))

case neg
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : ¬a = 0
⊢ Tendsto (⇑Valued.v)
    (Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a))
    (𝓝 (Valued.v a))
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: case neg
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : ¬a = 0
⊢ Tendsto (⇑Valued.v)
    (Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a))
    (𝓝 (Valued.v a))

Tactic:
WithZeroTopology.tendsto_of_ne_zero ((Valuation.ne_zero_iff Valued.v).mpr ha),

Goal state after:
case neg
K : Type u_2
inst✝ : Field K
a : adicCompletion K⟮X⟯ (idealX K)
this : ∀ (s : Set (adicCompletion K⟮X⟯ (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v.restrict x < ↑γ} ⊆ s
ha : ¬a = 0
⊢ ∀ᶠ (x : K⟮X⟯) in
    Filter.comap (fun x ↦ { toCompletion := ↑((WithVal.equiv (valuation K⟮X⟯ (idealX K))).symm x) }) (𝓝 a),
    Valued.v x = Valued.v a
Module: Mathlib.RingTheory.MvPowerSeries.Restricted

Goal state before:
pp: case inr
M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
f g : M → S
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
this :
  ∀ {C : M → ℝ},
    (∀ (a b : M), C (a + b) = C a * C b) →
      Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0) →
        Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0) →
          0 ≤ C → Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)
hC' : ¬0 ≤ C
⊢ Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)

pp: M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
⊢ Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)

Tactic:
· rw [tendsto_zero_iff_norm_tendsto_zero]
    simpa using this (C := |C|) (by simp [hC]) (by simpa using hf.norm)
      (by simpa using hg.norm) (fun _ => by simp)

Goal state after:
M : Type u_3
S : Type u_4
inst✝³ : AddMonoid M
inst✝² : Finset.HasAntidiagonal M
inst✝¹ : NormedRing S
inst✝ : IsUltrametricDist S
f g : M → S
C : M → ℝ
hC : ∀ (a b : M), C (a + b) = C a * C b
hf : Tendsto (fun i ↦ ‖f i‖ * C i) cofinite (𝓝 0)
hg : Tendsto (fun i ↦ ‖g i‖ * C i) cofinite (𝓝 0)
hC' : 0 ≤ C
⊢ Tendsto (fun a ↦ ‖∑ p ∈ antidiagonal a, f p.1 * g p.2‖ * C a) cofinite (𝓝 0)
Module: Mathlib.RingTheory.LaurentSeries

Goal state before:
pp: K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) ∈ adicCompletionIntegers K⟮X⟯ (idealX K)

Tactic:
mem_adicCompletionIntegers,

Goal state after:
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
⊢ Valued.v ((LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F)) ≤ 1
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]
  ext i v
  cases i using Fin.cases <;> simp

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✝ : IsPrecomplete I R
x : Perfection (R ⧸ I) p
y : R
n : ℕ
h : (Ideal.Quotient.mk I) y = (coeff (R ⧸ I) p n) x
⊢ x.teichmullerFun ≡ y ^ p ^ n [SMOD I ^ (n + 1)]

Tactic:
by
  have := (exists_teichmullerFun x).choose_spec (n + 1)
  rw [smul_eq_mul, Ideal.mul_top] at this
  exact this.symm.trans <| .pow_pow_add_one (I.natCast_mem_of_charP_quotient p) (m := n) <| by
    simp [SModEq.idealQuotientMk, h]

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

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ (bind₁ (W_ R)) (xInTermsOfW p R n) = X n

Tactic:
induction n using Nat.strongRecOn with | ind n H => ?_

Goal state after:
case ind
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
H : ∀ m < n, (bind₁ (W_ R)) (xInTermsOfW p R m) = X m
⊢ (bind₁ (W_ R)) (xInTermsOfW p R n) = X n
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
n : ℕ
⊢ (x * y).coeff n = peval (wittMul p n) ![x.coeff, y.coeff]

Tactic:
by
  simp [(· * ·), Mul.mul, eval]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ verschiebung x = x * ↑p

Tactic:
rw [← frobenius_verschiebung, frobenius_zmodp]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
h : ∀ (R : Type u) [_Rcr : CommRing R] (x y : 𝕎 R) (n : ℕ), (ghostComponent n) (f x y) = (ghostComponent n) (g x y)
φ : ℕ → 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 × ℕ → ℤ
⊢ (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)

Tactic:
specialize h (ULift ℤ) (mk p fun i => ⟨x (0, i)⟩) (mk p fun i => ⟨x (1, i)⟩) k

Goal state after:
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 :
  (ghostComponent k) (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })) =
    (ghostComponent k) (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) }))
⊢ (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) =
    (eval₂Hom ((MvPolynomial.eval x).comp C) fun i ↦ (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
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 ^ (j + 1) * (↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n)) =
    C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) * C ↑p

Tactic:
← C_eq_coe_nat

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 ^ (j + 1) * (C ↑((p ^ (n - i)).choose (j + 1)) * (C ↑p ^ i * C ⅟↑p ^ n)) =
    C ((Int.castRingHom ℚ) ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) * C ↑p