mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)))).op))
            x,
          (ConcreteCategory.hom (δ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.castSucc.succ)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
          stdSimplex.objMk₁ j.castSucc.succ).2
      k

Tactic:
rw [stdSimplex.δ_objMk₁_of_le _ _ (by simpa using! Fin.le_of_lt hij)]

Goal state after:
case snd
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
k : Fin (n + 1 + 1)
⊢ ((ConcreteCategory.hom
              (X.map
                (stdSimplex.objEquiv
                    ((ConcreteCategory.hom (δ Δ[n + 1] i.succ))
                      (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)))).op))
            x,
          stdSimplex.objMk₁ (j.castSucc.castSucc.succ.castPred ⋯)).2
      k =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
            (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
          stdSimplex.objMk₁ j.castSucc.succ).2
      k
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
j : Fin (n + 2)
hj : j < i.castSucc
⊢ stdSimplex.δ j ≫ r.map = const x

Tactic:
δ_map_of_lt _ j hj

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f g : X.PtSimplex n x
i : Fin (n + 1)
r : f.RelStruct g i
f' g' : X.PtSimplex n x
hf : f = f'
hg : g = g'
j : Fin (n + 2)
hj : j < i.castSucc
⊢ const x = const x
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv

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
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
h : (↑f').range = ⊤
f'symm : f'.NonlinearRightInverse := ⋯
c : ℝ≥0 := ⋯
hc : c = f'symm.nnnorm⁻¹ / 2
f'symm_pos : 0 < f'symm.nnnorm
cpos : 0 < c
s : Set E
s_nhds : s ∈ 𝓝 a
hs : ApproximatesLinearOn f f' s c
⊢ f'symm.nnnorm⁻¹ ≠ 0

Tactic:
simp [ne_of_gt f'symm_pos]

Goal state after:
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
x : F
⊢ v x ^ 1 = w x

Tactic:
rcases eq_or_ne x 0 with rfl | h₀

Goal state after:
case inl
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
⊢ v 0 ^ 1 = w 0

case inr
F : Type u_1
inst✝ : Field F
v w : AbsoluteValue F ℝ
h : v.IsEquiv w
hw : ¬w.IsNontrivial
x : F
h₀ : x ≠ 0
⊢ v x ^ 1 = w x
Module: Mathlib.Analysis.AbsoluteValue.Equivalence

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u : ι
⊢ Tendsto (fun i ↦ (WithAbs.equiv (v u)).symm (y i)) atTop (𝓝 (∑ j, Pi.single j (z j) u))

Tactic:
y,

Goal state after:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : Finite ι
v : ι → AbsoluteValue F ℝ
h : ∀ (i : ι), (v i).IsNontrivial
hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)
this : Fintype ι
z : (i : ι) → WithAbs (v i)
r : ℝ
hr : r > 0
a : ι → F
hx : ∀ (i : ι), 1 < (v i) (a i) ∧ ∀ (j : ι), j ≠ i → (v j) (a i) < 1
y : ℕ → F := fun n ↦ ∑ i, 1 / (1 + (a i)⁻¹ ^ n) * (WithAbs.equiv (v i)) (z i)
u : ι
⊢ Tendsto (fun i ↦ (WithAbs.equiv (v u)).symm (∑ i_1, 1 / (1 + (a i_1)⁻¹ ^ i) * (WithAbs.equiv (v i_1)) (z i_1))) atTop
    (𝓝 (∑ j, Pi.single j (z j) u))
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
⊢ analyticOrderAt (f • g) z₀ = ↑(analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀)

Tactic:
(hf.smul hg).analyticOrderAt_eq_natCast

Goal state after:
case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
g : 𝕜 → E
z₀ : 𝕜
f : 𝕜 → 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
hf' : ¬analyticOrderAt f z₀ = ⊤
hg' : ¬analyticOrderAt g z₀ = ⊤
f' : 𝕜 → 𝕜
h₁f' : AnalyticAt 𝕜 f' z₀
h₂f' : f' z₀ ≠ 0
h₃f' : f =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt f z₀ • f' z
g' : 𝕜 → E
h₁g' : AnalyticAt 𝕜 g' z₀
h₂g' : g' z₀ ≠ 0
h₃g' : g =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ analyticOrderNatAt g z₀ • g' z
⊢ ∃ g_1,
    AnalyticAt 𝕜 g_1 z₀ ∧
      g_1 z₀ ≠ 0 ∧
        ∀ᶠ (z : 𝕜) in 𝓝 z₀, (f • g) z = (z - z₀) ^ (analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀) • g_1 z
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
this : CauchySeq u
x : E
hx : Tendsto u atTop (𝓝 x)
xmem : x ∈ closedBall b ε
⊢ Tendsto u atTop (𝓝[closedBall b ε] x)

Tactic:
simp only [nhdsWithin, tendsto_inf, hx, true_and, tendsto_principal]

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
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
this : CauchySeq u
x : E
hx : Tendsto u atTop (𝓝 x)
xmem : x ∈ closedBall b ε
⊢ ∀ᶠ (a : ℕ) in atTop, u a ∈ closedBall b ε
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
h : (edgeMk f).CompStruct (edgeMk g) (edgeMk (f ≫ g))
⊢ homEquiv ((edgeMk (f ≫ g)).toTruncated.map φ) =
    homEquiv ((edgeMk f).toTruncated.map φ) ≫ homEquiv ((edgeMk g).toTruncated.map φ)

Tactic:
exact (nerve.homEquiv_comp (h.toTruncated.map φ)).symm

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
⊢ analyticOrderAt f z₀ = ↑n + 1 ↔ analyticOrderAt (deriv f) z₀ = ↑n

Tactic:
by
  have H {m : ℕ} {n : ℕ∞} : n = m ↔ m ≤ n ∧ ¬ m + 1 ≤ n := by
    cases n with | top => simp | coe _ => norm_cast; lia
  rw [← Nat.cast_add_one n, H, H, analyticOrderAt_deriv_ge_iff hf hzero, ← Nat.cast_add_one n,
    analyticOrderAt_deriv_ge_iff hf hzero]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : 𝕜
f g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt (f + g) x ↔ MeromorphicAt f x

Tactic:
by
  rw [add_comm]
  exact meromorphicAt_add_iff_meromorphicAt₁ hg

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv

Goal state before:
pp: x✝ : ℂ
⊢ -sin x✝ / cos x✝ = -(sin x✝ / cos x✝)

Tactic:
neg_div

Goal state after:
x✝ : ℂ
⊢ -(sin x✝ / cos x✝) = -(sin x✝ / cos x✝)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
⊢ MeromorphicAt (f ∘ fun x ↦ x - c) x ↔ MeromorphicAt f (x - c)

Tactic:
sub_eq_add_neg,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x c : 𝕜
f : 𝕜 → E
⊢ MeromorphicAt (f ∘ fun x ↦ x + -c) x ↔ MeromorphicAt f (x + -c)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
by_cases h : UniqueDiffWithinAt ℂ s x

Goal state after:
case pos
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
⊢ MeromorphicOn (f ∘ fun x ↦ x - c) U ↔ MeromorphicOn f (U - {c})

Tactic:
sub_eq_add_neg,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
⊢ MeromorphicOn (f ∘ fun x ↦ x + -c) U ↔ MeromorphicOn f (U + -{c})
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case pos
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
rw [uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin] at h

Goal state after:
case pos
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : (𝓝[s \ {x}] x).NeBot
hc : c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
⊢ choose r 1 = r

Tactic:
rw [choose_one_right', npow_one]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
inst✝¹ : SecondCountableTopology 𝕜
inst✝ : CompleteSpace E
h : MeromorphicOn f U
⊢ ({z | AnalyticAt 𝕜 f z}ᶜ ∩ U).Countable

Tactic:
apply (HereditarilyLindelofSpace.isLindelof _).countable_of_isDiscrete
    (isDiscrete_of_codiscreteWithin _)
  simpa using! eventually_codiscreteWithin_analyticAt f h

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

Goal state before:
pp: case e'_9
a : ℕ
z : ℂ
⊢ (1 - z) ^ (a + 1) = (1 - z) ^ (↑a + 1)

pp: case e'_10
a n : ℕ
⊢ ↑((a + n).choose a) = Ring.choose (↑a + 1 + ↑n - 1) n

Tactic:
· norm_cast

Goal state after:
case e'_10
a n : ℕ
⊢ ↑((a + n).choose a) = Ring.choose (↑a + 1 + ↑n - 1) n
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x ↦ x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ ContDiff ℝ ↑(n + 1) fun x ↦ x ^ p

Tactic:
rw [Nat.cast_add_one, contDiff_succ_iff_deriv, deriv_rpow_const' p]

Goal state after:
case succ
n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x ↦ x ^ p
p : ℝ
h : ↑n ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ fun x ↦ x ^ p) ∧
    (↑n = ⊤ → AnalyticOn ℝ (fun x ↦ x ^ p) Set.univ) ∧ ContDiff ℝ ↑n fun x ↦ p * x ^ (p - 1)
Module: Mathlib.Analysis.Analytic.RadiusLiminf

Goal state before:
pp: case a
𝕜 : 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
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ p.radius ≤ liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop

Tactic:
refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Goal state after:
case a
𝕜 : 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
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < p.radius
⊢ ↑r ≤ liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
Module: Mathlib.Analysis.Analytic.RadiusLiminf

Goal state before:
pp: case a
𝕜 : 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
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop ≤ p.radius

Tactic:
refine ENNReal.le_of_forall_nnreal_lt fun r hr => ?_

Goal state after:
case a
𝕜 : 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
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
r : ℝ≥0
hr : ↑r < liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
⊢ ↑r ≤ p.radius
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a b : ℝ
⊢ HasFPowerSeriesOnBall (fun x ↦ (b - a) / (1 - x) + a / (1 - x) ^ 2)
    (FormalMultilinearSeries.ofScalars ℝ fun x ↦ a * ↑x + b) 0 1

Tactic:
by
  convert!
    (one_div_one_sub_hasFPowerSeriesOnBall_zero.const_smul (c := b - a)).add
      (one_div_one_sub_sq_hasFPowerSeriesOnBall_zero.const_smul (c := a)) using 2
  · simp [div_eq_mul_inv]
  · ext; simp; ring

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

Goal state before:
pp: u : ℕ → EReal
⊢ linearGrowthSup (-u) = -linearGrowthInf u

Tactic:
rw [linearGrowthInf, ← limsup_neg]
  refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
  rw [Pi.neg_apply, Pi.neg_apply, div_eq_mul_inv, div_eq_mul_inv, ← neg_mul]

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

Goal state before:
pp: ⊢ expGrowthInf 0 ≤ ⊥

Tactic:
rw [← expGrowthSup_zero]

Goal state after:
⊢ expGrowthInf 0 ≤ expGrowthSup 0
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
v_top : Tendsto v atTop atTop
u_0 : u = ⊥
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u

Tactic:
rw [u_0, Pi.bot_comp, linearGrowthSup_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ - 0 = μ

Tactic:
rw [sub_def]
  apply le_antisymm
  · simp [sInf_le]
  · simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ ∫ (a : α), g i a • (f a - c) + g i a • c ∂μ = ∫ (y : α), g i y • f y ∂μ

Tactic:
simp only [smul_sub, sub_add_cancel]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ∞
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞

Tactic:
by
  by_cases hl : HaveLebesgueDecomposition μ ν
  · suffices (∫⁻ x in toMeasurable μ s, μ.rnDeriv ν x ∂ν) < ∞ from
      lt_of_le_of_lt (lintegral_mono_set (subset_toMeasurable _ _)) this
    rw [← withDensity_apply _ (measurableSet_toMeasurable _ _)]
    calc
      _ ≤ (singularPart μ ν) (toMeasurable μ s) + _ := le_add_self
      _ = μ s := by rw [← Measure.add_apply, ← haveLebesgueDecomposition_add, measure_toMeasurable]
      _ < ⊤ := hs.lt_top
  · simp only [Measure.rnDeriv, dif_neg hl, Pi.zero_apply, lintegral_zero, ENNReal.zero_lt_top]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: x y : ℝ
hxy : x < y
⊢ dist ((x + y) / 2) x ≤ 1 * ((y - x) / 2)

Tactic:
Real.dist_eq,

Goal state after:
x y : ℝ
hxy : x < y
⊢ |(x + y) / 2 - x| ≤ 1 * ((y - x) / 2)
Module: Mathlib.MeasureTheory.Covering.OneDim

Goal state before:
pp: x y : ℝ
hxy : x < y
⊢ dist y ((x + y) / 2) ≤ 1 * ((y - x) / 2)

Tactic:
Real.dist_eq,

Goal state after:
x y : ℝ
hxy : x < y
⊢ |y - (x + y) / 2| ≤ 1 * ((y - x) / 2)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this✝ : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
hξε : (ξ + E.indicator fun x ↦ ↑ε) ∈ measurableLE ν μ
this : ∫⁻ (a : α), ξ a + E.indicator (fun x ↦ ↑ε) a ∂ν ≤ sSup (measurableLEEval ν μ)
⊢ ∫⁻ (a : α), ξ a ∂ν < ∫⁻ (a : α), ξ a ∂ν + ↑ε * ν E

Tactic:
refine ENNReal.lt_add_right ?_ (ENNReal.mul_pos_iff.2 ⟨ENNReal.coe_pos.2 hε₁, hE₂⟩).ne'

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this✝ : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : 0 < ν E
hE₃ : ∀ (A : Set α), MeasurableSet A → ↑ε * ν (A ∩ E) ≤ (μ - ν.withDensity ξ) (A ∩ E)
hε₂ : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A ∩ E, ↑ε + ξ a ∂ν ≤ μ (A ∩ E)
hξε : (ξ + E.indicator fun x ↦ ↑ε) ∈ measurableLE ν μ
this : ∫⁻ (a : α), ξ a + E.indicator (fun x ↦ ↑ε) a ∂ν ≤ sSup (measurableLEEval ν μ)
⊢ ∫⁻ (a : α), ξ a ∂ν ≠ ∞
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
hst : t ⊆ s
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }),
    ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) ≤ eVariationOn f s

Tactic:
rintro ⟨n, ⟨u, hu, ut⟩⟩

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
hst : t ⊆ s
n : ℕ
u : ℕ → α
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) ≤ eVariationOn f s
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
E : Type u_2
inst✝² : PseudoEMetricSpace E
f : α → E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
hf : BoundedVariationOn f univ
a x : α
hx : ContinuousWithinAt f (Ici x) x
this : variationOnFromTo f univ a = fun y ↦ variationOnFromTo f univ a x + variationOnFromTo f univ x y
⊢ ContinuousWithinAt f (univ ∩ Ici x) x

Tactic:
simpa using hx

Goal state after: