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

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
key : ∀ p ∈ (B ∩ s) ×ˢ (B ∩ s), ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
u v : E
uv_in : (u, v) ∈ closure[instTopologicalSpaceProd] ((B ∩ s) ×ˢ (B ∩ s))
f_cont' : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt (f - ⇑f') s y
this : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s
u_in : u ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
v_in : v ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun y ↦ ε * ‖y.2 - y.1‖) (𝓝 u ×ˢ 𝓝 v) (𝓝 (ε * ‖v - u‖))

Tactic:
exact
      tendsto_const_nhds.mul
        (Tendsto.comp continuous_norm.continuousAt <| tendsto_snd.sub tendsto_fst)

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: 𝕂 : Type v
inst✝² : RCLike 𝕂
𝔸 : Type u
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
| ∀ (k : ℕ), a ≠ ↑k

Tactic:
ext

Goal state after:
𝕂 : Type v
inst✝² : RCLike 𝕂
𝔸 : Type u
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
k✝ : ℕ
| a ≠ ↑k✝
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this✝ : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun y ↦ ↑(-y) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x
⊢ HasDerivAt (fun y ↦ -↑(-y) ^ (r + 1) * cexp (↑π * I * r)) ((r + 1) * ↑(-x) ^ r * cexp (↑π * I * r)) x

Tactic:
convert! this.neg.mul_const _ using 1; ring

Goal state after:
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case zero
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : p (n + 0) = 0
⊢ p.iteratedFDerivSeries 0 n = 0

Tactic:
ext

Goal state after:
case zero
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : p (n + 0) = 0
x✝¹ : Fin n → E
x✝ : Fin 0 → E
⊢ ((p.iteratedFDerivSeries 0 n) x✝¹) x✝ = (0 x✝¹) x✝
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
ih : ∀ {n : ℕ}, p (n + k) = 0 → p.iteratedFDerivSeries k n = 0
n : ℕ
h : p (n + (k + 1)) = 0
⊢ p.iteratedFDerivSeries (k + 1) n = 0

Tactic:
ext

Goal state after:
case succ
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
ih : ∀ {n : ℕ}, p (n + k) = 0 → p.iteratedFDerivSeries k n = 0
n : ℕ
h : p (n + (k + 1)) = 0
x✝¹ : Fin n → E
x✝ : Fin (k + 1) → E
⊢ ((p.iteratedFDerivSeries (k + 1) n) x✝¹) x✝ = (0 x✝¹) x✝
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : BinomialRing R
r s : R
k : ℕ
h : Commute r s
⊢ choose (r + s) k = ∑ ij ∈ antidiagonal k, choose r ij.1 * choose s ij.2

Tactic:
by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero k),
    ← descPochhammer_eq_factorial_smul_choose, smul_sum, descPochhammer_smeval_add _ h]
  refine sum_congr rfl ?_
  intro x hx
  rw [← Nat.choose_mul_factorial_mul_factorial (HasAntidiagonal.antidiagonal.fst_le hx),
    tsub_eq_of_eq_add_rev (List.Nat.mem_antidiagonal.mp hx).symm, mul_assoc, nsmul_eq_mul,
    Nat.cast_mul, Nat.cast_mul, ← mul_assoc _ (x.1.factorial : R), mul_assoc _ (x.2.factorial : R),
    ← mul_assoc (x.2.factorial : R), Nat.cast_commute x.2.factorial,
    mul_assoc _ (x.2.factorial : R), ← nsmul_eq_mul x.2.factorial]
  simp [mul_assoc, descPochhammer_eq_factorial_smul_choose]

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a b : ℂ
⊢ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ a * ↑n + b) =
    (b - a) • FormalMultilinearSeries.ofScalars ℂ 1 + a • FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑n + 1

Tactic:
ext

Goal state after:
case e'_10
a b : ℂ
n✝ : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℂ (fun n ↦ a * ↑n + b) n✝) fun x ↦ 1) =
    (((b - a) • FormalMultilinearSeries.ofScalars ℂ 1 + a • FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑n + 1) n✝)
      fun x ↦ 1
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
⊢ binomialSeries ℝ a =
    Complex.reCLM.compFormalMultilinearSeries ((binomialSeries ℂ a).compContinuousLinearMap Complex.ofRealCLM)

Tactic:
ext

Goal state after:
case e'_10
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
n✝ : ℕ
⊢ ((binomialSeries ℝ a n✝) fun x ↦ 1) =
    (Complex.reCLM.compFormalMultilinearSeries ((binomialSeries ℂ a).compContinuousLinearMap Complex.ofRealCLM) n✝)
      fun x ↦ 1
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a b : ℝ
⊢ (FormalMultilinearSeries.ofScalars ℝ fun x ↦ a * ↑x + b) =
    (b - a) • FormalMultilinearSeries.ofScalars ℝ 1 + a • FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1

Tactic:
ext

Goal state after:
case e'_10
a b : ℝ
n✝ : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun x ↦ a * ↑x + b) n✝) fun x ↦ 1) =
    (((b - a) • FormalMultilinearSeries.ofScalars ℝ 1 + a • FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1) n✝)
      fun x ↦ 1
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

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
f : E → F
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
⊢ ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x) = iteratedFDerivWithin 𝕜 n f s x

Tactic:
ext

Goal state after:
𝕜 : 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
f : E → F
s : Set E
x : E
h : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
x✝ : Fin n → E
⊢ (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x)) x✝ = (iteratedFDerivWithin 𝕜 n f s x) x✝
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
⊢ ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x) = iteratedFDerivWithin 𝕜 n f s x

Tactic:
ext

Goal state after:
𝕜 : 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
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
x✝ : Fin n → E
⊢ (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x)) x✝ = (iteratedFDerivWithin 𝕜 n f s x) x✝
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ dist x z + dist y z < ↑r + ↑r

Tactic:
gcongr <;> simpa

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
hK1 hK2 : 0 < 1
hA : AntilipschitzWith 1 ⇑(Equiv.refl X)
hL : LipschitzWith 1 ⇑(Equiv.refl X)
⊢ mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D = D

Tactic:
ext

Goal state after:
case carrier
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
hK1 hK2 : 0 < 1
hA : AntilipschitzWith 1 ⇑(Equiv.refl X)
hL : LipschitzWith 1 ⇑(Equiv.refl X)
x✝ : X
⊢ x✝ ∈ (mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).carrier ↔ x✝ ∈ D.carrier

case packingRadius
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
hK1 hK2 : 0 < 1
hA : AntilipschitzWith 1 ⇑(Equiv.refl X)
hL : LipschitzWith 1 ⇑(Equiv.refl X)
⊢ ↑(mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).packingRadius = ↑D.packingRadius

case coveringRadius
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
hK1 hK2 : 0 < 1
hA : AntilipschitzWith 1 ⇑(Equiv.refl X)
hL : LipschitzWith 1 ⇑(Equiv.refl X)
⊢ ↑(mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D).coveringRadius = ↑D.coveringRadius
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith K₁f ⇑f
hf_lip : LipschitzWith K₂f ⇑f
hg_anti : AntilipschitzWith K₁g ⇑g
hg_lip : LipschitzWith K₂g ⇑g
⊢ mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D) =
    mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D

Tactic:
ext

Goal state after:
case carrier
X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith K₁f ⇑f
hf_lip : LipschitzWith K₂f ⇑f
hg_anti : AntilipschitzWith K₁g ⇑g
hg_lip : LipschitzWith K₂g ⇑g
x✝ : Z
⊢ x✝ ∈
      (mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip
          (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D)).carrier ↔
    x✝ ∈ (mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D).carrier

case packingRadius
X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith K₁f ⇑f
hf_lip : LipschitzWith K₂f ⇑f
hg_anti : AntilipschitzWith K₁g ⇑g
hg_lip : LipschitzWith K₂g ⇑g
⊢ ↑(mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip
          (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D)).packingRadius =
    ↑(mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D).packingRadius

case coveringRadius
X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith K₁f ⇑f
hf_lip : LipschitzWith K₂f ⇑f
hg_anti : AntilipschitzWith K₁g ⇑g
hg_lip : LipschitzWith K₂g ⇑g
⊢ ↑(mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip
          (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D)).coveringRadius =
    ↑(mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D).coveringRadius
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ (fun D ↦
        (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯
          ⋯)
      ((fun D ↦ (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
        D) =
    D

Tactic:
ext

Goal state after:
case carrier
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
x✝ : X
⊢ x✝ ∈
      ((fun D ↦
            (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯
              ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
            D)).carrier ↔
    x✝ ∈ D.carrier

case packingRadius
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ ↑((fun D ↦
            (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯
              ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
            D)).packingRadius =
    ↑D.packingRadius

case coveringRadius
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ ↑((fun D ↦
            (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯
              ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
            D)).coveringRadius =
    ↑D.coveringRadius
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ (fun D ↦ (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
      ((fun D ↦
          (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯
            ⋯)
        D) =
    D

Tactic:
ext

Goal state after:
case carrier
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
x✝ : Y
⊢ x✝ ∈
      ((fun D ↦ (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius
                ⋯ ⋯ ⋯)
            D)).carrier ↔
    x✝ ∈ D.carrier

case packingRadius
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ ↑((fun D ↦ (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius
                ⋯ ⋯ ⋯)
            D)).packingRadius =
    ↑D.packingRadius

case coveringRadius
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ ↑((fun D ↦ (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
          ((fun D ↦
              (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius
                ⋯ ⋯ ⋯)
            D)).coveringRadius =
    ↑D.coveringRadius
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
⊢ (mapIsometry (IsometryEquiv.refl X)) D = D

Tactic:
ext

Goal state after:
case carrier
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x✝ : X
⊢ x✝ ∈ ((mapIsometry (IsometryEquiv.refl X)) D).carrier ↔ x✝ ∈ D.carrier

case packingRadius
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
⊢ ↑((mapIsometry (IsometryEquiv.refl X)) D).packingRadius = ↑D.packingRadius

case coveringRadius
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
⊢ ↑((mapIsometry (IsometryEquiv.refl X)) D).coveringRadius = ↑D.coveringRadius
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
⊢ (mapIsometry (f.trans g)) D = (mapIsometry g) ((mapIsometry f) D)

Tactic:
ext

Goal state after:
case carrier
X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
x✝ : Z
⊢ x✝ ∈ ((mapIsometry (f.trans g)) D).carrier ↔ x✝ ∈ ((mapIsometry g) ((mapIsometry f) D)).carrier

case packingRadius
X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
⊢ ↑((mapIsometry (f.trans g)) D).packingRadius = ↑((mapIsometry g) ((mapIsometry f) D)).packingRadius

case coveringRadius
X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
⊢ ↑((mapIsometry (f.trans g)) D).coveringRadius = ↑((mapIsometry g) ((mapIsometry f) D)).coveringRadius
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ 0 < ↑n

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : 1 ≤ n
⊢ ↑n > 0

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ⊢ linearGrowthInf ⊤ = ⊤

Tactic:
← liminf_const (f := atTop (α := ℕ)) ⊤

Goal state after:
⊢ linearGrowthInf ⊤ = liminf (fun x ↦ ⊤) atTop
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthInf (u + v) ≤ linearGrowthInf u + linearGrowthSup v

Tactic:
rw [add_comm u v, add_comm (linearGrowthInf u) (linearGrowthSup v)]
  exact linearGrowthInf_add_le h'.symm h.symm

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ 0 < ↑n

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : 1 ≤ n
⊢ ↑n > 0

Tactic:
by norm_cast

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

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst✝ : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ ρ (⋃ p ∈ h.index, h.covering p) = ∑' (p : ↑h.index), ρ (h.covering ↑p)

Tactic:
measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx

Goal state after:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst✝ : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ ∑' (p : ↑h.index), ρ (h.covering ↑p) = ∑' (p : ↑h.index), ρ (h.covering ↑p)
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this✝ : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
μt : μ t ≤ 0
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
hx : x ∉ t
i : ↑s
H : x ∉ u' ↑i
⊢ f x ≤ (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x

Tactic:
simp only [H, le_top, not_false_iff, piecewise_eq_of_notMem]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᵐ[μ.restrict (s ∪ t)] g
h1 : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : ∀ᵐ (x : α) ∂μ, x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x

Tactic:
filter_upwards [h1, h2] with x h1 h2 hx

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᵐ[μ.restrict (s ∪ t)] g
h1✝ : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2✝ : ∀ᵐ (x : α) ∂μ, x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
x : α
h1 : x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
hx : x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ
⊢ f x = g x
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
this : 0 < μ ({x | f x ≤ ⨍ (a : α), f a ∂μ} \ N)
x : α
hx : x ∈ {x | f x ≤ ⨍ (a : α), f a ∂μ}
hxN : x ∉ N
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Tactic:
exact ⟨x, hxN, hx⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
⊢ 0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}

Tactic:
have := measure_le_setAverage_pos hμ hμ₁ (integrable_toReal_of_lintegral_ne_top hf h)

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ∞
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this : 0 < μ {x | x ∈ s ∧ (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ}
⊢ 0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}