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

Goal state before:
pp: case refine_1
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist ((↑‖n.2 - x‖)⁻¹ • (g n.2 - g x)) ((↑‖n.2 - x‖)⁻¹ • (f n.1 n.2 - f n.1 x)) < ε
⊢ Tendsto (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) (l.curry (𝓝 x)) (𝓝 0)

Tactic:
rw [Metric.tendsto_nhds]

Goal state after:
case refine_1
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist ((↑‖n.2 - x‖)⁻¹ • (g n.2 - g x)) ((↑‖n.2 - x‖)⁻¹ • (f n.1 n.2 - f n.1 x)) < ε
⊢ ∀ ε > 0,
    ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x), dist ((↑‖x_1.2 - x‖)⁻¹ • (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x))) 0 < ε
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case refine_2
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this : 𝓝 0 = 𝓝 (0 + 0 + 0)
⊢ Tendsto (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) (l.curry (𝓝 x)) (𝓝 0)

Tactic:
rw [Metric.tendsto_nhds]

Goal state after:
case refine_2
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this : 𝓝 0 = 𝓝 (0 + 0 + 0)
⊢ ∀ ε > 0,
    ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
      dist ((↑‖x_1.2 - x‖)⁻¹ • (f x_1.1 x_1.2 - f x_1.1 x - ((f' x_1.1 x) x_1.2 - (f' x_1.1 x) x))) 0 < ε
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this : 𝓝 0 = 𝓝 (0 + 0 + 0)
h1 : Tendsto (fun n ↦ g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0)
h2 : Tendsto (fun n ↦ g' x - f' n x) l (𝓝 0)
n : ι × E
hx : ¬x = n.2
⊢ n.2 - x ≠ 0

Tactic:
intro hx'

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this : 𝓝 0 = 𝓝 (0 + 0 + 0)
h1 : Tendsto (fun n ↦ g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0)
h2 : Tendsto (fun n ↦ g' x - f' n x) l (𝓝 0)
n : ι × E
hx : ¬x = n.2
hx' : n.2 - x = 0
⊢ False
Module: Mathlib.Data.Set.Pointwise.Support

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Zero γ
c : α
hc : c ≠ 0
f : β → γ
⊢ (support fun x ↦ f (c⁻¹ • x)) = c • support f

Tactic:
by
  ext x
  simp only [mem_smul_set_iff_inv_smul_mem₀ hc, mem_support]

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

Goal state before:
pp: F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := (Homeomorph.smul ⋯.unit).toMeasurableEquiv
⊢ ENNReal.ofReal |(S ^ finrank ℝ E)⁻¹| ≠ 0

Tactic:
simpa only [Ne, ENNReal.ofReal_eq_zero, not_le, abs_pos] using inv_ne_zero (pow_ne_zero _ hS)

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

Goal state before:
pp: case h'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
K : Set G := tsupport f
⊢ HasCompactSupport (uncurry fun x y ↦ f x * (D x)⁻¹ * g (y⁻¹ * x))

Tactic:
have K_comp : IsCompact K := h'f

Goal state after:
case h'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
K : Set G := tsupport f
K_comp : IsCompact K
⊢ HasCompactSupport (uncurry fun x y ↦ f x * (D x)⁻¹ * g (y⁻¹ * x))
Module: Mathlib.Analysis.Calculus.BumpFunction.Normed

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
x : E
hx : x ∉ closedBall c f.rOut
⊢ ↑f x = 0

Tactic:
apply f.zero_of_le_dist (le_of_lt _)

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : HasContDiffBump E
inst✝³ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : IsLocallyFiniteMeasure μ
x : E
hx : x ∉ closedBall c f.rOut
⊢ f.rOut < dist x c
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
⊢ Continuous[instTopologicalSpaceProd, _] fun a ↦ f (a.2 * a.1) * (D (a.2 * a.1))⁻¹

Tactic:
exact (hf.comp (continuous_snd.mul continuous_fst)).mul
          ((D_cont.comp (continuous_snd.mul continuous_fst)).inv₀ (fun x ↦ (D_pos _).ne'))

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

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

Tactic:
have K_comp : IsCompact K := h'f

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
K : Set G := tsupport f
K_comp : IsCompact K
⊢ HasCompactSupport (uncurry fun x y ↦ f (y * x) * (D (y * x))⁻¹ * g x)
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case ha
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 := ⋯
this✝ : BorelSpace E
R : ℝ
hR : 1 < R
⊢ 0 < R - 1

pp: case hb
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 := ⋯
this✝ : BorelSpace E
R : ℝ
hR : 1 < R
⊢ 0 < R + 1

Tactic:
<;>

Goal state after:
case ha
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 := ⋯
this✝ : BorelSpace E
R : ℝ
hR : 1 < R
⊢ 0 < R - 1

case hb
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 := ⋯
this✝ : BorelSpace E
R : ℝ
hR : 1 < R
⊢ 0 < R + 1
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case ha
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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right✝ : (R, x).2 ∈ univ
⊢ 0 < R - 1

pp: case hb
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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right✝ : (R, x).2 ∈ univ
⊢ 0 < R + 1

Tactic:
<;>

Goal state after:
case ha
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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right✝ : (R, x).2 ∈ univ
⊢ 0 < R - 1

case hb
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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right✝ : (R, x).2 ∈ univ
⊢ 0 < R + 1
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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right✝ : (R, x).2 ∈ univ
A : 0 < (R - 1) / (R + 1)
⊢ R - 1 < R + 1

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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right✝ : (R, x).2 ∈ univ
A : 0 < (R - 1) / (R + 1)
⊢ 0 < R + 1

Tactic:
<;>

Goal state after:
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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right✝ : (R, x).2 ∈ univ
A : 0 < (R - 1) / (R + 1)
⊢ R - 1 < R + 1

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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
x : E
hR : 1 < R
right✝ : (R, x).2 ∈ univ
A : 0 < (R - 1) / (R + 1)
⊢ 0 < R + 1
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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
⊢ R - 1 < R + 1

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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
⊢ 0 < R + 1

Tactic:
<;>

Goal state after:
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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
⊢ R - 1 < R + 1

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 := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
R : ℝ
hR : 1 < R
A : 0 < (R + 1) / 2
⊢ 0 < R + 1
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)

Tactic:
<;>

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j) ∧
    (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i) ∧
    (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: case inl.left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j)

pp: case inl.right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)

pp: case inr.left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i)

pp: case inr.right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)

Tactic:
<;>

Goal state after:
case inl.left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c j)

case inl.right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r i ≤ dist (a.c i) (a.c j)
H₂ : a.r j ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * (τ * a.r i)

case inr.left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r j ≤ (a.r (last N))⁻¹ * dist (a.c j) (a.c i)

case inr.right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i j : Fin N.succ
hij : i ≠ j
H₁ : a.r j ≤ dist (a.c j) (a.c i)
H₂ : a.r i ≤ τ * a.r j
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * (τ * a.r j)
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: case left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N))

pp: case right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)

Tactic:
<;>

Goal state after:
case left
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r i ≤ (a.r (last N))⁻¹ * dist (a.c i) (a.c (last N))

case right
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
i : Fin (N + 1)
hi : i < last N
H₁ : a.r i ≤ dist (a.c i) (a.c (last N))
H₂ : a.r (last N) ≤ τ * a.r i
⊢ (a.r (last N))⁻¹ * a.r (last N) ≤ (a.r (last N))⁻¹ * (τ * a.r i)