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

Goal state before:
pp: case pos
σ : 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
⊢ (coeff m) φ = ∑ p ∈ antidiagonal m, (coeff p.1) (X s ^ n) * (coeff p.2) fun m ↦ (coeff (m + single s n)) φ

Tactic:
Finset.sum_eq_single (single s n, m - single s n)

Goal state after:
case pos
σ : 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
⊢ (coeff m) φ =
    (coeff (single s n, m - single s n).1) (X s ^ n) *
      (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ

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
⊢ ∀ b ∈ antidiagonal m,
    b ≠ (single s n, m - single s n) → ((coeff b.1) (X s ^ n) * (coeff b.2) fun m ↦ (coeff (m + single s n)) φ) = 0

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
⊢ (single s n, m - single s n) ∉ antidiagonal m →
    ((coeff (single s n, m - single s n).1) (X s ^ n) *
        (coeff (single s n, m - single s n).2) fun m ↦ (coeff (m + single s n)) φ) =
      0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
f : ι → ℕ
g : ι → R
s : Finset ι
⊢ ∏ i ∈ s, (monomial (f i)) (g i) = (monomial (∑ i ∈ s, f i)) (∏ i ∈ s, g i)

Tactic:
by
  simpa [monomial, Finsupp.single_finsetSum] using
    MvPowerSeries.prod_monomial (fun i ↦ Finsupp.single () (f i)) g s

Goal state after:
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ embedding a = embedding b

Tactic:
simp only [Completion.algebraMap_def, Algebra.algebraMap_self, RingHom.id_apply,
        extension_extends, Valuation.restrict_inj] at this

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
⊢ embedding a = embedding b
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : r = 0
⊢ 0 ≤ exp (-↑n) ↔ 0 ∈ v.asIdeal ^ n

Tactic:
zero_le,

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
hr : r = 0
⊢ True ↔ 0 ∈ v.asIdeal ^ n
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ ∀ (a_1 b : σ →₀ ℕ),
    a_1 + b = d →
      (coeff a_1) (f a) * (coeff b) (∏ x ∈ s, f x) =
        ∑ x ∈ (s.finsuppAntidiag b).attach, ∏ x_1 ∈ insert a s, (coeff (Function.update (⇑↑x) a a_1 x_1)) (f x_1)

Tactic:
rintro u v rfl

Goal state after:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
u v : σ →₀ ℕ
⊢ (coeff u) (f a) * (coeff v) (∏ x ∈ s, f x) =
    ∑ x ∈ (s.finsuppAntidiag v).attach, ∏ x_1 ∈ insert a s, (coeff (Function.update (⇑↑x) a u x_1)) (f x_1)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ ∑ p ∈ antidiagonal d, (coeff p.1) (f a) * (coeff p.2) (∏ x ∈ s, f x) =
    ∑ x ∈ antidiagonal d,
      ∑ i ∈ Finset.map { toFun := fun f ↦ (↑f).update a x.1, inj' := ⋯ } (s.finsuppAntidiag x.2).attach,
        ∏ i_1 ∈ insert a s, (coeff (i i_1)) (f i_1)

pp: case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ (↑(antidiagonal d)).PairwiseDisjoint fun p ↦
    Finset.map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

Tactic:
· apply Finset.sum_congr rfl
      simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]
      rintro u v rfl
      rw [ih, Finset.mul_sum, ← Finset.sum_attach]
      apply Finset.sum_congr rfl
      simp only [mem_attach, Finset.prod_insert ha, Function.update_self, forall_true_left,
        Subtype.forall]
      rintro x -
      rw [Finset.prod_congr rfl]
      intro i hi
      rw [Function.update_of_ne]
      exact ne_of_mem_of_not_mem hi ha

Goal state after:
case insert
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (d : σ →₀ ℕ), (coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff (l i)) (f i)
d : σ →₀ ℕ
⊢ (↑(antidiagonal d)).PairwiseDisjoint fun p ↦
    Finset.map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach
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 s : R
hs : s ∈ v.asIdeal.primeCompl
⊢ (valuation K v) (↑a / ↑s) ≤ 1

Tactic:
valuation_div_le_one_iff (K := K) v a (by aesop) (fun _ ↦ by contradiction)

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
a s : R
hs : s ∈ v.asIdeal.primeCompl
⊢ s ∉ v.asIdeal
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
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
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
apply_fun algebraMap _ K at hnd

Goal state after:
case h
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 :
  (algebraMap (↥(valuationSubringAtPrime K v)) K) (r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2) =
    (algebraMap (↥(valuationSubringAtPrime K v)) K) ((algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1)
⊢ 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 h
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
⊢ x * (algebraMap R K) ↑d = (algebraMap R K) n ∨ x * (algebraMap R K) n = (algebraMap R K) ↑d

Tactic:
apply_fun algebraMap _ K at hnd

Goal state after:
case h
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 :
  (algebraMap (↥(valuationSubringAtPrime K v)) K) (r * (algebraMap R ↥(valuationSubringAtPrime K v)) ↑(n, d).2) =
    (algebraMap (↥(valuationSubringAtPrime K v)) K) ((algebraMap R ↥(valuationSubringAtPrime K v)) (n, d).1)
⊢ 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_2
inst✝ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ weightedOrder w ((monomial d) a) = ↑((weight w) d)

Tactic:
classical
  rw [weightedOrder_monomial, if_neg h]

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 |
      (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r * a =
        a * (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r}

Tactic:
exact isClosed_eq (continuous_const_mul _) (continuous_mul_const _)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hm : constantCoeff f ^ m = 0
⊢ Tendsto (fun x ↦ f ^ x) atTop (𝓝 0)

Tactic:
tendsto_iff_coeff_tendsto,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hm : constantCoeff f ^ m = 0
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) (f ^ i)) atTop (𝓝 ((coeff d) 0))
Module: Mathlib.RingTheory.MvPowerSeries.PiTopology

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∀ (d : σ →₀ ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a) →
    ∃ a, ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)

Tactic:
· intro h
    choose a h using h
    exact ⟨a, by simpa using! h⟩

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
a : adicCompletion K v
ha : 1 < Valued.v a
ϖ : R
hϖ : v.intValuation ϖ = exp (-1)
⊢ Valued.v ((algebraMap R (adicCompletion K v)) ϖ) = (exp 1)⁻¹

Tactic:
simp [valuedAdicCompletion_eq_valuation, valuation_of_algebraMap, hϖ, exp]

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✝² : 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
⊢ (Function.support n).Finite

Tactic:
change n =ᶠ[cofinite] 0

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
⊢ n =ᶠ[cofinite] 0
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent (constantCoeff f)
⊢ Tendsto (fun x ↦ f ^ x) atTop (𝓝 0)

Tactic:
tendsto_iff_coeff_tendsto,

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsLinearTopology R R
f : MvPowerSeries σ R
hf : IsTopologicallyNilpotent (constantCoeff f)
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i ↦ (coeff d) (f ^ i)) atTop (𝓝 ((coeff d) 0))
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
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ ⇑(eval₂Hom hφ ha) = eval₂ φ a

Tactic:
ext f

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
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
f : MvPowerSeries σ R
⊢ (eval₂Hom hφ ha) f = eval₂ φ a f
Module: Mathlib.RingTheory.PowerSeries.Evaluation

Goal state before:
pp: S : Type u_2
inst✝³ : CommRing S
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousAdd S
inst✝ : IsLinearTopology S S
a b : S
ha : HasEval a
hb : HasEval b
⊢ HasEval (a + b)

Tactic:
simp only [hasEval_iff] at ha hb ⊢

Goal state after:
S : Type u_2
inst✝³ : CommRing S
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousAdd S
inst✝ : IsLinearTopology S S
a b : S
ha : MvPowerSeries.HasEval fun x ↦ a
hb : MvPowerSeries.HasEval fun x ↦ b
⊢ MvPowerSeries.HasEval fun x ↦ a + b
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
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
⊢ Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑(aeval ha)

Tactic:
rw [coe_aeval]
  exact continuous_eval₂ (continuous_algebraMap R S) ha

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
⊢ Filter.Tendsto a Filter.cofinite (nhds 0) ↔ ∀ (d : τ →₀ ℕ), {s | (coeff d) (a s) ≠ 0}.Finite

Tactic:
by
  simp [tendsto_iff_coeff_tendsto, coeff_zero, nhds_discrete]

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
inst✝¹² : Algebra R S
a : σ → MvPowerSeries τ S
T : Type u_6
inst✝¹¹ : CommRing T
inst✝¹⁰ : UniformSpace T
inst✝⁹ : T2Space T
inst✝⁸ : CompleteSpace T
inst✝⁷ : IsUniformAddGroup T
inst✝⁶ : IsTopologicalRing T
inst✝⁵ : IsLinearTopology T T
inst✝⁴ : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
hε : Continuous ⇑ε
⊢ ε.comp (substAlgHom ha) = aeval ⋯

Tactic:
ext f

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
a : σ → MvPowerSeries τ S
T : Type u_6
inst✝¹¹ : CommRing T
inst✝¹⁰ : UniformSpace T
inst✝⁹ : T2Space T
inst✝⁸ : CompleteSpace T
inst✝⁷ : IsUniformAddGroup T
inst✝⁶ : IsTopologicalRing T
inst✝⁵ : IsLinearTopology T T
inst✝⁴ : Algebra R T
ε : MvPowerSeries τ S →ₐ[R] T
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
ha : HasSubst a
hε : Continuous ⇑ε
f : MvPowerSeries σ R
⊢ (ε.comp (substAlgHom ha)) f = (aeval ⋯) f
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f φ : R⟦X⟧
hf : constantCoeff f = 0
hφ : constantCoeff φ = 0
⊢ MvPowerSeries.order f ≤ (subst f φ).order

Tactic:
exact le_order_subst_right hf hφ

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
r : R
⊢ ↑(rescaleAlgHom r) = rescale r

Tactic:
ext f

Goal state after:
R : Type u_2
inst✝ : CommRing R
r : R
f : R⟦X⟧
n✝ : ℕ
⊢ (coeff n✝) (↑(rescaleAlgHom r) f) = (coeff n✝) ((rescale r) f)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this : UniformSpace R := ⊥
⊢ Set.range DFunLike.coe = {f | f 0 = 0}

Tactic:
ext f

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this : UniformSpace R := ⊥
f : ℕ → R
⊢ f ∈ Set.range DFunLike.coe ↔ f ∈ {f | f 0 = 0}
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : SMul 𝕜 E
inst✝ : TopologicalSpace E
s : Set E
x : E
ι : Sort u_3
p : ι → Prop
U : ι → Set E
h : (𝓝 0).HasBasis p U
⊢ tangentConeAt 𝕜 s x = ⋂ i, ⋂ (_ : p i), closure[inst✝] (univ • (U i ∩ (fun x_2 ↦ x + x_2) ⁻¹' s))

Tactic:
ext y

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : SMul 𝕜 E
inst✝ : TopologicalSpace E
s : Set E
x : E
ι : Sort u_3
p : ι → Prop
U : ι → Set E
h : (𝓝 0).HasBasis p U
y : E
⊢ y ∈ tangentConeAt 𝕜 s x ↔ y ∈ ⋂ i, ⋂ (_ : p i), closure[inst✝] (univ • (U i ∩ (fun x_2 ↦ x + x_2) ⁻¹' s))
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Semiring 𝕜
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
s : Set E
x : E
inst✝ : T2Space E
hx : ¬AccPt x (𝓟 s)
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun x_1 ↦ x + d x_1) l (𝓝 x)

Tactic:
simpa using tendsto_const_nhds.add hd₀

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
f : E → F
x : E
⊢ x ∈ support (fderiv 𝕜 f) → x ∈ tsupport f

Tactic:
rw [← not_imp_not, notMem_support]

Goal state after:
𝕜 : 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
⊢ x ∉ tsupport f → fderiv 𝕜 f x = 0
Module: Mathlib.Analysis.Calculus.Deriv.Support

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∈ support (deriv f) → x ∈ tsupport f

Tactic:
rw [← not_imp_not, notMem_support]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∉ tsupport f → deriv f x = 0
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : s ∈ 𝓝 x
⊢ derivWithin f s x = deriv f x

Tactic:
simp only [derivWithin, deriv, fderivWithin_of_mem_nhds h]

Goal state after:
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
x : E
s : Set E
⊢ HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x

Tactic:
by
  simp_rw [hasFDerivWithinAt_iff_isLittleOTVS]
  apply isLittleOTVS_insert
  simp only [sub_self, map_zero]

Goal state after:
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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst✝³] s
ht : IsOpen[inst✝³] t
x : E
hx : x ∈ s ∪ t
⊢ DifferentiableWithinAt 𝕜 f (s ∪ t) x

Tactic:
obtain (hx | hx) := hx

Goal state after:
case inl
𝕜 : 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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst✝³] s
ht : IsOpen[inst✝³] t
x : E
hx : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f (s ∪ t) x

case inr
𝕜 : 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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst✝³] s
ht : IsOpen[inst✝³] t
x : E
hx : x ∈ t
⊢ DifferentiableWithinAt 𝕜 f (s ∪ t) x
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
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst✝³] (s i)
x : E
i : ι
hxsi : x ∈ (fun i ↦ s i) i
⊢ DifferentiableWithinAt 𝕜 f (⋃ i, s i) x

Tactic:
exact (hf i).differentiableAt ((hs i).mem_nhds hxsi) |>.differentiableWithinAt

Goal state after: