mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case hx
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ x ∈ s ∩ Metric.eball x r

pp: case h's
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
·

Goal state after:
case hx
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ x ∈ s ∩ Metric.eball x r
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case h's
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
·

Goal state after:
case h's
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case h'
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ AnalyticOn 𝕜 f (s ∩ Metric.eball x r)

pp: case hs
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)

pp: case hx
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ x ∈ s ∩ Metric.eball x r

pp: case h's
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
·

Goal state after:
case h'
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ AnalyticOn 𝕜 f (s ∩ Metric.eball x r)
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case hs
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)

pp: case hx
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ x ∈ s ∩ Metric.eball x r

pp: case h's
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
·

Goal state after:
case hs
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ UniqueDiffOn 𝕜 (s ∩ Metric.eball x r)
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case hx
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ x ∈ s ∩ Metric.eball x r

pp: case h's
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
·

Goal state after:
case hx
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ x ∈ s ∩ Metric.eball x r
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case h's
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r

Tactic:
·

Goal state after:
case h's
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ Metric.eball x r) x
⊢ s ∩ Metric.eball x r ⊆ Metric.eball x r
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y ↑ε
⊢ s ⊆ ⋃ y ∈ N, closedEBall y ↑ε

Tactic:
·

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y ↑ε
⊢ s ⊆ ⋃ y ∈ N, closedEBall y ↑ε
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: 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

pp: 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

pp: 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

Tactic:
·

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
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case bot
y : EReal
h : ⊥ < y
⊢ ⊥.exp < y.exp

pp: case coe
y : EReal
a✝ : ℝ
h : ↑a✝ < y
⊢ (↑a✝).exp < y.exp

pp: case top
y : EReal
h : ⊤ < y
⊢ ⊤.exp < y.exp

Tactic:
·

Goal state after:
case bot
y : EReal
h : ⊥ < y
⊢ ⊥.exp < y.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case pos
x : ℝ
h_nonpos : x ≤ 0
⊢ ⊥ = ⊥

pp: case neg
x : ℝ
h_nonpos : ¬x ≤ 0
⊢ ↑(Real.log (ENNReal.ofReal x).toReal) = ↑(Real.log x)

Tactic:
·

Goal state after:
case pos
x : ℝ
h_nonpos : x ≤ 0
⊢ ⊥ = ⊥
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
h : ↑a✝ < y
⊢ (↑a✝).exp < y.exp

pp: case top
y : EReal
h : ⊤ < y
⊢ ⊤.exp < y.exp

Tactic:
·

Goal state after:
case coe
y : EReal
a✝ : ℝ
h : ↑a✝ < y
⊢ (↑a✝).exp < y.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case neg
x : ℝ
h_nonpos : ¬x ≤ 0
⊢ ↑(Real.log (ENNReal.ofReal x).toReal) = ↑(Real.log x)

Tactic:
·

Goal state after:
case neg
x : ℝ
h_nonpos : ¬x ≤ 0
⊢ ↑(Real.log (ENNReal.ofReal x).toReal) = ↑(Real.log x)
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe.bot
a✝ : ℝ
h : ↑a✝ < ⊥
⊢ (↑a✝).exp < ⊥.exp

pp: case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ < ↑a✝
⊢ (↑a✝¹).exp < (↑a✝).exp

pp: case coe.top
a✝ : ℝ
h : ↑a✝ < ⊤
⊢ (↑a✝).exp < ⊤.exp

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℝ
h : ↑a✝ < ⊥
⊢ (↑a✝).exp < ⊥.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ < ↑a✝
⊢ (↑a✝¹).exp < (↑a✝).exp

pp: case coe.top
a✝ : ℝ
h : ↑a✝ < ⊤
⊢ (↑a✝).exp < ⊤.exp

Tactic:
·

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
h : ↑a✝¹ < ↑a✝
⊢ (↑a✝¹).exp < (↑a✝).exp
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: 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

pp: 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

Tactic:
·

Goal state after:
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
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe.top
a✝ : ℝ
h : ↑a✝ < ⊤
⊢ (↑a✝).exp < ⊤.exp

Tactic:
·

Goal state after:
case coe.top
a✝ : ℝ
h : ↑a✝ < ⊤
⊢ (↑a✝).exp < ⊤.exp
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: 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

Tactic:
·

Goal state after:
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.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top
y : EReal
h : ⊤ < y
⊢ ⊤.exp < y.exp

Tactic:
·

Goal state after:
case top
y : EReal
h : ⊤ < y
⊢ ⊤.exp < y.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case bot
⊢ (-⊥).exp = ⊥.exp⁻¹

pp: case coe
a✝ : ℝ
⊢ (-↑a✝).exp = (↑a✝).exp⁻¹

pp: case top
⊢ (-⊤).exp = ⊤.exp⁻¹

Tactic:
·

Goal state after:
case bot
⊢ (-⊥).exp = ⊥.exp⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (-↑a✝).exp = (↑a✝).exp⁻¹

pp: case top
⊢ (-⊤).exp = ⊤.exp⁻¹

Tactic:
·

Goal state after:
case coe
a✝ : ℝ
⊢ (-↑a✝).exp = (↑a✝).exp⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top
⊢ (-⊤).exp = ⊤.exp⁻¹

Tactic:
·

Goal state after:
case top
⊢ (-⊤).exp = ⊤.exp⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case bot
y : EReal
⊢ (⊥ + y).exp = ⊥.exp * y.exp

pp: case coe
y : EReal
a✝ : ℝ
⊢ (↑a✝ + y).exp = (↑a✝).exp * y.exp

pp: case top
y : EReal
⊢ (⊤ + y).exp = ⊤.exp * y.exp

Tactic:
·

Goal state after:
case bot
y : EReal
⊢ (⊥ + y).exp = ⊥.exp * y.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
⊢ (↑a✝ + y).exp = (↑a✝).exp * y.exp

pp: case top
y : EReal
⊢ (⊤ + y).exp = ⊤.exp * y.exp

Tactic:
·

Goal state after:
case coe
y : EReal
a✝ : ℝ
⊢ (↑a✝ + y).exp = (↑a✝).exp * y.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).exp = (↑a✝).exp * ⊥.exp

pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).exp = (↑a✝¹).exp * (↑a✝).exp

pp: case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).exp = (↑a✝).exp * ⊤.exp

Tactic:
·

Goal state after:
case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).exp = (↑a✝).exp * ⊥.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).exp = (↑a✝¹).exp * (↑a✝).exp

pp: case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).exp = (↑a✝).exp * ⊤.exp

Tactic:
·

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).exp = (↑a✝¹).exp * (↑a✝).exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).exp = (↑a✝).exp * ⊤.exp

Tactic:
·

Goal state after:
case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).exp = (↑a✝).exp * ⊤.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inl
y : ℝ≥0∞
⊢ (0 * y).log = log 0 + y.log

pp: case inr.inl
y : ℝ≥0∞
⊢ (∞ * y).log = ∞.log + y.log

pp: case inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * y).log = x.log + y.log

Tactic:
·

Goal state after:
case inl
y : ℝ≥0∞
⊢ (0 * y).log = log 0 + y.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top
y : EReal
⊢ (⊤ + y).exp = ⊤.exp * y.exp

Tactic:
·

Goal state after:
case top
y : EReal
⊢ (⊤ + y).exp = ⊤.exp * y.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top.bot
⊢ (⊤ + ⊥).exp = ⊤.exp * ⊥.exp

pp: case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).exp = ⊤.exp * (↑a✝).exp

pp: case top.top
⊢ (⊤ + ⊤).exp = ⊤.exp * ⊤.exp

Tactic:
·

Goal state after:
case top.bot
⊢ (⊤ + ⊥).exp = ⊤.exp * ⊥.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl
y : ℝ≥0∞
⊢ (∞ * y).log = ∞.log + y.log

pp: case inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * y).log = x.log + y.log

Tactic:
·

Goal state after:
case inr.inl
y : ℝ≥0∞
⊢ (∞ * y).log = ∞.log + y.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).exp = ⊤.exp * (↑a✝).exp

pp: case top.top
⊢ (⊤ + ⊤).exp = ⊤.exp * ⊤.exp

Tactic:
·

Goal state after:
case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).exp = ⊤.exp * (↑a✝).exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top.top
⊢ (⊤ + ⊤).exp = ⊤.exp * ⊤.exp

Tactic:
·

Goal state after:
case top.top
⊢ (⊤ + ⊤).exp = ⊤.exp * ⊤.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl.inl
⊢ (∞ * 0).log = ⊤ + log 0

pp: case inr.inl.inr.inl
⊢ (∞ * ∞).log = ⊤ + ∞.log

pp: case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (∞ * y).log = ⊤ + y.log

Tactic:
·

Goal state after:
case inr.inl.inl
⊢ (∞ * 0).log = ⊤ + log 0
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl.inr.inl
⊢ (∞ * ∞).log = ⊤ + ∞.log

pp: case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (∞ * y).log = ⊤ + y.log

Tactic:
·

Goal state after:
case inr.inl.inr.inl
⊢ (∞ * ∞).log = ⊤ + ∞.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case bot
⊢ ⊥.exp.log = ⊥

pp: case coe
a✝ : ℝ
⊢ (↑a✝).exp.log = ↑a✝

pp: case top
⊢ ⊤.exp.log = ⊤

Tactic:
·

Goal state after:
case bot
⊢ ⊥.exp.log = ⊥
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (↑a✝).exp.log = ↑a✝

pp: case top
⊢ ⊤.exp.log = ⊤

Tactic:
·

Goal state after:
case coe
a✝ : ℝ
⊢ (↑a✝).exp.log = ↑a✝
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case top
⊢ ⊤.exp.log = ⊤

Tactic:
·

Goal state after:
case top
⊢ ⊤.exp.log = ⊤
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case pos
x : ℝ≥0∞
hx_top : x = ∞
⊢ x.log.exp = x

pp: case neg
x : ℝ≥0∞
hx_top : ¬x = ∞
⊢ x.log.exp = x

Tactic:
·

Goal state after:
case pos
x : ℝ≥0∞
hx_top : x = ∞
⊢ x.log.exp = x