mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : 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
⊢ ∃ y, p.c y ∉ p.iUnionUpTo p.lastStep ∧ p.τ⁻¹ * p.R p.lastStep < p.r y

Tactic:
by
    have := exists_lt_of_lt_csSup ?_ B
    · simpa only [exists_prop, mem_range, exists_exists_and_eq_and, Subtype.exists,
      Subtype.coe_mk]
    rw [← image_univ, image_nonempty]
    exact ⟨⟨_, h⟩, mem_univ _⟩

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

Goal state before:
pp: case inr.refine_3
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
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n ↦ (r n • g n) x
⊢ (range fun x ↦ ∑' (n : ℕ), (r n • g n) x) ⊆ Icc 0 1

Tactic:
· rintro - ⟨y, rfl⟩
    refine ⟨tsum_nonneg fun n => mul_nonneg (rpos n).le (g_nonneg n y), le_trans ?_ c_lt.le⟩
    have A : HasSum (fun n => (δ n : ℝ)) c := NNReal.hasSum_coe.2 δc
    simp only [Pi.smul_apply, smul_eq_mul, NNReal.val_eq_coe, ← A.tsum_eq]
    apply Summable.tsum_le_tsum _ (S y) A.summable
    intro n
    apply (le_abs_self _).trans
    simpa only [norm_iteratedFDeriv_zero] using! hr n 0 zero_le y

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

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < μ (support u)

Tactic:
u_support

Goal state after:
case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ 0 < μ (ball 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 ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : ‖y‖ ≤ 1
⊢ D + dist y 0 ≤ 1 + D

Tactic:
rw [← dist_zero_right] at h'y

Goal state after:
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 ∉ ball 0 (1 + D)
y : E
hy : y ∈ ball x D
h'y : dist y 0 ≤ 1
⊢ D + dist y 0 ≤ 1 + D
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case ind
α : 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))
⊢ False

Tactic:
have Gab :
    ∀ a b : Fin (Nat.succ N),
      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)) := by
    intro a b G_lt
    have ha : (a : ℕ) ≤ N := Nat.lt_succ_iff.1 a.2
    have hb : (b : ℕ) ≤ N := Nat.lt_succ_iff.1 b.2
    constructor
    · have := (fGn b hb).1
      simp only [iUnionUpTo, not_exists, exists_prop, mem_iUnion, not_and,
        Subtype.exists] at this
      simpa only [dist_comm, mem_ball, not_lt] using this (G a) G_lt
    · apply le_trans _ (fGn a ha).2
      have B : p.c (p.index (G b)) ∉ p.iUnionUpTo (G a) := by
        intro H; exact (fGn b hb).1 (p.monotone_iUnionUpTo G_lt.le H)
      let b' : { t // p.c t ∉ p.iUnionUpTo (G a) } := ⟨p.index (G b), B⟩
      apply @le_ciSup _ _ _ (fun t : { t // p.c t ∉ p.iUnionUpTo (G a) } => p.r t) _ b'
      refine ⟨p.r_bound, fun t ht => ?_⟩
      simp only [exists_prop, mem_range, Subtype.exists] at ht
      rcases ht with ⟨u, hu⟩
      rw [← hu.2]
      exact p.r_le _

Goal state after:
case ind
α : 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))
Gab :
  ∀ (a b : Fin N.succ),
    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))
⊢ False
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
⊢ (if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • -x) else 0) =
    if 1 < R then y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x) else 0

Tactic:
split_ifs

Goal state after:
case pos
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
h✝ : 1 < R
⊢ y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • -x) = y ((R - 1) / (R + 1)) (((R + 1) / 2)⁻¹ • x)

case neg
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
h✝ : ¬1 < R
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
u : ℕ → ℝ
left✝ : ∀ (m n : ℕ), m < n → u n < u m
zero_lt_u : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
A✝ : ∀ (n : ℕ), F (u n) ∈ closedBall 0 2
f : Fin N → E
fmem : f ∈ closedBall 0 2
φ : ℕ → ℕ
φ_mono : StrictMono φ
hf : Tendsto ((F ∘ u) ∘ φ) atTop (𝓝 f)
i j : Fin N
hij : i ≠ j
A : Tendsto (fun n ↦ ‖F (u (φ n)) i - F (u (φ n)) j‖) atTop (𝓝 ‖f i - f j‖)
B : Tendsto (fun n ↦ 1 - u (φ n)) atTop (𝓝 (1 - 0))
⊢ (fun i j ↦ 1 ≤ ‖f i - f j‖) i j

Tactic:
rw [sub_zero] at B

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
u : ℕ → ℝ
left✝ : ∀ (m n : ℕ), m < n → u n < u m
zero_lt_u : ∀ (n : ℕ), 0 < u n
hu : Tendsto u atTop (𝓝 0)
A✝ : ∀ (n : ℕ), F (u n) ∈ closedBall 0 2
f : Fin N → E
fmem : f ∈ closedBall 0 2
φ : ℕ → ℕ
φ_mono : StrictMono φ
hf : Tendsto ((F ∘ u) ∘ φ) atTop (𝓝 f)
i j : Fin N
hij : i ≠ j
A : Tendsto (fun n ↦ ‖F (u (φ n)) i - F (u (φ n)) j‖) atTop (𝓝 ‖f i - f j‖)
B : Tendsto (fun n ↦ 1 - u (φ n)) atTop (𝓝 1)
⊢ (fun i j ↦ 1 ≤ ‖f i - f j‖) i j
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
f : Fin N → E
hf : ∀ (i : Fin N), ‖f i‖ ≤ 2
h'f : Pairwise fun i j ↦ 1 ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ False

Tactic:
have s_card : s.card = N := by rw [Finset.card_image_of_injective _ finj]; exact Finset.card_fin N

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
F : ℝ → Fin N → E
hF : ∀ (δ : ℝ), 0 < δ → (∀ (i : Fin N), ‖F δ i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖F δ i - F δ j‖
f : Fin N → E
hf : ∀ (i : Fin N), ‖f i‖ ≤ 2
h'f : Pairwise fun i j ↦ 1 ≤ ‖f i - f j‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = N
⊢ False
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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
⊢ μ' = μ

Tactic:
have A s : μ' s = haarScalarFactor μ' μ • μ s :=
    measure_isMulInvariant_eq_smul_of_isCompact_closure _ _ isClosed_closure.isCompact

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✝³ : IsProbabilityMeasure μ
inst✝² : IsProbabilityMeasure μ'
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ'.IsHaarMeasure
this : CompactSpace G
A : ∀ (s : Set G), μ' s = μ'.haarScalarFactor μ • μ s
⊢ μ' = μ
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : Pairwise fun i j ↦ 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
⊢ False

Tactic:
have : 1 - goodδ E ≤ ‖f i - f j‖ := h' h

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ
f : Fin n → E
h✝ : ∀ (i : Fin n), ‖f i‖ ≤ 2
h' : Pairwise fun i j ↦ 1 - goodδ E ≤ ‖f i - f j‖
i j : Fin n
hij : f i = f j
h : ¬i = j
this : 1 - goodδ E ≤ ‖f i - f j‖
⊢ False
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: 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
⊢ 1 - δ ≤ 1 - δ / 4

Tactic:
linarith only [δnonneg]

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

Goal state before:
pp: case pos
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
y : G
hy : y ∈ s
h'y : m ∪ {y} ∈ A
ym : y ∈ m
this : y ∈ y • (k * k⁻¹)
⊢ y ∈ ⋃ x ∈ m, x • (k * k⁻¹)

Tactic:
exact mem_biUnion ym this

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
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : μ'.InnerRegularCompactLTTop
s : Set G
hs : μ s ≠ ∞
h's : μ' s ≠ ∞
c : ℝ≥0 := μ'.haarScalarFactor μ
B : ∀ (s : Set G), MeasurableSet s → μ s < ∞ → μ' s < ∞ → μ' s = (c • μ) s
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
⊢ μ' s = μ'.haarScalarFactor μ • μ s

Tactic:
have mu'_t : μ' t = μ' s := by
    apply le_antisymm
    · exact (measure_mono inter_subset_left).trans (measure_toMeasurable s).le
    · exact measure_mono st

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✝³ : IsFiniteMeasureOnCompacts μ'
inst✝² : μ'.IsMulLeftInvariant
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : μ'.InnerRegularCompactLTTop
s : Set G
hs : μ s ≠ ∞
h's : μ' s ≠ ∞
c : ℝ≥0 := μ'.haarScalarFactor μ
B : ∀ (s : Set G), MeasurableSet s → μ s < ∞ → μ' s < ∞ → μ' s = (c • μ) s
t : Set G := toMeasurable μ' s ∩ toMeasurable μ s
st : s ⊆ t
mu'_t : μ' t = μ' s
⊢ μ' s = μ'.haarScalarFactor μ • μ s
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✝² : μ'.IsMulLeftInvariant
inst✝¹ : μ.Regular
inst✝ : μ'.Regular
U : Set G
hU : IsOpen[inst✝⁹] U
⊢ ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), μ' K = (μ'.haarScalarFactor μ • μ) U

Tactic:
hU.measure_eq_iSup_isCompact

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✝² : μ'.IsMulLeftInvariant
inst✝¹ : μ.Regular
inst✝ : μ'.Regular
U : Set G
hU : IsOpen[inst✝⁹] U
⊢ ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), μ' K = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), (μ'.haarScalarFactor μ • μ) K
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 • μ
⊢ (c * c) • μ = c ^ 2 • μ

Tactic:
pow_two

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 • μ
⊢ (c * c) • μ = (c * c) • μ
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 • μ
⊢ (c * c) • μ = c ^ 2 • μ

Tactic:
pow_two

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 • μ
⊢ (c * c) • μ = (c * c) • μ
Module: Mathlib.Topology.MetricSpace.Holder

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
f : X → Y
C : ℝ≥0
A : Set X
⊢ Convex ℝ≥0 {r | HolderOnWith C r f A}

Tactic:
intro r hr s hs _ _ _ _ ht
  rw [smul_eq_mul, smul_eq_mul, ← mul_comm r, ← mul_comm s]
  exact hr.interpolate_const hs ht

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
x y : X
hf : HolderOnWith C r f s
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ ↑r

Tactic:
rw [← ENNReal.coe_le_coe, ← edist_nndist, ENNReal.coe_mul,
    ENNReal.coe_rpow_of_nonneg _ r.coe_nonneg]
  apply hf.edist_le_of_le hx hy
  rwa [edist_nndist, ENNReal.coe_le_coe]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.Abs

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
⊢ HasStrictFDerivAt (fun x ↦ |f x|) (-f') x

Tactic:
convert! (hasStrictDerivAt_abs_neg h₀).hasStrictFDerivAt.comp x hf using 1
  ext y
  simp

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ x ↔
    ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f univ x) =
      iteratedFDerivWithin 𝕜 2 f univ x

Tactic:
exact isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ _)

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
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
N : ℕ∞ω
n : ℕ
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun y ↦ (f y) (g y)) x‖ ≤
    ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Tactic:
by
  simp only [← iteratedFDerivWithin_univ]
  exact norm_iteratedFDerivWithin_clm_apply hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ
    (Set.mem_univ x) hn

Goal state after:
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
inst✝ : CompleteSpace E
f : E → F
s : Set E
x : E
h'f : ContDiffWithinAt 𝕜 2 f s x
hf : (fderivWithin 𝕜 f s x).IsInvertible
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ ∃ N,
    ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y)) s x ∧
      ContDiffWithinAt 𝕜 1 (fun y ↦ ↑(N y).symm) s x ∧
        (∀ᶠ (y : E) in 𝓝[s] x, ↑(N y) = fderivWithin 𝕜 f s y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun y ↦ ↑(N y).symm) s x) v =
              -↑(N x).symm ∘SL (fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v ∘SL ↑(N x).symm

Tactic:
by
  classical
  rcases hf with ⟨M, hM⟩
  let U := {y | ∃ (N : E ≃L[𝕜] F), N = fderivWithin 𝕜 f s y}
  have hU : U ∈ 𝓝[s] x := by
    have I : range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F) ∈ 𝓝 (fderivWithin 𝕜 f s x) := by
      rw [← hM]
      exact M.nhds
    have : ContinuousWithinAt (fderivWithin 𝕜 f s) s x :=
      (h'f.fderivWithin_right (m := 1) hs le_rfl hx).continuousWithinAt
    exact this I
  let N : E → (E ≃L[𝕜] F) := fun x ↦ if h : x ∈ U then h.choose else M
  have eN : (fun y ↦ (N y : E →L[𝕜] F)) =ᶠ[𝓝[s] x] fun y ↦ fderivWithin 𝕜 f s y := by
    filter_upwards [hU] with y hy
    simpa only [hy, ↓reduceDIte, N] using Exists.choose_spec hy
  have e'N : N x = fderivWithin 𝕜 f s x := by apply mem_of_mem_nhdsWithin hx eN
  have hN : ContDiffWithinAt 𝕜 1 (fun y ↦ (N y : E →L[𝕜] F)) s x := by
    have : ContDiffWithinAt 𝕜 1 (fun y ↦ fderivWithin 𝕜 f s y) s x :=
      h'f.fderivWithin_right (m := 1) hs le_rfl hx
    apply this.congr_of_eventuallyEq eN e'N
  have hN' : ContDiffWithinAt 𝕜 1 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x := by
    have : ContDiffWithinAt 𝕜 1 (ContinuousLinearMap.inverse ∘ (fun y ↦ (N y : E →L[𝕜] F))) s x :=
      (contDiffAt_map_inverse (N x)).comp_contDiffWithinAt x hN
    convert! this with y
    simp only [Function.comp_apply, ContinuousLinearMap.inverse_equiv]
  refine ⟨N, hN, hN', eN, fun v ↦ ?_⟩
  have A' y : ContinuousLinearMap.compL 𝕜 F E F (N y : E →L[𝕜] F) ((N y).symm : F →L[𝕜] E)
      = ContinuousLinearMap.id 𝕜 F := by ext; simp
  have : fderivWithin 𝕜 (fun y ↦ ContinuousLinearMap.compL 𝕜 F E F (N y : E →L[𝕜] F)
      ((N y).symm : F →L[𝕜] E)) s x v = 0 := by
    simp [A', fderivWithin_const_apply]
  have I : (N x : E →L[𝕜] F) ∘L (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v) =
      - (fderivWithin 𝕜 (fun y ↦ (N y : E →L[𝕜] F)) s x v) ∘L ((N x).symm : F →L[𝕜] E) := by
    rw [ContinuousLinearMap.fderivWithin_of_bilinear _ (hN.differentiableWithinAt one_ne_zero)
      (hN'.differentiableWithinAt one_ne_zero) (hs x hx)] at this
    simpa [eq_neg_iff_add_eq_zero] using this
  have B (M : F →L[𝕜] E) : M = ((N x).symm : F →L[𝕜] E) ∘L ((N x) ∘L M) := by
    ext; simp
  rw [B (fderivWithin 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) s x v), I]
  simp only [ContinuousLinearMap.comp_neg, eN.fderivWithin_eq e'N]

Goal state after: