mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : MvPowerSeries σ R
⊢ Continuous[instTopologicalSpace R, inst✝⁷.toTopologicalSpace] (eval₂ φ a)

Tactic:
;

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
⊢ Continuous[instTopologicalSpace R, inst✝⁷.toTopologicalSpace] (eval₂ φ a)
Module: Mathlib.RingTheory.PowerSeries.Evaluation

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this : HasSum (fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
d : Unit →₀ ℕ
hd : d ∉ Set.range (Finsupp.single ())
⊢ (Finsupp.single () (d ())) default = d default

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this : HasSum (fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
d : Unit →₀ ℕ
hd : d ∉ Set.range (Finsupp.single ())
⊢ (Finsupp.single () (d ())) default = d default
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
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
d : τ →₀ ℕ
i : σ
⊢ i ∉ {s | (coeff d) (a s) ≠ 0} → i ∉ {s | (coeff d) ↑((MvPowerSeries.truncTotal (x s)) (a s)) ≠ 0}

Tactic:
;

Goal state after:
σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
d : τ →₀ ℕ
i : σ
⊢ i ∉ {s | (coeff d) (a s) ≠ 0} → i ∉ {s | (coeff d) ↑((MvPowerSeries.truncTotal (x s)) (a s)) ≠ 0}
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
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
x✝¹ : σ → MvPowerSeries τ S
x✝ : MvPowerSeries σ R
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (subst x✝¹ x✝) = (coeff n✝) (eval₂ (algebraMap R (MvPowerSeries τ S)) x✝¹ x✝)

Tactic:
;

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
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
x✝¹ : σ → MvPowerSeries τ S
x✝ : MvPowerSeries σ R
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (subst x✝¹ x✝) = (coeff n✝) (eval₂ (algebraMap R (MvPowerSeries τ S)) x✝¹ x✝)
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
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
x✝¹ : σ → MvPowerSeries τ S
x✝ : MvPowerSeries σ R
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (subst x✝¹ x✝) = (coeff n✝) (eval₂ (algebraMap R (MvPowerSeries τ S)) x✝¹ x✝)

Tactic:
simp +instances [subst, DiscreteUniformity.eq_bot]

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n

Tactic:
;

Goal state after:
c : ℝ
f : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
⊢ cantorFunctionAux c f n = 0 ∨ cantorFunctionAux c f n = c ^ n
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Tactic:
;

Goal state after:
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
h3 : ∀ (n : ℕ), f n = true → g n = true
n : ℕ
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case true
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
h3 : g n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g n

Tactic:
;

Goal state after:
case true
c : ℝ
f g : ℕ → Bool
h1 : 0 ≤ c
h2 : c < 1
n : ℕ
h : f n = true
h3 : g n = true
⊢ cantorFunctionAux c f n ≤ cantorFunctionAux c g 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
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
⊢ Continuous (eval₂ (algebraMap R (MvPowerSeries τ S)) a)

Tactic:
exact continuous_eval₂ (continuous_algebraMap _ _) ha.hasEval

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

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
⊢ ¬cantorFunction c f = cantorFunction c g

Tactic:
have : ∃ n, f n ≠ g n := Function.ne_iff.mp h

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
⊢ ¬cantorFunction c f = cantorFunction c g
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
υ : Type u_7
T : Type u_8
inst✝¹ : CommRing T
inst✝ : Algebra S T
b : τ → MvPowerSeries υ T
ha : HasSubst a
hb : HasSubst b
this✝ : UniformSpace S := ⋯
this : UniformSpace T := ⋯
⊢ Filter.Tendsto (⇑(substAlgHom hb)) (nhds 0) (nhds 0)

Tactic:
simpa [← map_zero (substAlgHom (R := S) hb)] using! (continuous_subst hb).continuousAt

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case hx
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
⊢ 1 ≤ ↑n

Tactic:
;

Goal state after:
case hx
f : ℕ → ℂ
s s' : ℂ
h : s.re ≤ s'.re
n : ℕ
hn : ¬n = 0
⊢ 1 ≤ ↑n
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: ⊢ LSeries 0 = 0

Tactic:
ext
  simp [LSeries, LSeries.term]

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

Goal state before:
pp: case pos
σ : 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
f : MvPowerSeries σ R
inst✝ : Finite τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
hx : ∀ (i : σ), k ≤ x i
d : τ →₀ ℕ
hd : Finsupp.degree d < k
n : σ →₀ ℕ
⊢ (coeff n) f • ∑ l ∈ n.support.finsuppAntidiag d, ∏ i ∈ n.support, (coeff (l i)) (a i ^ n i) =
    (coeff n) f • ∑ l ∈ n.support.finsuppAntidiag d, ∏ i ∈ n.support, (coeff (l i)) (↑((truncTotal (x i)) (a i)) ^ n i)

Tactic:
congr! 3 with l hl i hi

Goal state after:
case pos.a.a
σ : 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
f : MvPowerSeries σ R
inst✝ : Finite τ
x : σ → ℕ
k : ℕ
ha : HasSubst a
hx : ∀ (i : σ), k ≤ x i
d : τ →₀ ℕ
hd : Finsupp.degree d < k
n : σ →₀ ℕ
l : σ →₀ τ →₀ ℕ
hl : l ∈ n.support.finsuppAntidiag d
i : σ
hi : i ∈ n.support
⊢ (coeff (l i)) (a i ^ n i) = (coeff (l i)) (↑((truncTotal (x i)) (a i)) ^ n i)
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

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

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
q x✝ : ℕ
⊢ (if hq : 1 < q then { toFun := Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) 0) 0, map_zero' := ⋯ }
      else (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff 0))
      x✝ =
    0 x✝
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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
⊢ (truncTotal k) (subst a f) = (truncTotal k) (∑ i ∈ range k, subst a ((homogeneousComponent i) f))

Tactic:
by
  rw [truncTotal_subst_eq_truncTotal_subst_sum ha ha₁, ← substAlgHom_apply ha, map_sum]
  simp

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
⊢ MvPowerSeries.subst (fun x ↦ a) ↑((Polynomial.aeval (MvPolynomial.X ())) p) = (Polynomial.aeval a) p

Tactic:
MvPowerSeries.subst_coe,

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) ((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
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬(MvPowerSeries.coeff i) f = 0
⊢ (MvPowerSeries.coeff (Finsupp.single () (i ()))) f ≠ 0

Tactic:
;

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
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬(MvPowerSeries.coeff i) f = 0
⊢ (MvPowerSeries.coeff (Finsupp.single () (i ()))) f ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case e'_2
R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬(MvPowerSeries.coeff i) f = 0
⊢ Finsupp.single () (i ()) = i

Tactic:
;

Goal state after:
case e'_2
R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬(MvPowerSeries.coeff i) f = 0
⊢ Finsupp.single () (i ()) = i
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this : UniformSpace R := ⊥
f : ArithmeticFunction R
⊢ ⇑f ∈ {f | f 0 = 0}

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
this : UniformSpace R := ⊥
f : ArithmeticFunction R
⊢ ⇑f ∈ {f | f 0 = 0}
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
⊢ Tendsto (fun p ↦ ((DFunLike.coe ∘ fun s ↦ ∏ b ∈ s, f b) p.1, (DFunLike.coe ∘ fun s ↦ ∏ b ∈ s, f b) p.2))
    (atTop ×ˢ atTop) (⨅ i, comap (fun a ↦ (a.1 i, a.2 i)) (𝓟 SetRel.id))

Tactic:
tendsto_iInf,

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
⊢ ∀ (i : ℕ),
    Tendsto (fun p ↦ ((DFunLike.coe ∘ fun s ↦ ∏ b ∈ s, f b) p.1, (DFunLike.coe ∘ fun s ↦ ∏ b ∈ s, f b) p.2))
      (atTop ×ˢ atTop) (comap (fun a ↦ (a.1 i, a.2 i)) (𝓟 SetRel.id))
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
⊢ ((∏ x ∈ u \ t, f x) * ∏ x ∈ t, f x) n = ((∏ x ∈ v \ t, f x) * ∏ x ∈ t, f x) n

Tactic:
replace hu : ∀ i ∈ u \ t, i ∈ s := by
    intro i hi
    rw [Finset.mem_sdiff, Set.Finite.mem_toFinset, Set.notMem_compl_iff] at hi
    exact hi.2

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
⊢ ((∏ x ∈ u \ t, f x) * ∏ x ∈ t, f x) n = ((∏ x ∈ v \ t, f x) * ∏ x ∈ t, f x) n
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ 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✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b✝ : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a b : σ → R
x✝ : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((rescale (a * b)) x✝) = (coeff n✝) ((rescale a * rescale b) x✝)

Tactic:
;

Goal state after:
σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ 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✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b✝ : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a b : σ → R
x✝ : MvPowerSeries σ R
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((rescale (a * b)) x✝) = (coeff n✝) ((rescale a * rescale b) x✝)
Module: Mathlib.Analysis.Calculus.TangentCone.Defs

Goal state before:
pp: R : Type u
E : Type v
inst✝² : AddCommGroup E
inst✝¹ : SMul R E
inst✝ : TopologicalSpace E
s : Set E
x y : E
h : y ∈ tangentConeAt R s x
⊢ ∃ α l,
    ∃ (_ : l.NeBot), ∃ c d, Tendsto d l (𝓝 0) ∧ (∀ᶠ (n : α) in l, x + d n ∈ s) ∧ Tendsto (fun n ↦ c n • d n) l (𝓝 y)

Tactic:
rw [tangentConeAt, mem_ofPred, ← map₂_smul, ← map_prod_eq_map₂, ClusterPt,
    ← neBot_inf_comap_iff_map'] at h
  refine ⟨R × E, _, h, Prod.fst, Prod.snd, ?_, ?_, ?_⟩
  · refine (tendsto_snd (f := ⊤)).mono_left <| inf_le_right.trans <| ?_
    gcongr
    apply nhdsWithin_le_nhds
  · refine .filter_mono inf_le_right ?_
    rw [top_prod, eventually_comap]
    filter_upwards [eventually_mem_nhdsWithin]
    simp +contextual
  · exact tendsto_comap.mono_left inf_le_left

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

Goal state before:
pp: case h
𝕜 : 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
inst✝ : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
h' : ¬AccPt x (𝓟 s)
⊢ tangentConeAt 𝕜 s x ⊆ 0

Tactic:
;

Goal state after:
case h
𝕜 : 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
inst✝ : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
h' : ¬AccPt x (𝓟 s)
⊢ tangentConeAt 𝕜 s x ⊆ 0
Module: Mathlib.Analysis.Calculus.TangentCone.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DivisionSemiring 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
s : Set E
x y : E
α : Type u_3
l : Filter α
inst✝ : l.NeBot
c : α → 𝕜
hc₀ : Tendsto c l (𝓝[≠] 0)
hmem : ∀ᶠ (n : α) in l, x + c n • y ∈ s
⊢ y ∈ tangentConeAt 𝕜 s x

Tactic:
tendsto_nhdsWithin_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : DivisionSemiring 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
s : Set E
x y : E
α : Type u_3
l : Filter α
inst✝ : l.NeBot
c : α → 𝕜
hc₀ : Tendsto c l (𝓝 0) ∧ ∀ᶠ (n : α) in l, c n ∈ {0}ᶜ
hmem : ∀ᶠ (n : α) in l, x + c n • y ∈ s
⊢ y ∈ tangentConeAt 𝕜 s x
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
s : Set E
x : E
⊢ HasFDerivWithinAt f 0 s x

Tactic:
obtain rfl | ⟨a, rfl⟩ := s.eq_empty_or_singleton_of_subsingleton
  · simp
  · exact HasFDerivWithinAt.singleton

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
hε : ∞ ≠ 0
x✝ : α
⊢ 1 * egauge 𝕜 V (g x✝) ≤ ∞ * egauge 𝕜 V (g x✝)

Tactic:
;

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
f : α → E
g : α → F
l : Filter α
h : f =o[𝕜; l] g
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
hε : ∞ ≠ 0
x✝ : α
⊢ 1 * egauge 𝕜 V (g x✝) ≤ ∞ * egauge 𝕜 V (g x✝)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
hc : C < ‖0‖₊
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : TopologicalSpace F
inst✝¹ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
inst✝ : ContinuousConstSMul 𝕜 F
ι : Sort u_7
p : ι → Prop
U : ι → Set E
hb : (𝓝 0).HasBasis p U
h : ∀ (i : ι), p i → ∃ C, ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
i : ι
hi : p i
C : ℝ≥0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 (U i) (f x)) ≤ᶠ[l] fun x ↦ ↑C * egauge 𝕜 V (g x)
hc : C < ‖0‖₊
⊢ False
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this :
  (𝓝 fun i ↦ 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
⊢ (fun x i ↦ f i x) =o[𝕜; l] g

Tactic:
← Pi.zero_def

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup F
inst✝⁵ : TopologicalSpace F
inst✝⁴ : Module 𝕜 F
l : Filter α
g : α → F
ι : Type u_7
E : ι → Type u_8
inst✝³ : (i : ι) → AddCommGroup (E i)
inst✝² : (i : ι) → Module 𝕜 (E i)
inst✝¹ : (i : ι) → TopologicalSpace (E i)
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
f : (i : ι) → α → E i
h : ∀ (i : ι), f i =o[𝕜; l] g
this :
  (𝓝 0).HasBasis (fun If ↦ If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 0 ∧ Balanced 𝕜 (If.2 i)) fun If ↦
    If.1.pi fun i ↦ id (If.2 i)
⊢ (fun x i ↦ f i x) =o[𝕜; l] g
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
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun n ↦ c n • d n) l (𝓝 v)
⊢ Tendsto (fun n ↦ x + d n) l (𝓝[s] x)

Tactic:
tendsto_nhdsWithin_iff

Goal state after:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun n ↦ c n • d n) l (𝓝 v)
⊢ Tendsto (fun n ↦ x + d n) l (𝓝 x) ∧ ∀ᶠ (n : α) in l, x + d n ∈ s
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
c : F
x✝ : 𝕜
⊢ derivWithin (fun x ↦ c) s x✝ = 0 x✝

Tactic:
;

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
c : F
x✝ : 𝕜
⊢ derivWithin (fun x ↦ c) s x✝ = 0 x✝