mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

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

Tactic:
apply hk.induction_on (p := fun t ↦ μ t = 0)
  · exact measure_empty
  · exact fun s t hst ht ↦ measure_mono_null hst ht
  · exact fun s t hs ht ↦ measure_union_null hs ht
  · intro x hx
    obtain ⟨u, ux, hu⟩ : ∃ u ∈ 𝓝[s] x, μ u = 0 := by
      simpa [everywherePosSubset, (h'k hx).1] using (h'k hx).2
    exact ⟨u, nhdsWithin_mono x (h'k.trans sdiff_subset) ux, hu⟩

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
x : E
hx : x ∈ ⋃ f ∈ T, support ↑f
⊢ ∃ n, x ∈ support (g n)

Tactic:
obtain ⟨i, iT, hi⟩ : ∃ i ∈ T, x ∈ support (i : E → ℝ) := by
      simpa only [mem_iUnion, exists_prop] using! hx

Goal state after:
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
x : E
hx : x ∈ ⋃ f ∈ T, support ↑f
i : ι
iT : i ∈ T
hi : x ∈ support ↑i
⊢ ∃ n, x ∈ support (g n)
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
this : p.index y = Classical.epsilon fun b ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b
⊢ p.c (Classical.epsilon fun b ↦ p.c b ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r b) ∉ p.iUnionUpTo y

Tactic:
exact (Classical.epsilon_spec h).1

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
⊢ IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1))

Tactic:
closure_ball (0 : E) one_ne_zero

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ IsCompact (closedBall 0 1)
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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ ∫ (t : E), ((lsmul ℝ ℝ) (w D t)) (φ x) ∂μ = 1

Tactic:
simp only [lsmul_apply, smul_eq_mul, integral_mul_const, w_integral E Dpos, Bx,
    one_mul]

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

Goal state before:
pp: case refine_1
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)
⊢ Integrable (fun i ↦ w D i * φ (x - i)) μ

Tactic:
have B : LocallyIntegrable (φ : E → ℝ) μ :=
      (locallyIntegrable_const _).indicator measurableSet_closedBall

Goal state after:
case refine_1
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 φ μ
⊢ Integrable (fun i ↦ w D i * φ (x - i)) μ
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
ha : ↑a ≤ N
hb : ↑b ≤ N
B : p.c (p.index (G ↑b)) ∉ p.iUnionUpTo (G ↑a)
b' : { t // p.c t ∉ p.iUnionUpTo (G ↑a) } := ⟨p.index (G ↑b), B⟩
t : ℝ
u : β
hu : p.c u ∉ p.iUnionUpTo (G ↑a) ∧ p.r u = t
⊢ p.r u ≤ p.r_bound

Tactic:
exact p.r_le _

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

Goal state before:
pp: case refine_3
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (↿w) (Ioo 0 1 ×ˢ univ)

Tactic:
apply ContDiffOn.mul
    · norm_cast
      refine
        (contDiffOn_const.mul ?_).inv fun x hx =>
          ne_of_gt (mul_pos (u_int_pos E) (pow_pos (abs_pos_of_pos hx.1.1) (finrank ℝ E)))
      apply ContDiffOn.pow
      simp_rw [← Real.norm_eq_abs]
      apply ContDiffOn.norm ℝ
      · exact contDiffOn_fst
      · intro x hx; exact ne_of_gt hx.1.1
    · apply (u_smooth E).comp_contDiffOn
      exact ContDiffOn.smul (contDiffOn_fst.inv fun x hx => ne_of_gt hx.1.1) contDiffOn_snd

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)
this : o ∩ v i = ⋃ x ∈ u i, o ∩ closedBall (↑x) (r ↑x)
⊢ μ (o ∩ v i) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))

Tactic:
this,

Goal state after:
α : 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)
this : o ∩ v i = ⋃ x ∈ u i, o ∩ closedBall (↑x) (r ↑x)
⊢ μ (⋃ x ∈ u i, o ∩ closedBall (↑x) (r ↑x)) = ∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑x))
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:
this,

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
⊢ a.r (last N) ≤ 2
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))
⊢ HasSum (fun x ↦ μ (o ∩ closedBall (↑↑x) (r ↑↑x))) (μ (o ∩ v i))

Tactic:
rw [B]

Goal state after:
α : 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))
⊢ HasSum (fun x ↦ μ (o ∩ closedBall (↑↑x) (r ↑↑x))) (∑' (x : ↑(u i)), μ (o ∩ closedBall (↑↑x) (r ↑↑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✝ : μ'.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}
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
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → ρ s = ∞
Hν : ν.IsEverywherePos s
x : G
_hx : x ∈ s
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ' u = ν u

Tactic:
obtain ⟨t, t_comp, t_mem⟩ : ∃ t, IsCompact t ∧ t ∈ 𝓝 x := exists_compact_mem_nhds x

Goal state after:
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}
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
h'm : ¬m.Countable
H : ∀ (ρ : Measure G), ρ.IsEverywherePos s → ρ s = ∞
Hν : ν.IsEverywherePos s
x : G
_hx : x ∈ s
t : Set G
t_comp : IsCompact t
t_mem : t ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x, ∀ u ⊆ t, μ' u = ν u
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
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous[inst✝¹², inst✝⁶] ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
this✝¹ : IsFiniteMeasure μ
this✝ : (map (⇑f) μ).IsHaarMeasure
C : ℝ≥0 := (map (⇑f) μ).haarScalarFactor ν
hC : map (⇑f) μ = C • ν
this : C = 1
⊢ map (⇑f) μ = ν

Tactic:
this,

Goal state after:
G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous[inst✝¹², inst✝⁶] ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
this✝¹ : IsFiniteMeasure μ
this✝ : (map (⇑f) μ).IsHaarMeasure
C : ℝ≥0 := (map (⇑f) μ).haarScalarFactor ν
hC : map (⇑f) μ = 1 • ν
this : C = 1
⊢ map (⇑f) μ = ν
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : LocallyCompactSpace G
inst✝ : μ.Regular
c : ℝ≥0∞ := ↑(μ.inv.haarScalarFactor μ)
hc : μ.inv = c • μ
this✝² : map Inv.inv (map Inv.inv μ) = c ^ 2 • μ
μeq : μ = c ^ 2 • μ
K : PositiveCompacts G
this✝¹ : c ^ 2 * μ ↑K = 1 ^ 2 * μ ↑K
this✝ : c ^ 2 = 1 ^ 2
this : c = 1
⊢ c • μ = μ

Tactic:
this,

Goal state after:
G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : LocallyCompactSpace G
inst✝ : μ.Regular
c : ℝ≥0∞ := ↑(μ.inv.haarScalarFactor μ)
hc : μ.inv = c • μ
this✝² : map Inv.inv (map Inv.inv μ) = c ^ 2 • μ
μeq : μ = c ^ 2 • μ
K : PositiveCompacts G
this✝¹ : c ^ 2 * μ ↑K = 1 ^ 2 * μ ↑K
this✝ : c ^ 2 = 1 ^ 2
this : c = 1
⊢ 1 • μ = μ
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : LocallyCompactSpace G
inst✝ : μ.InnerRegular
c : ℝ≥0∞ := ↑(μ.inv.haarScalarFactor μ)
hc : μ.inv = c • μ
this✝² : map Inv.inv (map Inv.inv μ) = c ^ 2 • μ
μeq : μ = c ^ 2 • μ
K : PositiveCompacts G
this✝¹ : c ^ 2 * μ ↑K = 1 ^ 2 * μ ↑K
this✝ : c ^ 2 = 1 ^ 2
this : c = 1
⊢ c • μ = μ

Tactic:
this,

Goal state after:
G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : LocallyCompactSpace G
inst✝ : μ.InnerRegular
c : ℝ≥0∞ := ↑(μ.inv.haarScalarFactor μ)
hc : μ.inv = c • μ
this✝² : map Inv.inv (map Inv.inv μ) = c ^ 2 • μ
μeq : μ = c ^ 2 • μ
K : PositiveCompacts G
this✝¹ : c ^ 2 * μ ↑K = 1 ^ 2 * μ ↑K
this✝ : c ^ 2 = 1 ^ 2
this : c = 1
⊢ 1 • μ = μ
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD
gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B ∘SL ↑↑isoE).flip ∘SL ↑↑isoF).flip
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y ↦ (B (f y)) (g y)) s x‖ ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

Tactic:
let Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
    ContinuousLinearMap.compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)
      (ContinuousLinearMap.compL 𝕜 Fu G Gu (isoG.symm : G →L[𝕜] Gu)) Bu₀

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD
gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B ∘SL ↑↑isoE).flip ∘SL ↑↑isoF).flip
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y ↦ (B (f y)) (g y)) s x‖ ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: case inr
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 := NNReal.mk (↑s / ↑r) ⋯
θ₂ : ℝ≥0 := NNReal.mk (1 - ↑s / ↑r) ⋯
hθ : θ₁ + θ₂ = 1
hθt : r * θ₁ + 0 * θ₂ = s
hθC : C * D ^ (↑r - ↑s) = C ^ ↑θ₁ * (C * D ^ ↑r) ^ ↑θ₂
⊢ HolderOnWith (C ^ ↑θ₁ * (C * D ^ ↑r) ^ ↑θ₂) (r * θ₁ + 0 * θ₂) f A

Tactic:
exact hf.interpolate (hf.holderOnWith_zero_of_bounded hA) hθ

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
a✝ : m ∈ Finset.univ
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(↑p).countPerms * ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(n.choose ↑m * (↑p).countPerms) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)

Tactic:
this,

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
a✝ : m ∈ Finset.univ
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖) =
    ↑(n.choose ↑m * (↑p).countPerms) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
i : Fin (n + 1)
hi : i ∈ Finset.univ
⊢ ‖(-1) ^ ↑i • (f (v i)) (i.removeNth v)‖ ≤ ‖f‖ * ∏ i, ‖v i‖

Tactic:
rw [norm_isUnit_zsmul _ (.pow _ isUnit_one.neg), i.prod_univ_succAbove, ← mul_assoc]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
i : Fin (n + 1)
hi : i ∈ Finset.univ
⊢ ‖(f (v i)) (i.removeNth v)‖ ≤ ‖f‖ * ‖v i‖ * ∏ i_1, ‖v (i.succAbove i_1)‖
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ < 0
hx : f x₀ = 0
⊢ ∀ᶠ (x : ℝ) in 𝓝 x₀, sign (f x) = sign (x₀ - x)

Tactic:
simpa [Left.sign_neg, -neg_sub, ← neg_sub x₀] using
    eventually_nhdsWithin_sign_eq_of_deriv_pos
      (f := (-f ·)) (x₀ := x₀) (by simpa [deriv.neg]) (by simpa)

Goal state after: