mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
this :
  (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑n') ≤
    ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) * (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q)
⊢ ↑C * ↑γ = ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p)

Tactic:
simp_rw [eLpNormLESNormFDerivOfEqInnerConst, γ]

Goal state after:
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
this :
  (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑n') ≤
    ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) * (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q)
⊢ ↑C * ↑(NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯) =
    ↑(eLpNormLESNormFDerivOneConst μ ↑(↑(finrank ℝ E)).conjExponent *
        (↑p * (↑(finrank ℝ E) - 1) / (↑(finrank ℝ E) - ↑p)).toNNReal)
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
⊢ μHE[finrank ℝ V] = volume

Tactic:
by
  rw [← (stdOrthonormalBasis ℝ V).measurePreserving_repr_symm.map_eq,
    ← (stdOrthonormalBasis ℝ V).repr.toIsometryEquiv
      |>.symm.measurePreserving_euclideanHausdorffMeasure _ |>.map_eq,
    EuclideanSpace.euclideanHausdorffMeasure_eq_volume]
  simp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: case e_f
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
hrank : finrank ℝ ↥s.directionᗮ = finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction
⊢ volume (Prod.mk x ⁻¹' ⇑(s.direction.measurableEquivProd ↑p).symm ⁻¹' t) =
    μHE[finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction] u

Tactic:
euclideanHausdorffMeasure_eq ⟨x +ᵥ p, hxp⟩,

Goal state after:
case e_f
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
hrank : finrank ℝ ↥s.directionᗮ = finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction
⊢ volume (Prod.mk x ⁻¹' ⇑(s.direction.measurableEquivProd ↑p).symm ⁻¹' t) =
    (Measure.map (⇑(IsometryEquiv.vaddConst ⟨↑(x +ᵥ p), hxp⟩)) volume) u
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
n : ℕ
⊢ (mkMetric'.pre (fun s ↦ m (ediam s)) (↑n)⁻¹).trim = mkMetric'.pre (fun s ↦ m (ediam s)) (↑n)⁻¹

Tactic:
refine mkMetric'.trim_pre _ (fun s => ?_) _

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
n : ℕ
s : Set X
⊢ m (ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) = m (ediam 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
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
⊢ ↑(f.normDet ^ 2) = LinearMap.det (adjoint f ∘ₗ f)

Tactic:
have : CompleteSpace V := FiniteDimensional.complete 𝕜 V
  exact f.toContinuousLinearMap.normDet_sq

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : I = 0
⊢ 4⁻¹ *
      (↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ -
        -I * ↑‖I • y - x‖ * ↑‖I • y - x‖) =
    4⁻¹ *
      (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
        I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)

pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : ¬I = 0
⊢ 4⁻¹ *
      (↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ -
        -I * ↑‖I • y - x‖ * ↑‖I • y - x‖) =
    4⁻¹ *
      (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
        I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)

Tactic:
· simp only [hI, neg_zero, zero_mul]

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
hI : ¬I = 0
⊢ 4⁻¹ *
      (↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖ + -I * ↑‖I • y + x‖ * ↑‖I • y + x‖ -
        -I * ↑‖I • y - x‖ * ↑‖I • y - x‖) =
    4⁻¹ *
      (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
        I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖)
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup U
inst✝⁶ : InnerProductSpace 𝕜 U
inst✝⁵ : FiniteDimensional 𝕜 U
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace 𝕜 V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
⊢ (g ∘ₗ f).normDet = g.normDet * f.normDet

Tactic:
by_cases htop : f.range = ⊤
  · rw [normDet_comp]
    congrm ?_ * _
    suffices (g.domRestrict f.range).normDet * (id : V →ₗ[𝕜] V).normDet = g.normDet by simpa
    have : f.range = id.range := by simp [htop]
    convert! (normDet_comp LinearMap.id g).symm
  · have hker : f.ker ≠ ⊥ := by
      simpa [ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank h] using htop
    have hker' : (g ∘ₗ f).ker ≠ ⊥ := by
      contrapose hker with hbot
      simpa [hbot] using ker_le_ker_comp f g
    simp [normDet_eq_zero_iff_ker_ne_bot.mpr hker, normDet_eq_zero_iff_ker_ne_bot.mpr hker']

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr.inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
dpos : 0 < d
⊢ μH[d] {x} ≤ 1

Tactic:
have := nullSingletonClass_hausdorff X dpos
      simp only [zero_le, measure_singleton]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Reproducing

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : RKHS 𝕜 H X V
inst✝² : CompleteSpace H
inst✝¹ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
inst✝ : Fact K.PosSemidef
f : OfKernel K
h : (ContinuousLinearMap.pi fun x ↦ adjoint (kerFun K x)) f = 0
i : X × V
a : 𝕜
f✝ : X × V →₀ 𝕜
a✝² : i ∉ f✝.support
a✝¹ : a ≠ 0
a✝ : ⟪↑f✝, f⟫_𝕜 = 0
this : ⟪i.2, (ContinuousLinearMap.pi fun x ↦ adjoint (kerFun K x)) f i.1⟫_𝕜 = ⟪i.2, 0 i.1⟫_𝕜
⊢ ?m.168

Tactic:
by simpa [OfKernel.kerFun, adjoint_inner_right] using this

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
⊢ ∏ x, volume ((fun i ↦ Ioo ↑(a i) ↑(b i)) x) ≤ μH[↑(Fintype.card ι)] (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i))

Tactic:
have Hle : volume ≤ (μH[Fintype.card ι] : Measure (ι → ℝ)) := by
      refine le_hausdorffMeasure _ _ ∞ ENNReal.coe_lt_top fun s _ => ?_
      rw [ENNReal.rpow_natCast]
      exact Real.volume_pi_le_diam_pow s

Goal state after:
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
Hle : volume ≤ μH[↑(Fintype.card ι)]
⊢ ∏ x, volume ((fun i ↦ Ioo ↑(a i) ↑(b i)) x) ≤ μH[↑(Fintype.card ι)] (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i))
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ o.volumeForm ![x, y] = -o.volumeForm ![y, x]

Tactic:
convert! o.volumeForm.map_swap ![y, x] (_ : (0 : Fin 2) ≠ 1)

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ![x, y] = ![y, x] ∘ ⇑(Equiv.swap 0 1)

E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≠ 1
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪x, o.rightAngleRotationAux₁ y⟫ = -(o.areaForm x) y

Tactic:
rw [real_inner_comm]
  simp [o.areaForm_swap y x]

Goal state after:
Module: Mathlib.Analysis.Matrix.LDL

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ lower hS * diag hS * (lower hS)ᴴ = S

Tactic:
LDL.lower,

Goal state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ (lowerInv hS)⁻¹ * diag hS * (lowerInv hS)⁻¹ᴴ = S
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (o.kahler x) a * (o.kahler a) y = ↑‖a‖ ^ 2 * (o.kahler x) y

Tactic:
trans ((‖a‖ ^ 2 :) : ℂ) * o.kahler x y

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (o.kahler x) a * (o.kahler a) y = ↑(‖a‖ ^ 2) * (o.kahler x) y

E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ↑(‖a‖ ^ 2) * (o.kahler x) y = ↑‖a‖ ^ 2 * (o.kahler x) y
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin f s = ∫ (u : ℝ), cexp (-s * ↑u) • f (rexp (-u))

Tactic:
rw [mellin, ← rexp_neg_image_aux, integral_image_eq_integral_abs_deriv_smul
        MeasurableSet.univ rexp_neg_deriv_aux rexp_neg_injOn_aux]
      simp [rexp_cexp_aux]

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

Goal state before:
pp: case succ
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
s : ℂ
IH : DifferentiableAt ℂ Gamma (s + 1)
hsre : -↑(n + 1) < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
hsne : s ≠ 0
this : DifferentiableAt ℂ (Gamma ∘ fun s ↦ s + 1) s
⊢ DifferentiableAt ℂ Gamma s

Tactic:
apply (this.fun_div differentiableAt_id hsne).congr_of_eventuallyEq

Goal state after:
case succ
s✝ : ℂ
hs✝ : ∀ (m : ℕ), s✝ ≠ -↑m
n : ℕ
s : ℂ
IH : DifferentiableAt ℂ Gamma (s + 1)
hsre : -↑(n + 1) < s.re
hs : ∀ (m : ℕ), s ≠ -↑m
hsne : s ≠ 0
this : DifferentiableAt ℂ (Gamma ∘ fun s ↦ s + 1) s
⊢ Gamma =ᶠ[𝓝 s] fun i ↦ (Gamma ∘ fun s ↦ s + 1) i / id i
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case refine_1.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n

Tactic:
conv => enter [2]; rw [← div_one (‖z‖ ^ n)]

Goal state after:
case refine_1.inr
z : ℂ
hz : ‖z‖ < 1
n : ℕ
hn : n > 0
⊢ ‖z‖ ^ n / ↑n ≤ ‖z‖ ^ n / 1
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
⊢ ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t

Tactic:
refine (ae_restrict_mem measurableSet_Ioi).mono fun t ht z hz => ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a b : ℝ
f : ℝ → E
s : ℂ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s.re < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s.re
F : ℂ → ℝ → E := fun z t ↦ ↑t ^ (z - 1) • f t
F' : ℂ → ℝ → E := fun z t ↦ (↑t ^ (z - 1) * ↑(log t)) • f t
v : ℝ
hv0 : 0 < v
hv1 : v < s.re - b
hv2 : v < a - s.re
bound : ℝ → ℝ := fun t ↦ (t ^ (s.re + v - 1) + t ^ (s.re - v - 1)) * |log t| * ‖f t‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
t : ℝ
ht : t ∈ Ioi 0
z : ℂ
hz : z ∈ Metric.ball s v
⊢ ‖F' z t‖ ≤ bound t
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: 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)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x ↦ u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = F 1 - 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

Tactic:
hF1,

Goal state after:
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)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x ↦ u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0 - 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 1 / 2 * log 2 - log (3 / 2) < 0

Tactic:
rw [mul_comm, ← mul_div_assoc, div_sub' two_ne_zero]

Goal state after:
case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ (log 2 * 1 - 2 * log (3 / 2)) / 2 < 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case e'_11
⊢ Ioi (-1) = (fun x ↦ 1 / 2 * x) ⁻¹' Ioi (-(1 / 2))

Tactic:
preimage_const_mul_Ioi₀ (_ : ℝ) one_half_pos,

Goal state after:
case e'_11
⊢ Ioi (-1) = Ioi (-(1 / 2) / (1 / 2))
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case inr
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
hs : Convex k s
this : ∀ {s : Set V}, Convex k s → IsClosed[inst✝²] s → Convex k (asymptoticCone k s)
hs' : ¬IsClosed[inst✝²] s
⊢ Convex k (asymptoticCone k (closure[inst✝²] s))

Tactic:
exact this hs.closure isClosed_closure

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

Goal state before:
pp: case refine_1
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).Regular
σ : Equiv.Perm (Fin (m + 1))
x : P ≃ᵢ P
hx : (s.reindex e).points ∘ ⇑((e.symm.trans σ).trans e) = ⇑x ∘ (s.reindex e).points
⊢ ∃ x, s.points ∘ ⇑σ = ⇑x ∘ s.points

Tactic:
refine ⟨x, ?_⟩

Goal state after:
case refine_1
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).Regular
σ : Equiv.Perm (Fin (m + 1))
x : P ≃ᵢ P
hx : (s.reindex e).points ∘ ⇑((e.symm.trans σ).trans e) = ⇑x ∘ (s.reindex e).points
⊢ s.points ∘ ⇑σ = ⇑x ∘ s.points
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_2
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.Regular
σ : Equiv.Perm (Fin (n + 1))
x : P ≃ᵢ P
hx : s.points ∘ ⇑((e.trans σ).trans e.symm) = ⇑x ∘ s.points
⊢ ∃ x, (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points

Tactic:
refine ⟨x, ?_⟩

Goal state after:
case refine_2
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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.Regular
σ : Equiv.Perm (Fin (n + 1))
x : P ≃ᵢ P
hx : s.points ∘ ⇑((e.trans σ).trans e.symm) = ⇑x ∘ s.points
⊢ (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (fun x ↦ ‖f x‖) univ x
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : w ∈ {y | ‖f y‖ = M}
⊢ ∀ᶠ (y : X) in 𝓝 w, y ∈ {y | ‖f y‖ = M}

Tactic:
filter_upwards [mem_map.mp <| hf.tendsto w (Metric.ball_mem_nhds (f w) hM)] with u hu

Goal state after:
X : Type u_1
E : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (fun x ↦ ‖f x‖) univ x
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : w ∈ {y | ‖f y‖ = M}
u : X
hu : u ∈ f ⁻¹' Metric.ball (f w) M
⊢ ‖f u‖ = M
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / ↑(2 * k)! =
    ((z * I) ^ (2 * k) / ↑(2 * k)! + (-z * I) ^ (2 * k) / ↑(2 * k)!) / 2 +
      ((z * I) ^ (2 * k) * (z * I) / ↑(2 * k + 1)! + (-z * I) ^ (2 * k) * (-z * I) / ↑(2 * k + 1)!) / 2

Tactic:
pow_mul,

Goal state after:
case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦ ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2)
    ((NormedSpace.exp (z * I) + NormedSpace.exp (-z * I)) / 2)
k : ℕ
⊢ ((z * I) ^ 2) ^ k / ↑(2 * k)! =
    (((z * I) ^ 2) ^ k / ↑(2 * k)! + ((-z * I) ^ 2) ^ k / ↑(2 * k)!) / 2 +
      (((z * I) ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! + ((-z * I) ^ 2) ^ k * (-z * I) / ↑(2 * k + 1)!) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) * (z * I) / ↑(2 * k + 1)! / I =
    ((-z * I) ^ (2 * k) / ↑(2 * k)! - (z * I) ^ (2 * k) / ↑(2 * k)!) * I / 2 +
      ((-z * I) ^ (2 * k) * (-z * I) / ↑(2 * k + 1)! - (z * I) ^ (2 * k) * (z * I) / ↑(2 * k + 1)!) * I / 2

Tactic:
pow_mul,

Goal state after:
case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ ((z * I) ^ 2) ^ k * (z * I) / ↑(2 * k + 1)! / I =
    (((-z * I) ^ 2) ^ k / ↑(2 * k)! - ((z * I) ^ 2) ^ k / ↑(2 * k)!) * I / 2 +
      (((-z * I) ^ 2) ^ k * (-z * I) / ↑(2 * k + 1)! - ((z * I) ^ 2) ^ k * (z * I) / ↑(2 * k + 1)!) * I / 2
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: q : ℍ
hq : q.re = 0
n : ℕ
hq2 : q ^ 2 = -↑(normSq q)
k : ℝ := ↑(2 * n)!
⊢ k⁻¹ • q ^ (2 * n) = k⁻¹ • (-↑(normSq q)) ^ n

Tactic:
pow_mul,

Goal state after:
q : ℍ
hq : q.re = 0
n : ℕ
hq2 : q ^ 2 = -↑(normSq q)
k : ℝ := ↑(2 * n)!
⊢ k⁻¹ • (q ^ 2) ^ n = k⁻¹ • (-↑(normSq q)) ^ n