mathlib-initiative/mathlib-tactics huggingface dataset:
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
b : ℝ≥0
hb : 1 < b
x y : K
h_mono : Monotone ⇑(toNNReal ⋯)
⊢ (toNNReal ⋯) ((valuation K v) (x + y)) ≤ (toNNReal ⋯) (max ((valuation K v) x) ((valuation K v) y))

Tactic:
exact h_mono ((v.valuation _).map_add x y)

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
⊢ (ε.comp (MvPolynomial.eval₂Hom φ a)) p = MvPolynomial.eval₂ (ε.comp φ) (fun s ↦ ε (a s)) p

Tactic:
MvPolynomial.comp_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₂Hom (ε.comp φ) fun i ↦ ε (a i)) p = MvPolynomial.eval₂ (ε.comp φ) (fun s ↦ ε (a s)) p
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) (f * g)) 0 n =
    ∑ x ∈ n.divisorsAntidiagonal,
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 x.1 *
        Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 x.2

Tactic:
Function.extend_apply' _ _ _ hn,

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
⊢ 0 n =
    ∑ x ∈ n.divisorsAntidiagonal,
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 x.1 *
        Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 x.2
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ¬∃ k, q ^ k = n
⊢ Function.extend (fun x ↦ q ^ x) (fun x_1 ↦ (PowerSeries.coeff x_1) (x • 1)) 0 n = (x • 1) n

Tactic:
Function.extend_apply' _ _ _ hn,

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : 1 < q
hn : ¬∃ k, q ^ k = n
⊢ 0 n = (x • 1) n
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝³ : CommRing R
τ : Type u_4
S : Type u_5
inst✝² : CommRing S
inst✝¹ : Algebra R S
a : σ → MvPowerSeries τ S
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
⊢ (truncTotal k) ((substAlgHom ha) (∑ i ∈ range k, (homogeneousComponent i) f)) =
    (truncTotal k) (∑ i ∈ range k, subst a ((homogeneousComponent i) f))

Tactic:
map_sum

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
f : MvPowerSeries σ R
inst✝ : Finite τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
⊢ (truncTotal k) (∑ x ∈ range k, (substAlgHom ha) ((homogeneousComponent x) f)) =
    (truncTotal k) (∑ i ∈ range k, subst a ((homogeneousComponent i) f))
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝⁴ : CommRing R
τ : Type u_4
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra R S
a : σ → MvPowerSeries τ S
f : MvPowerSeries σ R
inst✝¹ : Finite τ
x : σ → ℕ
k : ℕ
inst✝ : Finite σ
h : ∀ (i : σ), constantCoeff (a i) = 0
hx : ∀ (i : σ), k ≤ x i
⊢ (truncTotal k) (∑ i ∈ range k, subst (fun i ↦ ↑((truncTotal (x i)) (a i))) ((homogeneousComponent i) f)) =
    (truncTotal k) ((substAlgHom ⋯) (∑ i ∈ range k, (homogeneousComponent i) f))

Tactic:
map_sum

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
f : MvPowerSeries σ R
inst✝¹ : Finite τ
x : σ → ℕ
k : ℕ
inst✝ : Finite σ
h : ∀ (i : σ), constantCoeff (a i) = 0
hx : ∀ (i : σ), k ≤ x i
⊢ ∑ x_1 ∈ range k, (truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) ((homogeneousComponent x_1) f)) =
    (truncTotal k) ((substAlgHom ⋯) (∑ i ∈ range k, (homogeneousComponent i) f))
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
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
⊢ 0 (p ^ i * n) =
    Function.extend (fun x ↦ p ^ x) (fun x ↦ (PowerSeries.coeff x) (PowerSeries.subst (PowerSeries.X ^ k) f)) 0
        (p ^ i) *
      Function.extend (fun x ↦ p ^ x) (fun x ↦ (PowerSeries.coeff x) (PowerSeries.subst (PowerSeries.X ^ k) f)) 0 n

pp: case neg.hb
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
⊢ ¬∃ a, p ^ a = p ^ i * n

Tactic:
Function.extend_apply' _ _ _ hn,

Goal state after:
case neg
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
⊢ 0 (p ^ i * n) =
    Function.extend (fun x ↦ p ^ x) (fun x ↦ (PowerSeries.coeff x) (PowerSeries.subst (PowerSeries.X ^ k) f)) 0
        (p ^ i) *
      0 n

case neg.hb
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
⊢ ¬∃ a, p ^ a = p ^ i * n
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inr
𝕜 : 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
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑(‖c⁻¹‖₊ * ‖a‖₊)

Tactic:
← nnnorm_mul

Goal state after:
case inr
𝕜 : 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
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑‖c⁻¹ * a‖₊
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case succ.zero
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n : ℕ
i : ι
hi : 0 + 1 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) (0 + 1) = 1 (0 + 1)

pp: case succ.succ
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n✝ : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) (n + 1 + 1) = 1 (n + 1 + 1)

Tactic:
· simp [hf]

Goal state after:
case succ.succ
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n✝ : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) (n + 1 + 1) = 1 (n + 1 + 1)
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
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousConstSMul 𝕜 E
⊢ tangentConeAt 𝕜 (closure[inst✝²] s) x = tangentConeAt 𝕜 s x

Tactic:
by
  refine Subset.antisymm ?_ (tangentConeAt_mono subset_closure)
  simp only [(nhds_basis_opens _).tangentConeAt_eq_biInter_closure]
  refine iInter₂_mono fun U hU ↦ closure_minimal ?_ isClosed_closure
  grw [(isOpenMap_add_left x).preimage_closure_subset_closure_preimage, hU.2.inter_closure,
    set_smul_closure_subset]

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

Goal state before:
pp: case hcd
𝕜 : 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
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
⊢ Tendsto (fun n ↦ 1 n • (n + -x)) (𝓝 x) (𝓝 0)

Tactic:
· simp only [Pi.one_apply, one_smul]
    exact Continuous.tendsto' (by fun_prop) _ _ (by simp)

Goal state after:
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
inst✝ : Nontrivial E
h : UniqueDiffWithinAt 𝕜 s x
h' : ¬AccPt x (𝓟 s)
⊢ False

Tactic:
have : Dense (Submodule.span 𝕜 (0 : Set E) : Set E) :=
    h.1.mono <| by gcongr; exact tangentConeAt_subset_zero h'

Goal state after:
𝕜 : 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)
this : Dense ↑(Submodule.span 𝕜 0)
⊢ False
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
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)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 W (k x)
⊢ ∃ V ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (k x)

Tactic:
refine ⟨W, hW₀, fun ε hε ↦ ?_⟩

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =o[𝕜; l] g
hgk : g =O[𝕜; l] k
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)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
⊢ (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 W (k x)
Module: Mathlib.Analysis.Asymptotics.TVS

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

Tactic:
refine ⟨W, hW₀, fun ε hε ↦ ?_⟩

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜 F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
k : α → G
hfg : f =O[𝕜; l] g
hgk : g =o[𝕜; l] k
U : Set E
hU₀ : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)
W : Set G
hW₀ : W ∈ 𝓝 0
hW : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 V (g x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 W (k x)
ε : ℝ≥0
hε : ε ≠ 0
⊢ (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 W (k x)
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 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
f' : E →L[𝕜] F
x : E
s : Set E
inst✝ : T1Space E
⊢ HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x

pp: 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
f' : E →L[𝕜] F
x : E
s : Set E
inst✝ : T1Space E
y : E
h : x ≠ y
⊢ HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x

Tactic:
· apply hasFDerivWithinAt_insert_self

Goal state after:
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
f' : E →L[𝕜] F
x : E
s : Set E
inst✝ : T1Space E
y : E
h : x ≠ y
⊢ HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s 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
inst✝ : ContinuousSMul 𝕜 E
f : α → 𝕜
g : α → E
l : Filter α
h₀ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
⊢ g =o[𝕜; l] f ↔ Tendsto (fun x ↦ (f x)⁻¹ • g x) l (𝓝 0)

Tactic:
refine ⟨IsLittleOTVS.tendsto_inv_smul, fun h ↦ ?_⟩
  refine (((isLittleOTVS_one (𝕜 := 𝕜)).mpr h).smul_left f).congr' (h₀.mono fun x hx ↦ ?_) (by simp)
  by_cases h : f x = 0 <;> simp [h, hx]

Goal state after:
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
⊢ p.radius / ‖u‖ₑ ≤ (p.compContinuousLinearMap u).radius

Tactic:
obtain (rfl | h_zero) := eq_zero_or_nnnorm_pos u

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
⊢ p.radius / ‖0‖ₑ ≤ (p.compContinuousLinearMap 0).radius

case inr
𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →L[𝕜] F
h_zero : 0 < ‖u‖₊
⊢ p.radius / ‖u‖ₑ ≤ (p.compContinuousLinearMap u).radius
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : ‖y - x‖ₑ < r
m : ℕ
hm : n ≤ m
⊢ f y = p.partialSum m (y - x)

Tactic:
← mem_eball_zero_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y - x ∈ Metric.eball 0 r
m : ℕ
hm : n ≤ m
⊢ f y = p.partialSum m (y - x)
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Nontrivial E
⊢ ofScalars E c = 0 ↔ c = 0

Tactic:
simp [FormalMultilinearSeries.ext_iff, funext_iff]

Goal state after:
Module: Mathlib.Analysis.Analytic.CPolynomialDef

Goal state before:
pp: case ht
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F := ⋯
⊢ Function.support f ⊆ ⇑changeOriginIndexEquiv ⁻¹' Sigma.fst ⁻¹' {m | m < n}

Tactic:
refine fun s ↦ Not.imp_symm fun hs ↦ ?_

Goal state after:
case ht
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
s : (k : ℕ) × (l : ℕ) × { s // s.card = l }
hs : s ∉ ⇑changeOriginIndexEquiv ⁻¹' Sigma.fst ⁻¹' {m | m < n}
⊢ f s = 0
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
⊢ r ≤ 0

Tactic:
have := FormalMultilinearSeries.summable_norm_mul_pow _ hr

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : Summable fun n ↦ ‖ofScalars E c n‖ * ↑r ^ n
⊢ r ≤ 0
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A✝ : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
k : ℕ
hk : ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
I : ∀ (w : E), ‖w‖₊ < r' → ‖∑ i ∈ Finset.Ico k n, (p i) fun x ↦ w‖ ≤ ε / 4
⊢ ‖∑ i ∈ Finset.Ico k n, (p i) fun x ↦ y‖ ≤ ε / 4

Tactic:
exact I _ yr'

Goal state after:
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ p.rightInv i x 0 = ContinuousMultilinearMap.uncurry0 𝕜 F x

Tactic:
rightInv

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ ContinuousMultilinearMap.uncurry0 𝕜 F x = ContinuousMultilinearMap.uncurry0 𝕜 F x
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ p.rightInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm

Tactic:
rightInv

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
⊢ (p.comp q n) v = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (q.applyComposition c v) + (p 1) fun x ↦ (q n) v

Tactic:
have A :
    (Finset.univ : Finset (Composition n)) =
      {c | 1 < Composition.length c}.toFinset ∪ {Composition.single n hn} := by
    refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
    by_cases h : 1 < c.length
    · simp [h]
    · have : c.length = 1 := by
        refine (eq_iff_le_not_lt.2 ⟨?_, h⟩).symm; exact c.length_pos_of_pos hn
      rw [← Composition.eq_single_iff_length hn] at this
      simp [this]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
hn : 0 < n
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 F E
v : Fin n → F
A : univ = {c | 1 < c.length}.toFinset ∪ {Composition.single n hn}
⊢ (p.comp q n) v = ∑ c ∈ {c | 1 < c.length}.toFinset, (p c.length) (q.applyComposition c v) + (p 1) fun x ↦ (q n) v