mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case pos
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

case neg
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun x ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
y : ℝ
hy : y ∈ Set.Iio 0
⊢ ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)

Tactic:
ofReal_cpow_of_nonpos (le_of_lt hy)

Goal state after:
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
y : ℝ
hy : y ∈ Set.Iio 0
⊢ (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: a : ℂ
n : ℕ
⊢ (descPochhammer ℤ n).smeval a = iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0

Tactic:
let B := Metric.ball (0 : ℂ) 1

Goal state after:
a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
⊢ (descPochhammer ℤ n).smeval a = iteratedDeriv n (fun x ↦ (1 + x) ^ a) 0
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
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)
⊢ HasDerivAt (fun y ↦ y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x)

Tactic:
conv in ↑_ ^ _ => rw [(by ring : r = r + 1 - 1)]

Goal state after:
case inr
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)
⊢ HasDerivAt (fun y ↦ y ^ (r + 1 - 1 + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_12.e_a.e_a
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π =
    rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1

pp: case e'_12.e_a.e_a
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ p.2 * (p.1 ^ p.2 * p.1⁻¹) = p.1 ^ p.2 * p.2 * p.1⁻¹

Tactic:
<;>

Goal state after:
case e'_12.e_a.e_a
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π =
    rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1

case e'_12.e_a.e_a
p : ℝ × ℝ
hp : p.1 < 0
this : (fun x ↦ x.1 ^ x.2) =ᶠ[𝓝 p] fun x ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4✝ : Prod.instAddCommGroup = Prod.normedAddCommGroup.toAddCommGroup
e_5✝ : Prod.instModule ≍ Prod.normedSpace.toModule
e_6✝ : instTopologicalSpaceProd = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
e_8✝ : instAddCommGroup = normedCommRing.toCommRing.toAddCommGroup
e_9✝ : Semiring.toModule ≍ (NormedAlgebra.toNormedSpace ℝ).toModule
⊢ p.2 * (p.1 ^ p.2 * p.1⁻¹) = p.1 ^ p.2 * p.2 * p.1⁻¹
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e.e'_10.zero
w x : ℂ
hw : w ≠ x
⊢ ((FormalMultilinearSeries.ofScalars ℂ (fun i ↦ Nat.casesOn i (w ^ (-2)) 0) 0) fun x ↦ 1) =
    (constFormalMultilinearSeries ℂ ℂ (1 / w ^ 2) 0) fun x ↦ 1

pp: case e.e'_10.succ
w x : ℂ
hw : w ≠ x
n✝ : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℂ (fun i ↦ Nat.casesOn i (w ^ (-2)) 0) (n✝ + 1)) fun x ↦ 1) =
    (constFormalMultilinearSeries ℂ ℂ (1 / w ^ 2) (n✝ + 1)) fun x ↦ 1

Tactic:
<;>

Goal state after:
case e.e'_10.zero
w x : ℂ
hw : w ≠ x
⊢ ((FormalMultilinearSeries.ofScalars ℂ (fun i ↦ Nat.casesOn i (w ^ (-2)) 0) 0) fun x ↦ 1) =
    (constFormalMultilinearSeries ℂ ℂ (1 / w ^ 2) 0) fun x ↦ 1

case e.e'_10.succ
w x : ℂ
hw : w ≠ x
n✝ : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℂ (fun i ↦ Nat.casesOn i (w ^ (-2)) 0) (n✝ + 1)) fun x ↦ 1) =
    (constFormalMultilinearSeries ℂ ℂ (1 / w ^ 2) (n✝ + 1)) fun x ↦ 1
Module: Mathlib.Analysis.Analytic.RadiusLiminf

Goal state before:
pp: case a
𝕜 : 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
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ p.radius ≤ liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop

pp: case a
𝕜 : 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
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop ≤ p.radius

Tactic:
<;>

Goal state after:
case a
𝕜 : 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
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ p.radius ≤ liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop

case a
𝕜 : 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
this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)
⊢ liminf (fun n ↦ 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop ≤ p.radius
Module: Mathlib.Analysis.Asymptotics.Completion

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F
f : α → E
g : α → F
l : Filter α
⊢ (fun x ↦ ↑(g x)) =o[l] f ↔ g =o[l] f

Tactic:
simp only [isLittleO_iff, norm_coe]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F
f : α → E
g : α → F
l : Filter α
⊢ (f =o[l] fun x ↦ ↑(g x)) ↔ f =o[l] g

Tactic:
simp only [isLittleO_iff, norm_coe]

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

Goal state before:
pp: case h₁
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 < ↑r

pp: case h₂
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 y z < ↑r

Tactic:
<;>

Goal state after:
case h₁
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 < ↑r

case h₂
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 y z < ↑r
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

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

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

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

Tactic:
<;>

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.SpecialFunctions.Log.ERealExp

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

pp: case coe
a✝ : ℝ
⊢ (↑a✝).exp = 0 ↔ ↑a✝ = ⊥

pp: case top
⊢ ⊤.exp = 0 ↔ ⊤ = ⊥

Tactic:
<;>

Goal state after:
case bot
⊢ ⊥.exp = 0 ↔ ⊥ = ⊥

case coe
a✝ : ℝ
⊢ (↑a✝).exp = 0 ↔ ↑a✝ = ⊥

case top
⊢ ⊤.exp = 0 ↔ ⊤ = ⊥
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case bot
⊢ ⊥.exp = ∞ ↔ ⊥ = ⊤

pp: case coe
a✝ : ℝ
⊢ (↑a✝).exp = ∞ ↔ ↑a✝ = ⊤

pp: case top
⊢ ⊤.exp = ∞ ↔ ⊤ = ⊤

Tactic:
<;>

Goal state after:
case bot
⊢ ⊥.exp = ∞ ↔ ⊥ = ⊤

case coe
a✝ : ℝ
⊢ (↑a✝).exp = ∞ ↔ ↑a✝ = ⊤

case top
⊢ ⊤.exp = ∞ ↔ ⊤ = ⊤
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case pos
x y : ℝ≥0∞
h : x < y
h✝¹ : x = 0
h✝ : y = 0
⊢ ⊥ < ⊥

pp: case pos
x y : ℝ≥0∞
h : x < y
h✝² : x = 0
h✝¹ : ¬y = 0
h✝ : y = ∞
⊢ ⊥ < ⊤

pp: case neg
x y : ℝ≥0∞
h : x < y
h✝² : x = 0
h✝¹ : ¬y = 0
h✝ : ¬y = ∞
⊢ ⊥ < ↑(Real.log y.toReal)

pp: case pos
x y : ℝ≥0∞
h : x < y
h✝² : ¬x = 0
h✝¹ : x = ∞
h✝ : y = 0
⊢ ⊤ < ⊥

pp: case pos
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : x = ∞
h✝¹ : ¬y = 0
h✝ : y = ∞
⊢ ⊤ < ⊤

pp: case neg
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : x = ∞
h✝¹ : ¬y = 0
h✝ : ¬y = ∞
⊢ ⊤ < ↑(Real.log y.toReal)

pp: case pos
x y : ℝ≥0∞
h : x < y
h✝² : ¬x = 0
h✝¹ : ¬x = ∞
h✝ : y = 0
⊢ ↑(Real.log x.toReal) < ⊥

pp: case pos
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : ¬x = ∞
h✝¹ : ¬y = 0
h✝ : y = ∞
⊢ ↑(Real.log x.toReal) < ⊤

pp: case neg
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : ¬x = ∞
h✝¹ : ¬y = 0
h✝ : ¬y = ∞
⊢ ↑(Real.log x.toReal) < ↑(Real.log y.toReal)

Tactic:
<;>

Goal state after:
case pos
x y : ℝ≥0∞
h : x < y
h✝¹ : x = 0
h✝ : y = 0
⊢ ⊥ < ⊥

case pos
x y : ℝ≥0∞
h : x < y
h✝² : x = 0
h✝¹ : ¬y = 0
h✝ : y = ∞
⊢ ⊥ < ⊤

case neg
x y : ℝ≥0∞
h : x < y
h✝² : x = 0
h✝¹ : ¬y = 0
h✝ : ¬y = ∞
⊢ ⊥ < ↑(Real.log y.toReal)

case pos
x y : ℝ≥0∞
h : x < y
h✝² : ¬x = 0
h✝¹ : x = ∞
h✝ : y = 0
⊢ ⊤ < ⊥

case pos
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : x = ∞
h✝¹ : ¬y = 0
h✝ : y = ∞
⊢ ⊤ < ⊤

case neg
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : x = ∞
h✝¹ : ¬y = 0
h✝ : ¬y = ∞
⊢ ⊤ < ↑(Real.log y.toReal)

case pos
x y : ℝ≥0∞
h : x < y
h✝² : ¬x = 0
h✝¹ : ¬x = ∞
h✝ : y = 0
⊢ ↑(Real.log x.toReal) < ⊥

case pos
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : ¬x = ∞
h✝¹ : ¬y = 0
h✝ : y = ∞
⊢ ↑(Real.log x.toReal) < ⊤

case neg
x y : ℝ≥0∞
h : x < y
h✝³ : ¬x = 0
h✝² : ¬x = ∞
h✝¹ : ¬y = 0
h✝ : ¬y = ∞
⊢ ↑(Real.log x.toReal) < ↑(Real.log y.toReal)
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
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

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

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

Tactic:
<;>

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

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

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

Tactic:
<;>

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: case carrier
X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x✝ : X
⊢ x✝ ∈ ((mapIsometry (IsometryEquiv.refl X)) D).carrier ↔ x✝ ∈ D.carrier

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

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

Tactic:
<;>

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

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
⊢ ↑((mapIsometry (f.trans g)) D).packingRadius = ↑((mapIsometry g) ((mapIsometry 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
⊢ ↑((mapIsometry (f.trans g)) D).coveringRadius = ↑((mapIsometry g) ((mapIsometry 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
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: case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthInf v + linearGrowthSup fun x ↦ b) = linearGrowthInf v

pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊤

pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊥

Tactic:
<;>

Goal state after:
case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthInf v + linearGrowthSup fun x ↦ b) = linearGrowthInf v

u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊤

u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊥
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthSup v + linearGrowthSup fun x ↦ b) = linearGrowthSup v

pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊥ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊤

pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊤ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊥

Tactic:
<;>

Goal state after:
case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthSup v + linearGrowthSup fun x ↦ b) = linearGrowthSup v

u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊥ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊤

u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊤ ∨ (linearGrowthSup fun x ↦ b) ≠ ⊥
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case refine_1
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ ⊥ * ↑n ≤ ↑0

pp: case refine_2
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ ↑0 ≤ b * ↑n

Tactic:
<;>

Goal state after:
case refine_1
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ ⊥ * ↑n ≤ ↑0

case refine_2
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ ↑0 ≤ b * ↑n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: case inl
u v : ℕ → ℝ≥0∞
hb : 0 ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n
⊢ (expGrowthInf fun x ↦ 0 * v x) ≤ expGrowthInf v

Tactic:
simp only [zero_mul, ← Pi.zero_def, expGrowthInf_zero, bot_le]

Goal state after: