mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : AddGroup G
inst✝ : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t✝ : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
⊢ ‖(L (f t)) (g (x - t))‖ ≤ 0

Tactic:
have : x - t ∉ support g := by
      refine mt (fun hxt => hu ?_) ht
      refine ⟨_, Set.neg_mem_neg.mpr (subset_closure hxt), _, hx, ?_⟩
      simp only [neg_sub, sub_add_cancel]

Goal state after:
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✝¹ : AddGroup G
inst✝ : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t✝ : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
this : x - t ∉ support g
⊢ ‖(L (f t)) (g (x - t))‖ ≤ 0
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
this : ‖id x‖ ^ 2 ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x

Tactic:
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✝⁴ : AddCommGroup G
inst✝³ : MeasurableNeg G
inst✝² : μ.IsAddLeftInvariant
inst✝¹ : MeasurableAdd₂ G
inst✝ : SFinite μ
x₀ : G
s : Set G
hbg : BddAbove ((fun i ↦ ‖g i‖) '' (fun t ↦ x₀ - t) ⁻¹' s)
hs : MeasurableSet s
h2s : (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ s
hf : IntegrableOn f s μ
hmg : AEStronglyMeasurable g μ
⊢ ConvolutionExistsAt f g x₀ L μ

Tactic:
by
  refine BddAbove.convolutionExistsAt' L ?_ hs h2s hf ?_
  · simp_rw [← sub_eq_neg_add, hbg]
  · have : AEStronglyMeasurable g (map (fun t : G => x₀ - t) μ) :=
      hmg.mono_ac (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous
    apply this.mono_measure
    exact map_mono restrict_le_self (measurable_const.sub measurable_id')

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

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

Tactic:
have h1 : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (fun t => L (f t) (g (x - t))) μ :=
    Eventually.of_forall
      (hf.aestronglyMeasurable.convolution_integrand_snd L hg.continuous.aestronglyMeasurable)

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

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A✝ :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
A : IsCompact ({q₀.1} ×ˢ k)
t : Set (P × G)
kt : {q₀.1} ×ˢ k ⊆ t
t_open : IsOpen[instTopologicalSpaceProd] t
ht : Bornology.IsBounded (g' '' t)
⊢ ∃ ε, 0 < ε ∧ thickening ε ({q₀.1} ×ˢ k) ⊆ t ∧ ball q₀.1 ε ⊆ s

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε : ℝ, 0 < ε ∧ thickening ε (({q₀.fst} : Set P) ×ˢ k) ⊆ t :=
        A.exists_thickening_subset_open t_open kt

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A✝ :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
A : IsCompact ({q₀.1} ×ˢ k)
t : Set (P × G)
kt : {q₀.1} ×ˢ k ⊆ t
t_open : IsOpen[instTopologicalSpaceProd] t
ht : Bornology.IsBounded (g' '' t)
ε : ℝ
εpos : 0 < ε
hε : thickening ε ({q₀.1} ×ˢ k) ⊆ t
⊢ ∃ ε, 0 < ε ∧ thickening ε ({q₀.1} ×ˢ k) ⊆ t ∧ ball q₀.1 ε ⊆ s
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s
hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun n ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ HasDerivAt g (g' x) x

Tactic:
by
  refine hasDerivAt_of_tendstoLocallyUniformlyOn hs hf' ?_ hfg hx
  filter_upwards [hf] with n h z hz using ((h z hz).differentiableAt (hs.mem_nhds hz)).hasDerivAt

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
K : PositiveCompacts G := Classical.arbitrary (PositiveCompacts G)
n : ℕ
hn : 0 < haar (interior ↑K ∩ ⇑f ⁻¹' ball 1 ↑n)
⊢ ∃ s ∈ 𝓝 x, Bornology.IsBounded (⇑f '' s)

Tactic:
← mul_one x,

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)
n : ℕ
hn : 0 < haar (interior ↑K ∩ ⇑f ⁻¹' ball 1 ↑n)
⊢ ∃ s ∈ 𝓝 (x * 1), Bornology.IsBounded (⇑f '' s)
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case e_f
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
⊢ f x = f x * (D x)⁻¹ * D x

Tactic:
rw [mul_assoc, inv_mul_cancel₀ (D_pos x).ne', mul_one]

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 → ℝ := ⋯
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
⊢ HasCompactSupport (uncurry fun x y ↦ f (y * x) * (D (y * x))⁻¹ * g x)

Tactic:
· let K := tsupport f
        have K_comp : IsCompact K := h'f
        let L := tsupport g
        have L_comp : IsCompact L := h'g
        let M := (fun (p : G × G) ↦ p.1 * p.2⁻¹) '' (K ×ˢ L)
        have M_comp : IsCompact M :=
          (K_comp.prod L_comp).image (continuous_fst.mul continuous_snd.inv)
        have M'_comp : IsCompact (closure M) := M_comp.closure
        have : ∀ (p : G × G), p ∉ L ×ˢ closure M →
            f (p.2 * p.1) * (D (p.2 * p.1))⁻¹ * g p.1 = 0 := by
          rintro ⟨x, y⟩ hxy
          by_cases H : x ∈ L; swap
          · simp [image_eq_zero_of_notMem_tsupport H]
          have : f (y * x) = 0 := by
            apply image_eq_zero_of_notMem_tsupport
            contrapose hxy
            simp only [mem_prod, H, true_and]
            apply subset_closure
            simp only [M, mem_image, mem_prod, Prod.exists]
            exact ⟨y * x, x, ⟨hxy, H⟩, by group⟩
          simp [this]
        apply HasCompactSupport.intro' (L_comp.prod M'_comp) ?_ this
        exact (isClosed_tsupport g).prod isClosed_closure

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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ
⊢ IsFiniteMeasureOnCompacts μ'

Tactic:
by infer_instance

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✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
u : ℕ → ℝ
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → ℝ → ℝ := fun n x ↦ ↑((thickenedIndicator ⋯ {1}) x)
vf_cont : ∀ (n : ℕ), Continuous[inst✝⁷, _] (v n ∘ f)
I :
  ∀ (ν : Measure G),
    IsFiniteMeasureOnCompacts ν →
      Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂ν))
M : ∀ (n : ℕ), ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ
I1 :
  Tendsto (fun n ↦ ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop
    (𝓝 (∫ (x : G), {1}.indicator (fun x ↦ 1) (f x) ∂μ'))
⊢ IsFiniteMeasureOnCompacts (μ'.haarScalarFactor μ • μ)

Tactic:
by infer_instance

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))
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))
a : Fin (N + 1)
ha : a < last N
I : ↑a < N
⊢ p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑(last N)))) ∧
    p.r (p.index (G ↑(last N))) ≤ p.τ * p.r (p.index (G ↑a))

Tactic:
have : G a < G (Fin.last N) := by simp [G, I.ne, (hg a I).1]

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))
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))
a : Fin (N + 1)
ha : a < last N
I : ↑a < N
this : G ↑a < G ↑(last N)
⊢ p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑(last N)))) ∧
    p.r (p.index (G ↑(last N))) ≤ p.τ * p.r (p.index (G ↑a))
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)
ν : Measure G := haar
A : μ' s = μ'.haarScalarFactor ν • ν s
B : μ s = μ.haarScalarFactor ν • ν s
⊢ μ' s = μ'.haarScalarFactor μ • μ s

Tactic:
A,

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
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁸] s)
ν : Measure G := haar
A : μ' s = μ'.haarScalarFactor ν • ν s
B : μ s = μ.haarScalarFactor ν • ν s
⊢ μ'.haarScalarFactor ν • ν s = μ'.haarScalarFactor μ • μ s
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
J : 1 - δ ≤ 1 - δ / 4
K : 1 - δ / 4 ≤ τ⁻¹
hτ' : ∀ (k : Fin N.succ), τ⁻¹ ≤ a.r k
⊢ τ⁻¹ ≤ ‖a.c i - a.c j‖

Tactic:
rcases ah inej with (H | H)

Goal state after:
case inl
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 i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i
⊢ τ⁻¹ ≤ ‖a.c i - a.c j‖

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‖
Module: Mathlib.Analysis.Calculus.ContDiff.RestrictScalars

Goal state before:
pp: case h.hmn
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
x : E
f : E → F
n✝ : ℕ
s : Set E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn :
  ContDiffWithinAt 𝕜' (↑n) f s x →
    restrictScalars 𝕜 ∘ iteratedFDerivWithin 𝕜' n f s =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f s
h : ContDiffWithinAt 𝕜' (↑(n + 1)) f s x
t₀ : ContDiffWithinAt 𝕜' (↑n) f s x
t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1)) f s y
a : E
h₁a : restrictScalars 𝕜 ∘ iteratedFDerivWithin 𝕜' n f s =ᶠ[𝓝[s] a] iteratedFDerivWithin 𝕜 n f s
h₃a : ContDiffWithinAt 𝕜' (↑(n + 1)) f s a
h₄a : a ∈ s
m : Fin (n + 1) → E
⊢ ↑n < ↑(n + 1)

Tactic:
rw [Nat.cast_lt]
        simp

Goal state after:
Module: Mathlib.Analysis.Convex.NNReal

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module ℝ M
s : Set M
H : Convex ℝ≥0 s
x✝ : M
hx : x✝ ∈ s
y✝ : M
hy : y✝ ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ⟨a, ha⟩ + ⟨b, hb⟩ = 1

Tactic:
ext; simpa

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ ↑Cg * ↑(Cf ^ ↑rg) * edist x y ^ ↑(rf * rg)

Tactic:
NNReal.coe_mul,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ ↑Cg * ↑(Cf ^ ↑rg) * edist x y ^ (↑rf * ↑rg)
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
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
Bu_eq : (fun y ↦ (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y ↦ (B (f y)) (g y)) ∘ ⇑isoD
y : Eu
x : Fu
⊢ ‖B‖ * ‖isoE y‖ * ‖isoF x‖ = ‖B‖ * ‖y‖ * ‖x‖

Tactic:
by simp only [LinearIsometryEquiv.norm_map]

Goal state after: