mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

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
inst✝ : IsManifold I 1 M
x : M
y : E
⊢ y ∈ (extChartAt I x).target → MDiffAt[(extChartAt I x).target] ↑(extChartAt I x).symm y

Tactic:
hy

Goal state after:
𝕜 : 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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ MDiffAt[(extChartAt I x).target] ↑(extChartAt I x).symm y
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✝⁵ : TopologicalSpace (TotalSpace F E)
inst✝⁴ : (x : B) → TopologicalSpace (E x)
inst✝³ : FiberBundle F E
inst✝² : VectorBundle 𝕜 F E
inst✝¹ : ContMDiffVectorBundle n F E IB
s : (x : B) → E x
a : Set B
x₀ : B
e : Trivialization F TotalSpace.proj
inst✝ : MemTrivializationAtlas e
hx₀ : x₀ ∈ e.baseSet
⊢ ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a x₀ ↔
    ContMDiffWithinAt IB 𝓘(𝕜, F) n (fun x ↦ (↑e { proj := x, snd := s x }).2) a x₀

Tactic:
by
  rw [e.contMDiffWithinAt_iff]
  · change ContMDiffWithinAt IB IB n id a x₀ ∧ _ ↔ _
    simp [contMDiffWithinAt_id]
  · rwa [mem_source]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
y : E
⊢ y ∈ t → writtenInExtChartAt I I (Sum.inl x) Sum.swap y = id y

Tactic:
hy

Goal state after:
𝕜 : 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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
y : E
hy : y ∈ t
⊢ writtenInExtChartAt I I (Sum.inl x) Sum.swap y = id y
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
y : E
⊢ y ∈ t → writtenInExtChartAt I I (Sum.inr x) Sum.swap y = id y

Tactic:
hy

Goal state after:
𝕜 : 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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x : M'
t : Set E := ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
y : E
hy : y ∈ t
⊢ writtenInExtChartAt I I (Sum.inr x) Sum.swap y = id y
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q : M
hmem : ↑I.symm ⁻¹' (chartAt H q).target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I q) q
y : E
⊢ y ∈ ↑I.symm ⁻¹' (chartAt H q).target ∩ range ↑I → writtenInExtChartAt I I q Sum.inl y = id y

Tactic:
hy

Goal state after:
𝕜 : 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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q : M
hmem : ↑I.symm ⁻¹' (chartAt H q).target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I q) q
y : E
hy : y ∈ ↑I.symm ⁻¹' (chartAt H q).target ∩ range ↑I
⊢ writtenInExtChartAt I I q Sum.inl y = id y
Module: Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
hmem : ↑I.symm ⁻¹' (chartAt H q').target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I q') q'
y : E
⊢ y ∈ ↑I.symm ⁻¹' (chartAt H q').target ∩ range ↑I → writtenInExtChartAt I I q' Sum.inr y = id y

Tactic:
hy

Goal state after:
𝕜 : 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
M' : Type u_21
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
q' : M'
hmem : ↑I.symm ⁻¹' (chartAt H q').target ∩ range ↑I ∈ 𝓝[range ↑I] ↑(extChartAt I q') q'
y : E
hy : y ∈ ↑I.symm ⁻¹' (chartAt H q').target ∩ range ↑I
⊢ writtenInExtChartAt I I q' Sum.inr y = id y
Module: Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential

Goal state before:
pp: case fst
𝕜 : 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
s : Set M
F : Type u_9
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
Z : M → Type u_10
inst✝² : TopologicalSpace (TotalSpace F Z)
inst✝¹ : (b : M) → TopologicalSpace (Z b)
inst✝ : FiberBundle F Z
p : TotalSpace F Z
hs : UniqueMDiffAt[s] p.proj
h's : s ⊆ (trivializationAt F Z p.proj).baseSet
this :
  (↑(extChartAt I p.proj).symm ⁻¹' s ∩ range ↑I) ×ˢ univ ⊆
    ↑(extChartAt (I.prod 𝓘(𝕜, F)) p).symm ⁻¹' TotalSpace.proj ⁻¹' s ∩ range ↑(I.prod 𝓘(𝕜, F))
w : F := ⋯
⊢ (↑(extChartAt (I.prod 𝓘(𝕜, F)) p) p).1 = (↑(extChartAt I p.proj) p.proj, w).1

Tactic:
simp [FiberBundle.chartedSpace_chartAt]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.Atlas

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
inst✝ : IsManifold I 1 M
x₀ x : M
hx : x ∈ (chartAt H x₀).source
⊢ Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x₀) x =
    mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x)

Tactic:
have : MDiffAt[range I] ((chartAt H x₀).symm ∘ I.symm) (I (chartAt H x₀ x)) := by
    simpa using mdifferentiableWithinAt_extChartAt_symm (by simp [hx])
  simp [hx, mfderivWithin, this]

Goal state after:
Module: Mathlib.Topology.PartitionOfUnity

Goal state before:
pp: ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
⊢ {i | y ∈ closure[inst✝] (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure[inst✝] (support ⇑(ρ i))} →
    ρ.fintsupport y ⊆ ρ.fintsupport x₀

Tactic:
hy

Goal state after:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ y : X
hy : {i | y ∈ closure[inst✝] (support ⇑(ρ i))} ⊆ {i | x₀ ∈ closure[inst✝] (support ⇑(ρ i))}
⊢ ρ.fintsupport y ⊆ ρ.fintsupport x₀
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
u : Set M
s : (x : M) → V x
ψ : M → 𝕜
hψ : ContMDiffOn I 𝓘(𝕜, 𝕜) n ψ u
ht : IsOpen u
ht' : tsupport ψ ⊆ u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) u
y : M
⊢ y ∈ (tsupport ψ)ᶜ → ⟨y, (ψ • s) y⟩ = zeroSection F V y

Tactic:
hy

Goal state after:
𝕜 : 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
u : Set M
s : (x : M) → V x
ψ : M → 𝕜
hψ : ContMDiffOn I 𝓘(𝕜, 𝕜) n ψ u
ht : IsOpen u
ht' : tsupport ψ ⊆ u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) n (fun x ↦ ⟨x, s x⟩) u
y : M
hy : y ∈ (tsupport ψ)ᶜ
⊢ ⟨y, (ψ • s) y⟩ = zeroSection F V y
Module: Mathlib.Geometry.Manifold.PartitionOfUnity

Goal state before:
pp: case refine_1
ι : Type uι
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
U : ι → Set M
ho : ∀ (i : ι), IsOpen[inst✝⁵] (U i)
hU : s ⊆ ⋃ i, U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ ∀ (s t : Set M),
    IsClosed[inst✝⁵] s →
      IsClosed[inst✝⁵] t →
        Disjoint s t → ∃ f, ContMDiff I 𝓘(ℝ, ℝ) ∞ ⇑f ∧ EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Icc 0 1

Tactic:
· intro s t hs ht hd
    rcases exists_contMDiffMap_zero_one_of_isClosed I hs ht hd with ⟨f, hf⟩
    exact ⟨f, f.contMDiff, hf⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ∞
⊢ f ≤ᵐ[μ.restrict s] fun x ↦ b

Tactic:
rw [EventuallyLE, ae_restrict_iff₀ (hs.mono μ.restrict_le_self)]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → 0 ≤ ∫ (x : α) in s, f x ∂μ
b : ℝ
hb_neg : b < 0
s : Set α := {x | f x ≤ b}
hs : NullMeasurableSet s μ
mus : μ s < ∞
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ b
Module: Mathlib.Analysis.Calculus.TangentCone.Pi

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : (i : ι) → TopologicalSpace (E i)
inst✝² : ∀ (i : ι), ContinuousAdd (E i)
inst✝¹ : ∀ (i : ι), ContinuousConstSMul 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
inst✝ : DecidableEq ι
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
⊢ y ∈ tangentConeAt 𝕜 (s i) (x i) → Pi.single i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (univ.pi s)) x

Tactic:
hy

Goal state after:
𝕜 : Type u_1
inst✝⁶ : Semiring 𝕜
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (E i)
inst✝⁴ : (i : ι) → Module 𝕜 (E i)
inst✝³ : (i : ι) → TopologicalSpace (E i)
inst✝² : ∀ (i : ι), ContinuousAdd (E i)
inst✝¹ : ∀ (i : ι), ContinuousConstSMul 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
inst✝ : DecidableEq ι
i : ι
hi : ∀ (j : ι), j ≠ i → x j ∈ closure[inst✝³ j] (s j)
y : E i
hy : y ∈ tangentConeAt 𝕜 (s i) (x i)
⊢ Pi.single i y ∈ tangentConeAt 𝕜 (closure[Pi.topologicalSpace] (univ.pi s)) x
Module: Mathlib.Order.SuccPred.IntervalSucc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : OrderBot α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : LinearOrder β
f : α → β
hf : ∀ (a : α), f ⊥ ≤ f a
h2f : ¬BddAbove (range f)
⊢ ⋃ a, Ico (f a) (f (succ a)) = Ici (f ⊥)

Tactic:
simpa using biUnion_Ici_Ico_map_succ (f := f) (a := ⊥) (by simpa) (by simpa)

Goal state after:
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 a..b, deriv f x ∈ uIcc 0 (f b - f a)

Tactic:
rw [intervalIntegral.integral_symm, 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.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c y : ℝ
⊢ y ∈ Iio x → slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x y = ((fun a ↦ ⨍ (y : ℝ) in a, f y) ∘ fun y ↦ Icc y x) y

Tactic:
hy

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c y : ℝ
hy : y ∈ Iio x
⊢ slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x y = ((fun a ↦ ⨍ (y : ℝ) in a, f y) ∘ fun y ↦ Icc y x) y
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c y : ℝ
⊢ y ∈ Ioi x → slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x y = ((fun a ↦ ⨍ (y : ℝ) in a, f y) ∘ fun y ↦ Icc x y) y

Tactic:
hy

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
hf : LocallyIntegrable f volume
hg : ∀ (x y : ℝ), IntervalIntegrable f volume x y
LDT : ∀ᵐ (x : ℝ), Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
h : ∀ {a b : ℝ}, ∫ (t : ℝ) in Ioc a b, f t = ∫ (t : ℝ) in Icc a b, f t
x : ℝ
hx : Tendsto (fun a ↦ ⨍ (y : ℝ) in a, f y) ((vitaliFamily volume 1).filterAt x) (𝓝 (f x))
c y : ℝ
hy : y ∈ Ioi x
⊢ slope (fun x ↦ ∫ (t : ℝ) in c..x, f t) x y = ((fun a ↦ ⨍ (y : ℝ) in a, f y) ∘ fun y ↦ Icc x y) y
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case h't
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 (ℝ × ℝ) := ⋯
s : Set ℝ := ⋯
⊢ ∀ a ∈ t, IsClosed (Icc a.1 a.2)

Tactic:
simp [isClosed_Icc]

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

Goal state before:
pp: case hbc
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
⊢ ‖L y - L w‖ ≤ ‖L‖ * ‖y - w‖

Tactic:
exact L.lipschitz.norm_sub_le _ _

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

Goal state before:
pp: case h
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1

Tactic:
rw [nhdsWithin_le_iff, mem_nhdsWithin]

Goal state after:
case h
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ ∃ u, IsOpen u ∧ 1 ∈ u ∧ u ∩ stolzCone s ⊆ stolzSet M
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
g : ↑u → ℝ := fun z ↦ dist (f (↑z).1) (f (↑z).2)
g_nonneg : 0 ≤ g
s : Finset ↑u
this : ∀ z ∈ s, g z ≤ r / (b - d) * ((↑z).2 - (↑z).1)
⊢ ∑ i ∈ s, r / (b - d) * ((↑i).2 - (↑i).1) ≤ r

Tactic:
← Finset.mul_sum

Goal state after:
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
g : ↑u → ℝ := fun z ↦ dist (f (↑z).1) (f (↑z).2)
g_nonneg : 0 ≤ g
s : Finset ↑u
this : ∀ z ∈ s, g z ≤ r / (b - d) * ((↑z).2 - (↑z).1)
⊢ r / (b - d) * ∑ i ∈ s, ((↑i).2 - (↑i).1) ≤ r
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 → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
x : E
hx : ‖x‖ = 1
y : E
⊢ ‖y‖ = 1 → x ≠ y → ([x -[ℝ] y] \ sphere 0 1).Nonempty

Tactic:
hy

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
⊢ x ≠ y → ([x -[ℝ] y] \ sphere 0 1).Nonempty
Module: Mathlib.Analysis.InnerProductSpace.Convex

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ 2 * (1 * 1 + ‖y‖ * ‖y‖) - ‖x - y‖ ^ 2 ≤ 4 - ε ^ 2

Tactic:
hy

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ 2 * (1 * 1 + 1 * 1) - ‖x - y‖ ^ 2 ≤ 4 - ε ^ 2
Module: Mathlib.Analysis.Complex.AbsMax

Goal state before:
pp: case refine_3
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖f w‖ / ‖w - z‖ < ‖f z‖ / r

Tactic:
← dist_eq_norm

Goal state after:
case refine_3
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖f w‖ / dist w z < ‖f z‖ / r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y))

Tactic:
rw [← arctan_tan (x := _ + _)]

Goal state after:
x y : ℝ
h : x * y < 1
⊢ arctan (tan (arctan x + arctan y)) = arctan ((x + y) / (1 - x * y))

case hx₁
x y : ℝ
h : x * y < 1
⊢ -(π / 2) < arctan x + arctan y

case hx₂
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan 2⁻¹ + arctan 3⁻¹ = π / 4

Tactic:
arctan_add

Goal state after:
⊢ arctan ((2⁻¹ + 3⁻¹) / (1 - 2⁻¹ * 3⁻¹)) = π / 4

⊢ 2⁻¹ * 3⁻¹ < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan (2 * 2⁻¹ / (1 - 2⁻¹ ^ 2)) = arctan 1 + arctan 7⁻¹

pp: case h₁
⊢ -1 < 2⁻¹

pp: case h₂
⊢ 2⁻¹ < 1

Tactic:
arctan_add

Goal state after:
⊢ arctan (2 * 2⁻¹ / (1 - 2⁻¹ ^ 2)) = arctan ((1 + 7⁻¹) / (1 - 1 * 7⁻¹))

⊢ 1 * 7⁻¹ < 1

case h₁
⊢ -1 < 2⁻¹

case h₂
⊢ 2⁻¹ < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan (2 * 3⁻¹ / (1 - 3⁻¹ ^ 2)) + arctan 7⁻¹ = π / 4

pp: case h₁
⊢ -1 < 3⁻¹

pp: case h₂
⊢ 3⁻¹ < 1

Tactic:
arctan_add

Goal state after:
⊢ arctan ((2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) + 7⁻¹) / (1 - 2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) * 7⁻¹)) = π / 4

⊢ 2 * 3⁻¹ / (1 - 3⁻¹ ^ 2) * 7⁻¹ < 1

case h₁
⊢ -1 < 3⁻¹

case h₂
⊢ 3⁻¹ < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan (2 * (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) / (1 - (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) ^ 2)) = arctan 1 + arctan 239⁻¹

pp: case h₁
⊢ -1 < 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)

pp: case h₂
⊢ 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2) < 1

pp: case h₁
⊢ -1 < 5⁻¹

pp: case h₂
⊢ 5⁻¹ < 1

Tactic:
arctan_add

Goal state after:
⊢ arctan (2 * (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) / (1 - (2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)) ^ 2)) = arctan ((1 + 239⁻¹) / (1 - 1 * 239⁻¹))

⊢ 1 * 239⁻¹ < 1

case h₁
⊢ -1 < 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2)

case h₂
⊢ 2 * 5⁻¹ / (1 - 5⁻¹ ^ 2) < 1

case h₁
⊢ -1 < 5⁻¹

case h₂
⊢ 5⁻¹ < 1