mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case top.refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ∞
n : ℝ
hn : n < ‖x‖
⊢ ‖x‖ = ‖Pi.single i x i‖

Tactic:
rw [Pi.single_eq_same]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
⊢ HasSum (fun i ↦ lp.single p i (↑f i)) f

Tactic:
by
  have hp₀ : 0 < p := zero_lt_one.trans_le Fact.out
  have hp' : 0 < p.toReal := ENNReal.toReal_pos hp₀.ne' hp
  have := lp.hasSum_norm hp' f
  rw [HasSum, Metric.tendsto_nhds] at this ⊢
  intro ε hε
  refine (this _ (Real.rpow_pos_of_pos hε p.toReal)).mono ?_
  intro s hs
  rw [← Real.rpow_lt_rpow_iff dist_nonneg (le_of_lt hε) hp']
  rw [dist_comm] at hs
  simp only [dist_eq_norm, Real.norm_eq_abs] at hs ⊢
  have H : ‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal =
      ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖f i‖ ^ p.toReal := by
    simpa only [coeFn_neg, Pi.neg_apply, lp.single_neg, Finset.sum_neg_distrib, neg_sub_neg,
      norm_neg, _root_.norm_neg] using lp.norm_compl_sum_single hp' (-f) s
  rw [← H] at hs
  have : |‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal| =
      ‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal := by
    simp only [Real.abs_rpow_of_nonneg (norm_nonneg _), abs_norm]
  exact this ▸ hs

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hx : x ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x

Tactic:
have : ‖id x‖ ^ 2 ≠ 0 := pow_ne_zero 2 (norm_pos_iff.2 hx).ne'
  simpa only [id, sqrt_sq, norm_nonneg] using (contDiffAt_id.norm_sq 𝕜).sqrt this

Goal state after:
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'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ t : G
ht : g (x₀ - t) = 0
⊢ (fun t ↦ (L (f t)) (g (x₀ - t))) t = 0

Tactic:
simp_rw [ht, (L _).map_zero]

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case refine_2
𝕜 : 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✝¹¹ : 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✝¹ : FirstCountableTopology G
inst✝ : SecondCountableTopologyEither G E'
hbg : BddAbove (range fun x ↦ ‖g x‖)
hf : Integrable f μ
hg : Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖
⊢ ∀ᵐ (a : G) ∂μ, ContinuousAt (fun x ↦ (L (f a)) (g (x - a))) x₀

Tactic:
filter_upwards with t; fun_prop

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.EuclideanDist

Goal state before:
pp: E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed[inst✝⁵] s
h : s ⊆ ⇑toEuclidean ⁻¹' Metric.ball (toEuclidean x) R
⊢ ∃ r ∈ Ioo 0 R, s ⊆ ball x r

Tactic:
← image_subset_iff

Goal state after:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed[inst✝⁵] s
h : ⇑toEuclidean '' s ⊆ Metric.ball (toEuclidean x) R
⊢ ∃ r ∈ Ioo 0 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
⊢ ∃ s ∈ 𝓝 x, Bornology.IsBounded (⇑f '' s)

Tactic:
let K : PositiveCompacts G := Classical.arbitrary _
  obtain ⟨n, hn⟩ : ∃ n : ℕ, 0 < haar (interior K ∩ f ⁻¹' ball 1 n) := by
    by_contra!
    simp_rw [nonpos_iff_eq_zero, ← measure_iUnion_null_iff, ← inter_iUnion, ← preimage_iUnion,
      iUnion_ball_nat, preimage_univ, inter_univ] at this
    exact this.not_gt <| isOpen_interior.measure_pos _ K.interior_nonempty
  rw [← mul_one x, ← smul_eq_mul]
  refine ⟨_, smul_mem_nhds_smul _ <| div_mem_nhds_one_of_haar_pos_ne_top haar _
    (isOpen_interior.measurableSet.inter <| hf measurableSet_ball) hn <|
      mt (measure_mono_top <| inter_subset_left.trans interior_subset) K.isCompact.measure_ne_top,
    ?_⟩
  have : Bornology.IsBounded (f '' (interior K ∩ f ⁻¹' ball 1 n)) :=
    isBounded_ball.subset <| (image_mono inter_subset_right).trans <| image_preimage_subset _ _
  rw [image_smul_distrib, image_div]
  exact (this.div this).smul _

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: case he
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ μ ∅ = 0

Tactic:
exact measure_empty

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
⊢ μ.InnerRegularWRT (fun s ↦ ∃ f, Continuous[inst✝⁷, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun s ↦
    MeasurableSet s ∧ μ s ≠ ∞

Tactic:
apply InnerRegularWRT.trans _ innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group
  intro K ⟨K_comp, K_closed⟩ r hr
  let L := μ.everywherePosSubset K
  have L_comp : IsCompact L := K_comp.everywherePosSubset
  have L_closed : IsClosed L := K_closed.everywherePosSubset
  refine ⟨L, everywherePosSubset_subset μ K, ?_, ?_⟩
  · have : μ.IsEverywherePos L :=
      isEverywherePos_everywherePosSubset_of_measure_ne_top K_closed.measurableSet
      K_comp.measure_lt_top.ne
    have L_Gδ : IsGδ L := this.IsGdelta_of_isMulLeftInvariant L_comp L_closed
    obtain ⟨⟨f, f_cont⟩, Lf, -, f_comp, -⟩ : ∃ f : C(G, ℝ), L = f ⁻¹' {1} ∧ EqOn f 0 ∅
        ∧ HasCompactSupport f ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
      exists_continuous_one_zero_of_isCompact_of_isGδ L_comp L_Gδ isClosed_empty
        (disjoint_empty L)
    exact ⟨f, f_cont, f_comp, Lf⟩
  · convert! hr using 1
    apply measure_congr
    exact everywherePosSubset_ae_eq_of_measure_ne_top K_closed.measurableSet
      K_comp.measure_lt_top.ne

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

Goal state before:
pp: case hfs
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : LocallyCompactSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : G → E
hg : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
p x : G
hp : p ∈ t
hx : g (x⁻¹ * p) ≠ 0
⊢ p⁻¹ * x ∈ k⁻¹

Tactic:
simpa only [Set.mem_inv, mul_inv_rev, inv_inv] using subset_tsupport _ hx

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case neg
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∉ Ioi 0
⊢ 0 = ∫ (t : ℝ), (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t)) ∂ν

Tactic:
convert! (integral_zero ℝ F).symm with t
    by_cases ht : 0 < t
    · rw [indicator_of_notMem (_ : x - t ∉ Ioi 0), map_zero]
      rw [notMem_Ioi] at h ⊢
      exact sub_nonpos.mpr (h.trans ht.le)
    · rw [indicator_of_notMem (mem_Ioi.not.mpr ht), map_zero, zero_apply]

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
n✝ : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n : ℕ
R : ℕ → ℝ
hR : ∀ (i : ℕ) (x : E), ‖iteratedFDeriv ℝ i (fun x ↦ g n x) x‖ ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
IR : ∀ i ≤ n, R i ≤ M
i : ℕ
hi : i ≤ n
x : E
⊢ ‖iteratedFDeriv ℝ i ((M⁻¹ * ↑(δ n)) • g n) x‖ = ‖(M⁻¹ * ↑(δ n)) • iteratedFDeriv ℝ i (g n) x‖

Tactic:
by
        rw [iteratedFDeriv_const_smul_apply]
        exact (g_smooth n).contDiffAt.of_le (mod_cast le_top)

Goal state after:
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
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (support fun x_1 ↦ (φ x).normed μ x_1) ∈ 𝒫 ball c i

Tactic:
refine fun ε hε ↦ (hφ ε hε).mono fun i hi ↦ ?_

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
ι : Type u_2
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ ε > 0, ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ (support fun x ↦ (φ i).normed μ x) ∈ 𝒫 ball c ε
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
⊢ False

Tactic:
suffices H : Function.Injective p.index from not_injective_of_ordinal p.index H

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
h : ¬{i | ¬∃ b, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty
⊢ Function.Injective p.index
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
D_pos : ∀ (x : G), 0 < D x
⊢ ∫ (x : G), ∫ (y : G), f (y * x) * (D (y * x))⁻¹ * g x ∂ν ∂μ = ∫ (x : G), (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x ∂μ

Tactic:
simp_rw [integral_mul_const]

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
D_pos : ∀ (x : G), 0 < D x
⊢ ∫ (x : G), (∫ (a : G), f (a * x) * (D (a * x))⁻¹ ∂ν) * g x ∂μ = ∫ (x : G), (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x ∂μ
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
D_pos : ∀ (x : G), 0 < D x
x : G
| (∫ (y : G), f y * (D y)⁻¹ ∂ν) * g x

Tactic:
rw [← integral_mul_right_eq_self _ x]

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
D_pos : ∀ (x : G), 0 < D x
x : G
| (∫ (x_1 : G), f (x_1 * x) * (D (x_1 * x))⁻¹ ∂ν) * g x
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
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁹] s)
r : ℝ≥0∞
hr : r < μ'.haarScalarFactor μ • μ s
ν : Measure G := μ'.haarScalarFactor μ • μ
this : ν s ≠ ∞
⊢ r < ν s

Tactic:
convert! hr

Goal state after:
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
⊢ ‖a.c j‖ ≤ a.r j + 1

Tactic:
simpa only [lastc, lastr, dist_zero_right] using a.inter' j

Goal state after:
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
i j : Fin N.succ
inej : i ≠ j
hi : 2 < ‖a.c i‖
hij : ‖a.c i‖ ≤ ‖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 ≤ δ
⊢ ‖a.c j‖ ≤ a.r j + 1

Tactic:
simpa only [lastc, lastr, dist_zero_right] using a.inter' j

Goal state after:
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
C D s : ℝ≥0
A : Set X
hA : ∀ x ∈ A, ∀ y ∈ A, edist x y ≤ ↑D
hf : HolderOnWith C r f A
hsr : ↑s ≤ ↑r
ht : 0 < s
hr : 0 < ↑r
θ₁ : ℝ≥0 := ⋯
θ₂ : ℝ≥0 := ⋯
⊢ ↑(θ₁ + θ₂) = ↑1

Tactic:
simp [θ₁, θ₂]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : SeminormedAddCommGroup Y
C C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
⊢ HolderWith (C + C') r (f + g)

Tactic:
intro x₁

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : SeminormedAddCommGroup Y
C C' r : ℝ≥0
f g : X → Y
hf : HolderWith C r f
hg : HolderWith C' r g
x₁ : X
⊢ ∀ (y : X), edist ((f + g) x₁) ((f + g) y) ≤ ↑(C + C') * edist x₁ y ^ ↑r
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
x : α
hx : ∃ i, ∃ x_1 ∈ S i, ↑x_1 = x
⊢ x ∈ s'

Tactic:
rcases hx with ⟨i, y, _, rfl⟩

Goal state after:
α : Type u_1
inst✝⁶ : MetricSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : HasBesicovitchCovering α
μ : Measure α
inst✝¹ : SFinite μ
inst✝ : μ.OuterRegular
ε : ℝ≥0∞
hε : ε ≠ 0
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
u : Set α
su : u ⊇ s
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
μu : μ u ≤ μ s + ε / 2
R : α → ℝ
hR : ∀ x ∈ s, R x > 0 ∧ ball x (R x) ⊆ u
t0 : Set α
r0 : α → ℝ
t0_count : t0.Countable
t0s : t0 ⊆ s
hr0 : ∀ x ∈ t0, r0 x ∈ f x ∩ Ioo 0 (R x)
μt0 : μ (s \ ⋃ x ∈ t0, closedBall x (r0 x)) = 0
t0_disj : t0.PairwiseDisjoint fun x ↦ closedBall x (r0 x)
s' : Set α := s \ ⋃ x ∈ t0, closedBall x (r0 x)
s's : s' ⊆ s
N : ℕ
τ : ℝ
hτ : 1 < τ
H : IsEmpty (SatelliteConfig α N τ)
v : Set α
s'v : v ⊇ s'
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
μv : μ v ≤ μ s' + ε / 2 / ↑N
r1 : α → ℝ
hr1 : ∀ x ∈ s', r1 x ∈ f x ∩ Ioo 0 1 ∧ closedBall x (r1 x) ⊆ v
q : BallPackage (↑s') α := { c := fun x ↦ ↑x, r := fun x ↦ r1 ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
S : Fin N → Set ↑s'
S_disj : ∀ (i : Fin N), (S i).PairwiseDisjoint fun j ↦ closedBall (q.c j) (q.r j)
hS : range q.c ⊆ ⋃ i, ⋃ j ∈ S i, ball (q.c j) (q.r j)
S_count : ∀ (i : Fin N), (S i).Countable
r : α → ℝ := fun x ↦ if x ∈ s' then r1 x else r0 x
r_t0 : ∀ x ∈ t0, r x = r0 x
i : Fin N
y : { x // x ∈ s' }
left✝ : y ∈ S i
⊢ ↑y ∈ s'
Module: Mathlib.Analysis.Calculus.DifferentialForm.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
ω : E → E [⋀^Fin n]→L[𝕜] F
x : E
⊢ alternatizeUncurryFin (fderivWithin 𝕜 ω univ x) = alternatizeUncurryFin (fderiv 𝕜 ω x)

Tactic:
fderivWithin_univ

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
ω : E → E [⋀^Fin n]→L[𝕜] F
x : E
⊢ alternatizeUncurryFin (fderiv 𝕜 ω x) = alternatizeUncurryFin (fderiv 𝕜 ω x)
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
f : E → 𝕜
hf : DifferentiableAt 𝕜 f x
hW : DifferentiableAt 𝕜 W x
⊢ lieBracket 𝕜 V (fun y ↦ f y • W y) x = (fderiv 𝕜 f x) (V x) • W x + f x • lieBracket 𝕜 V W x

Tactic:
simp_rw [← differentiableWithinAt_univ, ← lieBracketWithin_univ, fderiv] at hW hf ⊢

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
f : E → 𝕜
hW : DifferentiableWithinAt 𝕜 W univ x
hf : DifferentiableWithinAt 𝕜 f univ x
⊢ lieBracketWithin 𝕜 V (fun y ↦ f y • W y) univ x =
    (fderivWithin 𝕜 f univ x) (V x) • W x + f x • lieBracketWithin 𝕜 V W univ x
Module: Mathlib.Analysis.Calculus.VectorField

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
V W : E → E
x : E
f : E → F
hf : ContDiffAt 𝕜 2 f x
hsymm : IsSymmSndFDerivAt 𝕜 f x
hW : DifferentiableAt 𝕜 W x
hV : DifferentiableAt 𝕜 V x
⊢ (fderiv 𝕜 f x) (lieBracket 𝕜 V W x) =
    (fderiv 𝕜 (fun x ↦ (fderiv 𝕜 f x) (W x)) x) (V x) - (fderiv 𝕜 (fun x ↦ (fderiv 𝕜 f x) (V x)) x) (W x)

Tactic:
by
  simp only [← fderivWithin_univ, ← lieBracketWithin_univ, ← contDiffWithinAt_univ,
    ← isSymmSndFDerivWithinAt_univ, ← differentiableWithinAt_univ] at *
  exact fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt hf hsymm (by simp) (by simp)
    hW hV

Goal state after: