mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.Basic

Goal state before:
pp: n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this✝ : FiberBundle F E := a.toFiberBundle
this : VectorBundle 𝕜 F E := toVectorBundle a
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
⊢ b ∈ e.baseSet ∩ e'.baseSet →
    ↑(Trivialization.coordChangeL 𝕜 (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
          (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b) =
      contMDiffCoordChange n IB a he he' b

Tactic:
hb

Goal state after:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
EB : Type u_7
inst✝⁹ : NormedAddCommGroup EB
inst✝⁸ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝⁷ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁶ : TopologicalSpace B
inst✝⁵ : ChartedSpace HB B
inst✝⁴ : (x : B) → AddCommMonoid (E x)
inst✝³ : (x : B) → Module 𝕜 (E x)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff IB a n
this✝¹ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this✝ : FiberBundle F E := a.toFiberBundle
this : VectorBundle 𝕜 F E := toVectorBundle a
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ ↑(Trivialization.coordChangeL 𝕜 (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
        (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b) =
    contMDiffCoordChange n IB a he he' b
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁸ : TopologicalSpace H
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
G : Type u_7
inst✝⁶ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
M' : Type u_10
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n m : ℕ∞ω
h : M ≃ₘ^n⟮I, J⟯ N
f : N → M'
s : Set M
hm : m ≤ n
x✝ : M
⊢ x✝ ∈ s → ContMDiffWithinAt I I' m (f ∘ ⇑h) s x✝ ↔
    h.toEquiv x✝ ∈ ⇑h.symm ⁻¹' s → ContMDiffWithinAt J I' m f (⇑h.symm ⁻¹' s) (h.toEquiv x✝)

Tactic:
simp only [hm, coe_toEquiv, h.symm_apply_apply, contMDiffWithinAt_comp_diffeomorph_iff,
      mem_preimage]

Goal state after:
Module: Mathlib.Geometry.Manifold.BumpFunction

Goal state before:
pp: E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ tsupport ↑f ⊆ ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)

Tactic:
rw [tsupport, support_eq_symm_image]

Goal state after:
E : Type uE
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝¹ : FiniteDimensional ℝ E
inst✝ : T2Space M
⊢ closure[inst✝³] (↑(extChartAt I c).symm '' (ball (↑(extChartAt I c) c) f.rOut ∩ range ↑I)) ⊆
    ↑(extChartAt I c).symm '' (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: case refine_3
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
x : X
⊢ ∀ (x_1 : ι), (∃ x_2, (∃ i, ∃ (_ : ind i = x_1), x_2 ∈ t i) ∧ x_2 ∈ U x) → x_1 ∈ ind '' {i | ∃ x_2 ∈ t i, x_2 ∈ U x}

Tactic:
rintro i ⟨y, ⟨a, rfl, hya⟩, hyU⟩

Goal state after:
case refine_3
ι : Type u
X : Type v
inst✝¹ : TopologicalSpace X
inst✝ : ParacompactSpace X
u : ι → Set X
uo : ∀ (a : ι), IsOpen[inst✝¹] (u a)
uc : ⋃ i, u i = univ
α : Type v
t : α → Set X
hto : ∀ (b : α), IsOpen[inst✝¹] (t b)
ind : α → ι
hind : ∀ (b : α), t b ⊆ u (ind b)
t_inv : X → α
ht_inv : ∀ (x : X), x ∈ t (t_inv x)
U : X → Set X
hxU : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | (t i ∩ U x).Nonempty}.Finite
x y : X
hyU : y ∈ U x
a : α
hya : y ∈ t a
⊢ ind a ∈ ind '' {i | ∃ x_1 ∈ t i, x_1 ∈ U x}
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: ι : Type u
X : Type v
Y : Type w
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : R1Space X
inst✝ : ParacompactSpace X
⊢ NormalSpace X

Tactic:
have : ∀ s t : Set X, IsClosed s →
      (∀ x ∈ s, ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ t ⊆ v ∧ Disjoint u v) →
      ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v := fun s t hs H ↦ by
    /- For each `x ∈ s` we choose open disjoint `u x ∋ x` and `v x ⊇ t`. The sets `u x` form an
        open covering of `s`. We choose a locally finite refinement `u' : s → Set X`, then
        `⋃ i, u' i` and `(closure (⋃ i, u' i))ᶜ` are disjoint open neighborhoods of `s` and `t`. -/
    choose u v hu hv hxu htv huv using SetCoe.forall'.1 H
    rcases precise_refinement_set hs u hu fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, hxu _⟩ with
      ⟨u', hu'o, hcov', hu'fin, hsub⟩
    refine ⟨⋃ i, u' i, (closure (⋃ i, u' i))ᶜ, isOpen_iUnion hu'o, isClosed_closure.isOpen_compl,
      hcov', ?_, disjoint_compl_right.mono le_rfl (compl_le_compl subset_closure)⟩
    rw [hu'fin.closure_iUnion, compl_iUnion, subset_iInter_iff]
    refine fun i x hxt hxu ↦
      absurd (htv i hxt) (closure_minimal ?_ (isClosed_compl_iff.2 <| hv _) hxu)
    exact fun y hyu hyv ↦ (huv i).le_bot ⟨hsub _ hyu, hyv⟩
  -- Now we apply the lemma twice: first to `s` and `t`, then to `t` and each point of `s`.
  refine { normal := fun s t hs ht hst ↦ this s t hs fun x hx ↦ ?_ }
  rcases this t {x} ht fun y hy ↦ (by
    simp_rw [singleton_subset_iff]
    exact r1_separation <| ht.not_inseparable hy <| hst.notMem_of_mem_left hx)
    with ⟨v, u, hv, hu, htv, hxu, huv⟩
  exact ⟨u, v, hu, hv, singleton_subset_iff.1 hxu, htv, huv.symm⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp

Goal state before:
pp: α : Type u_1
G : Type u_2
p : ℝ≥0∞
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
f : α → G
hf : MemLp f p μ
hf_meas : StronglyMeasurable f
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ FinStronglyMeasurable f μ

Tactic:
borelize G
  have : SeparableSpace (Set.range f ∪ {0} : Set G) :=
    hf_meas.separableSpace_range_union_singleton
  let fs := SimpleFunc.approxOn f hf_meas.measurable (Set.range f ∪ {0}) 0 (by simp)
  refine ⟨fs, ?_, ?_⟩
  · have h_fs_Lp : ∀ n, MemLp (fs n) p μ :=
      SimpleFunc.memLp_approxOn_range hf_meas.measurable hf
    exact fun n => (fs n).measure_support_lt_top_of_memLp (h_fs_Lp n) hp_ne_zero hp_ne_top
  · intro x
    apply SimpleFunc.tendsto_approxOn
    apply subset_closure
    simp

Goal state after:
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✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
⊢ ∃ v,
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))

Tactic:
have : Nonempty (PartialRefinement u s (fun w => IsCompact (closure w))) :=
    ⟨⟨u, ∅, uo, us, False.elim, False.elim, fun _ => rfl⟩⟩

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
hs : IsCompact s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ x ∈ s, {i | x ∈ u i}.Finite
us : s ⊆ ⋃ i, u i
this : Nonempty (PartialRefinement u s fun w ↦ IsCompact (closure w))
⊢ ∃ v,
    s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ (∀ (i : ι), closure (v i) ⊆ u i) ∧ ∀ (i : ι), IsCompact (closure (v i))
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_3
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
U : M → Set M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed[inst✝⁴] s
hU : ∀ x ∈ s, U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
hB : ∀ x ∈ s, (𝓝 x).HasBasis (fun f ↦ tsupport ↑f ⊆ U x) fun f ↦ support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ a, support ↑(f a)
hfin : LocallyFinite fun a ↦ support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed[inst✝⁴] (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι), V i ⊆ (chartAt H (c i)).source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
i : ι
⊢ tsupport
      ↑({ c := c, toFun := fun i ↦ (f i).updateRIn (r i) ⋯, c_mem' := hcs, locallyFinite' := ⋯,
              eventuallyEq_one' := ⋯ }.toFun
          i) ⊆
    U
      ({ c := c, toFun := fun i ↦ (f i).updateRIn (r i) ⋯, c_mem' := hcs, locallyFinite' := ⋯,
            eventuallyEq_one' := ⋯ }.c
        i)

Tactic:
· simpa only [SmoothBumpFunction.support_updateRIn, tsupport] using hfU i

Goal state after:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: ι : Type uι
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
inst✝⁴ : FiniteDimensional ℝ E
n : ℕ∞
M : Type u_1
inst✝³ : MetricSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I ∞ M
inst✝ : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x (δ x) ⊆ U i

Tactic:
rcases Metric.exists_contMDiffMap_forall_closedEBall_subset I hK hU hKU hfin with ⟨δ, hδ0, hδ⟩
  refine ⟨δ, hδ0, fun i x hx => ?_⟩
  rw [← Metric.closedEBall_ofReal (hδ0 _).le]
  exact hδ i x hx

Goal state after:
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case neg
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
H : Type uH
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
inst✝³ : FiniteDimensional ℝ E
inst✝² : IsManifold I ∞ M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
n : ℕ∞
s : Set M
hs : IsOpen[inst✝⁵] s
f : SmoothPartitionOfUnity M I M
hf : f.IsSubordinate fun x ↦ (chartAt H x).source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).target ∩ ↑(chartAt H c).symm ⁻¹' s
g_diff : ∀ (c : M), ContMDiff I 𝓘(ℝ, ℝ) (↑n) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ (f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∉ s
c : M
Hx : x ∉ tsupport ⇑(f c)
⊢ (f c) x * g c (↑(chartAt H c) x) = 0

Tactic:
have : x ∉ support (f c) := by contrapose Hx; exact subset_tsupport _ Hx
        rw [notMem_support] at this
        simp [this]

Goal state after:
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
hg : Integrable g μ
v x : E
hx : LineDifferentiableAt ℝ f x v
⊢ Tendsto (fun n ↦ n⁻¹ • (f (x + n • v) - f x) * g x) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f x v * g x))

Tactic:
exact hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds

Goal state after:
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f g : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
h'f : HasCompactSupport f
hg : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] g
v : E
K : Set E := cthickening ‖v‖ (tsupport f)
K_compact : IsCompact K
x : E
hx : LineDifferentiableAt ℝ f x v
⊢ Tendsto (fun n ↦ n⁻¹ • (f (x + n • v) - f x) * g x) (𝓝[>] 0) (𝓝 (lineDeriv ℝ f x v * g x))

Tactic:
exact hx.hasLineDerivAt.tendsto_slope_zero_right.mul tendsto_const_nhds

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := fun n ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ l ∈ tangentConeAt 𝕜 s x

Tactic:
apply mem_tangentConeAt_of_seq atTop (c ∘ φ) (d ∘ φ)

Goal state after:
case refine_1.hd₀
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := ⋯
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (d ∘ φ) atTop (𝓝 0)

case refine_1.hds
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := ⋯
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, x + (d ∘ φ) n ∈ s

case refine_1.hcd
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : ℕ → E := ⋯
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : ℕ → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : l ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖)
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (fun n ↦ (c ∘ φ) n • (d ∘ φ) n) atTop (𝓝 l)
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
N : ℕ
x✝ : True
n : ℕ
hn : N ≤ n
this : ‖c‖ ^ n * ‖d n‖ < 1 / 2 ^ N
⊢ (fun x ↦ c ^ x) n • d n ∈ Metric.ball 0 ((1 / 2) ^ N)

Tactic:
simpa [norm_smul]

Goal state after:
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
b : β
⊢ b ∈ Ici (f a) → b ∈ ⋃ i ∈ Ici a, Ico (f i) (f (succ i))

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
b : β
hb : b ∈ Ici (f a)
⊢ b ∈ ⋃ i ∈ Ici a, Ico (f i) (f (succ i))
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
b : β
⊢ b ∈ Ioi (f a) → b ∈ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
b : β
hb : b ∈ Ioi (f a)
⊢ b ∈ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
m n : α
⊢ ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)

Tactic:
by
  rcases le_total n m with hnm | hmn
  · rw [Ico_eq_empty_of_le hnm, Ioc_eq_empty_of_le (hf hnm), biUnion_empty]
  · refine Succ.rec ?_ ?_ hmn
    · simp
    · intro k hmk ihk
      rw [← Ioc_union_Ioc_eq_Ioc (hf hmk) (hf <| le_succ _), union_comm, ← ihk]
      by_cases hk : IsMax k
      · rw [hk.succ_eq, Ioc_self, empty_union]
      · rw [Ico_succ_right_eq_insert_of_not_isMax hmk hk, biUnion_insert]

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

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a b : ℝ
f : ℝ → F
hf : AbsolutelyContinuousOnInterval f a b
⊢ AbsolutelyContinuousOnInterval (-f) a b

Tactic:
apply squeeze_zero (fun t ↦ ?_) (fun t ↦ ?_) (by simpa using! hf)
  · exact Finset.sum_nonneg (fun i hi ↦ by positivity)
  · simp

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

Goal state before:
pp: a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
⊢ deriv p x - deriv q x = deriv (p - q) x

Tactic:
have hx₆ : uIcc a b ∈ 𝓝 x := Icc_mem_nhds hx₄.left (lt_of_le_of_ne hx₄.right hx₃)

Goal state after:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
hx₆ : uIcc a b ∈ 𝓝 x
⊢ deriv p x - deriv q x = deriv (p - q) x
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
C : ℝ≥0
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : FiniteDimensional ℝ F
inst✝ : μ.IsAddHaarMeasure
f : E → F
h : LipschitzOnWith C f univ
⊢ ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x

Tactic:
simpa [differentiableWithinAt_univ] using h.ae_differentiableWithinAt_of_mem

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

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall x r)

Tactic:
← vadd_closedBall_zero

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (x +ᵥ closedBall 0 r)
Module: Mathlib.Analysis.Convex.StrictConvexSpace

Goal state before:
pp: case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall x r)

Tactic:
rw [← vadd_closedBall_zero]

Goal state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : PartialOrder 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (x +ᵥ closedBall 0 r)
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : E → F
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
hne : z ≠ w
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
this : ‖(f ∘ e) 1‖ = ‖(f ∘ e) 0‖
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w

Tactic:
by simpa [e]

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

Goal state before:
pp: z : ℂ
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

Tactic:
by_cases! h : ∀ k : ℤ, z ≠ (2 * k + 1) * π / 2

Goal state after:
case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

case neg
z : ℂ
h : ∃ k, z = (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ tan (z + z) = (tan z + tan z) / (1 - tan z * tan z)

Tactic:
tan_add (Or.inl ⟨h, h⟩)

Goal state after:
case pos
z : ℂ
h : ∀ (k : ℤ), z ≠ (2 * ↑k + 1) * ↑π / 2
⊢ (tan z + tan z) / (1 - tan z * tan z) = (tan z + tan z) / (1 - tan z * tan z)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: z : ℂ
h :
  ((∀ (k : ℤ), ↑z.re ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑z.im * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑z.re = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑z.im * I = (2 * ↑l + 1) * ↑π / 2
⊢ tan z = (tan ↑z.re + tanh ↑z.im * I) / (1 - tan ↑z.re * tanh ↑z.im * I)

Tactic:
convert! tan_add_mul_I h; exact (re_add_im z).symm

Goal state after: