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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
ε : ℝ
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hε : 0 < ε
⊢ ∃ g, ContDiff ℝ ∞ g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f a) ≤ δ

Tactic:
borelize E

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E → F
ε : ℝ
hf :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hε : 0 < ε
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ ∃ g, ContDiff ℝ ∞ g ∧ ∀ (a : E) (δ : ℝ), (∀ x ∈ ball a ε, dist (f x) (f a) ≤ δ) → dist (g a) (f 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
⊢ (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ν s = (μ'.haarScalarFactor μ * μ.haarScalarFactor ν) • ν s

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i ↦ ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = ↑i
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = ↑i
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
jxy : jx < jy
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
      {p.color ↑j}
⊢ sInf
      (univ \
        ⋃ j,
          ⋃ (_ :
            (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩
                closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
            {p.color ↑j}) =
    sInf (univ \ A)

Tactic:
]

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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : C(E, F)
⊢ ∀ (i : Set E × ℝ),
    IsCompact i.1 ∧ 0 < i.2 →
      ∃ y ∈ {f | ContDiff ℝ ∞ ⇑f}, y ∈ {y | (y, f) ∈ {fg | ∀ x ∈ i.1, (fg.1 x, fg.2 x) ∈ {p | dist p.1 p.2 < i.2}}}

Tactic:
]

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : C(E, F)
⊢ ∀ (i : Set E × ℝ),
    IsCompact i.1 ∧ 0 < i.2 →
      ∃ y ∈ {f | ContDiff ℝ ∞ ⇑f}, y ∈ {y | (y, f) ∈ {fg | ∀ x ∈ i.1, (fg.1 x, fg.2 x) ∈ {p | dist p.1 p.2 < i.2}}}
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i ↦ ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = ↑i
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = ↑i
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
jxy : jx < jy
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
      {p.color ↑j}
color_j : p.color jy = sInf (univ \ A)
⊢ sInf (univ \ A) ∈ univ \ A

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i ↦ ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = ↑i
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = ↑i
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
jxy : jx < jy
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
      {p.color ↑j}
color_j : p.color jy = sInf (univ \ A)
⊢ sInf (univ \ A) ∈ univ \ A
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)
⊢ (fun i j ↦ 1 ≤ ‖f i - f j‖) i j

Tactic:
]

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.Analysis.Calculus.BumpFunction.SmoothApprox

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
this : UniformContinuousOn (⇑f) (cthickening 1 K)
δ : ℝ
hδ : δ > 0
hfδ : ∀ x ∈ cthickening 1 K, ∀ y ∈ cthickening 1 K, dist x y < δ → dist (f x) (f y) < ε / 2
g : E → F
hgc : ContDiff ℝ ∞ g
hg : ∀ (a : E) (δ_1 : ℝ), (∀ x ∈ ball a (min 1 δ), dist (f x) (f a) ≤ δ_1) → dist (g a) (f a) ≤ δ_1
x : E
hx : x ∈ K
y : E
hy : dist y x < 1 ∧ dist y x < δ
⊢ dist (f y) (f x) ≤ ε / 2

Tactic:
]

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : C(E, F)
K : Set E
ε : ℝ
hK : IsCompact K
hε : 0 < ε
this : UniformContinuousOn (⇑f) (cthickening 1 K)
δ : ℝ
hδ : δ > 0
hfδ : ∀ x ∈ cthickening 1 K, ∀ y ∈ cthickening 1 K, dist x y < δ → dist (f x) (f y) < ε / 2
g : E → F
hgc : ContDiff ℝ ∞ g
hg : ∀ (a : E) (δ_1 : ℝ), (∀ x ∈ ball a (min 1 δ), dist (f x) (f a) ≤ δ_1) → dist (g a) (f a) ≤ δ_1
x : E
hx : x ∈ K
y : E
hy : dist y x < 1 ∧ dist y x < δ
⊢ dist (f y) (f x) ≤ ε / 2
Module: Mathlib.Analysis.Normed.Operator.Conformal

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : NormedSpace R G
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ cg • cf • lig.toContinuousLinearMap ∘SL lif.toContinuousLinearMap = cg • cf • (lig.comp lif).toContinuousLinearMap

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
G : Type u_4
inst✝⁶ : NormedField R
inst✝⁵ : SeminormedAddCommGroup M
inst✝⁴ : SeminormedAddCommGroup N
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : NormedSpace R G
cf : R
hcf : cf ≠ 0
lif : M →ₗᵢ[R] N
cg : R
hcg : cg ≠ 0
lig : N →ₗᵢ[R] G
⊢ cg • cf • lig.toContinuousLinearMap ∘SL lif.toContinuousLinearMap = cg • cf • (lig.comp lif).toContinuousLinearMap
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
⊢ Finset.univ.card = N

Tactic:
]

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
⊢ Finset.univ.card = N
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✝² : CompactSpace G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : IsFiniteMeasureOnCompacts μ
⊢ (μ.haarScalarFactor haar • haar).InnerRegular

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : CompactSpace G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : IsFiniteMeasureOnCompacts μ
⊢ (μ.haarScalarFactor haar • haar).InnerRegular
Module: Mathlib.Analysis.Calculus.Conformal.NormedSpace

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝³ : NormedAddCommGroup X
inst✝² : NormedAddCommGroup Y
inst✝¹ : NormedSpace ℝ X
inst✝ : NormedSpace ℝ Y
f : X → Y
x : X
f' : X →L[ℝ] Y
hf : HasFDerivAt f f' x
hf' : IsConformalMap f'
⊢ IsConformalMap f'

Tactic:
]

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝³ : NormedAddCommGroup X
inst✝² : NormedAddCommGroup Y
inst✝¹ : NormedSpace ℝ X
inst✝ : NormedSpace ℝ Y
f : X → Y
x : X
f' : X →L[ℝ] Y
hf : HasFDerivAt f f' x
hf' : IsConformalMap f'
⊢ IsConformalMap f'
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✝² : CompactSpace G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : IsFiniteMeasureOnCompacts μ
⊢ (μ.haarScalarFactor haar • haar).Regular

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
inst✝² : CompactSpace G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : IsFiniteMeasureOnCompacts μ
⊢ (μ.haarScalarFactor haar • haar).Regular
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
H : NoncompactSpace G
⊢ False

Tactic:
]

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
H : NoncompactSpace G
⊢ False
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
s_card : s.card = N
hs : ∀ c ∈ s, ‖c‖ ≤ 2
i j : Fin N
hij : ¬f j = f j
h : i = j
⊢ False

Tactic:
]

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
hs : ∀ c ∈ s, ‖c‖ ≤ 2
i j : Fin N
hij : ¬f j = f j
h : i = j
⊢ False
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
s_card : s.card = N
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : multiplicity E + 1 ≤ multiplicity E
⊢ False

Tactic:
]

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
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this : multiplicity E + 1 ≤ multiplicity E
⊢ False
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ 1 < 1 + ⋯.choose / 4

Tactic:
linarith [(exists_goodδ E).choose_spec.1]

Goal state after:
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‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ Finset.univ.card = n

Tactic:
]

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‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
⊢ Finset.univ.card = n
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‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
hs : ∀ c ∈ s, ‖c‖ ≤ 2
i j : Fin n
hij : ¬f j = f j
h : i = j
⊢ False

Tactic:
]

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‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
hs : ∀ c ∈ s, ‖c‖ ≤ 2
i j : Fin n
hij : ¬f j = f j
h : i = j
⊢ False
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‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - goodδ E ≤ ‖c - d‖
this : n ≤ multiplicity E
⊢ n ≤ multiplicity E

Tactic:
]

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‖
finj : Function.Injective f
s : Finset E := Finset.image f Finset.univ
s_card : s.card = n
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h's : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - goodδ E ≤ ‖c - d‖
this : n ≤ multiplicity E
⊢ n ≤ multiplicity E
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 < τ
⊢ (1 - δ / 4) * (1 + δ / 4) = 1 - δ ^ 2 / 16

Tactic:
by ring

Goal state after:
Module: Mathlib.Analysis.Calculus.Conformal.InnerProduct

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E → F
x : E
⊢ (∃ c, 0 < c ∧ ∀ (u v : E), ⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫ = c * ⟪u, v⟫) ↔
    ∃ c, 0 < c ∧ ∀ (u v : E), ⟪(fderiv ℝ f x) u, (fderiv ℝ f x) v⟫ = c * ⟪u, v⟫

Tactic:
]

Goal state after:
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
⊢ (1 - δ / 4) * τ ≤ 1

Tactic:
]

Goal state after:
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
⊢ (1 - δ / 4) * τ ≤ 1
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 ≤ τ⁻¹
k : Fin N.succ
⊢ a.r (last N) ≤ τ * a.r k

Tactic:
]

Goal state after:
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 ≤ τ⁻¹
k : Fin N.succ
⊢ a.r (last N) ≤ τ * a.r k
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
y : G
hy : y ∈ s
h'y : m ∪ {y} ∉ A
x : G
xm : x ∈ m
z : G
zy : z ∈ y • k
zx : z ∈ x • k
⊢ x * (x⁻¹ * z * (y⁻¹ * z)⁻¹) ∈ x • (k * k⁻¹)

Tactic:
]

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
y : G
hy : y ∈ s
h'y : m ∪ {y} ∉ A
x : G
xm : x ∈ m
z : G
zy : z ∈ y • k
zx : z ∈ x • k
⊢ x * (x⁻¹ * z * (y⁻¹ * z)⁻¹) ∈ x • (k * k⁻¹)