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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
w✝ : LinearOrder ι
wf : WellFoundedLT ι
ind : α → ι := fun x ↦ ⋯.min {i | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → x ∈ s i → False
D : ℕ → ι → Set α :=
  fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
hD :
  D = fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ x,
        ⋃ (_ : ind x = i), ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔ ∃ x, ind x = i ∧ eball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : eball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := eball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), n + k + 1 ≤ m → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : eball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ 2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1) + (2⁻¹ ^ (n + k + 1) + 2⁻¹ ^ m) = 2 * (2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1))

Tactic:
simp only [two_mul, add_comm]

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

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
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : IsManifold I ∞ M
inst✝⁹ : SigmaCompactSpace M
inst✝⁸ : T2Space M
n : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
hU_covers_univ : univ ⊆ ⋃ x, U x
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate U
s : (x : M) → V x := fun x ↦ ∑ᶠ (j : M), (ρ j) x • s_loc j x
this : ∀ (j : M), ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, (ρ j) x • s_loc j x⟩
hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, s x⟩
⊢ ∃ s, ∀ (x : M), s x ∈ t x

Tactic:
refine ⟨⟨s, hs⟩, fun x ↦ ?_⟩

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
inst✝¹¹ : FiniteDimensional ℝ E
inst✝¹⁰ : IsManifold I ∞ M
inst✝⁹ : SigmaCompactSpace M
inst✝⁸ : T2Space M
n : ℕ∞
F_fiber : Type u_1
inst✝⁷ : NormedAddCommGroup F_fiber
inst✝⁶ : NormedSpace ℝ F_fiber
V : M → Type u_2
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : (x : M) → Module ℝ (V x)
inst✝² : TopologicalSpace (TotalSpace F_fiber V)
inst✝¹ : FiberBundle F_fiber V
inst✝ : VectorBundle ℝ F_fiber V
t : (x : M) → Set (V x)
ht_conv : ∀ (x : M), Convex ℝ (t x)
W : M → Set M
h_nhds : ∀ (x₀ : M), W x₀ ∈ 𝓝 x₀
s_loc : M → (x : M) → V x
s_smooth : ∀ (x₀ : M), ContMDiffOn I (I.prod 𝓘(ℝ, F_fiber)) (↑n) (fun x ↦ ⟨x, s_loc x₀ x⟩) (W x₀)
h_mem_t : ∀ (x₀ y : M), y ∈ W x₀ → s_loc x₀ y ∈ t y
U : M → Set M := fun x ↦ interior (W x)
hU_covers_univ : univ ⊆ ⋃ x, U x
ρ : SmoothPartitionOfUnity M I M
hρU : ρ.IsSubordinate U
s : (x : M) → V x := fun x ↦ ∑ᶠ (j : M), (ρ j) x • s_loc j x
this : ∀ (j : M), ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, (ρ j) x • s_loc j x⟩
hs : ContMDiff I (I.prod 𝓘(ℝ, F_fiber)) ↑n fun x ↦ ⟨x, s x⟩
x : M
⊢ { toFun := s, contMDiff_toFun := hs } x ∈ t x
Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), (fun x ↦ c (f x)) =ᵐ[μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable ↑d
s : ↑d → StrongDual 𝕜 E
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
A : ∀ a ∈ t, (∀ (x : ↑d), (s x) a = 0) → a = 0
hfs : ∀ (y : ↑d), ∀ᵐ (x : α) ∂μ, (s y) (f x) = 0
hf' : ∀ᵐ (x : α) ∂μ, ∀ (y : ↑d), (s y) (f x) = 0
x : α
hx : ∀ (y : ↑d), (s y) (f x) = 0
h'x : f x ∈ t
⊢ f x = 0 x

Tactic:
exact A (f x) h'x hx

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

Goal state before:
pp: 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
inst✝ : SigmaCompactSpace M
hf : LocallyIntegrable f μ
h : ∀ (g : M → ℝ), ContMDiff I 𝓘(ℝ, ℝ) ∞ g → HasCompactSupport g → ∫ (x : M), g x • f x ∂μ = 0
this✝² : LocallyCompactSpace H✝
this✝¹ : LocallyCompactSpace M
this✝ : SecondCountableTopology H✝
this : SecondCountableTopology M
x✝ : MetricSpace M := metrizableSpaceMetric M
s : Set M
hs : IsCompact s
δ : ℝ
δpos : 0 < δ
hδ : IsCompact (cthickening δ s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 δ
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set M := fun n ↦ thickening (u n) s
K : Set M
K_compact : IsCompact K
vK : ∀ (n : ℕ), v n ⊆ K
g : ℕ → M → ℝ
g_supp : ∀ (n : ℕ), support (g n) = v n
g_diff : ∀ (n : ℕ), ContMDiff I 𝓘(ℝ, ℝ) ∞ (g n)
g_range : ∀ (n : ℕ), range (g n) ⊆ Icc 0 1
hg : ∀ (n : ℕ), ∀ x ∈ s, g n x = 1
bound : M → ℝ := K.indicator fun x ↦ ‖f x‖
A : ∀ (n : ℕ), AEStronglyMeasurable (fun x ↦ g n x • f x) μ
B : Integrable bound μ
C : ∀ (n : ℕ), ∀ᵐ (x : M) ∂μ, ‖g n x • f x‖ ≤ bound x
x : M
hxs : x ∉ s
H : ∀ᶠ (n : ℕ) in atTop, g n x = 0
⊢ (fun x ↦ 0) =ᶠ[atTop] fun n ↦ g n x • f x

Tactic:
by
          filter_upwards [H] with n hn using by simp [hn]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
⊢ ∃ c, 0 < c ∧ c < ∞ ∧ map (⇑L) μ = (c * addHaar univ) • ν

Tactic:
have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
this : FiniteDimensional 𝕜 E
⊢ ∃ c, 0 < c ∧ c < ∞ ∧ map (⇑L) μ = (c * addHaar univ) • ν
Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
s : Set F
hs : MeasurableSet s
⊢ (∀ᵐ (x : E) ∂μ, L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : CompleteSpace 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝² : μ.IsAddHaarMeasure
inst✝¹ : ν.IsAddHaarMeasure
inst✝ : LocallyCompactSpace E
h : Function.Surjective ⇑L
s : Set F
hs : MeasurableSet s
this : FiniteDimensional 𝕜 E
⊢ (∀ᵐ (x : E) ∂μ, L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this : FiniteDimensional 𝕜 E
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace

Goal state before:
pp: 𝕜 : 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 ∈ closedBall 0 1 \ ball 0 (1 / ‖r‖), ∃ φ, StrictMono φ ∧ Tendsto ((fun n ↦ c n • d n) ∘ φ) atTop (𝓝 l)

Tactic:
apply IsCompact.tendsto_subseq _ (fun n ↦ ?_)
    · exact (isCompact_closedBall 0 1).diff Metric.isOpen_ball
    simp only [Set.mem_sdiff, Metric.mem_closedBall, dist_zero_right, (c_le n).le,
      Metric.mem_ball, not_lt, true_and, le_c n]

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

Goal state before:
pp: case refine_1
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
G : ℝ → ℝ → ℝ := fun c x ↦ slope g x (x + c)
G_integrable : ∀ (n : ℕ), Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b))
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), Tendsto (fun n ↦ (fun n x ↦ G (↑n)⁻¹ x) n x) atTop (𝓝 (deriv f x))

pp: case refine_2
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
G : ℝ → ℝ → ℝ := fun c x ↦ slope g x (x + c)
G_integrable : ∀ (n : ℕ), Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b))
⊢ liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖(fun n x ↦ G (↑n)⁻¹ x) n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)

Tactic:
· rw [← restrict_Ioo_eq_restrict_Icc, MeasureTheory.ae_restrict_iff' measurableSet_Ioo]
    filter_upwards [hg.ae_differentiableAt] with x hx₁ hx₂
    rw [hfg hx₂]
    exact hx₁.hasDerivAt.tendsto_slope.comp <|
      tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
      (by convert! tendsto_const_nhds.add (tendsto_inv_atTop_nhds_zero_nat (𝕜 := ℝ)); simp)
      (by simp [eventually_ne_atTop 0])

Goal state after:
case refine_2
f : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc a b)
g : ℝ → ℝ := fun x ↦ f (max a (min x b))
hg : Monotone g
hfg : EqOn (deriv f) (deriv g) (Ioo a b)
G : ℝ → ℝ → ℝ := fun c x ↦ slope g x (x + c)
G_integrable : ∀ (n : ℕ), Integrable (G (↑n)⁻¹) (volume.restrict (Icc a b))
⊢ liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖(fun n x ↦ G (↑n)⁻¹ x) n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x - taylorWithinEval f n (Icc a b) a x‖ ≤ sSup (g '' Icc a b) * (x - a) ^ (n + 1) / ↑n !

Tactic:
refine taylor_mean_remainder_bound hab hf hx fun y => ?_

Goal state after:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
n : ℕ
hab : a ≤ b
hf : ContDiffOn ℝ (↑n + 1) f (Icc a b)
h : a < b
g : ℝ → ℝ := fun y ↦ ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖
x : ℝ
hx : x ∈ Icc a b
y : ℝ
⊢ y ∈ Icc a b → ‖iteratedDerivWithin (n + 1) f (Icc a b) y‖ ≤ sSup (g '' Icc a b)
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case inr
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this : x₀ ≠ x
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t

Tactic:
have : UniqueDiffOn ℝ [[x₀, x]] := uniqueDiffOn_uIcc this

Goal state after:
case inr
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (∏ x ∈ Finset.range ((1 + 1) * n), (m - ↑x)) * ((m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1)))

Tactic:
refine mul_nonneg ihn ?_

Goal state after:
case succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k ∈ Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1))
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx : x ≠ 0
⊢ 2 / (2 * √x) + log x / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹

Tactic:
div_mul_cancel_left₀ two_ne_zero,

Goal state after:
case e'_9
x : ℝ
hx : x ≠ 0
⊢ (√x)⁻¹ + log x / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x w : ℂ
hw : 1 * (w * w) + ?m.57 * w + ?m.58 = 0
⊢ ∃ w, w ≠ 0 ∧ 1 * (w * w) + -2 * x * w + 1 = 0

Tactic:
refine ⟨w, ?_, hw⟩

Goal state after:
x w : ℂ
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ w ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ sin x ≤ x

Tactic:
obtain rfl | hx := hx.eq_or_lt
  · simp
  · exact (sin_lt hx).le

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

Goal state before:
pp: x : ℝ
⊢ cos (arctan x) ^ 2 = (1 + x ^ 2)⁻¹

Tactic:
← inv_one_add_tan_sq (cos_arctan_pos x).ne',

Goal state after:
x : ℝ
⊢ (1 + tan (arctan x) ^ 2)⁻¹ = (1 + x ^ 2)⁻¹
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case inr
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)

Tactic:
mem_ball_iff_norm

Goal state after:
case inr
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] R₁, ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / r) ^ (n + 1)
Module: Mathlib.Analysis.Complex.Schwarz

Goal state before:
pp: case hz
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
⊢ z ∈ ball c r

Tactic:
mem_ball_iff_norm

Goal state after:
case hz
f : ℂ → ℂ
c z : ℂ
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : (fun x ↦ f x - f c) =o[𝓝 c] fun w ↦ (w - c) ^ n
hz : ‖z - c‖ < R₁
hR₁ : 0 < R₁
this :
  ∀ {R₁ : ℝ},
    DifferentiableOn ℂ f (ball c R₁) →
      MapsTo f (ball c R₁) (closedBall (f c) R₂) →
        z ∈ ball c R₁ →
          0 < R₁ →
            DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂) →
              ‖f z - f c‖ ≤ R₂ * (‖z - c‖ / R₁) ^ (n + 1)
hd' : ¬(DifferentiableOn ℂ f (closedBall c R₁) ∧ MapsTo f (closedBall c R₁) (closedBall (f c) R₂))
r : ℝ
hzr : ‖z - c‖ < r
hrR₁ : r < R₁
⊢ ‖z - c‖ < r
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝔻
⊢ |‖↑z‖| < 1

Tactic:
abs_norm

Goal state after:
z : 𝔻
⊢ ‖↑z‖ < 1
Module: Mathlib.Analysis.Complex.UnitDisc.Basic

Goal state before:
pp: z : 𝕔𝔻
⊢ |‖↑z‖| ≤ 1

Tactic:
abs_norm

Goal state after:
z : 𝕔𝔻
⊢ ‖↑z‖ ≤ 1
Module: Mathlib.Analysis.Meromorphic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
U : Set 𝕜
f : 𝕜 → E
h₁f : MeromorphicOn f U
h₂f : ∀ u ∈ U, meromorphicOrderAt f u ≠ ⊤
x : 𝕜
h₁x : AnalyticAt 𝕜 f x
h₂x : x ∈ U ∧ (meromorphicOrderAt f x = 0 ∨ meromorphicOrderAt f x = ⊤)
this : meromorphicOrderAt f x ≠ ⊤
⊢ f x ≠ 0

Tactic:
simp_all [← h₁x.analyticOrderAt_eq_zero, h₁x.meromorphicOrderAt_eq]

Goal state after:
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
⊢ ContinuousOn g (Set.Icc 0 (t Nat.zero) ×ˢ Set.univ)

Tactic:
refine (cont_0.comp continuous_snd).continuousOn.congr (fun ta ⟨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 ∈ Set.Icc 0 (t Nat.zero)
right✝ : ta.2 ∈ Set.univ
⊢ g ta = ((fun x ↦ g (0, x)) ∘ Prod.snd) ta
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
U✝ : Set 𝕜
z✝ : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
z : 𝕜
hz : z ∈ Function.support fun z ↦ if MeromorphicOn f U ∧ z ∈ U then (meromorphicOrderAt f z).untop₀ else 0
⊢ z ∈ U

Tactic:
by
    by_contra h₂z
    simp [h₂z] at hz

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
z : 𝕜
⊢ (divisor f⁻¹ U) z = (-divisor f U) z

Tactic:
by_cases h : MeromorphicOn f U ∧ z ∈ U

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
z : 𝕜
h : MeromorphicOn f U ∧ z ∈ U
⊢ (divisor f⁻¹ U) z = (-divisor f U) z

case neg
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
z : 𝕜
h : ¬(MeromorphicOn f U ∧ z ∈ U)
⊢ (divisor f⁻¹ U) z = (-divisor f U) z
Module: Mathlib.Analysis.Meromorphic.Divisor

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
R : ℝ
f : 𝕜 → E
⊢ (divisor f (sphere c R - {c})) z = (divisor f (sphere 0 R)) z

Tactic:
sphere_sub_singleton,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
z : 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
R : ℝ
f : 𝕜 → E
⊢ (divisor f (sphere (c - c) R)) z = (divisor f (sphere 0 R)) z