mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
⊢ ∀ (F : Filter K), Cauchy F → 𝓝 0 ⊓ F = ⊥ → Cauchy (map (fun x ↦ x⁻¹) F)

Tactic:
by
      rintro F hF h0
      have : ∃ γ₀ : (MonoidWithZeroHom.ValueGroup₀ (.ofClass hv.v))ˣ, ∃ M ∈ F,
          ∀ x ∈ M, (γ₀.1) ≤ v.restrict x := by
        rcases Filter.inf_eq_bot_iff.mp h0 with ⟨U, U_in, M, M_in, H⟩
        rcases Valued.mem_nhds_zero.mp U_in with ⟨γ₀, hU⟩
        exists γ₀, M, M_in
        intro x xM
        apply le_of_not_gt _
        intro hyp
        have : x ∈ U ∩ M := ⟨hU hyp, xM⟩
        rwa [H] at this
      rcases this with ⟨γ₀, M₀, M₀_in, H₀⟩
      rw [Valued.cauchy_iff] at hF ⊢
      refine ⟨hF.1.map _, ?_⟩
      replace hF := hF.2
      intro γ
      rcases hF (min (γ * γ₀ * γ₀) γ₀) with ⟨M₁, M₁_in, H₁⟩
      clear hF
      use (fun x : K => x⁻¹) '' (M₀ ∩ M₁)
      constructor
      · rw [mem_map]
        apply mem_of_superset (Filter.inter_mem M₀_in M₁_in)
        exact subset_preimage_image _ _
      · rintro _ ⟨x, ⟨x_in₀, x_in₁⟩, rfl⟩ _ ⟨y, ⟨_, y_in₁⟩, rfl⟩
        simp only
        specialize H₁ x x_in₁ y y_in₁
        replace x_in₀ := H₀ x x_in₀
        clear H₀
        apply Valuation.inversion_estimate
        · have : (v.restrict x) ≠ 0 := by
            intro h
            rw [h] at x_in₀
            simp at x_in₀
          exact (Valuation.ne_zero_iff _).mp this
        · refine lt_of_lt_of_le H₁ ?_
          grw [Units.min_val, mul_assoc, Units.val_mul, Units.val_mul, x_in₀]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : ⊤ = AddSubgroup.closure {x}
e : G ≃+o ↥⊤ := { toAddEquiv := AddSubsemigroup.topEquiv.symm, map_le_map_iff' := ⋯ }
e' : ↥⊤ ≃+o ↥(AddSubgroup.closure {x}) := { toAddEquiv := AddEquiv.subsemigroupCongr ⋯, map_le_map_iff' := ⋯ }
g : ↥⊤ ≃+o ℤ := { toAddEquiv := AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
g' : ↥(AddSubgroup.closure {1}) ≃+o ↥⊤ :=
  { toAddEquiv := AddEquiv.subsemigroupCongr int_orderAddMonoidIso_of_isLeast_pos._proof_2, map_le_map_iff' := ⋯ }
⊢ x = 0 ↔ 1 = 0

Tactic:
simp [h.left.ne']

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ MapsTo (fun x ↦ x + g) {x | 0 ≤ x} {x | g ≤ x}

Tactic:
· try intro
      simp [Function.onFun]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | 0 ≤ x}, ∀ b ∈ {x | 0 ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x + g) a b

Tactic:
· try intro
      simp [Function.onFun]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_3
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ MapsTo (fun x ↦ x - g) {x | g ≤ x} {x | 0 ≤ x}

Tactic:
· try intro
      simp [Function.onFun]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
this : ({x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ Nonempty (G ≃+o ℤ)
h : {x | 0 ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ ∀ a ∈ {x | g ≤ x}, ∀ b ∈ {x | g ≤ x}, a < b → Function.onFun (fun x1 x2 ↦ x1 < x2) (fun x ↦ x - g) a b

Tactic:
· try intro
      simp [Function.onFun]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
⊢ False

Tactic:
wlog! hy' : 0 < y generalizing y

Goal state after:
case pos.inr
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G), y ≠ 0 → 0 < y → False
hy' : y ≤ 0
⊢ False

G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
hy' : 0 < y
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff m) ((monomial n) a * φ) = if n ≤ m then a * (coeff (m - n)) φ else 0

Tactic:
by
  classical
  have :
    ∀ p ∈ antidiagonal m,
      coeff (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial n a) * coeff p.2 φ ≠ 0 → p.1 = n :=
    fun p _ hp => eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp)
  rw [coeff_mul, ← Finset.sum_filter_of_ne this, Finset.HasAntidiagonal.filter_fst_eq_antidiagonal
    _ n, Finset.sum_ite_index]
  simp only [Finset.sum_singleton, coeff_monomial_same, Finset.sum_empty]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
⊢ (monomial m) a * (monomial n) b = (monomial (m + n)) (a * b)

Tactic:
ext k

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
⊢ (coeff k) ((monomial m) a * (monomial n) b) = (coeff k) ((monomial (m + n)) (a * b))
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
⊢ (map f) (mk fun k ↦ Function.surjInv hf ((coeff k) g)) = g

Tactic:
ext k

Goal state after:
case h
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Surjective ⇑f
g : T⟦X⟧
k : ℕ
⊢ (coeff k) ((map f) (mk fun k ↦ Function.surjInv hf ((coeff k) g))) = (coeff k) g
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
⊢ u = v

Tactic:
ext k

Goal state after:
S : Type u_2
T : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring T
f : S →+* T
hf : Function.Injective ⇑f
u v : S⟦X⟧
huv : (map f) u = (map f) v
k : ℕ
⊢ (coeff k) u = (coeff k) v
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hsr : Ideal.span {r} ≠ 0
hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r})
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)) =
    exp (-↑(multiplicity v.asIdeal (Ideal.span {r})))

Tactic:
exp_inj,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hsr : Ideal.span {r} ≠ 0
hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r})
⊢ -↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors) =
    -↑(multiplicity v.asIdeal (Ideal.span {r}))
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : ↥(nonZeroDivisors R)
⊢ 0 < v.intValuation ↑x

Tactic:
rw [v.intValuation_if_neg (nonZeroDivisors.coe_ne_zero x)]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : ↥(nonZeroDivisors R)
⊢ 0 < exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑x})).factors))
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inl
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
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
obtain ⟨⟨n, d⟩, hnd⟩ := IsLocalization.surj v.asIdeal.primeCompl r

Goal state after:
case inl
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
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inr
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
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
obtain ⟨⟨n, d⟩, hnd⟩ := IsLocalization.surj v.asIdeal.primeCompl r

Goal state after:
case inr
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
x : K
r : ↥(valuationSubringAtPrime K v)
hr : (algebraMap (↥(valuationSubringAtPrime K v)) K) r = x⁻¹
n : R
d : ↥v.asIdeal.primeCompl
hnd :
  r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2 = (algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1
⊢ ∃ n d, x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
s : Finset ι
⊢ ∑ i ∈ s, weightedOrder w (f i) ≤ weightedOrder w (∏ i ∈ s, f i)

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih => grw [Finset.sum_cons ha, Finset.prod_cons ha, ih, le_weightedOrder_mul]

Goal state after:
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
x : adicCompletion K v
⊢ embedding ((valueGroupOrderIso K v) ((valuation K v).restrict x)) = embedding (Valued.v.restrict x.toCompletion)

Tactic:
embedding_valueGroupOrderIso,

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
x : adicCompletion K v
⊢ embedding ((valuation K v).restrict x) = embedding (Valued.v.restrict x.toCompletion)
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ (p.toSubring T hp).order ≤ p.order

pp: case refine_2
σ : Type u_1
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ p.order ≤ (p.toSubring T hp).order

Tactic:
· exact le_order fun d hd => by simp [coeff_of_lt_order hd, ← p.coeff_toSubring T hp]

Goal state after:
case refine_2
σ : Type u_1
R : Type u_3
inst✝ : Ring R
p : MvPowerSeries σ R
T : Subring R
hp : ∀ (n : σ →₀ ℕ), (coeff n) p ∈ T
⊢ p.order ≤ (p.toSubring T hp).order
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
H : IsTopologicallyNilpotent f
⊢ IsNilpotent (constantCoeff f)

Tactic:
replace H := H.map (continuous_constantCoeff R)

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
H : IsTopologicallyNilpotent (constantCoeff f)
⊢ IsNilpotent (constantCoeff f)
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
g : MvPowerSeries σ R
⊢ Tendsto (fun s ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : σ →₀ ℕ),
      Tendsto (fun s ↦ (coeff d) (∑ b ∈ s, f b)) (SummationFilter.unconditional ι).filter (𝓝 ((coeff d) g))

Tactic:
apply tendsto_iff_coeff_tendsto

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

Goal state before:
pp: case top
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : ∀ (i : ℕ), ↑i < ⊤ → (coeff i) φ = 0
⊢ ⊤ ≤ φ.order

Tactic:
| top =>

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

Goal state before:
pp: case top
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = ⊤ ↔ (∀ (i : ℕ), ↑i = ⊤ → (coeff i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → (coeff i) φ = 0

Tactic:
| top =>

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

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
⊢ eval₂ G s 0 = 0

Tactic:
eval₂_zero

Goal state after:
case zero
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
⊢ 0 = 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case inr.top
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
ho : φ.order = ⊤
⊢ ⊤ = emultiplicity X φ

Tactic:
| top =>

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

Goal state before:
pp: R : Type u_1
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
g : R⟦X⟧
⊢ Tendsto (fun s ↦ ∑ b ∈ s, f b) (SummationFilter.unconditional ι).filter (𝓝 g) ↔
    ∀ (d : ℕ), Tendsto (fun s ↦ (coeff d) (∑ b ∈ s, f b)) (SummationFilter.unconditional ι).filter (𝓝 ((coeff d) g))

Tactic:
apply tendsto_iff_coeff_tendsto

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

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

Tactic:
ext k

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
k : ℕ
⊢ (coeff k) (divXPowOrder 1) = (coeff k) 1
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 : σ → ℕ := ⋯
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := ⋯
D : Set (σ →₀ ℕ) := ⋯
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
⊢ ∀ c ∈ p.support, φ (MvPolynomial.coeff c p) * ∏ i ∈ c.support, a i ^ c i ∈ I

Tactic:
intro d _

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
d : σ →₀ ℕ
a✝ : d ∈ p.support
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I
Module: Mathlib.RingTheory.PowerSeries.Evaluation

Goal state before:
pp: S : Type u_2
inst✝² : CommRing S
inst✝¹ : TopologicalSpace S
inst✝ : IsLinearTopology S S
c x : S
hx : MvPowerSeries.HasEval fun x_1 ↦ x
⊢ MvPowerSeries.HasEval fun x_1 ↦ c * x

Tactic:
exact hx.mul_left _

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

Goal state before:
pp: σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝² : CommRing S
a : σ → MvPowerSeries τ S
inst✝¹ : TopologicalSpace S
inst✝ : DiscreteTopology S
⊢ HasSubst a ↔ HasEval a

Tactic:
by
  simp_rw [hasSubst_def, hasEval_def, coeff_zero_iff,
    isTopologicallyNilpotent_iff_constantCoeff_isNilpotent]

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case a
⊢ #ℝ ≤ 𝔠

pp: case a
⊢ 𝔠 ≤ #ℝ

Tactic:
· 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]

Goal state after:
case a
⊢ 𝔠 ≤ #ℝ
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
τ : Type u_3
⊢ HasSubst 0

Tactic:
hasSubst_iff

Goal state after:
R : Type u_2
inst✝ : CommRing R
τ : Type u_3
⊢ MvPowerSeries.HasSubst (Function.const Unit 0)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
ha : HasSubst a
f g : R⟦X⟧
⊢ subst a (f - g) = subst a f - subst a g

Tactic:
by
  rw [← coe_substAlgHom ha, map_sub]

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x : E
inst✝ : (𝓝[≠] 0).NeBot
⊢ egauge 𝕜 univ x = 0

Tactic:
rw [egauge_eq_zero_iff]

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x : E
inst✝ : (𝓝[≠] 0).NeBot
⊢ ∃ᶠ (c : 𝕜) in 𝓝 0, x ∈ c • univ
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
⊢ CauchySeq fun s ↦ ∏ b ∈ s, f b

Tactic:
CauchySeq,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
hf : ∀ (n : ℕ), ∀ᶠ (i : ι) in cofinite, (f i) n = 1 n
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
⊢ Cauchy (map (fun s ↦ ∏ b ∈ s, f b) atTop)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
⊢ (coeff (n + 1 + 1)) (subst (B + -(C ⅟((coeff 1) P) * C ((coeff (n + 1 + 1)) (subst B P)) * X ^ (n + 2))) P) = 0

Tactic:
rw [coeff_subst']

Goal state after:
case succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
⊢ ∑ᶠ (d : ℕ),
      (coeff d) P •
        (coeff (n + 1 + 1)) ((B + -(C ⅟((coeff 1) P) * C ((coeff (n + 1 + 1)) (subst B P)) * X ^ (n + 2))) ^ d) =
    0

case succ.succ.hb
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
⊢ HasSubst (B + -(C ⅟((coeff 1) P) * C ((coeff (n + 1 + 1)) (subst B P)) * X ^ (n + 2)))
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : t ⊆ u
hv : t ⊆ v
i : ι
hi : i ∈ u ∧ i ∉ t
⊢ i ∈ s

Tactic:
Set.Finite.mem_toFinset,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : t ⊆ u
hv : t ⊆ v
i : ι
hi : i ∈ u ∧ i ∉ sᶜ
⊢ i ∈ s
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hv : t ⊆ v
hu : ∀ i ∈ u \ t, i ∈ s
i : ι
hi : i ∈ v ∧ i ∉ t
⊢ i ∈ s

Tactic:
Set.Finite.mem_toFinset,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hv : t ⊆ v
hu : ∀ i ∈ u \ t, i ∈ s
i : ι
hi : i ∈ v ∧ i ∉ sᶜ
⊢ i ∈ s
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ ∑ᶠ (i : ℕ), (coeff i) P * (coeff (n + 1 + 1)) (B ^ i) = (coeff (n + 1 + 1)) (subst B P)

Tactic:
rw [coeff_subst']

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ ∑ᶠ (i : ℕ), (coeff i) P * (coeff (n + 1 + 1)) (B ^ i) = ∑ᶠ (d : ℕ), (coeff d) P • (coeff (n + 1 + 1)) (B ^ d)

case hb
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ HasSubst B
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case hb
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ HasSubst B

Tactic:
simp [HasSubst, ← PowerSeries.constantCoeff.eq_def, hB']

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ↑‖y‖₊ ≤ ↑r
⊢ ‖(fun x ↦ c • x) y‖ₑ / ↑r ≤ ‖c‖ₑ

Tactic:
NNReal.coe_le_coe

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ≥0
c : 𝕜
y : E
hy : ‖y‖₊ ≤ r
⊢ ‖(fun x ↦ c • x) y‖ₑ / ↑r ≤ ‖c‖ₑ