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

Goal state before:
pp: α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : H → α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasFDerivAt (fun x ↦ F x a) (F' x a) x
this : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasFDerivAt (fun x ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : H
x_in : x ∈ ball x₀ ε
⊢ ↑‖F' x a‖₊ ≤ ↑(Real.nnabs (bound a))

Tactic:
coe_nnnorm,

Goal state after:
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : H → α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasFDerivAt (fun x ↦ F x a) (F' x a) x
this : NormedSpace ℝ H := NormedSpace.restrictScalars ℝ 𝕜 H
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasFDerivAt (fun x ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : H
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ ↑(Real.nnabs (bound a))
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
⊢ ContinuousOn (fun y ↦ dist y x) s

Tactic:
fun_prop

Goal state after:
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:
subst s

Goal state after:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
hr : r ≤ 0
hs : IsClosed ∅
⊢ ∃ r' < r, ∅ ⊆ ball x r'
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
⊢ Continuous (dist x)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
⊢ Continuous (nndist x)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
⊢ Continuous NNReal.toReal

Tactic:
fun_prop

Goal state after:
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
⊢ ∃ s ∈ 𝓝 x, Bornology.IsBounded (⇑f '' s)

Tactic:
let K : PositiveCompacts G := Classical.arbitrary _

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)
⊢ ∃ s ∈ 𝓝 x, Bornology.IsBounded (⇑f '' s)
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : 𝕜
x_in : x ∈ ball x₀ ε
⊢ ↑‖F' x a‖₊ ≤ ↑(Real.nnabs (bound a))

Tactic:
coe_nnnorm,

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : 𝕜
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖ ≤ ↑(Real.nnabs (bound a))
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
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable g μ
hk : AEStronglyMeasurable k μ
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x ↦ ‖g x‖) (fun x ↦ ‖k x‖) x (mul ℝ ℝ) μ
hfgk : ConvolutionExistsAt (fun x ↦ ‖f x‖) ((fun x ↦ ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x ↦ ‖k x‖) x₀ (mul ℝ ℝ) ν
⊢ Measurable fun x ↦ x₀ - x.2 - x.1

Tactic:
fun_prop

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
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
x : G
⊢ Continuous[inst✝⁹, _] fun y ↦ g (y⁻¹ * x)

Tactic:
fun_prop

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
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
x : G
⊢ 0 < D x

Tactic:
have C : Continuous (fun y ↦ g (y⁻¹ * x)) := by fun_prop

Goal state after:
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
x : G
C : Continuous[inst✝⁹, _] fun y ↦ g (y⁻¹ * x)
⊢ 0 < D x
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := ⋯
f : E → ℝ := ⋯
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ toEuclidean x ∈ closedBall (toEuclidean x) c.rIn

Tactic:
apply mem_closedBall_self

Goal state after:
case refine_4
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := ⋯
f : E → ℝ := ⋯
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ 0 ≤ c.rIn
Module: Mathlib.Analysis.Calculus.BumpFunction.Normed

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ support (f.normed μ) = ball c f.rOut

Tactic:
unfold ContDiffBump.normed
  rw [support_div, f.support_eq, support_const f.integral_pos.ne', inter_univ]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
this : p.lastStep ∈ {i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}
⊢ ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep

Tactic:
simpa only [not_exists, mem_ofPred_eq, not_and_or, not_le, not_notMem]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
this : ∃ a ∈ range fun b ↦ p.r ↑b, p.τ⁻¹ * p.R p.lastStep < a
⊢ ∃ y, p.c y ∉ p.iUnionUpTo p.lastStep ∧ p.τ⁻¹ * p.R p.lastStep < p.r y

Tactic:
simpa only [exists_prop, mem_range, exists_exists_and_eq_and, Subtype.exists,
      Subtype.coe_mk]

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
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ AEMeasurable (⇑φ) μ'

Tactic:
fun_prop

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
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ AEStronglyMeasurable (⇑{ toFun := f, continuous_toFun := f_cont }) (map (⇑φ) μ')

Tactic:
fun_prop

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
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ AEMeasurable (⇑φ) μ

Tactic:
fun_prop

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
μ' μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
φ : G ≃ₜ* G
hG : LocallyCompactSpace G
f : G → ℝ
f_cont : Continuous[inst✝⁶, _] f
hf :
  HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont } ∧
    0 ≤ ⇑{ toFun := f, continuous_toFun := f_cont } ∧ { toFun := f, continuous_toFun := f_cont } 1 ≠ 0
int_f_ne_zero : ∫ (x : G), f x ∂map (⇑φ) μ ≠ 0
⊢ AEStronglyMeasurable (⇑{ toFun := f, continuous_toFun := f_cont }) (map (⇑φ) μ)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (HSMul.hSMul D⁻¹)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
F_comp : HasCompactSupport (w D)
B : LocallyIntegrable φ μ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (HSMul.hSMul D⁻¹)

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
a b : Fin N.succ
G_lt : G ↑a < G ↑b
⊢ p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧
    p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))

Tactic:
have ha : (a : ℕ) ≤ N := Nat.lt_succ_iff.1 a.2

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
a b : Fin N.succ
G_lt : G ↑a < G ↑b
ha : ↑a ≤ N
⊢ p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧
    p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s).Pairwise (Disjoint on fun c ↦ ball c δ)
A_subset : A ⊆ ball 0 ρ
I : 0 < δ
⊢ ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) = ∑ x ∈ s, ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1)

Tactic:
simp only [Finset.sum_const, nsmul_eq_mul, mul_assoc]

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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁸] s)
⊢ μ' s = μ'.haarScalarFactor μ • μ s

Tactic:
by
  let ν : Measure G := haar
  have A : μ' s = haarScalarFactor μ' ν • ν s :=
    measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop μ' ν hs h's
  have B : μ s = haarScalarFactor μ ν • ν s :=
    measure_isMulInvariant_eq_smul_of_isCompact_closure_of_innerRegularCompactLTTop μ ν hs h's
  rw [A, B, smul_smul, haarScalarFactor_eq_mul μ' μ ν]

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
⊢ ContinuousOn (⇑f) (cthickening 1 K)

Tactic:
fun_prop

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

Goal state before:
pp: case refine_3
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 := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ ∀ s ∈ c, s ⊆ ⋃ a ∈ c, a

Tactic:
intro a ac
      exact subset_biUnion_of_mem (u := id) ac

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

Goal state before:
pp: case inr
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ 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
τpos : 0 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin N.succ), τ⁻¹ ≤ a.r k
H : a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
⊢ τ⁻¹ ≤ ‖a.c i - a.c j‖

Tactic:
norm_sub_rev

Goal state after:
case inr
E : Type u_1
inst✝ : NormedAddCommGroup E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
hδ2 : δ ≤ 1
i j : Fin N.succ
inej : i ≠ 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
τpos : 0 < τ
I : (1 - δ / 4) * τ ≤ 1
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin N.succ), τ⁻¹ ≤ a.r k
H : a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
⊢ τ⁻¹ ≤ ‖a.c j - a.c i‖
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: case inr
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
H : last N ≤ i
this : i = last N
⊢ a.r (last N) ≤ 2

Tactic:
lastr

Goal state after:
case inr
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
H : last N ≤ i
this : i = last N
⊢ 1 ≤ 2
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: case inr
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
H : last N ≤ i
this : i = last N
⊢ a.r i ≤ 2

Tactic:
rw [this, lastr]

Goal state after:
case inr
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
H : last N ≤ i
this : i = last N
⊢ 1 ≤ 2