mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inl.inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this : f '' s = {f x}
⊢ μH[d] {f x} ≤ ↑0 ^ d * μH[↑r * d] s

Tactic:
rcases eq_or_lt_of_le hd with (rfl | h'd)

Goal state after:
case inl.inr.inl
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this : f '' s = {f x}
hd : 0 ≤ 0
⊢ μH[0] {f x} ≤ ↑0 ^ 0 * μH[↑r * 0] s

case inl.inr.inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
d : ℝ
hd : 0 ≤ d
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this : f '' s = {f x}
h'd : 0 < d
⊢ μH[d] {f x} ≤ ↑0 ^ d * μH[↑r * d] s
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ (↑Sᗮ.mulI).carrier ↔ x ∈ (↑S.symplComp).carrier

Tactic:
rw [← mem_iff, ← mem_iff, mem_symplComp_iff, mem_mapEquiv_iff, scalarSMulCLE_symm_apply,
    Units.inv_mk, Units.smul_mk_apply]

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ UnitI.inv • x ∈ Sᗮ ↔ ∀ y ∈ S, ⟪y, x⟫.im = 0
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inl.inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
⊢ μH[d] {x} ≤ ↑0 ^ d * μH[d] s

Tactic:
rcases eq_or_lt_of_le hd with (rfl | h'd)

Goal state after:
case inl.inr.inl
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
hd : 0 ≤ 0
⊢ μH[0] {x} ≤ ↑0 ^ 0 * μH[0] s

case inl.inr.inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
h'd : 0 < d
⊢ μH[d] {x} ≤ ↑0 ^ d * μH[d] s
Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
b a : F
x✝ : F →WOT[𝕜] F
| (starRingEnd 𝕜) ⟪a, x✝ b⟫_𝕜

Tactic:
← RCLike.star_def

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
b a : F
x✝ : F →WOT[𝕜] F
| star ⟪a, x✝ b⟫_𝕜
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
⊢ ContinuousAt (⇑f) 0

Tactic:
have bE' : (𝓝 (0 : E)).HasBasis (fun _ ↦ True) (fun n : ℕ ↦ (c ^ n) • b n) := by
    refine bE.1.to_hasBasis' ?_ ?_
    · intro n _
      use n
      exact ⟨trivial, (bE1 n).2 _ (by grw [norm_pow, hc1, one_pow])⟩
    · intro n _
      simpa using smul_mem_nhds_smul₀ (pow_ne_zero n c_ne) (bE1 n).1

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
⊢ ContinuousAt (⇑f) 0
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
h_tendsto : Tendsto (fun n ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n ↦ (c ^ n)⁻¹ • u n)
hf : IsVonNBounded 𝕜' (Set.range fun x ↦ (σ c ^ x)⁻¹ • f (u x))
⊢ False

Tactic:
have : Tendsto (f ∘ u) atTop (𝓝 0) := by
    have : Tendsto (fun n ↦ σ c ^ n) atTop (𝓝 0) :=
      tendsto_pow_atTop_nhds_zero_of_norm_lt_one (by simpa using hc1)
    have := hf.smul_tendsto_zero (.of_forall fun n ↦ Set.mem_range_self n) this
    exact this.congr fun n ↦ by simp [c_ne]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : Module 𝕜 E
inst✝⁴ : ContinuousSMul 𝕜 E
inst✝³ : NormedField 𝕜'
inst✝² : Module 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝¹ : RingHomIsometric σ
inst✝ : FirstCountableTopology E
f : E →ₛₗ[σ] F
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
c_ne : c ≠ 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i ↦ b i
bE' : (𝓝 0).HasBasis (fun x ↦ True) fun n ↦ c ^ n • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (i : ℕ), u i ∈ c ^ i • b i
hu' : ∀ (i : ℕ), f (u i) ∉ V
h_tendsto : Tendsto (fun n ↦ (c ^ n)⁻¹ • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n ↦ (c ^ n)⁻¹ • u n)
hf : IsVonNBounded 𝕜' (Set.range fun x ↦ (σ c ^ x)⁻¹ • f (u x))
this : Tendsto (⇑f ∘ u) atTop (𝓝 0)
⊢ False
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_1
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ AEStronglyMeasurable (fun t ↦ t ^ (s - 1) * f t) (volume.restrict (Ioo 0 ε))

Tactic:
refine AEStronglyMeasurable.mul ?_ (hfc.mono_set Ioo_subset_Ioi_self)

Goal state after:
case refine_1
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ AEStronglyMeasurable (fun t ↦ t ^ (s - 1)) (volume.restrict (Ioo 0 ε))
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
hab : b < a
hf : f =O[atTop] fun x ↦ x ^ (-a)
⊢ (fun t ↦ log t • f t) =O[atTop] fun x ↦ x ^ (-b)

Tactic:
refine
    ((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).isBigO.smul hf).congr'
      (Eventually.of_forall fun t => by rfl)
      ((eventually_gt_atTop 0).mp (Eventually.of_forall fun t ht => ?_))
  simp only
  rw [smul_eq_mul, ← rpow_add ht, ← sub_eq_add_neg, sub_eq_add_neg a, add_sub_cancel_left]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
v : ℂ
⊢ IntervalIntegrable (fun x ↦ ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume 0 (1 / 2)

Tactic:
by
  apply IntervalIntegrable.mul_continuousOn
  · refine intervalIntegral.intervalIntegrable_cpow' ?_
    rwa [sub_re, one_re, ← zero_sub, sub_lt_sub_iff_right]
  · apply continuousOn_of_forall_continuousAt
    intro x hx
    rw [uIcc_of_le (by positivity : (0 : ℝ) ≤ 1 / 2)] at hx
    apply ContinuousAt.cpow (by fun_prop) (by fun_prop)
    norm_cast
    exact ofReal_mem_slitPlane.2 <| by linarith only [hx.2]

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
hF : (mulSupport F).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hsub : (support fun i ↦ logDeriv (F i)) ⊆ ↑hF.toFinset
⊢ logDeriv (∏ᶠ (i : ι), F i) =ᶠ[codiscreteWithin U] ∑ᶠ (i : ι), logDeriv (F i)

Tactic:
finprod_eq_prod_of_mulSupport_subset F (s := hF.toFinset) (by simp),

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
hF : (mulSupport F).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hsub : (support fun i ↦ logDeriv (F i)) ⊆ ↑hF.toFinset
⊢ logDeriv (∏ i ∈ hF.toFinset, F i) =ᶠ[codiscreteWithin U] ∑ᶠ (i : ι), logDeriv (F i)
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
t : V → Set ℝ
ht : ∀ i ∈ Metric.sphere 0 1, t i ∈ atTop
u : V → Set V
hu : ∀ i ∈ Metric.sphere 0 1, u i ∈ 𝓝 i
smul_subset_s : ∀ i ∈ Metric.sphere 0 1, t i • u i ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, x ∈ Metric.sphere 0 1
h₂ : Metric.sphere 0 1 ⊆ ⋃ x ∈ cover, u x
x : P
hx : ‖x -ᵥ p‖ ∈ Set.Ioi 0 ∩ ⋂ x ∈ cover, t x
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
x'_mem : x' ∈ Metric.sphere 0 1
y : V
y_mem : y ∈ cover
hy : x' ∈ u y
⊢ x ∈ s

Tactic:
← vsub_vadd x p,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
t : V → Set ℝ
ht : ∀ i ∈ Metric.sphere 0 1, t i ∈ atTop
u : V → Set V
hu : ∀ i ∈ Metric.sphere 0 1, u i ∈ 𝓝 i
smul_subset_s : ∀ i ∈ Metric.sphere 0 1, t i • u i ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, x ∈ Metric.sphere 0 1
h₂ : Metric.sphere 0 1 ⊆ ⋃ x ∈ cover, u x
x : P
hx : ‖x -ᵥ p‖ ∈ Set.Ioi 0 ∩ ⋂ x ∈ cover, t x
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
x'_mem : x' ∈ Metric.sphere 0 1
y : V
y_mem : y ∈ cover
hy : x' ∈ u y
⊢ (x -ᵥ p) +ᵥ p ∈ s
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
t : V → Set ℝ
ht : ∀ i ∈ Metric.sphere 0 1, t i ∈ atTop
u : V → Set V
hu : ∀ i ∈ Metric.sphere 0 1, u i ∈ 𝓝 i
smul_subset_s : ∀ i ∈ Metric.sphere 0 1, t i • u i ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, x ∈ Metric.sphere 0 1
h₂ : Metric.sphere 0 1 ⊆ ⋃ x ∈ cover, u x
x : P
hx : ‖x -ᵥ p‖ ∈ Set.Ioi 0 ∩ ⋂ x ∈ cover, t x
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
x'_mem : x' ∈ Metric.sphere 0 1
y : V
y_mem : y ∈ cover
hy : x' ∈ u y
⊢ x ∈ s

Tactic:
rw [← vsub_vadd x p, ← show ‖x -ᵥ p‖ • x' = x -ᵥ p from smul_inv_smul₀ hx.1.ne' (x -ᵥ p)]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
p : P
t : V → Set ℝ
ht : ∀ i ∈ Metric.sphere 0 1, t i ∈ atTop
u : V → Set V
hu : ∀ i ∈ Metric.sphere 0 1, u i ∈ 𝓝 i
smul_subset_s : ∀ i ∈ Metric.sphere 0 1, t i • u i ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
cover : Finset V
h₁ : ∀ x ∈ cover, x ∈ Metric.sphere 0 1
h₂ : Metric.sphere 0 1 ⊆ ⋃ x ∈ cover, u x
x : P
hx : ‖x -ᵥ p‖ ∈ Set.Ioi 0 ∩ ⋂ x ∈ cover, t x
x' : V := ‖x -ᵥ p‖⁻¹ • (x -ᵥ p)
x'_mem : x' ∈ Metric.sphere 0 1
y : V
y_mem : y ∈ cover
hy : x' ∈ u y
⊢ ‖x -ᵥ p‖ • x' +ᵥ p ∈ s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
| ↑n ^ s

Tactic:
rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this✝ : ∀ (x : ℝ), x = x / ↑n * ↑n
this :
  ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑(x / ↑n * ↑n) ^ (s - 1) =
    ↑n • ∫ (x : ℝ) in 0 / ↑n..↑n / ↑n, ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1)
x : ℝ
hx : x ∈ Ioc 0 1
hn' : ↑n ≠ 0
| ↑n ^ (s - 1) * ↑n ^ 1
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
⊢ (∃ᶠ (p : V) in map (fun p ↦ p.1 • p.2) (atTop ×ˢ 𝓝 v), p ∈ s) ↔ ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.2 ∈ s

Tactic:
frequently_map

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
hs : ∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s
v : V
⊢ (∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 ∈ s) ↔ ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.2 ∈ s
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst✝²] s
hc : 0 ≤ c
hv : ∃ᶠ (a : V) in map (fun p ↦ p.1 • p.2) (atTop ×ˢ 𝓝 v), a +ᵥ p ∈ s
⊢ ∃ᶠ (x : k × V) in atTop ×ˢ 𝓝 v, c • x.2 +ᵥ p ∈ s

Tactic:
frequently_map

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs₁ : StarConvex k p s
hs₂ : IsClosed[inst✝²] s
hc : 0 ≤ c
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ p ∈ s
⊢ ∃ᶠ (x : k × V) in atTop ×ˢ 𝓝 v, c • x.2 +ᵥ p ∈ s
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : V) in map (fun p ↦ p.1 • p.2) (atTop ×ˢ 𝓝 v), a +ᵥ c • v +ᵥ p ∈ s
⊢ c • v +ᵥ p ∈ s

Tactic:
frequently_map

Goal state after:
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : IsStrictOrderedRing k
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
⊢ c • v +ᵥ p ∈ s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
by
  suffices ∀ m : ℕ, ⌊1 - s.re⌋₊ = m → Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s) by tauto
  intro m
  induction m generalizing s with intro hs
  | zero => -- Base case: `0 < re s`, so Gamma is given by the integral formula
    rw [Nat.floor_eq_zero, sub_lt_self_iff] at hs
    apply (approx_Gamma_integral_tendsto_Gamma_integral hs).congr'
    filter_upwards [eventually_ne_atTop 0] with n hn using
      (GammaSeq_eq_approx_Gamma_integral hs hn).symm
  | succ m IH => -- Induction step: use recurrence formulae in `s` for Gamma and GammaSeq
    -- Silly case `s = 0`: both sides are zero
    rcases eq_or_ne s 0 with rfl | hsne
    · unfold GammaSeq
      simp [Finset.prod_range_succ']
    specialize IH (s + 1) ?_
    · rw [Nat.floor_eq_iff' (by lia)] at hs
      have : s.re ≤ -m := by grind
      rw [Nat.floor_eq_iff <| by simpa using (show s.re ≤ 0 by grind)]
      grind [add_re, one_re]
    rw [Gamma_add_one _ hsne] at IH
    have := (IH.div_const s).congr' <| by
      filter_upwards [eventually_ne_atTop 0] with n using GammaSeq_add_one_left s
    simp only [mul_comm _ (s.GammaSeq _)] at this
    rwa [mul_div_cancel_left₀ _ hsne, ← mul_one (Gamma s),
      tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this
    simp_rw [add_assoc]
    exact tendsto_natCast_div_add_atTop (1 + s)

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f‖ * ‖g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
rw [le_add_iff_nonneg_right]

Goal state after:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ 0 ≤ ‖f 0‖
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : SeminormedAddCommGroup W
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : Ring R
inst✝² : Module R W
inst✝¹ : ContinuousConstSMul R W
inst✝ : SMulCommClass 𝕜 R W
p : W × (V →L[𝕜] W)
⊢ ({ toLinearEquiv := decompLinearEquiv 𝕜 R V W, norm_map' := ⋯ }.symm p).contLinear = p.2

Tactic:
← LinearIsometryEquiv.coe_symm_toLinearEquiv,

Goal state after:
𝕜 : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : SeminormedAddCommGroup W
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 V
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : Ring R
inst✝² : Module R W
inst✝¹ : ContinuousConstSMul R W
inst✝ : SMulCommClass 𝕜 R W
p : W × (V →L[𝕜] W)
⊢ ({ toLinearEquiv := decompLinearEquiv 𝕜 R V W, norm_map' := ⋯ }.symm p).contLinear = p.2
Module: Mathlib.Analysis.Normed.Affine.MazurUlam

Goal state before:
pp: E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans
    (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv
hx : e x = x
hy : e y = y
hm : e (midpoint ℝ x y) = midpoint ℝ x y
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)

Tactic:
simp only [e, trans_apply] at hm

Goal state after:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MetricSpace PE
inst✝⁴ : NormedAddTorsor E PE
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MetricSpace PF
inst✝ : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans
    (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv
hx : e x = x
hy : e y = y
hm :
  (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv
      (f.symm ((pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv (f (midpoint ℝ x y)))) =
    midpoint ℝ x y
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
⊢ Simplex.Scalene t

Tactic:
intro ⟨⟨x₁, x₂⟩, hx⟩ ⟨⟨y₁, y₂⟩, hy⟩ hxy

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₁ x₂ : Fin (2 + 1)
hx : (x₁, x₂).1 < (x₁, x₂).2
y₁ y₂ : Fin (2 + 1)
hy : (y₁, y₂).1 < (y₁, y₂).2
hxy :
  (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(x₁, x₂), hx⟩ =
    (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(y₁, y₂), hy⟩
⊢ ⟨(x₁, x₂), hx⟩ = ⟨(y₁, y₂), hy⟩
Module: Mathlib.Analysis.Normed.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Algebra ℚ R
inst✝² : UniformSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
r : R
⊢ exp (r • inr 1) = 1 + r • inr 1

Tactic:
← inr_smul,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : Algebra ℚ R
inst✝² : UniformSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
r : R
⊢ exp (inr (r • 1)) = 1 + inr (r • 1)