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

Goal state before:
pp: case pos.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.2 < q
⊢ (coeff x.1) f * (coeff x.2) g =
    (if (weight w) x.1 = p then (coeff x.1) f else 0) * if (weight w) x.2 = q then (coeff x.2) g else 0

Tactic:
if_neg (ne_of_lt h),

Goal state after:
case pos.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
d : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hd : (weight w) x.1 + (weight w) x.2 = p + q
hx : x.1 + x.2 = d
h : (weight w) x.2 < q
⊢ (coeff x.1) f * (coeff x.2) g = (if (weight w) x.1 = p then (coeff x.1) f else 0) * 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff n) φ ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑n

Tactic:
simpa using ⟨n, le_rfl, h⟩

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
⊢ uR • ↑J ∪ (uR * uR) • ↑J ⊆ uR • ↑J ∪ uR • ↑J

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
I : Submodule R M
hI : ↑I ∈ 𝓝 0
J : Submodule R' M
hJ : ↑J ∈ 𝓝 0
J_sub_I : ↑J ⊆ ↑I
uR : Set R := univ
uR' : Set R' := univ
hRR : uR * uR ⊆ uR
hRI : uR • ↑I ⊆ ↑I
hR'J : uR' • ↑J ⊆ ↑J
hRJ : uR • ↑J ⊆ ↑I
S : Set M := ↑J ∪ uR • ↑J
S_sub_I : S ⊆ ↑I
hRS : uR • S ⊆ S
⊢ uR' • ↑J ∪ uR • uR' • ↑J ⊆ ↑J ∪ uR • ↑J

Tactic:
by gcongr

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : ¬d = 1
⊢ 0 = Polynomial.X.coeff d

Tactic:
rw [coeff_X_of_ne_one h₂]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ ∑ p ∈ antidiagonal (φ.order.toNat + ψ.order.toNat), (coeff p.1) φ * (coeff p.2) ψ ≠ 0

Tactic:
Finset.sum_eq_single_of_mem ⟨φ.order.toNat, ψ.order.toNat⟩ (by simp)

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ (coeff (φ.order.toNat, ψ.order.toNat).1) φ * (coeff (φ.order.toNat, ψ.order.toNat).2) ψ ≠ 0

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ ≠ 0 ∧ ψ ≠ 0
⊢ ∀ b ∈ antidiagonal (φ.order.toNat + ψ.order.toNat),
    b ≠ (φ.order.toNat, ψ.order.toNat) → (coeff b.1) φ * (coeff b.2) ψ = 0
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
d : σ →₀ ℕ
hd : d ∈ D
⊢ ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, φ (MvPolynomial.coeff d p) ∈ I

Tactic:
have : Tendsto (φ ∘ coeff d ∘ toMvPowerSeries) (𝓝 0) (𝓝 0) :=
      hφ.comp (continuous_coeff R d) |>.comp continuous_induced_dom |>.tendsto' 0 0 (map_zero _)
    filter_upwards [this.eventually_mem hI] with f hf
    simpa using hf

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : UniformSpace R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝² : IsUniformAddGroup R
inst✝¹ : IsUniformAddGroup S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁵.toTopologicalSpace, inst✝³.toTopologicalSpace] ⇑φ
ha : HasEval a
I : Ideal S
hI : ↑I ∈ 𝓝 0
n : σ → ℕ := fun s ↦ sInf {n | a s ^ n.succ ∈ I}
hn_ne : ∀ (s : σ), {n | a s ^ n.succ ∈ I}.Nonempty
hn : (Function.support n).Finite
n₀ : σ →₀ ℕ := Finsupp.ofSupportFinite n hn
D : Set (σ →₀ ℕ) := Iic n₀
hD : D.Finite
this : ∀ᶠ (x : MvPolynomial σ R) in 𝓝 0, ∀ i ∈ D, φ (MvPolynomial.coeff i x) ∈ I
p : MvPolynomial σ R
hp : ∀ i ∈ D, φ (MvPolynomial.coeff i p) ∈ I
d : σ →₀ ℕ
a✝ : d ∈ p.support
hd : d ∉ D
⊢ φ (MvPolynomial.coeff d p) * ∏ i ∈ d.support, a i ^ d i ∈ I

Tactic:
apply Ideal.mul_mem_left
    simp only [mem_Iic, D, Finsupp.le_iff] at hd
    push Not at hd
    rcases hd with ⟨s, hs', hs⟩
    exact I.prod_mem hs' (I.pow_mem_of_pow_mem (Nat.sInf_mem (hn_ne s)) hs)

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : UniformSpace R
S : Type u_3
inst✝⁸ : CommRing S
inst✝⁷ : UniformSpace S
φ : R →+* S
a : σ → S
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : IsUniformAddGroup R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : CompleteSpace S
inst✝² : T2Space S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous[inst✝⁹.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑φ
ha : HasEval a
⊢ ⇑(eval₂Hom hφ ha) = eval₂ φ a

Tactic:
by
  ext f
  simp only [eval₂Hom_eq_extend, eval₂]
  split_ifs with h
  · obtain ⟨p, rfl⟩ := h
    simpa [MvPolynomial.coe_eval₂Hom] using
      toMvPowerSeries_isDenseInducing.extend_eq
        (toMvPowerSeries_uniformContinuous hφ ha).continuous p
  · rw [← eval₂Hom_eq_extend hφ ha]

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

Goal state before:
pp: case zero
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hn : f 0 = true
⊢ f_max 0 = true

pp: case succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
n✝ : ℕ
hn : f (n✝ + 1) = true
⊢ f_max (n✝ + 1) = true

Tactic:
· rw [fn] at hn
        contradiction

Goal state after:
case succ
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn✝ : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
n✝ : ℕ
hn : f (n✝ + 1) = true
⊢ f_max (n✝ + 1) = true
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case zero
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunction c f_max < cantorFunction c g_min

Tactic:
convert! this

Goal state after:
case e'_3
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunction c f_max = c / (1 - c)

case e'_4
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunction c g_min = 1
Module: Mathlib.NumberTheory.LSeries.Basic

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

Tactic:
rw [eventuallyEq_iff_exists_mem] at h ⊢

Goal state after:
f g : ℕ → ℂ
s : ℂ
h : ∃ s ∈ cofinite, Set.EqOn f g s
hf : LSeriesSummable f s
⊢ ∃ s_1 ∈ cofinite, Set.EqOn (term f s) (term g s) s_1
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: s : ℂ
n : ℕ
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  · rcases eq_or_ne n 1 with hn' | hn' <;>
    simp [hn, hn', delta]

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_div,

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‖ ≤ ‖↑C‖ / ‖↑n ^ (s + (1 - ↑x))‖
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: 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

Tactic:
· rw [ofPowerSeries_apply (one_lt_pow' hq hk), Function.extend_apply', Pi.zero_apply]
        simp_rw [← pow_mul, Nat.pow_right_inj hq, eq_comm, ← dvd_def]
        exact hn

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

Goal state before:
pp: 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
⊢ k ≤ Finsupp.degree n → (coeff n) f = 0

Tactic:
have : n.degree ≤ d.degree := by
        simp only [map_sum, Set.Finite.mem_toFinset, Function.mem_support, ne_eq] at hn
        exact aux (right_ne_zero_of_smul 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
this : Finsupp.degree n ≤ Finsupp.degree d
⊢ k ≤ Finsupp.degree n → (coeff n) f = 0
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
s : Set E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ 0 • s
⊢ ∀ (c : ℝ≥0∞), ‖0‖ₑ < c → r < c

Tactic:
intro b hb

Goal state after:
case inr
𝕜 : Type u_1
inst✝³ : NormedDivisionRing 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s : Set E
inst✝ : (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hs₀ : 0 ∈ s
h : ∀ (c : 𝕜), c ≠ 0 → 0 ∈ c • s → r ≤ ‖c‖ₑ
hc : 0 ∈ 0 • s
b : ℝ≥0∞
hb : ‖0‖ₑ < b
⊢ r < b
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
⊢ rescale 1 = RingHom.id (MvPowerSeries σ R)

Tactic:
by
  ext f n
  simp [coeff_rescale, Finsupp.prod]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he : (single 0 (e 0), single 1 (e 1)) ∉ antidiagonal e
he' : single 0 (e 0) + single 1 (e 1) = e
⊢ (MvPowerSeries.coeff (single 0 (e 0), single 1 (e 1)).1) (subst X₀ f) *
      (MvPowerSeries.coeff (single 0 (e 0), single 1 (e 1)).2) (subst X₁ f) =
    0

Tactic:
exact absurd (mem_antidiagonal.mpr he') he

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
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
x : α
hx₁ : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
hx₂ : egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ ↑ε * egauge 𝕜 V (g x) ≤ ↑ε * egauge 𝕜 W (k x)

Tactic:
by gcongr

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 : α → F
U : Set E
hU : U ∈ 𝓝 0
V₁ V₂ : Set F
hV : V₁ ⊆ V₂
hV₂ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V₂ (g x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V₂ (g x)
⊢ ↑ε * egauge 𝕜 V₂ (g x) ≤ ↑ε * egauge 𝕜 V₁ (g x)

Tactic:
by gcongr

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 : α → F
U : Set E
hU : U ∈ 𝓝 0
V₁ V₂ : Set F
hV : V₁ ⊆ V₂
hV₂ : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 V₂ (g x)
x : α
hx : egauge 𝕜 U (f x) ≤ egauge 𝕜 V₂ (g x)
⊢ egauge 𝕜 V₂ (g x) ≤ egauge 𝕜 V₁ (g x)

Tactic:
by gcongr

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
⊢ (fun x ↦ (f x, g x)) =o[𝕜; l] k

Tactic:
((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isLittleOTVS_iff
    (basis_sets _)

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
⊢ ∀ (i : Set E × Set F),
    (i.1 ∈ 𝓝 0 ∧ Balanced 𝕜 i.1) ∧ i.2 ∈ 𝓝 0 ∧ Balanced 𝕜 i.2 →
      ∃ j ∈ 𝓝 0,
        ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i.1 ×ˢ id i.2) (f x, g x) ≤ ↑ε * egauge 𝕜 (id j) (k x)
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
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_arg : Tendsto (fun n ↦ x + d n) l (𝓝[s] x)
this : (fun n ↦ c n • (f (x + d n) - f x) - f' (c n • d n)) =o[𝕜; l] 1
⊢ Tendsto (fun n ↦ c n • (f (x + d n) - f x)) l (𝓝 (f' v))

Tactic:
rw [isLittleOTVS_one] at this

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_arg : Tendsto (fun n ↦ x + d n) l (𝓝[s] x)
this : Tendsto (fun n ↦ c n • (f (x + d n) - f x) - f' (c n • d n)) l (𝓝 0)
⊢ Tendsto (fun n ↦ c n • (f (x + d n) - f x)) l (𝓝 (f' v))
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
h : HasFDerivWithinAt f f' t x
hst : s ⊆ t
⊢ 𝓝[s] x ×ˢ pure x ≤ 𝓝[t] x ×ˢ pure x

Tactic:
by gcongr

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : ¬AccPt x (𝓟 s)
⊢ HasFDerivWithinAt f f' s x

Tactic:
accPt_principal_iff_nhdsWithin,

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
s : Set E
h : ¬(𝓝[s \ {x}] x).NeBot
⊢ HasFDerivWithinAt f f' s x
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : TopologicalSpace F
f : E → F
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)
this : (fun x_1 ↦ f x_1 - f x) =o[𝕜; L] 1
⊢ Tendsto f L (𝓝 (f x))

Tactic:
rw [isLittleOTVS_one] at this

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)
this : Tendsto (fun x_1 ↦ f x_1 - f x) L (𝓝 0)
⊢ Tendsto f L (𝓝 (f x))
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

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
f : E → F
f' : E →L[𝕜] F
x₀ : E
hf : HasFDerivAt f f' x₀
s : Set E
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ ↑C

Tactic:
by
  refine hf.le_of_lip' C.coe_nonneg ?_
  filter_upwards [hs] with x hx using hlip.norm_sub_le hx (mem_of_mem_nhds hs)

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

Goal state before:
pp: case h₁
α : 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‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑ε_1 * egauge 𝕜 (ball 0 ↑δ) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x)
⊢ ↑δ / ↑δ ≤ 1

Tactic:
exact ENNReal.div_self_le_one

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

Goal state before:
pp: case h₂
α : 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‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑ε_1 * egauge 𝕜 (ball 0 ↑δ) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 ↑ε) (f x) ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x)
⊢ ↑‖c‖₊ / ↑‖c‖₊ ≤ 1

Tactic:
exact ENNReal.div_self_le_one

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

Goal state before:
pp: case h₁
α : 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‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < ↑ε
hx : ↑‖f x‖₊ ≤ ↑ε * ↑δ / ↑‖c‖₊ * ↑‖g x‖₊
⊢ ↑‖c‖₊ / ↑‖c‖₊ ≤ 1

Tactic:
exact ENNReal.div_self_le_one

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

Goal state before:
pp: case h₂
α : 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‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < ↑ε
hx : ↑‖f x‖₊ ≤ ↑ε * ↑δ / ↑‖c‖₊ * ↑‖g x‖₊
⊢ ↑ε / ↑ε ≤ 1

Tactic:
exact ENNReal.div_self_le_one

Goal state after: