mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
v.intValuationDef_if_neg hxy,

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors)) ≤
    max (v.intValuationDef x) (v.intValuationDef y)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
S₁ : Type u_5
S₂ : Type u_6
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : S₁ →+* S₂
p : MvPowerSeries σ R
⊢ (map g) ((map f) p) = (map (g.comp f)) p

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
S₁ : Type u_5
S₂ : Type u_6
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : S₁ →+* S₂
p : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff n) ((map g) ((map f) p)) = (coeff n) ((map (g.comp f)) p)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
⊢ (rescale b) ((rescale a) f) = (rescale (a * b)) f

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
a b : R
n : ℕ
⊢ (coeff n) ((rescale b) ((rescale a) f)) = (coeff n) ((rescale (a * b)) f)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
φ : R →+* S
r : R
f : R⟦X⟧
⊢ (rescale (φ r)) ((map φ) f) = (map φ) ((rescale r) f)

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
φ : R →+* S
r : R
f : R⟦X⟧
n : ℕ
⊢ (coeff n) ((rescale (φ r)) ((map φ) f)) = (coeff n) ((map φ) ((rescale r) f))
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
⊢ v.asIdeal ^ 2 < v.asIdeal

Tactic:
← Ideal.dvdNotUnit_iff_lt

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
⊢ DvdNotUnit v.asIdeal (v.asIdeal ^ 2)
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case inr.succ.inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : n' = 0
h'' : ¬(coeff 1) φ = (↑0 + 1) * (coeff 1) φ
⊢ False

Tactic:
norm_num at h''

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : Associates.mk v.asIdeal ≤ Associates.mk (Ideal.span {π})
notMem : ¬Associates.mk (v.asIdeal ^ 2) ≤ Associates.mk (Ideal.span {π})
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1

Tactic:
rw [← pow_one (Associates.mk v.asIdeal), Associates.prime_pow_dvd_iff_le hπ hv] at mem

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : 1 ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors
notMem : ¬Associates.mk (v.asIdeal ^ 2) ≤ Associates.mk (Ideal.span {π})
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors = 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
⊢ (coeff d) (f ^ n) = 0

Tactic:
coeff_pow

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
⊢ ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff (l i)) f = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
a b : R
hb : b ≠ 0
h : b ∈ v.asIdeal → a ∉ v.asIdeal
⊢ (valuation K v) (↑a / ↑b) ≤ 1 ↔ b ∉ v.asIdeal

Tactic:
by
  refine ⟨fun hv ↦ ?_, fun hb ↦ by
    simp [valuation_of_algebraMap, intValuation_eq_one_iff.2 hb, intValuation_le_one]⟩
  contrapose! hv
  have ha₀ : a ≠ 0 := fun _ ↦ by simp_all
  have hva : v.valuation K a ≠ 0 := (Valuation.ne_zero_iff _).2 (by simp [ha₀])
  have hvb : v.valuation K b ≠ 0 := (Valuation.ne_zero_iff _).2 (by simp [hb])
  rw [← WithZero.log_lt_log one_ne_zero ((Valuation.ne_zero_iff _).2 (by simp [ha₀, hb])),
    map_div₀, WithZero.log_div hva hvb, WithZero.log_one, Int.sub_pos,
    WithZero.log_lt_log hvb hva]
  simpa [valuation_of_algebraMap, intValuation_eq_one_iff.2 <| h hv, intValuation_lt_one_iff_mem]

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

Goal state before:
pp: case inr
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
φ : R⟦X⟧
hn : n > 0
⊢ (coeff 1) (φ ^ n) = ↑n * (coeff 1) φ * constantCoeff φ ^ (n - 1)

Tactic:
induction n with

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : R
φ : MvPowerSeries σ A
⊢ ((map (algebraMap R A)).comp C) a * φ = φ * ((map (algebraMap R A)).comp C) a

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : R
φ : MvPowerSeries σ A
n : σ →₀ ℕ
⊢ (coeff n) (((map (algebraMap R A)).comp C) a * φ) = (coeff n) (φ * ((map (algebraMap R A)).comp C) a)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ✝ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : R
σ : MvPowerSeries σ✝ A
⊢ a • σ = ((map (algebraMap R A)).comp C) a * σ

Tactic:
ext n

Goal state after:
σ✝ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : R
σ : MvPowerSeries σ✝ A
n : σ✝ →₀ ℕ
⊢ (coeff n) (a • σ) = (coeff n) (((map (algebraMap R A)).comp C) a * σ)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
⊢ n • weightedOrder w f ≤ weightedOrder w (f ^ n)

Tactic:
induction n with

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : ∀ (n : σ →₀ ℕ), (trunc' R n) f = (trunc' R n) g
⊢ f = g

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : ∀ (n : σ →₀ ℕ), (trunc' R n) f = (trunc' R n) g
n : σ →₀ ℕ
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : ∃ᶠ (m : σ →₀ ℕ) in atTop, (trunc' R m) f = (trunc' R m) g
⊢ f = g

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : ∃ᶠ (m : σ →₀ ℕ) in atTop, (trunc' R m) f = (trunc' R m) g
n : σ →₀ ℕ
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ (MonoidWithZeroHom.ofClass Valued.v).valueGroup = (MonoidWithZeroHom.ofClass (valuation K v)).valueGroup

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : (WithZero (Multiplicative ℤ))ˣ
⊢ n ∈ (MonoidWithZeroHom.ofClass Valued.v).valueGroup ↔ n ∈ (MonoidWithZeroHom.ofClass (valuation K v)).valueGroup
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case hp
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝⁴ : Field K
inst✝³ : CommSemiring S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
v : HeightOneSpectrum R
inst✝ : Algebra S K
r : S
⊢ IsClosed
    {a |
      (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r * a =
        a * (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r}

Tactic:
| hp =>

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case hp
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝⁴ : Field K
inst✝³ : CommSemiring S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
v : HeightOneSpectrum R
inst✝ : Algebra S K
r : S
⊢ IsClosed {a | r • a = (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r * a}

Tactic:
| hp =>

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

Goal state before:
pp: case inr
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
⊢ HasFiniteSupport fun i ↦ (coeff d) (∏ i ∈ i, f i)

Tactic:
apply (Finset.Iio i).powerset.finite_toSet.subset

Goal state after:
case inr
σ : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_5
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
d : σ →₀ ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
⊢ (support fun i ↦ (coeff d) (∏ i ∈ i, f i)) ⊆ ↑(Finset.Iio i).powerset
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
⊢ (v.intAdicAbv hb) r ≤ 1

Tactic:
simpa [intAdicAbv, intAdicAbvDef, toNNReal_le_one_iff hb] using intValuation_le_one v r

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ n • φ.order ≤ (φ ^ n).order

Tactic:
induction n with

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
⊢ X ^ f.order.toNat * f.divXPowOrder = f

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R⟦X⟧
n : ℕ
⊢ (coeff n) (X ^ f.order.toNat * f.divXPowOrder) = (coeff n) f
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ ↑n = emultiplicity X φ

Tactic:
rw [← hn, eq_comm]

Goal state after:
case inr.coe
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
⊢ emultiplicity X φ = ↑φ.order.toNat
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R⟦X⟧
⊢ IsUnit f → f.order = 0

Tactic:
by
  rintro ⟨⟨u, v, hu, hv⟩, hf⟩
  apply And.left
  rw [← add_eq_zero, ← hf, ← nonpos_iff_eq_zero, ← @order_one R _ _, ← hu]
  exact order_mul_ge _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ X.divXPowOrder = 1

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (coeff n) X.divXPowOrder = (coeff n) 1
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
⊢ HasFiniteSupport fun i ↦ (coeff n) (∏ i ∈ i, f i)

Tactic:
apply (Finset.Iio i).powerset.finite_toSet.subset

Goal state after:
case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
⊢ (support fun i ↦ (coeff n) (∏ i ∈ i, f i)) ⊆ ↑(Finset.Iio i).powerset
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
s : Finset ι
hs : ¬↑s ⊆ Set.Iio i
x : ι
hxs : x ∈ ↑s
hxi : i ≤ x
⊢ (f x).order ≤ ∑ i ∈ s, (f i).order

Tactic:
apply Finset.single_le_sum (by simp) hxs

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f = 0 ∨ g = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

Tactic:
rcases h with (h | h)

Goal state after:
case pos.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : f = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

case pos.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R⟦X⟧
h : g = 0
⊢ (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
⊢ (eval₂Hom φ a) p ∈ ↑I

Tactic:
coe_eval₂Hom,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
⊢ eval₂ φ a p ∈ ↑I
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: case e'_5
σ : Type u_1
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : UniformSpace R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
f : MvPowerSeries σ R
d : σ →₀ ℕ
⊢ (φ ((coeff d) f) * d.prod fun s e ↦ a s ^ e) = (⇑(eval₂Hom hφ ha) ∘ fun d ↦ (monomial d) ((coeff d) f)) d

Tactic:
simp only [Function.comp_apply, coe_eval₂Hom, ← MvPolynomial.coe_monomial,
      eval₂_coe, eval₂_monomial]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
r : R
⊢ (eval₂Hom ⋯ ha) (C r) = (algebraMap R S) r

Tactic:
coe_eval₂Hom,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ha : HasEval a
r : R
⊢ eval₂ (algebraMap R S) a (C r) = (algebraMap R S) r
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
f : ℕ → Bool
⊢ (fun n ↦ cantorFunctionAux c f (n + 1)) = fun n ↦ c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

Tactic:
ext n

Goal state after:
c : ℝ
f : ℕ → Bool
n : ℕ
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : σ → MvPowerSeries τ S
ha : HasSubst a
e : σ →₀ ℕ
r : R
⊢ subst a ((monomial e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n ↦ a s ^ n

Tactic:
rw [← coe_substAlgHom ha, substAlgHom_monomial]

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
⊢ (if hq : 1 < q then { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 1) 0, map_zero' := ⋯ }
    else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff 1)) =
    1

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
q n : ℕ
⊢ (if hq : 1 < q then { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 1) 0, map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff 1))
      n =
    1 n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
⊢ (if hq : 1 < q then
      { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f * g)) 0, map_zero' := ⋯ }
    else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f * g))) =
    (if hq : 1 < q then { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0, map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f)) *
      if hq : 1 < q then
        { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0, map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g)

Tactic:
ext n

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
⊢ (if hq : 1 < q then
        { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f * g)) 0, map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f * g)))
      n =
    ((if hq : 1 < q then
          { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0, map_zero' := ⋯ }
        else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f)) *
        if hq : 1 < q then
          { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0, map_zero' := ⋯ }
        else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: ⊢ #ℝ = 𝔠

Tactic:
apply le_antisymm
  · rw [Real.equivCauchy.cardinal_eq]
    apply mk_quotient_le.trans
    apply (mk_subtype_le _).trans_eq
    rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
  · convert! mk_le_of_injective (cantorFunction_injective _ _)
    · rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
    · exact 1 / 3
    · simp
    · norm_num

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

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
τ : Type u_4
S : Type u_5
inst✝ : CommRing S
a : σ → MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
f : MvPowerSeries σ R
⊢ (map h) (subst a f) = subst (fun i ↦ (map h) (a i)) ((map h) f)

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
τ : Type u_4
S : Type u_5
inst✝ : CommRing S
a : σ → MvPowerSeries τ R
ha : HasSubst a
h : R →+* S
f : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ (coeff n) ((map h) (subst a f)) = (coeff n) (subst (fun i ↦ (map h) (a i)) ((map h) f))
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
⊢ subst 0 f = (map (algebraMap R S)) (C (constantCoeff f))

Tactic:
ext n

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ (coeff n) (subst 0 f) = (coeff n) ((map (algebraMap R S)) (C (constantCoeff f)))
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ (coeff n) (subst 0 f) = (coeff n) ((map (algebraMap R S)) (C (constantCoeff f)))

Tactic:
coeff_subst (by simp [hasSubst_def]),

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : MvPowerSeries σ R
n : τ →₀ ℕ
⊢ ∑ᶠ (d : σ →₀ ℕ), (coeff d) f • (coeff n) (d.prod fun s e ↦ 0 s ^ e) =
    (coeff n) ((map (algebraMap R S)) (C (constantCoeff f)))
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
⊢ f * δ = f 1 • δ

Tactic:
ext n

Goal state after:
f : ℕ → ℂ
n : ℕ
⊢ (f * δ) n = (f 1 • δ) n