mathlib-initiative/mathlib-tactics huggingface dataset:
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
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
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' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
⊢ (interior (range ↑(I.toPartialEquiv ≫ (↑e).toEquiv.toPartialEquiv))).Nonempty

Tactic:
simp only [PartialEquiv.coe_trans, Equiv.toPartialEquiv_apply, LinearEquiv.coe_toEquiv,
      ContinuousLinearEquiv.coe_toLinearEquiv, toPartialEquiv_coe, range_comp,
      ContinuousLinearEquiv.image_eq_preimage_symm]

Goal state after:
𝕜 : 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
G' : Type u_8
inst✝⁸ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
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' : Type u_12
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
e : E ≃L[𝕜] E'
⊢ (interior (⇑e.symm ⁻¹' range ↑I)).Nonempty
Module: Mathlib.Geometry.Manifold.Diffeomorph

Goal state before:
pp: case hg
𝕜 : 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
G' : Type u_8
inst✝¹⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J✝¹ : ModelWithCorners 𝕜 F G
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'✝ : Type u_12
inst✝⁹ : TopologicalSpace N'✝
inst✝⁸ : ChartedSpace G' N'✝
n : ℕ∞ω
M' : Type u_13
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H M'
M'' : Type u_14
inst✝⁵ : TopologicalSpace M''
inst✝⁴ : ChartedSpace H M''
N : Type u_15
J✝ : Type u_16
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace H N'
⊢ ContMDiff I I n (Sum.inr ∘ Sum.inr)

Tactic:
exact ContMDiff.inr.comp ContMDiff.inr

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

Goal state before:
pp: case hg
𝕜 : 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
G' : Type u_8
inst✝¹⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J✝¹ : ModelWithCorners 𝕜 F G
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'✝ : Type u_12
inst✝⁹ : TopologicalSpace N'✝
inst✝⁸ : ChartedSpace G' N'✝
n : ℕ∞ω
M' : Type u_13
inst✝⁷ : TopologicalSpace M'
inst✝⁶ : ChartedSpace H M'
M'' : Type u_14
inst✝⁵ : TopologicalSpace M''
inst✝⁴ : ChartedSpace H M''
N : Type u_15
J✝ : Type u_16
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace H N
J : ModelWithCorners 𝕜 E' H
N' : Type u_17
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace H N'
⊢ ContMDiff I I n (Sum.elim (Sum.inl ∘ Sum.inr) Sum.inr)

Tactic:
exact ContMDiff.inr.sumMap contMDiff_id

Goal state after:
Module: Mathlib.Topology.Compactness.Paracompact

Goal state before:
pp: case refine_3
X : Type v
inst✝³ : TopologicalSpace X
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed[inst✝³] s
hB : ∀ x ∈ s, (𝓝 x).HasBasis (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := K'.shiftr.shiftr
Kdiff : ℕ → Set X := fun n ↦ K (n + 1) \ interior (K n)
hKcov : ∀ (x : X), x ∈ Kdiff (K'.find x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝¹ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT : ∀ (n : ℕ), Kdiff (n + 1) ∩ s ⊆ ⋃ x ∈ T n, B (↑x) (r n ⟨↑x, ⋯⟩)
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n ↦ ↑(T n)
x✝ : X
this✝ : (⋃ k, ⋃ (_ : k ≤ K'.find x✝ + 2), range (Sigma.mk k)).Finite
k : ℕ
c : ↑(Kdiff (k + 1) ∩ s)
hc : c ∈ T' k
x : X
hxB : x ∈ B (↑c) (r k c)
hxK : x ∈ interior (K (K'.find x✝ + 3))
this : x ∉ K k
⊢ k ≤ K'.find x✝ + 2

Tactic:
contrapose! this with hnk

Goal state after:
case refine_3
X : Type v
inst✝³ : TopologicalSpace X
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : SigmaCompactSpace X
inst✝ : T2Space X
ι : X → Type u
p : (x : X) → ι x → Prop
B : (x : X) → ι x → Set X
s : Set X
hs : IsClosed[inst✝³] s
hB : ∀ x ∈ s, (𝓝 x).HasBasis (p x) (B x)
K' : CompactExhaustion X := CompactExhaustion.choice X
K : CompactExhaustion X := K'.shiftr.shiftr
Kdiff : ℕ → Set X := fun n ↦ K (n + 1) \ interior (K n)
hKcov : ∀ (x : X), x ∈ Kdiff (K'.find x + 1)
Kdiffc : ∀ (n : ℕ), IsCompact (Kdiff n ∩ s)
this✝ : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), (K n)ᶜ ∈ 𝓝 ↑x
r : (n : ℕ) → (x : ↑(Kdiff (n + 1) ∩ s)) → ι ↑x
hrp : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), p (↑x) (r n x)
hr : ∀ (n : ℕ) (x : ↑(Kdiff (n + 1) ∩ s)), B (↑x) (r n x) ⊆ (K n)ᶜ
hxr : ∀ (n : ℕ) (x : X) (hx : x ∈ Kdiff (n + 1) ∩ s), B x (r n ⟨x, hx⟩) ∈ 𝓝 x
T : (n : ℕ) → Finset ↑(Kdiff (n + 1) ∩ s)
hT : ∀ (n : ℕ), Kdiff (n + 1) ∩ s ⊆ ⋃ x ∈ T n, B (↑x) (r n ⟨↑x, ⋯⟩)
T' : (n : ℕ) → Set ↑(Kdiff (n + 1) ∩ s) := fun n ↦ ↑(T n)
x✝ : X
this : (⋃ k, ⋃ (_ : k ≤ K'.find x✝ + 2), range (Sigma.mk k)).Finite
k : ℕ
c : ↑(Kdiff (k + 1) ∩ s)
hc : c ∈ T' k
x : X
hxB : x ∈ B (↑c) (r k c)
hxK : x ∈ interior (K (K'.find x✝ + 3))
hnk : K'.find x✝ + 2 < k
⊢ x ∈ K k
Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹⁰ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
F : Type u_5
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst✝⁵ : TopologicalSpace (TotalSpace F V)
inst✝⁴ : (x : M) → TopologicalSpace (V x)
inst✝³ : FiberBundle F V
inst✝² : (x : M) → AddCommGroup (V x)
inst✝¹ : (x : M) → Module 𝕜 (V x)
inst✝ : VectorBundle 𝕜 F V
s : (x : M) → V x
x₀ : M
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, (-s) x⟩) x₀

Tactic:
rw [← contMDiffWithinAt_univ] at hs ⊢
  exact hs.neg_section

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x : X
x✝ : x ∈ s
⊢ ⇑1 =ᶠ[𝓝 x] 1

Tactic:
ContinuousMap.coe_one

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s✝ : Set X
f : BumpCovering ι X s✝
i : ι
s : Set X
x : X
x✝ : x ∈ s
⊢ 1 =ᶠ[𝓝 x] 1
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp

Goal state before:
pp: case refine_1
α : 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 ≠ ∞
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
⊢ ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞

Tactic:
have h_fs_Lp : ∀ n, MemLp (fs n) p μ :=
      SimpleFunc.memLp_approxOn_range hf_meas.measurable hf

Goal state after:
case refine_1
α : 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 ≠ ∞
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(Set.range f ∪ {0})
fs : ℕ → α →ₛ G := SimpleFunc.approxOn f ⋯ (Set.range f ∪ {0}) 0 ⋯
h_fs_Lp : ∀ (n : ℕ), MemLp (⇑(fs n)) p μ
⊢ ∀ (n : ℕ), μ (support ⇑(fs n)) < ∞
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✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst✝⁵] s
⊢ ∃ f, f.IsSubordinate fun x ↦ (chartAt H ↑x).source

Tactic:
apply exists_isSubordinate _ hs _ (fun i ↦ (chartAt H _).open_source) (fun x hx ↦ ?_)

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✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed[inst✝⁵] s
x : M
hx : x ∈ s
⊢ x ∈ ⋃ i, (chartAt H ↑i).source
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: case hF_meas
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 : E
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (fun a ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ

Tactic:
filter_upwards with t
    apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable
    apply aestronglyMeasurable_const.fun_smul
    apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable
    apply AEMeasurable.aestronglyMeasurable
    exact hf.continuous.measurable.comp_aemeasurable' (aemeasurable_id'.add_const _)

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

Goal state before:
pp: case hF_meas
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 := ⋯
K_compact : IsCompact K
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0, AEStronglyMeasurable (fun a ↦ n⁻¹ • (f (a + n • v) - f a) * g a) μ

Tactic:
filter_upwards with t
    apply AEStronglyMeasurable.mul ?_ hg.aestronglyMeasurable
    apply aestronglyMeasurable_const.fun_smul
    apply AEStronglyMeasurable.sub _ hf.continuous.measurable.aestronglyMeasurable
    apply AEMeasurable.aestronglyMeasurable
    exact hf.continuous.measurable.comp_aemeasurable' (aemeasurable_id'.add_const _)

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

Goal state before:
pp: case bound_integrable
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 := ⋯
K_compact : IsCompact K
⊢ Integrable (K.indicator fun x ↦ ↑C * ‖v‖ * ‖g x‖) μ

Tactic:
rw [integrable_indicator_iff K_compact.measurableSet]
    exact ContinuousOn.integrableOn_compact K_compact (by fun_prop)

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

Goal state before:
pp: case h_mono
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed[inst✝⁴] s
t : ℕ → Set β := fun n ↦ closure[inst✝⁴] (compactCovering β n) ∩ s
B : s = ⋃ n, t n
m n : ℕ
⊢ m ≤ n → t m ⊆ t n

Tactic:
hmn

Goal state after:
case h_mono
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed[inst✝⁴] s
t : ℕ → Set β := fun n ↦ closure[inst✝⁴] (compactCovering β n) ∩ s
B : s = ⋃ n, t n
m n : ℕ
hmn : m ≤ n
⊢ t m ⊆ t n
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case inr
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
hab : ¬a ≤ b
this : f b ≤ f a
⊢ -∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f b - f a)

Tactic:
uIcc_of_ge (by linarith)

Goal state after:
case inr
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (uIcc a b)
h : ∫ (x : ℝ) in b..a, deriv f x ∈ uIcc 0 (f a - f b)
hab : ¬a ≤ b
this : f b ≤ f a
⊢ -∫ (x : ℝ) in b..a, deriv f x ∈ Icc (f b - f a) 0
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
⊢ ∑ i ∈ Finset.range (n, I).1, dist ((f • g) ((n, I).2 i).1) ((f • g) ((n, I).2 i).2) ≤
    C * ∑ i ∈ Finset.range (n, I).1, dist (g ((n, I).2 i).1) (g ((n, I).2 i).2) +
      D * ∑ i ∈ Finset.range (n, I).1, dist (f ((n, I).2 i).1) (f ((n, I).2 i).2)

Tactic:
simp only [Finset.mul_sum, ← Finset.sum_add_distrib]

Goal state after:
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
⊢ ∑ x ∈ Finset.range n, dist ((f • g) (I x).1) ((f • g) (I x).2) ≤
    ∑ x ∈ Finset.range n, (C * dist (g (I x).1) (g (I x).2) + D * dist (f (I x).1) (f (I x).2))
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
⊢ ∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) ≤ 1

Tactic:
have veq : (∑ i ∈ Finset.range p.1, edist (f (p.2.val (i + 1))) (f (p.2.val i))).toReal =
        ∑ i ∈ Finset.range p.1, dist (f (p.2.val i)) (f (p.2.val (i + 1))) := by
      rw [ENNReal.toReal_sum (by simp [edist_ne_top])]
      simp_rw [← dist_edist]; congr; ext i; nth_rw 1 [dist_comm]

Goal state after:
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ E ∈ disjWithin a b,
    ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ → ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
veq :
  (∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i))).toReal =
    ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))
⊢ ∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) ≤ 1
Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv

Goal state before:
pp: ⊢ StrictConcaveOn ℝ (Ioi 1) fun x ↦ √x * log x

Tactic:
by
  apply strictConcaveOn_of_deriv2_neg' (convex_Ioi 1) _ fun x hx => ?_
  · exact continuous_sqrt.continuousOn.mul
      (continuousOn_log.mono fun x hx => ne_of_gt (zero_lt_one.trans hx))
  · rw [deriv2_sqrt_mul_log x]
    exact div_neg_of_neg_of_pos (neg_neg_of_pos (log_pos hx))
      (mul_pos four_pos (pow_pos (sqrt_pos.mpr (zero_lt_one.trans hx)) 3))

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

Goal state before:
pp: case inr
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * (↑π / 2)) = 0

Tactic:
← mul_div_assoc,

Goal state after:
case inr
k l : ℤ
t : ∀ (n : ℤ), tan (↑n * ↑π / 2) = 0
hx : tan ((2 * ↑k + 1) * ↑π / 2) = 0
hy : tan ((2 * ↑l + 1) * ↑π / 2) = 0
hxy : tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
⊢ tan ((2 * ↑k + 1 + (2 * ↑l + 1)) * ↑π / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: case inr
k l : ℤ
⊢ tan ((2 * ↑k + 1) * ↑π / 2 + (2 * ↑l + 1) * ↑π / 2) =
    (tan ((2 * ↑k + 1) * ↑π / 2) + tan ((2 * ↑l + 1) * ↑π / 2)) /
      (1 - tan ((2 * ↑k + 1) * ↑π / 2) * tan ((2 * ↑l + 1) * ↑π / 2))

Tactic:
have t := tan_int_mul_pi_div_two
    obtain ⟨hx, hy, hxy⟩ := t (2 * k + 1), t (2 * l + 1), t (2 * k + 1 + (2 * l + 1))
    simp only [Int.cast_add, Int.cast_two, Int.cast_mul, Int.cast_one] at hx hy hxy
    rw [hx, hy, add_zero, zero_div, mul_div_assoc, mul_div_assoc, ←
      add_mul (2 * (k : ℂ) + 1) (2 * l + 1) (π / 2), ← mul_div_assoc, hxy]

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

Goal state before:
pp: case neg
z : ℂ
h : ∃ k, z = (2 * ↑k + 1) * ↑π / 2
⊢ tan (2 * z) = 2 * tan z / (1 - tan z ^ 2)

Tactic:
rw [two_mul, two_mul, sq, tan_add (Or.inr ⟨h, h⟩)]

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

Goal state before:
pp: x : ℂ
h : cos x ≠ -1
this : cos (x / 2) ≠ 0
⊢ cos (x / 2) ^ 2 - sin (x / 2) ^ 2 = (1 - tan (x / 2) ^ 2) / (1 + tan (x / 2) ^ 2)

Tactic:
div_eq_mul_inv (1 - tan (x / 2) ^ 2) (1 + tan (x / 2) ^ 2),

Goal state after:
x : ℂ
h : cos x ≠ -1
this : cos (x / 2) ≠ 0
⊢ cos (x / 2) ^ 2 - sin (x / 2) ^ 2 = (1 - tan (x / 2) ^ 2) * (1 + tan (x / 2) ^ 2)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ ∑ i ∈ Finset.range n, -2 * sin (a / 2) * sin (a * ↑i + b) =
    ∑ x ∈ Finset.range n, (cos (a * (↑(x + 1) - 1 / 2) + b) - cos (-(a * (↑x - 1 / 2) + b)))

Tactic:
by
      congr! 1 with x hx
      rw [cos_sub_cos]
      push_cast
      ring_nf

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

Goal state before:
pp: x : ℝ
⊢ |cos x| = |1| ↔ ∃ k, ↑k * π = x

Tactic:
abs_eq_abs,

Goal state after:
x : ℝ
⊢ cos x = 1 ∨ cos x = -1 ↔ ∃ k, ↑k * π = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
⊢ |sin x| = |1| ↔ ∃ k, π / 2 + ↑k * π = x

Tactic:
abs_eq_abs,

Goal state after:
x : ℝ
⊢ sin x = 1 ∨ sin x = -1 ↔ ∃ k, π / 2 + ↑k * π = x
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
⊢ (Ioo a x).Nonempty

Tactic:
by simpa using hxab.1

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

Goal state before:
pp: f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
⊢ dist (f z / (2 * ↑M - f z)) 0 ≤ 1 / R * dist z 0

Tactic:
← zero_div (2 * M - f 0),

Goal state after:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z | z.re ≤ M}
hz : z ∈ ball 0 R
hf₂ : f 0 = 0
⊢ dist (f z / (2 * ↑M - f z)) (0 / (2 * ↑M - f 0)) ≤ 1 / R * dist z 0
Module: Mathlib.Analysis.Normed.Module.Ball.Action

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜' E
r : ℝ
c : ↑(closedBall 0 1)
x : ↑(ball 0 r)
⊢ ‖↑c • ↑x‖ < r

Tactic:
by
        simpa only [norm_smul, one_mul] using
          mul_lt_mul' (mem_closedBall_zero_iff.1 c.2) (mem_ball_zero_iff.1 x.2) (norm_nonneg _)
            one_pos

Goal state after:
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 g : 𝕜 → E
hf : MeromorphicOn f U
hg : MeromorphicOn g U
hU : Preperfect U
h : f =ᶠ[codiscreteWithin U] g
⊢ ∀ᶠ (x : 𝕜) in 𝓝ˢ U, f =ᶠ[𝓝[≠] x] g

Tactic:
by
  rw [eventually_nhdsSet_iff_exists]
  use {x | f =ᶠ[𝓝[≠] x] g}
  simp only [Set.mem_ofPred_eq, imp_self, implies_true, and_true]
  constructor
  · apply isOpen_setOfPred_eventually_nhdsWithin
  · intro x hx
    rw [Set.mem_ofPred]
    exact eventuallyEq_nhdsNE_of_eventuallyEq_codiscreteWithin (hf x hx) (hg x hx) hx (hU x hx) h

Goal state after: