mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ HasSum (fun d ↦ φ ((coeff d) f) * a ^ d) (eval₂ φ a f)

Tactic:
simp only [PowerSeries.eval₂]

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)
⊢ HasSum (fun d ↦ φ ((coeff d) f) * a ^ d) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
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
⊢ HasSum (fun d ↦ φ ((coeff d) f) * d.prod fun s e ↦ a s ^ e) (eval₂ φ a f)

Tactic:
rw [← coe_eval₂Hom hφ ha, eval₂Hom_eq_extend hφ ha]
  convert! (hasSum_of_monomials_self f).map (eval₂Hom hφ ha) (?_) with d
  · simp only [Function.comp_apply, coe_eval₂Hom, ← MvPolynomial.coe_monomial,
      eval₂_coe, eval₂_monomial]
  · rw [coe_eval₂Hom]; exact continuous_eval₂ hφ ha

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

Goal state before:
pp: c : ℝ
f : ℕ → Bool
n : ℕ
⊢ cantorFunctionAux c f (n + 1) = c * cantorFunctionAux c (fun n ↦ f (n + 1)) n

Tactic:
cases h : f (n + 1) <;> simp [h, _root_.pow_succ']

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

Goal state before:
pp: case inr
x y : ℝ
h : y ≤ x
hlt : y < x
⊢ (Icc x y).Countable

Tactic:
simp [hlt]

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
⊢ MvPolynomial.coeff d ((truncTotal k) (subst a f)) =
    MvPolynomial.coeff d ((truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) f))

pp: case neg
σ : 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
⊢ MvPolynomial.coeff d ((truncTotal k) (subst a f)) =
    MvPolynomial.coeff d ((truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) f))

Tactic:
· rw [coeff_truncTotal _ hd, coeff_truncTotal _ hd, coeff_subst ha, coeff_subst, finsum_congr]
    · intro n
      simp_rw [Finsupp.prod, coeff_prod]
      congr! 3 with l hl i hi
      obtain ⟨hl₁, -⟩ := mem_finsuppAntidiag.mp hl
      have : (l i).degree ≤ d.degree :=
        hl₁ ▸ Finsupp.degree_mono (single_le_sum_of_canonicallyOrdered hi)
      exact_mod_cast (coeff_truncTotal_pow _ (by nlinarith [hx i])).symm
    · exact ha.truncTotal

Goal state after:
case neg
σ : 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
⊢ MvPolynomial.coeff d ((truncTotal k) (subst a f)) =
    MvPolynomial.coeff d ((truncTotal k) (subst (fun i ↦ ↑((truncTotal (x i)) (a i))) f))
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 τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
aux : ∀ {n : σ →₀ ℕ}, (coeff d) (n.prod fun s e ↦ a s ^ e) ≠ 0 → Finsupp.degree n ≤ Finsupp.degree d
⊢ ∑ x ∈ Set.Finite.toFinset h2, (coeff x) f • (coeff d) (x.prod fun s e ↦ a s ^ e) =
    ∑ i ∈ Set.Finite.toFinset h2,
      (coeff i) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (i.prod fun s e ↦ a s ^ e)

Tactic:
congr! 2 with n hn

Goal state after:
case pos.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 τ
k : ℕ
ha : HasSubst a
ha₁ : ∀ (i : σ), constantCoeff (a i) = 0
d : τ →₀ ℕ
hd : Finsupp.degree d < k
h1 : Function.HasFiniteSupport fun d_1 ↦ (coeff d_1) f • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
h2 :
  Function.HasFiniteSupport fun d_1 ↦
    (coeff d_1) (∑ i ∈ range k, (homogeneousComponent i) f) • (coeff d) (d_1.prod fun s e ↦ a s ^ e)
this : Set.Finite.toFinset h2 ⊆ Set.Finite.toFinset h1
aux : ∀ {n : σ →₀ ℕ}, (coeff d) (n.prod fun s e ↦ a s ^ e) ≠ 0 → Finsupp.degree n ≤ Finsupp.degree d
n : σ →₀ ℕ
hn : n ∈ Set.Finite.toFinset h2
⊢ (coeff n) f = (coeff n) (∑ i ∈ range k, (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 τ
k : ℕ
inst✝ : Finite σ
h : ∀ (i : σ), constantCoeff (a i) = 0
⊢ (truncTotal k) (subst a (∑ i ∈ range k, (homogeneousComponent i) f)) = (truncTotal k) (subst a ↑((truncTotal k) f))

Tactic:
truncTotal_eq_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 : ℕ
inst✝ : Finite σ
h : ∀ (i : σ), constantCoeff (a i) = 0
⊢ (truncTotal k) (subst a (∑ i ∈ range k, (homogeneousComponent i) f)) =
    (truncTotal k) (subst a (∑ i ∈ range k, (homogeneousComponent i) f))
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
q : ℕ
hq : IsPrimePow q
f : PowerSeries R
hf : PowerSeries.constantCoeff f = 1
⊢ ((ofPowerSeries q) f).IsMultiplicative

Tactic:
refine ⟨(ofPowerSeries_apply_one q f).trans hf, fun {m n} hmn ↦ ?_⟩
  obtain ⟨p, k, hp, hk, rfl⟩ := hq
  rw [← Nat.prime_iff] at hp
  rw [ofPowerSeries_pow p hk.ne']
  by_cases hm : ∃ i, p ^ i = m
  · obtain ⟨i, rfl⟩ := hm
    by_cases hn : ∃ j, p ^ j = n
    · obtain ⟨j, rfl⟩ := hn
      cases i
      · simp [hk.ne', hf]
      · cases j
        · simp [hk.ne', hf]
        · simp [hp.ne_one] at hmn
    · simp_rw [ofPowerSeries_apply hp.one_lt]
      rw [Function.extend_apply', Function.extend_apply' _ _ _ hn,
        Pi.zero_apply, Pi.zero_apply, mul_zero]
      contrapose! hn
      obtain ⟨j, hj⟩ := hn
      obtain ⟨v, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp (Dvd.intro_left _ hj.symm)
      exact ⟨v, rfl⟩
  · simp_rw [ofPowerSeries_apply hp.one_lt]
    rw [Function.extend_apply', Function.extend_apply' _ _ _ hm,
      Pi.zero_apply, Pi.zero_apply, zero_mul]
    contrapose! hm
    obtain ⟨i, hi⟩ := hm
    obtain ⟨j, -, rfl⟩ := (Nat.dvd_prime_pow hp).mp ⟨n, hi⟩
    exact ⟨j, rfl⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
x : E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ
hc : x ∈ 0 • s
⊢ x = 0

Tactic:
by
    grw [zero_smul_set_subset, Set.mem_zero] at hc
    exact hc

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
h : AccPt x (𝓟 s)
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x))

Tactic:
by simp [tangentConeAt_eq_univ h]

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.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 : E →ₗ[𝕜] F
hg : comap (⇑g) (𝓝 0) ≤ 𝓝 0
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V ((⇑g ∘ f) x)

Tactic:
rcases mem_comap.1 (hg hU) with ⟨V, hV, hgV⟩

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 : E →ₗ[𝕜] F
hg : comap (⇑g) (𝓝 0) ≤ 𝓝 0
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV : V ∈ 𝓝 0
hgV : ⇑g ⁻¹' V ⊆ U
⊢ ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V ((⇑g ∘ f) 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 : E →ₗ[𝕜] F
hg : comap (⇑g) (𝓝 0) ≤ 𝓝 0
⊢ f =O[𝕜; l] (⇑g ∘ f)

Tactic:
constructor
  intro U hU
  rcases mem_comap.1 (hg hU) with ⟨V, hV, hgV⟩
  use V, hV
  filter_upwards with a
  refine le_egauge_of_forall_ne_zero (mem_of_mem_nhds hV) fun c hc₀ hc ↦ ?_
  apply egauge_le_of_mem_smul
  grw [← hgV, ← (IsUnit.mk0 _ hc₀).preimage_smul_set]
  exact hc

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
f : 𝕜 → F
L : Filter (𝕜 × 𝕜)
inst✝ : ContinuousSMul 𝕜 F
f' : 𝕜 →L[𝕜] F
⊢ HasFDerivAtFilter f f' L ↔ HasDerivAtFilter f (f' 1) L

Tactic:
by simp [HasDerivAtFilter]

Goal state after:
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 :
  (𝓝 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)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ x ∈ I, U x ∈ 𝓝 0
Ub : ∀ x ∈ I, Balanced 𝕜 (U x)
⊢ ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, (egauge 𝕜 (I.pi fun i ↦ U i) fun i ↦ f i x) ≤ ↑ε * egauge 𝕜 j (g x)

Tactic:
have := fun i hi ↦ (h i).eventually_smallSets (U i) (hU i hi)

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)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ x ∈ I, U x ∈ 𝓝 0
Ub : ∀ x ∈ I, Balanced 𝕜 (U x)
this :
  ∀ i ∈ I,
    ∀ᶠ (V : Set F) in (𝓝 0).smallSets,
      ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ ↑ε * egauge 𝕜 V (g x)
⊢ ∃ j ∈ 𝓝 0, ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, (egauge 𝕜 (I.pi fun i ↦ U i) fun i ↦ f i x) ≤ ↑ε * egauge 𝕜 j (g x)
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 :
  (𝓝 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)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ x ∈ I, U x ∈ 𝓝 0
Ub : ∀ x ∈ I, Balanced 𝕜 (U x)
⊢ ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, (egauge 𝕜 (I.pi fun i ↦ U i) fun i ↦ f i x) ≤ egauge 𝕜 j (g x)

Tactic:
have := fun i hi ↦ (h i).eventually_smallSets (U i) (hU i hi)

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)
I : Set ι
U : (i : ι) → Set (E i)
hIf : I.Finite
hU : ∀ x ∈ I, U x ∈ 𝓝 0
Ub : ∀ x ∈ I, Balanced 𝕜 (U x)
this : ∀ i ∈ I, ∀ᶠ (V : Set F) in (𝓝 0).smallSets, ∀ᶠ (x : α) in l, egauge 𝕜 (U i) (f i x) ≤ egauge 𝕜 V (g x)
⊢ ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, (egauge 𝕜 (I.pi fun i ↦ U i) fun i ↦ f i x) ≤ egauge 𝕜 j (g x)
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
⊢ constFormalMultilinearSeries 𝕜 E 0 = 0

Tactic:
ext n
  induction n <;> simp

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : G [×n]→L[𝕜] G'
x y : G
⊢ ((((curryFinFinset 𝕜 G G' hk hl) f) fun x_1 ↦ x) fun x ↦ y) = f (s.piecewise (fun x_1 ↦ x) fun x ↦ y)

Tactic:
refine (curryFinFinset_symm_apply_piecewise_const hk hl _ _ _).symm.trans ?_
  rw [LinearIsometryEquiv.symm_apply_apply]

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

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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : y ∈ Metric.eball x r
⊢ AnalyticWithinAt 𝕜 f univ y

Tactic:
exact hf.analyticWithinAt_of_mem (by simpa using h)

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

Goal state before:
pp: case pos
𝕜 : 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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
hr : p.radius = 0
⊢ AnalyticOnNhd 𝕜 p.sum (Metric.eball 0 p.radius)

Tactic:
simp [hr]

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

Goal state before:
pp: m M N : ℕ
i : (n : ℕ) × Composition n
hi : i ∈ compPartialSumTargetSet m M N
⊢ ∃ j, ∃ (hj : j ∈ compPartialSumSource m M N), compChangeOfVariables m M N j hj = i

Tactic:
by
  rcases i with ⟨n, c⟩
  refine ⟨⟨c.length, c.blocksFun⟩, ?_, ?_⟩
  · simp only [compPartialSumTargetSet, Set.mem_ofPred_eq] at hi
    simp only [mem_compPartialSumSource_iff, hi.left, hi.right, true_and, and_true]
    exact fun a => c.one_le_blocks' _
  · dsimp [compChangeOfVariables]
    rw [Composition.sigma_eq_iff_blocks_eq]
    simp only [Composition.blocksFun]
    conv_rhs => rw [← List.ofFn_get c.blocks]

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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ a * ‖↑i.symm‖ +
      ∑ x_1 ∈ Ico 2 (n + 1),
        a ^ x_1 *
          (‖↑i.symm‖ * ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖) =
    ‖↑i.symm‖ * a +
      ‖↑i.symm‖ * C *
        ∑ k ∈ Ico 2 (n + 1),
          a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖

Tactic:
mul_assoc C,

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
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ a * ‖↑i.symm‖ +
      ∑ x_1 ∈ Ico 2 (n + 1),
        a ^ x_1 *
          (‖↑i.symm‖ *
            ∑ x_2 ∈ {c | 1 < c.length}.toFinset, C * (r ^ x_2.length * ∏ j, ‖p.rightInv i x (x_2.blocksFun j)‖)) =
    ‖↑i.symm‖ * a +
      ‖↑i.symm‖ * C *
        ∑ k ∈ Ico 2 (n + 1),
          a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j, ‖p.rightInv i x (c.blocksFun j)‖
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s

Tactic:
by
  refine ⟨?_, AnalyticOnNhd.analyticOn⟩
  intro hf x m
  rcases Metric.mem_nhds_iff.mp (hs.mem_nhds m) with ⟨r, r0, rs⟩
  rcases hf x m with ⟨p, t, fp⟩
  exact ⟨p, min (.ofReal r) t,
  { r_pos := lt_min (by positivity) fp.r_pos
    r_le := min_le_of_right_le fp.r_le
    hasSum := by
      intro y ym
      simp only [mem_eball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at ym
      refine fp.hasSum ?_ ym.2
      apply mem_insert_of_mem
      apply rs
      simp only [mem_ball, dist_self_add_left, ym.1] }⟩

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

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ HasFDerivAtFilter (g ∘ f) (g' ∘SL f') L

Tactic:
refine .of_isLittleOTVS <| calc
    (fun p ↦ (g ∘ f) p.1 - (g ∘ f) p.2 - (g' ∘L f') (p.1 - p.2))
      = fun p ↦ (g (f p.1) - g (f p.2) - g' (f p.1 - f p.2)) +
          g' (f p.1 - f p.2 - f' (p.1 - p.2)) := by
      ext; simp
    _ =o[𝕜; L] (fun p ↦ p.1 - p.2) := .add ?Hg ?Hf

Goal state after:
case Hg
𝕜 : 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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ (fun p ↦ g (f p.1) - g (f p.2) - g' (f p.1 - f p.2)) =o[𝕜; L] fun p ↦ p.1 - p.2

case Hf
𝕜 : 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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ (fun p ↦ g' (f p.1 - f p.2 - f' (p.1 - p.2))) =o[𝕜; L] fun p ↦ p.1 - p.2
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x ↦ ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x ↦ 1
n : ℕ
⊢ max ‖p n‖ ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖

Tactic:
refine (max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)).trans ?_

Goal state after:
case a
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
r : ℝ≥0
hr : ↑r < p.radius ∧ ↑r < q.radius
this : (fun x ↦ ‖p x‖ * ↑r ^ x + ‖q x‖ * ↑r ^ x) =O[atTop] fun x ↦ 1
n : ℕ
⊢ ‖p n‖ + ‖q n‖ ≤ ‖‖p n‖ + ‖q n‖‖
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ (pf.unshift z).radius

Tactic:
rw [FormalMultilinearSeries.radius_unshift]
    exact hf.r_le

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ (pf.unshift z).radius

Tactic:
rw [FormalMultilinearSeries.radius_unshift]
    exact hf.r_le

Goal state after: