mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
⊢ ∃ i, 0 < (f i) x

Tactic:
have H := f.sum_eq_one hx

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∑ᶠ (i : ι), (f i) x = 1
⊢ ∃ i, 0 < (f i) x
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∀ᶠ (y : X) in 𝓝 x₀, ρ.fintsupport y ⊆ ρ.fintsupport x₀

Tactic:
apply (ρ.locallyFinite.closure.eventually_subset (fun _ ↦ isClosed_closure) x₀).mono

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ ∀ (x : X),
    {i | x ∈ closure[inst✝] (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure[inst✝] (support ⇑(ρ i))} →
      ρ.fintsupport x ⊆ ρ.fintsupport x₀
Module: Mathlib.Topology.ShrinkingLemma

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

Tactic:
suffices ∀ i, i ∈ v.carrier from
    ⟨v, v.subset_iUnion, fun i => v.isOpen _, fun i => v.closure_subset (this i)⟩

Goal state after:
ι : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝ : NormalSpace X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this✝ : Nonempty (PartialRefinement u s ⊤)
this : ∀ (c : Set (PartialRefinement u s ⊤)), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ∃ ub, ∀ v ∈ c, v ≤ ub
v : PartialRefinement u s ⊤
hv : IsMax v
⊢ ∀ (i : ι), i ∈ v.carrier
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → IntegrableOn f s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫ (x : α) in s, f x ∂μ = 0
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ∞
⊢ f =ᵐ[μ.restrict t] 0

Tactic:
by
  suffices h_and : f ≤ᵐ[μ.restrict t] 0 ∧ 0 ≤ᵐ[μ.restrict t] f from
    h_and.1.mp (h_and.2.mono fun x hx1 hx2 => le_antisymm hx2 hx1)
  refine
    ⟨?_,
      ae_nonneg_restrict_of_forall_setIntegral_nonneg hf_int_finite
        (fun s hs hμs => (hf_zero s hs hμs).symm.le) ht hμt⟩
  suffices h_neg : 0 ≤ᵐ[μ.restrict t] -f by
    refine h_neg.mono fun x hx => ?_
    rw [Pi.neg_apply] at hx
    simpa using hx
  refine
    ae_nonneg_restrict_of_forall_setIntegral_nonneg (fun s hs hμs => (hf_int_finite s hs hμs).neg)
      (fun s hs hμs => ?_) ht hμt
  simp_rw [Pi.neg_apply]
  rw [integral_neg, neg_nonneg]
  exact (hf_zero s hs hμs).le

Goal state after:
Module: Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff

Goal state before:
pp: case refine_2
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen[inst✝⁵] U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
h : ∫ (x : ↑↑U), Function.extend Subtype.val g 0 ↑x • f ↑x ∂Measure.comap Subtype.val μ = 0
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
⊢ ∫ (x : ↥U), g x • f ↑x ∂Measure.comap Subtype.val μ = 0

Tactic:
simp_rw [Subtype.val_injective.extend_apply] at h

Goal state after:
case refine_2
E : Type u_1
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
inst✝⁷ : CompleteSpace F
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : IsManifold I ∞ M
inst✝² : MeasurableSpace M
inst✝¹ : BorelSpace M
inst✝ : T2Space M
f : M → F
μ : Measure M
U✝ : Set M
hU : IsOpen[inst✝⁵] U✝
hSig : IsSigmaCompact U✝
hf : LocallyIntegrableOn f U✝ μ
meas_U : MeasurableSet U✝
U : Opens M := { carrier := U✝, is_open' := hU }
this : SigmaCompactSpace ↥U
g : ↥U → ℝ
g_smth : ContMDiff I 𝓘(ℝ, ℝ) ∞ g
g_supp : HasCompactSupport g
h : ∫ (x : ↑↑U), g x • f ↑x ∂Measure.comap Subtype.val μ = 0
⊢ ∫ (x : ↥U), g x • f ↑x ∂Measure.comap Subtype.val μ = 0
Module: Mathlib.Analysis.Calculus.TangentCone.Seq

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
c : 𝕜
hc : 1 < ‖c‖
d : ℕ → E
hds : ∀ (n : ℕ), x + d n ∈ s
hd : ∀ (n : ℕ), ‖d n‖ < (1 / (2 * ‖c‖)) ^ n
⊢ Tendsto (fun n ↦ (fun x ↦ c ^ x) n • d n) atTop (𝓝 0)

Tactic:
rw [atTop_basis.tendsto_iff (Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one)]
        refine fun N _ ↦ ⟨N, trivial, fun n hn ↦ ?_⟩
        rw [Set.mem_Ici] at hn
        suffices ‖c‖ ^ n * ‖d n‖ < 1 / (2 ^ N) by simpa [norm_smul]
        rw [← lt_div_iff₀' (by positivity)]
        refine (hd n).trans_le ?_
        grw [hn]
        · simp [mul_pow, div_eq_inv_mul]
        · norm_num1

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case hh
⊢ Tendsto (fun E ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)) totalLengthFilter (𝓝 0)

pp: case hgf
⊢ (fun x ↦ 0) ≤ fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)

pp: case hfh
⊢ (fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) ≤ fun E ↦
    ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)

Tactic:
· convert! ENNReal.tendsto_ofReal (Filter.tendsto_comap)
    simp

Goal state after:
case hgf
⊢ (fun x ↦ 0) ≤ fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)

case hfh
⊢ (fun E ↦ volume (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)) ≤ fun E ↦
    ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, x_1 ∈ {x}ᶜ → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ}, 0 < α → ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
⊢ ∃ a ∈ t, (Prod.snd - Prod.fst) a = ε ∧ a.1 = x

Tactic:
refine ⟨(x, x + ε), ⟨⟨hx.1.1, by linarith, by linarith⟩, ?_⟩, by simp, rfl⟩

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, x_1 ∈ {x}ᶜ → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
evn_bound : ∀ {α : ℝ}, 0 < α → ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε < α
evn_pos : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, 0 < ε
ε : ℝ
hε₁ : 0 < ε
hε₂ : ε < η
hε₃ : ε < δ
hε₄ : ε < (b - x) / 2
⊢ dist (slope f (x, x + ε).1 (x, x + ε).2) (f' (x, x + ε).1) < η
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum : ∀ (s : Finset ↑u) (g : ℝ → ℝ → ℝ), ∑ b ∈ s, g (↑b).1 (↑b).2 = ∑ z ∈ u_coe s, g z.1 z.2
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ : Tendsto (fun s ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2)) (SummationFilter.unconditional ↑u).filter (𝓝 y)
sum_tendsto :
  Tendsto
    (fun x ↦ ∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2) + ∑ z ∈ u_coe x, dist (f z.1) (f z.2))
    atTop (𝓝 y)
s : Finset ↑u
⊢ dist (f d) (f b) ≤
    dist (f ((T s).2 0).1) (f ((T s).2 (u_coe s).card).1) +
      dist (f ((T s).2 (u_coe s).card).1) (f ((T s).2 (u_coe s).card).2)

Tactic:
← dist_triangle

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum : ∀ (s : Finset ↑u) (g : ℝ → ℝ → ℝ), ∑ b ∈ s, g (↑b).1 (↑b).2 = ∑ z ∈ u_coe s, g z.1 z.2
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ : Tendsto (fun s ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2)) (SummationFilter.unconditional ↑u).filter (𝓝 y)
sum_tendsto :
  Tendsto
    (fun x ↦ ∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2) + ∑ z ∈ u_coe x, dist (f z.1) (f z.2))
    atTop (𝓝 y)
s : Finset ↑u
⊢ dist (f d) (f b) ≤ dist (f ((T s).2 0).1) (f ((T s).2 (u_coe s).card).2)
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖

Tactic:
by
  rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
  rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha,
    norm_smul_of_nonneg hb, add_mul]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
y : F
hy : y ≠ 0
⊢ Set.InjOn Norm.norm {x | SameRay ℝ x y}

Tactic:
simpa only [SameRay.sameRay_comm] using norm_injOn_ray_left hy

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (fun x ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : ℝ → ℝ := fun x ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
obtain ⟨C, hC⟩ := g_ac.const_of_ae_hasDerivAt_zero g_ae_deriv_zero

Goal state after:
f : ℝ → ℝ
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
f_deriv_integral_ac : AbsolutelyContinuousOnInterval (fun x ↦ ∫ (v : ℝ) in a..x, deriv f v) a b
g : ℝ → ℝ := fun x ↦ f x - ∫ (t : ℝ) in a..x, deriv f t
g_ac : AbsolutelyContinuousOnInterval g a b
g_ae_deriv_zero : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt g 0 x
C : ℝ
hC : ∀ x ∈ uIcc a b, g x = C
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : x ∈ sphere 0 1
y : E
hy : y ∈ sphere 0 1
h₂ : ‖x + y‖ = 2
⊢ x = y

Tactic:
rw [mem_sphere_zero_iff_norm] at hx hy

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
h₂ : ‖x + y‖ = 2
⊢ x = y
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case right
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ∀ n ≥ B₂, ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range n, (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε

Tactic:
replace hB₂ := hB₂ (max B₁ B₂) (by simp)

Goal state after:
case right
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
g : ℂ → ℂ := fun z ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
⊢ ‖∑' (n : ℕ), f n * z ^ n - l‖ < ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case inr
x : ℂ
x_eq : ∃ k, x = (2 * ↑k + 1) * ↑π / 2
l : ℤ
⊢ ∃ l_1, -((2 * ↑l + 1) * ↑π / 2) = (2 * ↑l_1 + 1) * ↑π / 2

Tactic:
use -l - 1

Goal state after:
case h
x : ℂ
x_eq : ∃ k, x = (2 * ↑k + 1) * ↑π / 2
l : ℤ
⊢ -((2 * ↑l + 1) * ↑π / 2) = (2 * ↑(-l - 1) + 1) * ↑π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := ⋯
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ cos y ^ 2 ≠ 1

Tactic:
rw [cos_sq']

Goal state after:
x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ 1 - sin y ^ 2 ≠ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4

Tactic:
by
  rw [show 4 * arctan _ = 2 * (2 * _) by ring, two_mul_arctan, two_mul_arctan, ← arctan_one,
    sub_eq_iff_eq_add, arctan_add] <;> norm_num

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ x ∈ {y_1 | y_1 ∈ S ∧ y_1 < y} ∧ slope f y x = slope f x y

Tactic:
by simp only [slope_comm, mem_ofPred_eq, hxy, and_true]; exact interior_subset hxs

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

Goal state before:
pp: ⊢ ∀ (x : ℝ), ‖deriv cos x‖₊ ≤ 1

Tactic:
simpa using! abs_sin_le_one

Goal state after:
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case h
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ 1 - θ ^ 2 / 2 ≤ Real.cos θ

Tactic:
exact Real.one_sub_sq_div_two_le_cos

Goal state after:
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℤ
hn : ↑n ≠ 0
⊢ IsCoveringMapOn (fun x ↦ x ^ n) {0}ᶜ

Tactic:
by
  have (x : 𝕜) : x ^ n = 0 ↔ x = 0 := zpow_eq_zero_iff (by aesop)
  refine .of_isCoveringMap_restrictPreimage _ (by simp) ?_ ?_
  · convert isClosed_singleton (x := (0 : 𝕜)).isOpen_compl
    ext; simp [this]
  · convert! (isCoveringMap_zpow n hn).comp_homeomorph (.setCongr _) using 1
    ext; simpa using! (this _).not

Goal state after:
Module: Mathlib.Analysis.Complex.CoveringMap

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this : NeZero n
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(rootsOfUnity n 𝕜)

Tactic:
have := ((isClosedMap_pow 𝕜 n).restrictPreimage {0}ᶜ).isQuotientMap
    (by fun_prop) (.restrictPreimage _ surj)

Goal state after:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : ProperSpace 𝕜
n : ℕ
hn : ↑n ≠ 0
surj : Function.Surjective fun x ↦ x ^ n
this✝ : NeZero n
this : IsQuotientMap ({0}ᶜ.restrictPreimage fun x ↦ x ^ n)
⊢ IsQuotientCoveringMap (fun x ↦ x ^ n) ↥(rootsOfUnity n 𝕜)
Module: Mathlib.Topology.Homotopy.Lifting

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
ta : ↑I × A
x✝ : ta ∈ Set.Icc 0 (t Nat.zero) ×ˢ Set.univ
ht : ta.1 = 0
right✝ : ta.2 ∈ Set.univ
⊢ g ta = ((fun x ↦ g (0, x)) ∘ Prod.snd) ta

Tactic:
rw [← ta.eta, ht]

Goal state after:
case refine_1
E : Type u_1
X : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
p : E → X
f : C(↑I × A, X)
g : ↑I × A → E
g_lifts : p ∘ g = ⇑f
cont_0 : Continuous[inst✝, inst✝²] fun x ↦ g (0, x)
a : A
cont_a : Continuous[_, inst✝²] fun x ↦ g (x, a)
q : E → OpenPartialHomeomorph E X
mem_source : ∀ (x : E), x ∈ (q x).source
hpq : ∀ (x : E), p = ↑(q x)
t : ℕ → ↑I
t_0 : t 0 = 0
t_mono : Monotone t
t_sub : ∀ (n : ℕ), ∃ i, Set.Icc (t n) (t (n + 1)) ⊆ (fun x ↦ g (x, a)) ⁻¹' (q i).source
n_max : ℕ
h_max : ∀ m ≥ n_max, t m = 1
ta : ↑I × A
x✝ : ta ∈ Set.Icc 0 (t Nat.zero) ×ˢ Set.univ
ht : ta.1 = 0
right✝ : ta.2 ∈ Set.univ
⊢ g (0, ta.2) = ((fun x ↦ g (0, x)) ∘ Prod.snd) (0, ta.2)
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
⊢ (divisor (f₁ + f₂) U)⁻ ≤ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻

Tactic:
intro z
  by_cases! hz : z ∉ U
  · simp [hz]
  simp only [Function.locallyFinsuppWithin.negPart_apply, Function.locallyFinsuppWithin.max_apply]
  by_cases hf₁₂ : meromorphicOrderAt (f₁ + f₂) z = ⊤
  · simp [divisor_apply (hf₁.add hf₂) hz, hf₁₂, negPart_nonneg]
  rw [← negPart_min]
  apply ((le_iff_posPart_negPart _ _).1 (min_divisor_le_divisor_add hf₁ hf₂ hz hf₁₂)).2

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

Goal state before:
pp: case mpr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or : MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ ↑n < 0 ∧ f x = 0
h₂ : ↑n < 0
⊢ ∃ n g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g

Tactic:
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff h₁).1 hn.symm

Goal state after:
case mpr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₁ : MeromorphicAt f x
h₃ : f x = 0
n : ℤ
hn : ↑n = meromorphicOrderAt f x
meromorphicNFAt_iff_analyticAt_or : MeromorphicNFAt f x ↔ AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ ↑n < 0 ∧ f x = 0
h₂ : ↑n < 0
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ ∃ n g, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: case insert
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  (∀ i ∈ s, MeromorphicOn (f i) U) →
    (∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤) → divisor (∏ i ∈ s, f i) U = ∑ i ∈ s, divisor (f i) U
h₁f : ∀ i ∈ insert a s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
this : ∀ z ∈ U, meromorphicOrderAt (∏ i ∈ s, f i) z ≠ ⊤
⊢ divisor (f a) U + divisor (∏ n ∈ s, f n) U = divisor (f a) U + ∑ x ∈ s, divisor (f x) U

Tactic:
hs (fun i hi ↦ h₁f i (mem_insert_of_mem hi))
        (fun i hi ↦ h₂f i (mem_insert_of_mem hi))

Goal state after:
case insert
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  (∀ i ∈ s, MeromorphicOn (f i) U) →
    (∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤) → divisor (∏ i ∈ s, f i) U = ∑ i ∈ s, divisor (f i) U
h₁f : ∀ i ∈ insert a s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
this : ∀ z ∈ U, meromorphicOrderAt (∏ i ∈ s, f i) z ≠ ⊤
⊢ divisor (f a) U + ∑ i ∈ s, divisor (f i) U = divisor (f a) U + ∑ x ∈ s, divisor (f x) U
Module: Mathlib.Analysis.Meromorphic.NormalForm

Goal state before:
pp: case mpr.inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] (fun x_1 ↦ x_1 - x) ^ n • g
⊢ meromorphicOrderAt f x = 0

Tactic:
· have : n = 0 := by
        by_contra hContra
        have := h₃g.eq_of_nhds
        simp only [Pi.smul_apply', Pi.pow_apply, sub_self, zero_zpow n hContra, zero_smul] at this
        tauto
      simp only [this, zpow_zero] at h₃g
      apply (meromorphicOrderAt_eq_int_iff hf.meromorphicAt).2
      use g, h₁g, h₂g
      simp only [zpow_zero]
      exact h₃g.filter_mono nhdsWithin_le_nhds

Goal state after: