mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ x ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.1, (coeff x.snd.1) φ₁ * (coeff x.snd.2) φ₂ * (coeff x.fst.2) φ₃ =
    ∑ x ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.2,
      (coeff x.fst.1) φ₁ * ((coeff x.snd.1) φ₂ * (coeff x.snd.2) φ₃)

Tactic:
apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩)

Goal state after:
case hi
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.1,
    (match a with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩) ∈
      (antidiagonal n).sigma fun a ↦ antidiagonal a.2

case hj
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.2,
    (match a with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩) ∈
      (antidiagonal n).sigma fun a ↦ antidiagonal a.1

case left_neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.1,
    (match
        match a with
        | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩ with
      | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩) =
      a

case right_neg
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.2,
    (match
        match a with
        | ⟨(i, _j), (k, l)⟩ => ⟨(i + k, l), (i, k)⟩ with
      | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩) =
      a

case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ a ∈ (antidiagonal n).sigma fun a ↦ antidiagonal a.1,
    (coeff a.snd.1) φ₁ * (coeff a.snd.2) φ₂ * (coeff a.fst.2) φ₃ =
      (coeff
            (match a with
                | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).fst.1)
          φ₁ *
        ((coeff
              (match a with
                  | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).snd.1)
            φ₂ *
          (coeff
              (match a with
                  | ⟨(_i, j), (k, l)⟩ => ⟨(k, l + j), (l, j)⟩).snd.2)
            φ₃)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : x = 0
⊢ (if x * y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x * y})).factors))) =
    (if x = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors))) *
      if y = 0 then 0 else exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))

Tactic:
rw [hx, zero_mul, if_pos rfl, zero_mul]

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

Goal state before:
pp: case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
ih : X s ^ n = (monomial (single s n)) 1
⊢ (monomial (single s n)) 1 * (monomial (single s 1)) 1 = (monomial (single s n + single s 1)) 1

Tactic:
monomial_mul_monomial,

Goal state after:
case succ
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
ih : X s ^ n = (monomial (single s n)) 1
⊢ (monomial (single s n + single s 1)) (1 * 1) = (monomial (single s n + single s 1)) 1
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos.h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : (single s n, m - single s n) ∉ antidiagonal m
⊢ False

Tactic:
apply hni

Goal state after:
case pos.h₁
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
hni : (single s n, m - single s n) ∉ antidiagonal m
⊢ (single s n, m - single s n) ∈ antidiagonal m
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
ha0 : embedding a ≠ embedding 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h0' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : v x = v y
⊢ v x = embedding b

Tactic:
← hy

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
ha0 : embedding a ≠ embedding 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h0' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : v x = v y
⊢ v x = v y
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : x = 0
⊢ 0 < valueGroup₀_equiv_extensionValuation ↑γ ↔ extension 0 < ↑γ

Tactic:
simp only [valueGroup₀_equiv_extensionValuation, valueGroup₀_hom_extensionValuation,
              MulEquiv.ofBijective_apply, coe_mk, ZeroHom.coe_mk]
            rw [Valuation.restrict_def, restrict₀_apply, dif_neg]
            · have hext : hv.extension 0 = 0 := by rw [extension_eq_zero_iff]
              simp [hext]
            · simp [← v.restrict.zero_iff, v.restrict_def,
                (restrict₀_surjective (.ofClass hv.v) _).choose_spec]

Goal state after:
Module: Mathlib.Data.Finsupp.Interval

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f g : ι →₀ α
⊢ #((f.support ∪ g.support).finsupp ⇑(f.rangeIcc g)) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i))

Tactic:
card_finsupp,

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq α
f g : ι →₀ α
⊢ ∏ i ∈ f.support ∪ g.support, #((f.rangeIcc g) i) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i))
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : n ≠ 0
⊢ (truncTotal n) ↑p = p ↔ p.totalDegree < n

Tactic:
truncTotal,

Goal state after:
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : Finite σ
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : n ≠ 0
⊢ (truncFinset R ⋯.toFinset) ↑p = p ↔ p.totalDegree < n
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 y : K
⊢ { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm (x + y)) } =
    { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm x) } +
      { toCompletion := ↑((WithVal.equiv (HeightOneSpectrum.valuation K v)).symm y) }

Tactic:
by
  apply adicCompletion.ext; simp [UniformSpace.Completion.coe_add]

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
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
⊢ UniformContinuousConstSMul S (WithVal (valuation K v))

Tactic:
refine ⟨fun l ↦ ?_⟩

Goal state after:
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
l : S
⊢ UniformContinuous fun x ↦ l • x
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 : (adicCompletion K v)ˣ
h : a ∈ (adicCompletionIntegers K v).units
⊢ Valued.v ↑a = 1

Tactic:
convert! isUnit_iff_valued_eq_one.1 (Submonoid.unitsEquivIsUnitSubmonoid _ ⟨_, h⟩).2

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

Goal state before:
pp: R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
h : Tendsto (fun i ↦ (f i).order) atTop (𝓝 ⊤)
⊢ Summable fun x ↦ ∏ i ∈ x, f i

Tactic:
by
  rcases isEmpty_or_nonempty ι with hempty | hempty
  · apply Summable.of_finite
  refine (summable_iff_summable_coeff _).mpr fun n ↦ summable_of_hasFiniteSupport ?_
  simp_rw [ENat.tendsto_nhds_top_iff_natCast_lt, eventually_atTop] at h
  obtain ⟨i, hi⟩ := h n
  apply (Finset.Iio i).powerset.finite_toSet.subset
  suffices ∀ s : Finset ι, coeff n (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa
  intro s hs
  contrapose hs
  obtain ⟨x, hxs, hxi⟩ := Set.not_subset.mp hs
  rw [Set.mem_Iio, not_lt] at hxi
  refine coeff_of_lt_order _ <| (hi x hxi).trans_le <| le_trans ?_ (le_order_prod _ _)
  apply Finset.single_le_sum (by simp) hxs

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
p : R⟦X⟧
T : Subring R
hp : ∀ (n : ℕ), (coeff n) p ∈ T
⊢ p.order ≤ (p.toSubring T hp).order

Tactic:
· exact le_order _ _ fun d hd => by
      exact_mod_cast (coeff_toSubring p T hp) ▸ (coeff_of_lt_order d hd)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
f : MvPowerSeries σ R
hf : f ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ (coeff e) (-f) ∈ Jd.1

Tactic:
simp only [map_neg, neg_mem, hf e he]

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

Goal state before:
pp: S : Type u_2
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
⊢ MvPowerSeries.HasEval fun x ↦ 0

Tactic:
exact MvPowerSeries.HasEval.zero

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

Goal state before:
pp: case h
σ : 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
T : Type u_4
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
p : MvPolynomial σ R
⊢ (MvPolynomial.eval₂Hom (ε.comp φ) fun i ↦ ε (a i)) p = MvPolynomial.eval₂ (ε.comp φ) (fun s ↦ ε (a s)) p

Tactic:
MvPolynomial.coe_eval₂Hom

Goal state after:
case h
σ : 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
T : Type u_4
inst✝⁶ : UniformSpace T
inst✝⁵ : CompleteSpace T
inst✝⁴ : T2Space T
inst✝³ : CommRing T
inst✝² : IsTopologicalRing T
inst✝¹ : IsLinearTopology T T
inst✝ : IsUniformAddGroup T
ε : S →+* T
hε : Continuous[inst✝¹⁴.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑ε
p : MvPolynomial σ R
⊢ MvPolynomial.eval₂ (ε.comp φ) (fun i ↦ ε (a i)) p = MvPolynomial.eval₂ (ε.comp φ) (fun s ↦ ε (a s)) p
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠

Tactic:
rw [← continuum_power_aleph0]

Goal state after:
case a
x : Cardinal.{u_1}
h₁ : 2 ≤ x
h₂ : x ≤ 𝔠
⊢ x ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
S : Type u_5
inst✝ : CommRing S
this : UniformSpace S := ⊥
⊢ HasSubst fun s ↦ X s

Tactic:
simpa [hasSubst_iff_hasEval_of_discreteTopology] using HasEval.X

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ Cardinal.lift.{0, u_1} (Module.rank ℝ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)

Tactic:
← lift_rank_mul_lift_rank ℝ ℂ E,

Goal state after:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ Cardinal.lift.{u_1, 0} (Module.rank ℝ ℂ) * Cardinal.lift.{0, u_1} (Module.rank ℂ E) =
    Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
q : ℕ
hq : 1 < q
f : PowerSeries R
n : ℕ
⊢ ((ofPowerSeries q) f) n = Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 n

Tactic:
simp [ofPowerSeries, dif_pos hq]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ i, q ^ i = n
⊢ ((ofPowerSeries (q ^ k)) f) n = ((ofPowerSeries q) (PowerSeries.subst (PowerSeries.X ^ k) f)) n

Tactic:
rwa [ofPowerSeries_apply hq, ofPowerSeries_apply (one_lt_pow' hq hk),
        Function.extend_apply', Function.extend_apply']

Goal state after:
case neg.hb
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
n : ℕ
hn : ¬∃ i, q ^ i = n
⊢ ¬∃ a, (q ^ k) ^ a = n
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f : PowerSeries R
hf : PowerSeries.constantCoeff f = 1
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
i : ℕ
hmn : (p ^ i).Coprime n
hn : ∃ j, p ^ j = n
⊢ ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (p ^ i * n) =
    ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) (p ^ i) *
      ((ofPowerSeries p) (PowerSeries.subst (PowerSeries.X ^ k) f)) n

Tactic:
obtain ⟨j, rfl⟩ := hn
      cases i
      · simp [hk.ne', hf]
      · cases j
        · simp [hk.ne', hf]
        · simp [hp.ne_one] at hmn

Goal state after:
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
p : Polynomial R
⊢ (MvPolynomial.aeval fun x ↦ a) ((Polynomial.aeval (MvPolynomial.X ())) p) = (Polynomial.aeval a) p

Tactic:
← AlgHom.comp_apply

Goal state after:
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
p : Polynomial R
⊢ ((MvPolynomial.aeval fun x ↦ a).comp (Polynomial.aeval (MvPolynomial.X ()))) p = (Polynomial.aeval a) p
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
p : Polynomial R
⊢ (substAlgHom ha) ↑p = (Polynomial.aeval a) p

Tactic:
rw [p.toPowerSeries_toMvPowerSeries, substAlgHom, MvPowerSeries.coe_substAlgHom,
    MvPowerSeries.subst_coe, ← AlgHom.comp_apply]

Goal state after:
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
p : Polynomial R
⊢ ((MvPolynomial.aeval fun x ↦ a).comp (Polynomial.aeval (MvPolynomial.X ()))) p = (Polynomial.aeval a) p
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
⊢ ∀ (c_1 : 𝕜), c • x ∈ c_1 • s → ‖c‖ₑ * egauge 𝕜 s x ≤ ‖c_1‖ₑ

Tactic:
rintro a ⟨y, hy, hxy⟩

Goal state after:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case e_a.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
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ (i + 1 + 1)) =
    (coeff (n + 1 + 1)) (B ^ (i + 1 + 1)) - if i + 1 + 1 = 1 then k else 0

Tactic:
simp only [add_assoc, Nat.reduceAdd]

Goal state after:
case e_a.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
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ (coeff (n + 2)) ((B + -(C k * X ^ (n + 2))) ^ (i + 2)) = (coeff (n + 2)) (B ^ (i + 2)) - if i + 2 = 1 then k else 0
Module: Mathlib.Analysis.Calculus.FDeriv.Const

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
⊢ HasFDerivWithinAt f 0 {x} x

Tactic:
by
  refine .of_not_accPt ?_
  rw [accPt_iff_clusterPt, inf_principal]
  simp [ClusterPt]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Const

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivAt f 0 x

Tactic:
rw [← hasFDerivWithinAt_univ, subsingleton_univ.eq_singleton_of_mem (mem_univ x)]
  exact hasFDerivWithinAt_singleton f x

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
s : Set 𝕜
hfg : EqOn f g s
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
x : 𝕜
hx : x ∈ s
⊢ derivWithin f s x = derivWithin g s x

Tactic:
exact derivWithin_congr hfg (hfg hx)

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ ε, 0 < ε ∧ ↑ε * ↑‖c‖₊ / ↑r < 1

Tactic:
apply Eventually.exists_gt

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
l : Filter α
f : α → E
inst✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
⊢ ∀ᶠ (x : ℝ≥0) in 𝓝 0, ↑x * ↑‖c‖₊ / ↑r < 1
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
F : Type u_3
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
hf : HasFDerivAtFilter f f' L
⊢ (fun p ↦ f p.1 - f p.2) =O[𝕜; L] fun p ↦ p.1 - p.2

Tactic:
by
  simpa using hf.isLittleOTVS.isBigOTVS.fun_add f'.isBigOTVS_comp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)
⊢ g =o[𝕜; l] f

Tactic:
refine (((isLittleOTVS_one (𝕜 := 𝕜)).mpr h).smul_left f).congr' (h₀.mono fun x hx ↦ ?_) (by simp)

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : TopologicalSpace E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
h : Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)
x : α
hx : f x = 0 → g x = 0
⊢ (fun x ↦ f x • (f x)⁻¹ • g x) x = g x
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
l : Filter α
f : α → E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
h : Tendsto (fun x_1 ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
⊢ ∃ r, 0 < r ∧ r ≤ 1 ∧ ↑r ≤ (egauge 𝕜 U x)⁻¹

Tactic:
apply Eventually.exists_gt

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
l : Filter α
f : α → E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
h : Tendsto (fun x_1 ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
⊢ ∀ᶠ (x_1 : ℝ≥0) in 𝓝 0, x_1 ≤ 1 ∧ ↑x_1 ≤ (egauge 𝕜 U x)⁻¹
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
r : ℝ
hr₀ : 0 < r
⊢ ∃ j, 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 r) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)

Tactic:
lift C to ℝ≥0 using hC₀.le

Goal state after:
case mpr
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
r : ℝ
hr₀ : 0 < r
C : ℝ≥0
hC₀ : ↑C > 0
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ↑C * ‖g x‖
⊢ ∃ j, 0 < j ∧ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 r) (f x) ≤ egauge 𝕜 (ball 0 j) (g x)