mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f f' : G → E
g g' : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : MeasurableAdd₂ G
inst✝² : MeasurableNeg G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddRightInvariant
h1 : f =ᵐ[μ] f'
h2 : g =ᵐ[μ] g'
x : G
⊢ (f ⋆[L, μ] g) x = (f' ⋆[L, μ] g') x

Tactic:
apply integral_congr_ae

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f f' : G → E
g g' : G → E'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : MeasurableAdd₂ G
inst✝² : MeasurableNeg G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddRightInvariant
h1 : f =ᵐ[μ] f'
h2 : g =ᵐ[μ] g'
x : G
⊢ (fun a ↦ (L (f a)) (g (x - a))) =ᵐ[μ] fun a ↦ (L (f' a)) (g' (x - a))
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: case inr
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L
h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t ↦ (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t ↦ (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1
⊢ HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L', μ] fderiv 𝕜 g) x₀) x₀

Tactic:
have hK' : IsCompact K' := (hcg.fderiv 𝕜).isCompact.neg.add (isCompact_closedBall x₀ 1)

Goal state after:
case inr
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := precompR G L
h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t ↦ (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t ↦ (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := -tsupport (fderiv 𝕜 g) + closedBall x₀ 1
hK' : IsCompact K'
⊢ HasFDerivAt (f ⋆[L, μ] g) ((f ⋆[L', μ] fderiv 𝕜 g) x₀) x₀
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
p : P
hp : p ∈ s
x : G
hx : g p x ≠ 0
A : support (g p) ⊆ k
⊢ Continuous[inst✝³, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g p)

Tactic:
refine hg.comp_continuous (.prodMk_right _) fun x => ?_

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
p : P
hp : p ∈ s
x✝ : G
hx : g p x✝ ≠ 0
A : support (g p) ⊆ k
x : G
⊢ (p, x) ∈ s ×ˢ univ
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
x₀ : H
s : Set H
inst✝ : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound t)) (fun x ↦ F x t) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x ↦ F x t) (F' t) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.restrict (Set.Ioc b a))
hF_meas :
  (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧
    ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀

Tactic:
rw [ae_restrict_uIoc_iff] at h_lip h_diff

Goal state after:
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
x₀ : H
s : Set H
inst✝ : NormedSpace ℝ H
μ : Measure ℝ
F : H → ℝ → E
F' : ℝ → H →L[ℝ] E
a b : ℝ
bound : ℝ → ℝ
hs : s ∈ 𝓝 x₀
hF_int : IntervalIntegrable (F x₀) μ a b
h_lip :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 ↦ F x_1 x) s) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 ↦ F x_1 x) s
bound_integrable : IntervalIntegrable bound μ a b
h_diff :
  (∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc a b), HasFDerivAt (fun x_1 ↦ F x_1 x) (F' x) x₀) ∧
    ∀ᵐ (x : ℝ) ∂μ.restrict (Set.Ioc b a), HasFDerivAt (fun x_1 ↦ F x_1 x) (F' x) x₀
hF'_meas : AEStronglyMeasurable F' (μ.restrict (Set.Ioc a b)) ∧ AEStronglyMeasurable F' (μ.restrict (Set.Ioc b a))
hF_meas :
  (∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc a b))) ∧
    ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Set.Ioc b a))
⊢ IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x ↦ ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddCommGroup G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : μ.IsNegInvariant
inst✝¹ : MeasurableNeg G
inst✝ : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
⊢ ∫ (t : G), (L (f t)) (g (-x - t)) ∂μ = ∫ (t : G), (L (f (-t))) (g (x + t)) ∂μ

Tactic:
apply integral_congr_ae

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
x : G
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddCommGroup G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : μ.IsNegInvariant
inst✝¹ : MeasurableNeg G
inst✝ : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
⊢ (fun a ↦ (L (f a)) (g (-x - a))) =ᵐ[μ] fun a ↦ (L (f (-a))) (g (x + a))
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ∅
hr : r ≤ 0
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
subset_empty_iff

Goal state after:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s = ∅
hr : r ≤ 0
⊢ ∃ r' < r, s ⊆ ball x r'
Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁸ : MeasurableSpace G
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace H
inst✝¹ : SeminormedGroup H
inst✝ : OpensMeasurableSpace H
f : G →* H
hf : Measurable ⇑f
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
this : haar (interior ↑K ∩ ⇑f ⁻¹' ⋃ i, ball 1 ↑i) = 0
⊢ False

Tactic:
iUnion_ball_nat,

Goal state after:
G : Type u_1
H : Type u_2
inst✝⁸ : MeasurableSpace G
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : LocallyCompactSpace G
inst✝² : MeasurableSpace H
inst✝¹ : SeminormedGroup H
inst✝ : OpensMeasurableSpace H
f : G →* H
hf : Measurable ⇑f
x : G
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
this : haar (interior ↑K ∩ ⇑f ⁻¹' univ) = 0
⊢ False
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
F' : Type uF'
F'' : Type uF''
inst✝²⁶ : NormedAddCommGroup E
inst✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedAddCommGroup E''
inst✝²³ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝²² : RCLike 𝕜
inst✝²¹ : NormedSpace 𝕜 E
inst✝²⁰ : NormedSpace 𝕜 E'
inst✝¹⁹ : NormedSpace 𝕜 E''
inst✝¹⁸ : NormedSpace ℝ F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁵ : CompleteSpace F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : CompleteSpace F'
inst✝¹⁰ : NormedAddCommGroup F''
inst✝⁹ : NormedSpace ℝ F''
inst✝⁸ : NormedSpace 𝕜 F''
inst✝⁷ : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst✝⁶ : AddGroup G
inst✝⁵ : SFinite μ
inst✝⁴ : SFinite ν
inst✝³ : μ.IsAddRightInvariant
inst✝² : MeasurableAdd₂ G
inst✝¹ : ν.IsAddRightInvariant
inst✝ : MeasurableNeg G
hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)
x₀ : G
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ
hi : Integrable (uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
⊢ ∫ (t : G), ∫ (s : G), (L₂ ((L (f s)) (g (t - s)))) (k (x₀ - t)) ∂ν ∂μ =
    ∫ (t : G), ∫ (s : G), (L₃ (f s)) ((L₄ (g (t - s))) (k (x₀ - t))) ∂ν ∂μ

Tactic:
hL

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i ↦ ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
⊢ (s i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)

pp: case inr.refine_2
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i ↦ ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
⊢ range q.c ⊆ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)

Tactic:
· -- show that balls of the same color are disjoint
    intro x hx y hy x_ne_y
    obtain ⟨jx, jx_lt, jxi, rfl⟩ :
      ∃ jx : Ordinal, jx < p.lastStep ∧ p.color jx = i ∧ x = p.index jx := by
      simpa only [s, exists_prop, mem_iUnion, mem_singleton_iff] using hx
    obtain ⟨jy, jy_lt, jyi, rfl⟩ :
      ∃ jy : Ordinal, jy < p.lastStep ∧ p.color jy = i ∧ y = p.index jy := by
      simpa only [s, exists_prop, mem_iUnion, mem_singleton_iff] using hy
    wlog jxy : jx ≤ jy generalizing jx jy
    · exact (this jy jy_lt jyi hy jx jx_lt jxi hx x_ne_y.symm (le_of_not_ge jxy)).symm
    replace jxy : jx < jy := by
      rcases lt_or_eq_of_le jxy with (H | rfl); · { exact H }; · { exact (x_ne_y rfl).elim }
    let A : Set ℕ :=
      ⋃ (j : { j // j < jy })
        (_ : (closedBall (p.c (p.index j)) (p.r (p.index j)) ∩
          closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
        {p.color j}
    have color_j : p.color jy = sInf (univ \ A) := by rw [TauPackage.color]
    have h : p.color jy ∈ univ \ A := by
      rw [color_j]
      apply csInf_mem
      refine ⟨N, ?_⟩
      simp only [A, not_exists, true_and, exists_prop, mem_iUnion, mem_singleton_iff, not_and,
        mem_univ, Set.mem_sdiff, Subtype.exists]
      intro k hk _
      exact (p.color_lt (hk.trans jy_lt) hN).ne'
    simp only [A, not_exists, true_and, exists_prop, mem_iUnion, mem_singleton_iff, not_and,
      mem_univ, Set.mem_sdiff, Subtype.exists] at h
    specialize h jx jxy
    contrapose! h
    simpa only [jxi, jyi, and_true, eq_self_iff_true, ← not_disjoint_iff_nonempty_inter] using h

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i ↦ ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
⊢ range q.c ⊆ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ 1 < goodτ E

Tactic:
dsimp [goodτ, goodδ]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ 1 < 1 + ⋯.choose / 4
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ j
hi : ‖a.c i‖ ≤ 2
hj : 2 < ‖a.c j‖
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
D : 0 ≤ 1 - δ / 4
hcrj : ‖a.c j‖ ≤ a.r j + 1
I : a.r i ≤ 2
J : (1 - δ / 4) * τ ≤ 1
H : a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
⊢ τ * 2 ≤ 5 / 4 * 2

Tactic:
by gcongr; linarith only [hδ1, hδ2]

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

Goal state before:
pp: G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : LocallyCompactSpace G
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := ⋯
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := ⋯
m : Set G
m_max : Maximal (fun x ↦ x ∈ A) m
hms : m ⊆ s
hdj : m.PairwiseDisjoint fun x ↦ x • k
sm : s ⊆ ⋃ x ∈ m, x • (k * k⁻¹)
hm : m.Nonempty
ρ : Measure G
hρ : ρ.IsEverywherePos s
M : ∀ (i : ↑m), MeasurableSet (s ∩ ↑i • k)
h'm : ρ s ≠ ∞
⊢ ρ (⋃ i, s ∩ ↑i • k) < ∞

Tactic:
· exact lt_of_le_of_lt (measure_mono (by simp [inter_subset_left])) h'm.lt_top

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x ↦ ↑x, r := fun x ↦ r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i ↦ ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
A : s = ⋃ i, s ∩ v i
S : ∑ _i, μ s / ↑N ≤ ∑ i, μ (s ∩ v i)
i : Fin N
hi : μ s / (↑N + 1) < μ (s ∩ v i)
B : μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))
w : Finset ↑(u i)
hw : μ s / (↑N + 1) < ∑ x ∈ w, μ (o ∩ closedBall (↑↑x) (r ↑↑x))
H : μ (o \ ⋃ x ∈ w, closedBall (↑↑x) (r ↑↑x)) ≤ ↑N / (↑N + 1) * μ s
⊢ μ (s \ ⋃ x ∈ Finset.image (fun x ↦ ↑↑x) w, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s

Tactic:
rw [Finset.set_biUnion_finset_image]
      exact le_trans (measure_mono (sdiff_subset_sdiff so (Subset.refl _))) H

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : E
n : ℕ
s : Set E
φ : E → E [×n]→L[𝕜'] F
h : DifferentiableWithinAt 𝕜' φ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ ⇑(fderivWithin 𝕜 (restrictScalars 𝕜 ∘ φ) s x) =
    restrictScalars 𝕜 ∘ ⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x))

Tactic:
simp only [← restrictScalarsLinear_apply]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : E
n : ℕ
s : Set E
φ : E → E [×n]→L[𝕜'] F
h : DifferentiableWithinAt 𝕜' φ s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ ⇑(fderivWithin 𝕜 (⇑(restrictScalarsLinear 𝕜) ∘ φ) s x) =
    ⇑(restrictScalarsLinear 𝕜) ∘ ⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x))
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k l : ℕ
α β : ↑I
f : E → F
a : E
hf : ContDiffPointwiseHolderAt k α f a
hle : toLex (l, β) ≤ toLex (k, α)
⊢ (ofLex (toLex (l, β))).1 = (ofLex (toLex (k, α))).1 ∧ (ofLex (toLex (l, β))).2 ≤ (ofLex (toLex (k, α))).2 →
    ContDiffPointwiseHolderAt l β f a

Tactic:
by rintro ⟨rfl, hle⟩; exact hf.of_exponent_le hle

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: case refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k : ℕ
α : ↑I
f : E → F
a : E
g : E → F
hf : ContDiffPointwiseHolderAt k α f a
hfg : f =ᶠ[𝓝 a] g
⊢ (fun x ↦ iteratedFDeriv ℝ k g a) =ᶠ[𝓝 a] fun x ↦ iteratedFDeriv ℝ k f a

Tactic:
hfg.symm.iteratedFDeriv ℝ _ |>.self_of_nhds

Goal state after:
case refine_2
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k : ℕ
α : ↑I
f : E → F
a : E
g : E → F
hf : ContDiffPointwiseHolderAt k α f a
hfg : f =ᶠ[𝓝 a] g
⊢ (fun x ↦ iteratedFDeriv ℝ k f a) =ᶠ[𝓝 a] fun x ↦ iteratedFDeriv ℝ k f a
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
t : Finset (α × ℝ)
ht : P t
B : Set α := ⋃ p ∈ t, closedBall p.1 p.2
hB : B = ⋃ p ∈ t, closedBall p.1 p.2
B_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] B
s' : Set α := s \ B
r : α → ℝ
hr : ∀ x ∈ s', r x ∈ f x ∩ Ioo 0 1 ∧ Disjoint B (closedBall x (r x))
v : Finset α
vs' : ↑v ⊆ s'
hμv : μ (s' \ ⋃ x ∈ v, closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s'
hv : (↑v).PairwiseDisjoint fun x ↦ closedBall x (r x)
⊢ s \ ⋃ p ∈ t ∪ Finset.image (fun x ↦ (x, r x)) v, closedBall p.1 p.2 = s' \ ⋃ x ∈ v, closedBall x (r x)

Tactic:
rw [Finset.set_biUnion_union, ← sdiff_sdiff, Finset.set_biUnion_finset_image]

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

Goal state before:
pp: case pos
f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : a ≤ b
⊢ ContinuousOn f (Icc a b)

Tactic:
exact Ioo_union_both g₀ ▸ hd₀.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)

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

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
x : ℝ
hx₀ : 0 < slope f x₀ x
hx₁ : x ∈ {x₀}ᶜ
⊢ sign (f x) = sign (x - x₀)

Tactic:
mem_compl_iff,

Goal state after:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
x : ℝ
hx₀ : 0 < slope f x₀ x
hx₁ : x ∉ {x₀}
⊢ sign (f x) = sign (x - x₀)