mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
⊢ ((bif f 0 then 1 else 0) + c * cantorFunction c fun n ↦ f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n ↦ g (n + 1)

Tactic:
hn 0 <| zero_lt_succ n

Goal state after:
case succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
⊢ ((bif g 0 then 1 else 0) + c * cantorFunction c fun n ↦ f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n ↦ g (n + 1)
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
⊢ ((bif f 0 then 1 else 0) + c * cantorFunction c fun n ↦ f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n ↦ g (n + 1)

Tactic:
rw [hn 0 <| zero_lt_succ n]

Goal state after:
case succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
n : ℕ
ih : ∀ {f g : ℕ → Bool}, (∀ k < n, f k = g k) → f n = false → g n = true → cantorFunction c f < cantorFunction c g
f g : ℕ → Bool
hn : ∀ k < n + 1, f k = g k
fn : f (n + 1) = false
gn : g (n + 1) = true
⊢ ((bif g 0 then 1 else 0) + c * cantorFunction c fun n ↦ f (n + 1)) <
    (bif g 0 then 1 else 0) + c * cantorFunction c fun n ↦ g (n + 1)
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
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
f : MvPowerSeries σ R
n : τ →₀ ℕ
hn : ¬n = 0
⊢ (coeff 0) f • (coeff n) (Finsupp.prod 0 fun s e ↦ 0 s ^ e) = (algebraMap R S) ((coeff n) (C (constantCoeff f)))

Tactic:
simp [coeff_C_of_ne_zero hn, coeff_one, hn]

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

Goal state before:
pp: ⊢ Fintype.card (Fin 2) = 2

Tactic:
Fintype.card_fin

Goal state after:
⊢ 2 = 2
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inl
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ 0 = f 0 / 0 ^ s

Tactic:
zero_cpow hs,

Goal state after:
case inl
s : ℂ
hs : s ≠ 0
f : ℕ → ℂ
⊢ 0 = f 0 / 0
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
⊢ 0 ≤ if n = 0 then 0 else a n / ↑n ^ ↑x

Tactic:
split_ifs with hn

Goal state after:
case pos
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
hn : n = 0
⊢ 0 ≤ 0

case neg
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
hn : ¬n = 0
⊢ 0 ≤ a n / ↑n ^ ↑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
w : τ → ℕ
ha : HasSubst a
f : MvPowerSeries σ R
⊢ ⨅ d, ⨅ (_ : (coeff d) f ≠ 0), (Finsupp.weight (weightedOrder w ∘ a)) d ≤ weightedOrder w (subst a f)

Tactic:
by
  apply MvPowerSeries.le_weightedOrder
  intro d hd
  rw [coeff_subst ha, finsum_eq_zero_of_forall_eq_zero]
  intro x
  by_cases hfx : f.coeff x = 0
  · simp [hfx]
  rw [coeff_eq_zero_of_lt_weightedOrder w, smul_zero]
  refine hd.trans_le (((biInf_le _ hfx).trans ?_).trans (le_weightedOrder_prod ..))
  simp only [Finsupp.weight_apply, Finsupp.sum, Function.comp_apply]
  exact Finset.sum_le_sum fun i hi ↦ .trans (by simp) (le_weightedOrder_pow ..)

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

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[atTop] g
hf : LSeriesSummable f s
⊢ LSeriesSummable g s

Tactic:
by
  rw [← Nat.cofinite_eq_atTop] at h
  refine (summable_norm_iff.mpr hf).of_norm_bounded_eventually ?_
  have : term f s =ᶠ[cofinite] term g s := by
    rw [eventuallyEq_iff_exists_mem] at h ⊢
    obtain ⟨S, hS, hS'⟩ := h
    refine ⟨S \ {0}, sdiff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩
    rw [Set.mem_sdiff, Set.mem_singleton_iff] at hn
    simp [hn.2, hS' hn.1]
  exact this.symm.mono fun n hn ↦ by simp [hn]

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ ∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re

Tactic:
replace h := h.norm
  use tsum fun n ↦ ‖term f s n‖
  by_contra! ⟨n, hn₀, hn⟩
  have := h.le_tsum n fun _ _ ↦ norm_nonneg _
  rw [norm_term_eq, if_neg hn₀,
    div_le_iff₀ <| Real.rpow_pos_of_pos (Nat.cast_pos.mpr <| Nat.pos_of_ne_zero hn₀) _] at this
  exact (this.trans_lt hn).false.elim

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

Goal state before:
pp: case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
hn' : 0 < ↑n ^ s.re
⊢ ‖f n‖ / ‖↑n ^ s‖ ≤ ‖↑C‖ / ‖↑n ^ (s + (1 - ↑x))‖

Tactic:
norm_natCast_cpow_of_pos hn,

Goal state after:
case inr
f : ℕ → ℂ
x : ℝ
s : ℂ
hs : x < s.re
C : ℝ
hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)
hC₀ : 0 ≤ C
hsum : Summable fun n ↦ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
n : ℕ
hn : n > 0
hn' : 0 < ↑n ^ s.re
⊢ ‖f n‖ / ↑n ^ s.re ≤ ‖↑C‖ / ↑n ^ (s + (1 - ↑x)).re
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

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

Tactic:
ext n
    split_ifs with hq
    · simp only [Algebra.algebraMap_eq_smul_one, coe_mk]
      by_cases hn : ∃ k, q ^ k = n
      · obtain ⟨k, rfl⟩ := hn
        simp [(Nat.pow_right_injective hq).extend_apply, one_apply, hq.ne']
      · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply, smul_map, one_apply_ne, smul_zero]
        contrapose hn
        exact ⟨0, by simp [hn]⟩
    · simp

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = if k ∣ i then (algebraMap R R) ((PowerSeries.coeff (i / k)) f) else 0

Tactic:
split_ifs with hn

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : k ∣ i
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = (algebraMap R R) ((PowerSeries.coeff (i / k)) f)

case neg
R : Type u_1
inst✝ : CommRing R
q k : ℕ
hk : k ≠ 0
f : PowerSeries R
hq : 1 < q
i : ℕ
hn : ¬k ∣ i
⊢ ((ofPowerSeries (q ^ k)) f) (q ^ i) = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
k : ℕ
hk : k ≠ 0
f : R⟦X⟧
n : ℕ
⊢ (coeff n) (subst (X ^ k) f) = if k ∣ n then (algebraMap R S) ((coeff (n / k)) f) else 0

Tactic:
split_ifs with h
  · rw [coeff_subst' (.X_pow hk), finsum_eq_single _ (n / k), ← pow_mul, Nat.mul_div_cancel' h,
      coeff_X_pow_self, Algebra.algebraMap_eq_smul_one]
    intro j hj
    rw [← pow_mul, coeff_X_pow, if_neg, smul_zero]
    contrapose hj
    rw [hj, Nat.mul_div_cancel_left j hk.pos]
  · rw [coeff_subst' (.X_pow hk), finsum_eq_zero_of_forall_eq_zero]
    intro j
    rw [← pow_mul, coeff_X_pow, if_neg, smul_zero]
    contrapose h
    use j

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

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
hc : 1 < ‖c‖
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝², non_trivial := ⋯ }
h₀ : 0 ≠ 0 ∨ ‖x‖ ≠ 0
⊢ egauge 𝕜 (ball 0 ↑0) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑0

Tactic:
rw [ENNReal.coe_zero, ENNReal.div_zero (mul_ne_zero _ _)]
    · apply le_top
    · simpa using one_pos.trans hc
    · simpa [enorm, ← NNReal.coe_eq_zero] using h₀

Goal state after:
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 : 𝕜
h : x ∉ tsupport f
⊢ deriv f x = 0

Tactic:
by
  rw [notMem_tsupport_iff_eventuallyEq] at h
  simp [h.deriv_eq]

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
g : α → F
l : Filter α
⊢ 0 =o[𝕜; l] g

Tactic:
by
  refine ⟨fun U hU ↦ ?_⟩
  use univ
  simp [egauge_zero_right _ (Filter.nonempty_of_mem hU), EventuallyLE]

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
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
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
⊢ ∃ j ∈ 𝓝 0,
    ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ ↑ε * egauge 𝕜 (id j) (k x)

Tactic:
rcases ((hf.eventually_smallSets U hU).and (hg.eventually_smallSets V hV)).exists_mem_of_smallSets
    with ⟨W, hW, hWf, hWg⟩

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
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =o[𝕜; l] k
hg : g =o[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 W (k x)
hWg : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)
⊢ ∃ j ∈ 𝓝 0,
    ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ ↑ε * egauge 𝕜 (id j) (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
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
⊢ ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)

Tactic:
rcases ((hf.eventually_smallSets U hU).and (hg.eventually_smallSets V hV)).exists_mem_of_smallSets
    with ⟨W, hW, hWf, hWg⟩

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
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)
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 𝕜
⊢ toSpanSingleton 𝕜 (derivWithin f s x) = fderivWithin 𝕜 f s x

Tactic:
by simp [derivWithin]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x₀ : 𝕜
C : ℝ≥0
hlip : LipschitzWith C f
⊢ ‖deriv f x₀‖ ≤ ↑C

Tactic:
simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lipschitz 𝕜 hlip

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

Goal state before:
pp: case empty
𝕜 : 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' ∅ x

Tactic:
| empty =>

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

Goal state before:
pp: case refine_1
𝕜 : 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
inst✝³ : ContinuousAdd E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (fun n ↦ ‖c n‖) l atTop
⊢ Tendsto (fun n ↦ (c n)⁻¹ • v) l (𝓝 0)

Tactic:
rw [tendsto_norm_atTop_iff_cobounded] at hc

Goal state after:
case refine_1
𝕜 : 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
inst✝³ : ContinuousAdd E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto c l (Bornology.cobounded 𝕜)
⊢ Tendsto (fun n ↦ (c n)⁻¹ • v) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.TVS

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

Tactic:
lift r to ℝ≥0 using hr₀.le

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

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

Tactic:
apply Eventually.exists_gt
      refine Continuous.tendsto' ?_ _ _ (by simp) |>.eventually_lt_const zero_lt_one
      fun_prop (disch := intros; first | apply ENNReal.coe_ne_top | positivity)

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
inst✝³ : ContinuousAdd E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (L ×ˢ pure x)
⊢ (fun x_1 ↦ f x_1 - f x) =o[𝕜; L] 1

Tactic:
refine h.isBigOTVS_sub |>.comp_tendsto prod_pure.ge |>.trans_isLittleOTVS ?_

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
f' : E →L[𝕜] F
x : E
inst✝³ : ContinuousAdd E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (L ×ˢ pure x)
⊢ ((fun p ↦ p.1 - p.2) ∘ fun a ↦ (a, x)) =o[𝕜; L] 1
Module: Mathlib.Analysis.Asymptotics.TVS

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

Tactic:
refine (egauge_le_one _ ha).trans ?_
        simp [hr₁]

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

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

Tactic:
lift r to ℝ≥0 using hr₀.le

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

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

Tactic:
lift r to ℝ≥0 using hr₀.le

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

Goal state before:
pp: case mpr
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
⊢ f =O[l] g → f =O[𝕜; l] g

Tactic:
· rw [nhds_basis_ball.isBigOTVS_iff nhds_basis_ball, isBigO_iff']
    have hc₀ : 0 < ‖c‖₊ := one_pos.trans hc
    rintro ⟨C, hC₀, hC⟩ r hr₀
    lift C to ℝ≥0 using hC₀.le; norm_cast at hC₀
    lift r to ℝ≥0 using hr₀.le; norm_cast at hr₀
    refine ⟨r / (C * ‖c‖₊), by positivity, hC.mono fun x hx ↦ ?_⟩
    calc
      egauge 𝕜 (ball 0 r) (f x) ≤ ‖c‖ₑ * ‖f x‖ₑ / r :=
        egauge_ball_le_of_one_lt_norm hc <| .inl hr₀.ne'
      _ ≤ ‖c‖ₑ * (C * ‖g x‖ₑ) / r := by
        gcongr
        simp only [enorm_eq_nnnorm, ← coe_nnnorm] at hx ⊢
        exact mod_cast hx
      _ = ‖g x‖ₑ / (r / (C * ‖c‖₊) : ℝ≥0) := by
        simp_all [pos_iff_ne_zero, ENNReal.div_eq_inv_mul, ENNReal.mul_inv]
        ac_rfl
      _ ≤ _ := div_le_egauge_ball _ _ _

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

Goal state before:
pp: case e'_5
𝕜 : 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
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
s : Finset (Fin n)
⊢ ‖p n‖₊ * r ^ s.card * r' ^ (n - s.card) = ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))

Tactic:
mul_assoc

Goal state after:
case e'_5
𝕜 : 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
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
s : Finset (Fin n)
⊢ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card)) = ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x✝ : Fin k → E
⊢ (∑' (n : ℕ), (p.changeOriginSeries k n) fun x_1 ↦ x) x✝ =
    (∑ k_1 ∈ Finset.range (n - k), (p.changeOriginSeries k k_1) fun x_1 ↦ x) x✝

Tactic:
tsum_eq_sum (f := fun m => p.changeOriginSeries k m (fun _ => x)) (s := Finset.range (n - k))

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x✝ : Fin k → E
⊢ (∑ b ∈ Finset.range (n - k), (p.changeOriginSeries k b) fun x_1 ↦ x) x✝ =
    (∑ k_1 ∈ Finset.range (n - k), (p.changeOriginSeries k k_1) fun x_1 ↦ x) x✝

𝕜 : 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
k : ℕ
x : E
x✝ : Fin k → E
⊢ ∀ b ∉ Finset.range (n - k), ((p.changeOriginSeries k b) fun x_1 ↦ x) = 0