mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : (volume.addHaarScalarFactor μH[0] • μH[0]) {0} = 1
⊢ μHE[0] = μH[0]

Tactic:
smul_apply,

Goal state after:
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : volume.addHaarScalarFactor μH[0] • μH[0] {0} = 1
⊢ μHE[0] = μH[0]
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: case inr
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℕ
h✝ : d₁ < d₂
s : Set X
h : μH[↑d₁] s = ⊤
⊢ (volume.addHaarScalarFactor μH[↑d₁] • μH[↑d₁]) s = ⊤

Tactic:
smul_apply,

Goal state after:
case inr
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℕ
h✝ : d₁ < d₂
s : Set X
h : μH[↑d₁] s = ⊤
⊢ volume.addHaarScalarFactor μH[↑d₁] • μH[↑d₁] s = ⊤
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty ↑s
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(affineSpan ℝ s).direction := AffineIsometryEquiv.constVSub ℝ ⟨hne.some, ⋯⟩
hs_eq : s = Subtype.val '' Subtype.val ⁻¹' s
⊢ ↑(finrank ℝ ↥(vectorSpan ℝ s)) = ↑(finrank ℝ ↥(vectorSpan ℝ (Subtype.val '' Subtype.val ⁻¹' s)))

pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty ↑s
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(affineSpan ℝ s).direction := AffineIsometryEquiv.constVSub ℝ ⟨hne.some, ⋯⟩
hs_eq : s = Subtype.val '' Subtype.val ⁻¹' s
⊢ (interior (⇑φ '' Subtype.val ⁻¹' s)).Nonempty

Tactic:
← hs_eq

Goal state after:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty ↑s
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(affineSpan ℝ s).direction := AffineIsometryEquiv.constVSub ℝ ⟨hne.some, ⋯⟩
hs_eq : s = Subtype.val '' Subtype.val ⁻¹' s
⊢ ↑(finrank ℝ ↥(vectorSpan ℝ s)) = ↑(finrank ℝ ↥(vectorSpan ℝ s))

E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hcvx : Convex ℝ s
hne : s.Nonempty
this : Nonempty ↑s
φ : ↥(affineSpan ℝ s) ≃ᵃⁱ[ℝ] ↥(affineSpan ℝ s).direction := AffineIsometryEquiv.constVSub ℝ ⟨hne.some, ⋯⟩
hs_eq : s = Subtype.val '' Subtype.val ⁻¹' s
⊢ (interior (⇑φ '' Subtype.val ⁻¹' s)).Nonempty
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : dimH s < ↑(finrank ℝ E)
⊢ Dense sᶜ

Tactic:
refine fun x => mem_closure_iff_nhds.2 fun t ht => nonempty_iff_ne_empty.2 fun he => hs.not_ge ?_

Goal state after:
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : dimH s < ↑(finrank ℝ E)
x : E
t : Set E
ht : t ∈ 𝓝 x
he : t ∩ sᶜ = ∅
⊢ ↑(finrank ℝ E) ≤ dimH s
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
⊢ ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 fun x ↦ f (b x)).det

Tactic:
suffices ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 (f.rangeRestrict <| b ·)).det by
    simpa

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
⊢ ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 fun x ↦ f.rangeRestrict (b x)).det
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c✝ : ℝ
c : ℝ := -c✝
hc : 0 < c
x : H
⊢ ‖x‖ ^ 2 * c = re ⟪((algebraMap ℝ 𝕜) c • 1) x, x⟫_𝕜

Tactic:
smul_apply,

Goal state after:
𝕜 : Type u_1
H : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : CompleteSpace H
inst✝¹ : Algebra ℝ (H →L[𝕜] H)
inst✝ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
f : H →L[𝕜] H
hf : f.IsPositive
c✝ : ℝ
c : ℝ := -c✝
hc : 0 < c
x : H
⊢ ‖x‖ ^ 2 * c = re ⟪(algebraMap ℝ 𝕜) c • 1 x, x⟫_𝕜
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_1
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
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| μH[↑(finrank ℝ E)] (⇑e '' K)

Tactic:
congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]

Goal state after:
case a.d
ι : Type u_1
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
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
K : Set E
hK : IsCompact K
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| ↑(Fintype.card (Fin (finrank ℝ E)))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_1
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
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| μH[↑(finrank ℝ E)] (⇑e '' U)

Tactic:
congr; congr; rw [← Fintype.card_fin (finrank ℝ E)]

Goal state after:
case a.d
ι : Type u_1
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
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
U : Set E
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hU' : U.Nonempty
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq ⋯
| ↑(Fintype.card (Fin (finrank ℝ E)))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ ‖c⁻¹‖₊ ^ d • μH[d] s = ‖c‖₊⁻¹ ^ d • μH[d] s

Tactic:
nnnorm_inv

Goal state after:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
⊢ ‖c‖₊⁻¹ ^ d • μH[d] s = ‖c‖₊⁻¹ ^ d • μH[d] s
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁸ : NormedField 𝕜₁
inst✝¹⁷ : NormedField 𝕜₂
inst✝¹⁶ : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module 𝕜₃ G
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective ⇑σ₂₃
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun a ↦ z ((g.comp a) x)

Tactic:
let invPair : RingHomInvPair σ₂₃ σ_equiv.symm := RingHomInvPair.of_ringEquiv σ_equiv

Goal state after:
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
E : Type u_9
F : Type u_10
G : Type u_11
inst✝¹⁸ : NormedField 𝕜₁
inst✝¹⁷ : NormedField 𝕜₂
inst✝¹⁶ : NormedField 𝕜₃
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : TopologicalSpace E
inst✝¹² : Module 𝕜₁ E
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : TopologicalSpace F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module 𝕜₃ G
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
x : E
z : StrongDual 𝕜₃ G
σ_bij : Function.Bijective ⇑σ₂₃
σ_equiv : 𝕜₂ ≃+* 𝕜₃ := RingEquiv.ofBijective σ₂₃ σ_bij
invPair : RingHomInvPair σ₂₃ ↑σ_equiv.symm := RingHomInvPair.of_ringEquiv σ_equiv
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun a ↦ z ((g.comp a) x)
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: w z : ℂ
⊢ ↑⟪w, z⟫ + (Complex.orientation.areaForm w) z • I = z * (starRingEnd ℂ) w

Tactic:
apply Complex.ext <;> simp [mul_comm]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (a * t) = ↑a ^ (1 - s) • ↑(a * t) ^ (s - 1) • f (a * t)

Tactic:
rw [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), ← mul_smul,
      (by ring : 1 - s = -(s - 1)), cpow_neg, inv_mul_cancel_left₀]

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑a ^ (s - 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun x ↦ ↑x * g x) atTop (𝓝 t)
⊢ Tendsto (fun x ↦ (1 + g x) ^ ↑x) atTop (𝓝 (cexp t))

Tactic:
apply ((continuous_exp.tendsto _).comp (tendsto_mul_log_one_add_of_tendsto hg)).congr'
  have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded
    hg.norm.isBoundedUnder_le (RCLike.tendsto_ofReal_atTop_cobounded ℂ)
  filter_upwards [hg0.eventually_ne (show 0 ≠ -1 by simp)] with x hg1
  dsimp
  rw [cpow_def_of_ne_zero, mul_comm]
  intro hg0
  rw [← add_eq_zero_iff_neg_eq.mp hg0] at hg1
  norm_num at hg1

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
| Complex.cos ↑x ^ n

Tactic:
rw [← Nat.sub_add_cancel hn, pow_add]

Goal state after:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
| Complex.cos ↑x ^ (n - 2) * Complex.cos ↑x ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y ↦ y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ 0 < (id (1 - ↑x)).re

Tactic:
id,

Goal state after:
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y ↦ y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ 0 < (1 - ↑x).re
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e'_5
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this✝¹ :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm : Tendsto (fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this✝ :
  ((fun x_1 ↦
        (fun n ↦ logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
          (fun b ↦ log (x - 1)) x_1) ∘
      fun a ↦ a + 1) =
    fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)
this : f (x - 1 + 1) = f (x - 1) + log (x - 1)
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0

Tactic:
rw [sub_add_cancel] at this

Goal state after:
case e'_5
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
this✝¹ :
  ∀ᶠ (n : ℕ) in atTop,
    logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
hm : Tendsto (fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)) atTop (𝓝 (f (x - 1) - f 1 + log (x - 1)))
this✝ :
  ((fun x_1 ↦
        (fun n ↦ logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
          (fun b ↦ log (x - 1)) x_1) ∘
      fun a ↦ a + 1) =
    fun n ↦ logGammaSeq x n + x * (log (↑n + 1) - log ↑n)
this : f x = f (x - 1) + log (x - 1)
⊢ f x - f 1 = f (x - 1) - f 1 + log (x - 1) - x * 0
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
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
v u : V
this : (fun x ↦ x.1 • x.2 + u) =ᶠ[atTop ×ˢ 𝓝 v] (Function.uncurry fun x1 x2 ↦ x1 • x2) ∘ fun x ↦ (x.1, x.2 + x.1⁻¹ • u)
⊢ map (fun p ↦ p.1 • p.2 + u) (atTop ×ˢ 𝓝 v) ≤ map (fun p ↦ p.1 • p.2) (atTop ×ˢ 𝓝 v)

Tactic:
rw [map_congr this, ← map_map]

Goal state after:
case a
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
v u : V
this : (fun x ↦ x.1 • x.2 + u) =ᶠ[atTop ×ˢ 𝓝 v] (Function.uncurry fun x1 x2 ↦ x1 • x2) ∘ fun x ↦ (x.1, x.2 + x.1⁻¹ • u)
⊢ map (Function.uncurry fun x1 x2 ↦ x1 • x2) (map (fun x ↦ (x.1, x.2 + x.1⁻¹ • u)) (atTop ×ˢ 𝓝 v)) ≤
    map (fun p ↦ p.1 • p.2) (atTop ×ˢ 𝓝 v)
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹² : Field k
inst✝¹¹ : LinearOrder k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : AddTorsor V P
inst✝⁷ : TopologicalSpace V
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : IsStrictOrderedRing k
inst✝³ : IsTopologicalAddGroup V
inst✝² : ContinuousSMul k V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
t₁ : Set k
ht₁ : t₁ ∈ atTop
t₂ : Set V
hs : t₁ • t₂ ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
x✝ : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : c ∈ Set.Ioi 0
⊢ (fun x ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 ((fun x ↦ x +ᵥ p) (c • u) -ᵥ p)

Tactic:
rw [vadd_vsub]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹² : Field k
inst✝¹¹ : LinearOrder k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : AddTorsor V P
inst✝⁷ : TopologicalSpace V
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : IsStrictOrderedRing k
inst✝³ : IsTopologicalAddGroup V
inst✝² : ContinuousSMul k V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
t₁ : Set k
ht₁ : t₁ ∈ atTop
t₂ : Set V
hs : t₁ • t₂ ⊆ (fun x ↦ x +ᵥ p) ⁻¹' s
t₃ : Set V
ht₃ : t₃ ∈ 𝓝 v
ht₂ : ∀ x ∈ t₃, t₂ ∈ 𝓝 x
c : k
x✝ : c ∈ t₁ ∩ Set.Ioi 0
u : V
hu : u ∈ t₃
hc₁ : c ∈ t₁
hc₂ : c ∈ Set.Ioi 0
⊢ (fun x ↦ x +ᵥ p) ⁻¹' s ∈ 𝓝 (c • u)
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
⊢ v ∈ asymptoticCone k s ↔ ∃ᶠ (x : V) in 𝓝 v, x ∈ s

Tactic:
← map_snd_prod (atTop (α := k)) (𝓝 v),

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
⊢ v ∈ asymptoticCone k s ↔ ∃ᶠ (x : V) in map Prod.snd (atTop ×ˢ 𝓝 v), x ∈ 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✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
⊢ id c • (a • v + b • u) +ᵥ p ∈ s

Tactic:
id,

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✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : k
hc : 0 ≤ c
⊢ c • (a • v + b • u) +ᵥ p ∈ s
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: ⊢ Continuous fun q ↦ q.im

Tactic:
simpa only [← sub_re_self] using! continuous_id.sub (continuous_coe.comp continuous_re)

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Ultra

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
n : ℕ
⊢ ‖↑n‖₊ ≤ 1

Tactic:
induction n with
  | zero => simp only [Nat.cast_zero, nnnorm_zero, zero_le]
  | succ n hn => simpa only [Nat.cast_add, Nat.cast_one, hn, max_eq_right] using
    nnnorm_add_one_le_max_nnnorm_one (n : R)

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x : R
⊢ ‖x + 0‖ ≤ max ‖x‖ ‖0‖

Tactic:
simpa only [add_zero] using le_max_left _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : ↑(m + 1) < (a / max 1 ‖x‖) ^ m
⊢ ‖x + 1‖ ≤ a

Tactic:
rw [div_pow, lt_div_iff₀ (by positivity), ← nsmul_eq_mul] at hm

Goal state after:
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R) (m : ℕ), ‖x + 1‖ ^ m ≤ (m + 1) • max 1 (‖x‖ ^ m)
x : R
a : ℝ
ha : max 1 ‖x‖ < a
ha' : 1 < a
m : ℕ
hm : (m + 1) • max 1 ‖x‖ ^ m < a ^ m
⊢ ‖x + 1‖ ≤ a
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝⁶ : SeminormedCommRing R
S : Type u_2
inst✝⁵ : Ring S
inst✝⁴ : Algebra R S
f✝ : AlgebraNorm R S
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra A S
inst✝ : IsScalarTower R A S
hinj : Function.Injective ⇑(algebraMap A S)
f : AlgebraNorm R S
r : R
x : A
⊢ f ((algebraMap A S) (r • x)) = ‖r‖ * f ((algebraMap A S) x)

Tactic:
by
    simp only [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply]
    simp only [← smul_eq_mul, algebraMap_smul, map_smul_eq_mul]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
c : α
c_ab : c > a + b
x : ι
a_x : u x < a
⊢ v x < b → (u + v) x < c

Tactic:
b_x

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
c : α
c_ab : c > a + b
x : ι
a_x : u x < a
b_x : v x < b
⊢ (u + v) x < c
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u + v)
h' : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u + v)
a : α
a_u : a < liminf u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
x : ι
a_x : a < u x
⊢ b < v x → c < (u + v) x

Tactic:
b_x

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : AddLeftMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u + v)
h' : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f (u + v)
a : α
a_u : a < liminf u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
x : ι
a_x : a < u x
b_x : b < v x
⊢ c < (u + v) x