mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ ‖w‖ * ‖w‖ = 0

Tactic:
← mul_right_inj' C_pos.ne',

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
v w : V
mem_w_orthogonal : w ∈ (↑(continuousLinearMapOfBilin B)).rangeᗮ
C : ℝ
C_pos : 0 < C
coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u
⊢ C * (‖w‖ * ‖w‖) = C * 0
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
hT : ¬Dense ↑T.domain
y : ↥T†.domain
⊢ ↑T† y = 0

Tactic:
change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
  simp only [hT, not_false_iff, dif_neg, LinearMap.zero_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ Function.Injective ⇑(adjoint T ∘ₗ T) ↔ ∀ i < finrank 𝕜 E, 0 < T.singularValues i

Tactic:
← ker_eq_bot,

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
⊢ (adjoint T ∘ₗ T).ker = ⊥ ↔ ∀ i < finrank 𝕜 E, 0 < T.singularValues i
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : E ⊗[𝕜] F
hx : inner 𝕜 x x = 0
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite 𝕜 ↥E'
iF' : Module.Finite 𝕜 ↥F'
hz : {x} ⊆ ↑(mapIncl E' F').range
⊢ x = 0

Tactic:
obtain ⟨y : E' ⊗ F', rfl : mapIncl E' F' y = x⟩ := Set.singleton_subset_iff.mp hz

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
E' : Submodule 𝕜 E
F' : Submodule 𝕜 F
iE' : Module.Finite 𝕜 ↥E'
iF' : Module.Finite 𝕜 ↥F'
y : ↥E' ⊗[𝕜] ↥F'
hx : inner 𝕜 ((mapIncl E' F') y) ((mapIncl E' F') y) = 0
hz : {(mapIncl E' F') y} ⊆ ↑(mapIncl E' F').range
⊢ (mapIncl E' F') y = 0
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
⊢ T.singularValues = 0 ↔ T = 0

Tactic:
constructor <;> intro h

Goal state after:
case mp
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
h : T.singularValues = 0
⊢ T = 0

case mpr
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
h : T = 0
⊢ T.singularValues = 0
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x' : E
y y' : F
⊢ dist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖y'‖

Tactic:
grw [dist_eq_norm, norm_sub_le]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x' : E
y y' : F
⊢ ‖x ⊗ₜ[𝕜] y‖ + ‖x' ⊗ₜ[𝕜] y'‖ ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖y'‖
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] F
s : Set F
⊢ dimH (⇑e ⁻¹' s) = dimH s

Tactic:
rw [← e.image_symm_eq_preimage, e.symm.dimH_image]

Goal state after:
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
f : U →ₗᵢ[𝕜] V
⊢ f.normDet = 1

Tactic:
obtain ⟨b⟩ := (f.normDet_ne_zero_tfae.out 4 3).mp f.injective

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
f : U →ₗᵢ[𝕜] V
b : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
⊢ f.normDet = 1
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
f : U →ₗᵢ[𝕜] V
⊢ f.normDet = 1

Tactic:
by
  obtain ⟨b⟩ := (f.normDet_ne_zero_tfae.out 4 3).mp f.injective
  rw [normDet_eq_norm_det_toMatrix_rangeRestrict _ (stdOrthonormalBasis 𝕜 U) b]
  apply CStarRing.norm_of_mem_unitary
  exact Matrix.det_of_mem_unitary <| (f.equivRange).toMatrix_mem_unitaryGroup _ _

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

Goal state before:
pp: U : Type u_5
V : Type u_6
inst✝⁸ : NormedAddCommGroup U
inst✝⁷ : InnerProductSpace ℝ U
inst✝⁶ : FiniteDimensional ℝ U
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MeasurableSpace U
inst✝² : BorelSpace U
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
f : U →ₗ[ℝ] V
s : Set U
h : ¬f.ker = ⊥
this : μH[↑(finrank ℝ U)] (⇑f.range.subtypeₗᵢ '' ⇑f.rangeRestrict '' s) = 0
⊢ μH[↑(finrank ℝ U)] (⇑f '' s) = ENNReal.ofReal f.normDet * μH[↑(finrank ℝ U)] s

Tactic:
by
      simpa [(f.normDet_eq_zero_tfae.out 1 0).mp h, Set.image_image]

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

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

Tactic:
have h₁ : ‖-x - y‖ = ‖x + y‖ := by rw [← neg_add', norm_neg]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : I * I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ -
        I * 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖) =
    4⁻¹ *
      (-I *
        (𝓚 ‖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.StandardSubspace

Goal state before:
pp: case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
y : H
⊢ y ∈ S → ⟪y, x⟫.im = 0

Tactic:
hy

Goal state after:
case mp
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ (u : H), -(I • u) ∈ S → inner ℝ u x = 0
y : H
hy : y ∈ S
⊢ ⟪y, x⟫.im = 0
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: case mpr
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ y ∈ S, ⟪y, x⟫.im = 0
u✝ : H
⊢ -(I • u✝) ∈ S → inner ℝ u✝ x = 0

Tactic:
hy

Goal state after:
case mpr
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
x : H
S : ClosedSubmodule ℝ H
h : ∀ y ∈ S, ⟪y, x⟫.im = 0
u✝ : H
hy : -(I • u✝) ∈ S
⊢ inner ℝ u✝ x = 0
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 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 : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ ((OuterMeasure.comap f) (OuterMeasure.mkMetric fun r ↦ r ^ d)) s = (OuterMeasure.mkMetric fun r ↦ r ^ d) s

Tactic:
OuterMeasure.isometry_comap_mkMetric _ hf (hd.imp_left _)

Goal state after:
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 : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ (OuterMeasure.mkMetric fun r ↦ r ^ d) s = (OuterMeasure.mkMetric fun r ↦ r ^ d) s

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 : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set X
⊢ 0 ≤ d → Monotone fun r ↦ r ^ d
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case refine_2
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
i : ι
x✝ : i ∈ Finset.univ
⊢ ENNReal.ofReal (↑(b i) - ↑(a i)) ≠ ∞

Tactic:
· simp only [ENNReal.ofReal_ne_top, Ne, not_false_iff]

Goal state after:
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 : E
⊢ ⟪a, x⟫ • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) x

Tactic:
by_cases ha : a = 0
  · simp [ha]
  apply (o.basisRightAngleRotation a ha).ext
  intro i
  fin_cases i
  · simp [mul_comm, real_inner_comm]
  · simp [mul_comm, o.areaForm_swap a x]

Goal state after:
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.kahler (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.kahler x) y

Tactic:
simp only [kahler_rightAngleRotation_left, kahler_rightAngleRotation_right]

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
⊢ Complex.I * (-Complex.I * (o.kahler x) y) = (o.kahler x) y
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : StrongDual 𝕜 F ≃ StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ↑(e_dual f) = e.dualMap ↑f
⊢ ⇑e '' closure s = closure (⇑e '' s)

Tactic:
have he' (f : StrongDual 𝕜 E) : (e_dual.symm f : F →ₗ[𝕜] 𝕜) = e.symm.dualMap f := by
    simp only [DFunLike.ext'_iff, ContinuousLinearMap.coe_coe] at he ⊢
    have (g : StrongDual 𝕜 E) : ⇑g = e_dual.symm g ∘ e := by
      have := he _ ▸ congr(⇑$(e_dual.apply_symm_apply g)).symm
      simpa
    ext x
    conv_rhs => rw [LinearEquiv.dualMap_apply, ContinuousLinearMap.coe_coe, this]
    simp
  refine e.image_closure_of_convex hs ?_ ?_
  · simpa [← he] using fun f ↦ map_continuous (e_dual f)
  · simpa [← he'] using fun f ↦ map_continuous (e_dual.symm f)

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y ↦ y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (Complex.cos ∘ fun y ↦ y * (2 * z)) (-Complex.sin (↑x * (2 * z)) * (2 * z)) ↑x
c :
  HasDerivAt (fun i ↦ -(Complex.cos (↑i * (2 * z)) / (2 * z))) (-(-(Complex.sin (↑x * (2 * z)) * (2 * z)) / (2 * z))) x
⊢ HasDerivAt (fun y ↦ -Complex.cos (2 * z * ↑y) / (2 * z)) (Complex.sin (2 * z * ↑x)) x

Tactic:
field_simp at c ⊢

Goal state after:
z : ℂ
hz : z ≠ 0
x : ℝ
a : HasDerivAt (fun y ↦ y * (2 * z)) (2 * z) ↑x
b : HasDerivAt (Complex.cos ∘ fun y ↦ y * (2 * z)) (-Complex.sin (↑x * (2 * z)) * (2 * z)) ↑x
c : HasDerivAt (fun i ↦ -(Complex.cos (↑i * 2 * z) / (2 * z))) (Complex.sin (2 * z * ↑x)) x
⊢ HasDerivAt (fun y ↦ -(Complex.cos (2 * z * ↑y) / (2 * z))) (Complex.sin (2 * z * ↑x)) x
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2.hg
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)‖
⊢ IntervalIntegrable (fun t ↦ t ^ (s - b - 1)) volume 0 ε

Tactic:
exact intervalIntegral.intervalIntegrable_rpow' (by linarith)

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

Goal state before:
pp: case e'_9
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ ↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2) =
    Complex.cos ↑x * ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) ↑x +
      Complex.sin ↑x * (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x)

Tactic:
simp only [Complex.ofReal_cos, Complex.ofReal_sin]

Goal state after:
case e'_9
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ Complex.cos ↑x ^ n - (↑n - 1) * Complex.sin ↑x ^ 2 * Complex.cos ↑x ^ (n - 2) =
    Complex.cos ↑x * ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) ↑x +
      Complex.sin ↑x * (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in 0 / a..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ∫ (x : ℝ) in 0..a, ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 1))

Tactic:
zero_div

Goal state after:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
⊢ ∫ (x : ℝ) in 0..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) =
    ∫ (x : ℝ) in 0..a, ↑a ^ (s - 1) * ↑a ^ (t - 1) * (↑(x / a) ^ (s - 1) * (1 - ↑(x / a)) ^ (t - 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))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
⊢ IntegrableOn bound (Ioi 0) volume

Tactic:
simp_rw [bound, add_mul, mul_assoc]

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))
h4 : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), ∀ z ∈ Metric.ball s v, ‖F' z t‖ ≤ bound t
⊢ IntegrableOn (fun t ↦ t ^ (s.re + v - 1) * (|log t| * ‖f t‖) + t ^ (s.re - v - 1) * (|log t| * ‖f t‖)) (Ioi 0) volume
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
this✝¹ : ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n.succ) = (2 * ↑n + 1) / (2 * ↑n + 2) * C
this✝ :
  ↑π * z * (A * (1 - z ^ 2 / (↑n + 1) ^ 2)) *
      ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ) =
    ↑π * z * A * ((1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ))
this :
  (1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * B
⊢ ↑π * z * A * B / ↑C =
    ↑π * z * A *
        ((1 - z ^ 2 / ↑n.succ ^ 2) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n.succ)) /
      ↑((2 * ↑n + 1) / (2 * ↑n + 2) * C)

Tactic:
rw [this, Complex.ofReal_mul, Complex.ofReal_div]
      have : (C : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr (integral_cos_pow_pos _).ne'
      have : 2 * (n : ℂ) + 1 ≠ 0 := by
        convert! (Nat.cast_add_one_ne_zero (2 * n) : (↑(2 * n) + 1 : ℂ) ≠ 0)
        simp
      have : (n : ℂ) + 1 ≠ 0 := Nat.cast_add_one_ne_zero n
      simp [field]

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

Goal state before:
pp: case refine_1
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
⊢ 0 < y → (log ∘ f) (y + 1) = (log ∘ f) y + log y

Tactic:
hy

Goal state after:
case refine_1
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
hy : 0 < y
⊢ (log ∘ f) (y + 1) = (log ∘ f) y + log y
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
n : ℤ
y : 𝕜
⊢ AnalyticAt 𝕜 f y → logDeriv (f ^ n) y = (n • logDeriv f) y

Tactic:
hy

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
U : Set 𝕜
hf : MeromorphicOn f U
n : ℤ
y : 𝕜
hy : AnalyticAt 𝕜 f y
⊢ logDeriv (f ^ n) y = (n • logDeriv f) y
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
v : V
p : P
⊢ asymptoticNhds k P v = atTop • 𝓝 v +ᵥ pure p

Tactic:
by
  rw [← asymptoticNhds_eq_smul, asymptoticNhds_vadd_pure]

Goal state after:
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 = ↑n ^ (s - 1) * ↑n

Tactic:
conv_lhs => 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 = ↑n ^ (s - 1) * ↑n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos.ofNat
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.ofNat a✝)
⊢ Gamma (-↑a✝) * Gamma (1 - -↑a✝) = 0

Tactic:
Complex.Gamma_neg_nat_eq_zero,

Goal state after:
case pos.ofNat
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.ofNat a✝)
⊢ 0 * Gamma (1 - -↑a✝) = 0
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inl.inr
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
nth_rw 2 [dist_comm]
    apply hs.ne (a₁ := ⟨(i₁, i₂), h₁₂lt⟩) (a₂ := ⟨(i₄, i₃), h₄₃lt⟩)
    cases h₁₂₄₃ <;> simp [*]

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

Goal state before:
pp: case pos.negSucc
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.negSucc a✝)
⊢ Gamma (1 + ↑a✝) * Gamma (-↑a✝) = 0

Tactic:
Complex.Gamma_neg_nat_eq_zero,

Goal state after:
case pos.negSucc
z : ℂ
pi_ne : ↑π ≠ 0
a✝ : ℕ
hk : z = -↑(Int.negSucc a✝)
⊢ Gamma (1 + ↑a✝) * 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ
n : ℕ
ih : ∀ (z : ℂ), (∀ (k : ℕ), z ≠ -↑k) → Gamma (z + ↑n) / Gamma z = Polynomial.eval z (ascPochhammer ℂ n)
z : ℂ
hz : ∀ (k : ℕ), z ≠ -↑k
⊢ Gamma (z + ↑(n + 1)) / Gamma z = Polynomial.eval z (ascPochhammer ℂ (n + 1))

Tactic:
suffices h : Gamma (z + n + 1) = Gamma (z + n) * (z + n) by
      simp [ascPochhammer_succ_right, ← ih z hz, div_mul_eq_mul_div, h, ← add_assoc]

Goal state after:
case succ
n : ℕ
ih : ∀ (z : ℂ), (∀ (k : ℕ), z ≠ -↑k) → Gamma (z + ↑n) / Gamma z = Polynomial.eval z (ascPochhammer ℂ n)
z : ℂ
hz : ∀ (k : ℕ), z ≠ -↑k
⊢ Gamma (z + ↑n + 1) = Gamma (z + ↑n) * (z + ↑n)