mathlib-initiative/mathlib-tactics huggingface dataset:
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
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis * bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis = 1
this : ‖(bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * h.some.toBasis.toMatrix ⇑bv.toBasis).det‖ = 1
⊢ ‖(bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * h.some.toBasis.toMatrix ⇑bv.toBasis).det‖ *
      ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖ =
    ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
rw [this, one_mul]

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

Goal state before:
pp: 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
⊢ t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u

Tactic:
ext x

Goal state after:
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
x : P
⊢ x ∈ t ∩ ↑(mk' (↑(x✝ +ᵥ p)) s.directionᗮ) ↔ x ∈ Subtype.val '' u
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: case e_μ
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
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
v' : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, ⋯⟩
⊢ volume = ‖v‖ₑ • map (⇑f) volume

Tactic:
suffices volume = ‖v'‖ₑ • volume.map f by simpa [v']

Goal state after:
case e_μ
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
p : P
v : V
hv : v ≠ 0
t : Set P
ht : MeasurableSet t
hrank : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction = 1
hrank' : finrank ℝ ↥(AffineSubspace.mk' p (ℝ ∙ v)).directionᗮ = finrank ℝ V - 1
f : ℝ ≃L[ℝ] ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction :=
  (ContinuousLinearEquiv.toSpanNonzeroSingleton ℝ v hv).trans
    (ContinuousLinearEquiv.ofEq (ℝ ∙ v) (AffineSubspace.mk' p (ℝ ∙ v)).direction ⋯)
hf : MeasurableEmbedding ⇑f
p' : ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⟨p, ⋯⟩
g : ℝ → ↥(AffineSubspace.mk' p (ℝ ∙ v)) := ⇑(IsometryEquiv.vaddConst p') ∘ ⇑f
hadd : MeasurableEmbedding ⇑(IsometryEquiv.vaddConst p')
hg : MeasurableEmbedding g
v' : ↥(AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, ⋯⟩
⊢ volume = ‖v'‖ₑ • map (⇑f) volume
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
⊢ ∀ (c : ℝ≥0), c ≠ 0 → μH[d₂] s ≤ ↑c * μH[d₁] s

Tactic:
intro c hc

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h : d₁ < d₂
s : Set X
H : μH[d₂] s ≠ 0 ∧ μH[d₁] s ≠ ∞
c : ℝ≥0
hc : c ≠ 0
⊢ μH[d₂] s ≤ ↑c * μH[d₁] s
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ Sᗮ.mulI = S.symplComp

Tactic:
ext x

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ (↑Sᗮ.mulI).carrier ↔ x ∈ (↑S.symplComp).carrier
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
⊢ S.mulI.mulI = S

Tactic:
ext x

Goal state after:
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ (↑S.mulI.mulI).carrier ↔ x ∈ (↑S).carrier
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
⊢ ∀ x ∈ spectrum ℝ f, 0 ≤ x

Tactic:
intro c hc

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 : ℝ
hc : c ∈ spectrum ℝ f
⊢ 0 ≤ c
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
n : ℕ
a✝ : True
⊢ ‖c‖ ^ n ≤ 1

Tactic:
hc1,

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
n : ℕ
a✝ : True
⊢ 1 ^ n ≤ 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
⊢ (o.kahler x) (o.rightAngleRotation y) = Complex.I * (o.kahler x) y

Tactic:
simp only [o.areaForm_rightAngleRotation_right, o.inner_rightAngleRotation_right,
    o.kahler_apply_apply, Complex.ofReal_neg, Complex.real_smul]
  linear_combination -ω x y * Complex.I_sq

Goal state after:
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
f : StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : StrongDual 𝕜 E), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
⊢ ⇑(e_dual.symm f) = ⇑(e.symm.dualMap ↑f)

Tactic:
ext x

Goal state after:
𝕜 : 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
f : StrongDual 𝕜 E
he : ∀ (f : StrongDual 𝕜 F), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
this : ∀ (g : StrongDual 𝕜 E), ⇑g = ⇑(e_dual.symm g) ∘ ⇑e
x : F
⊢ (e_dual.symm f) x = (e.symm.dualMap ↑f) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case convert_2
s : ℂ
hs : 0 < s.re
⊢ MeasureTheory.LocallyIntegrableOn (fun x ↦ ↑(rexp (-x))) (Ioi 0) MeasureTheory.volume

Tactic:
refine (Continuous.continuousOn ?_).locallyIntegrableOn measurableSet_Ioi

Goal state after:
case convert_2
s : ℂ
hs : 0 < s.re
⊢ Continuous fun x ↦ ↑(rexp (-x))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ↑s ≠ -↑m

Tactic:
simp_rw [← Complex.ofReal_natCast, ← Complex.ofReal_neg, Ne, Complex.ofReal_inj]

Goal state after:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ¬s = -↑m
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
⊢ 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))

Tactic:
← sub_eq_add_neg,

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.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)
t : ℝ
ht : 0 < t
⊢ t ^ (a - b + -a) = t ^ (-b)

Tactic:
← sub_eq_add_neg,

Goal state after:
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)
t : ℝ
ht : 0 < t
⊢ t ^ (a - b - a) = t ^ (-b)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, (-1) ^ (i + 1) * z ^ i / ↑i) atTop (nhds (log (1 + z)))

Tactic:
rw [← tendsto_sub_nhds_zero_iff]

Goal state after:
case refine_2
z : ℂ
hz : ‖z‖ < 1
⊢ Tendsto (fun x ↦ ∑ i ∈ Finset.range x, (-1) ^ (i + 1) * z ^ i / ↑i - log (1 + z)) atTop (nhds 0)
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
w : ℝ
hw1 : 0 < w
hw2 : w < a - s.re
w' : ℝ
hw1' : 0 < w'
hw2' : w' < s.re - b
⊢ ∃ v, 0 < v ∧ v < s.re - b ∧ v < a - s.re

Tactic:
exact
      ⟨min w w', lt_min hw1 hw1', (min_le_right _ _).trans_lt hw2', (min_le_left _ _).trans_lt hw2⟩

Goal state after:
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‖
⊢ MellinConvergent (fun t ↦ log t • f t) s ∧ HasDerivAt (mellin f) (mellin (fun t ↦ log t • f t) s) s

Tactic:
have h1 : ∀ᶠ z : ℂ in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict <| Ioi 0) := by
    refine Eventually.of_forall fun z => AEStronglyMeasurable.smul ?_ hfc.aestronglyMeasurable
    refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
    refine continuousOn_of_forall_continuousAt fun t ht => ?_
    exact continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_gt ht)

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))
⊢ MellinConvergent (fun t ↦ log t • f t) s ∧ HasDerivAt (mellin f) (mellin (fun t ↦ log t • f t) s) s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))

Tactic:
(by abel : s + t - 1 = 1 + (s - 1) + (t - 1)),

Goal state after:
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
⊢ ↑a ^ (1 + (s - 1) + (t - 1)) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
⊢ 0 < ↑n - 1

Tactic:
rw [← Nat.cast_one, sub_pos, Nat.cast_lt]

Goal state after:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
⊢ 1 < n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u * u.betaIntegral (↑n.succ + 1) = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u.betaIntegral (↑(n + 1) + 1) = ↑(n + 1)! / ∏ j ∈ Finset.range (n + 1 + 1), (u + ↑j)

Tactic:
mul_comm u _,

Goal state after:
case succ.refine_2
n : ℕ
IH : ∀ {u : ℂ}, 0 < u.re → u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
u : ℂ
hu : 0 < u.re
this : u.betaIntegral (↑n.succ + 1) * u = ↑n.succ * (u + 1).betaIntegral ↑n.succ
⊢ u.betaIntegral (↑(n + 1) + 1) = ↑(n + 1)! / ∏ j ∈ Finset.range (n + 1 + 1), (u + ↑j)
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
α : Type u_4
l : Filter α
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P
⊢ (asymptoticNhds k P v).NeBot

Tactic:
rw [asymptoticNhds_eq_smul_vadd v p]

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
α : Type u_4
l : Filter α
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P
⊢ (atTop • 𝓝 v +ᵥ pure p).NeBot
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
c : k
hc : 0 < c
p : P
⊢ map₂ (fun x1 x2 ↦ x1 • x2) atTop (map (fun x ↦ c • x) (𝓝 v)) +ᵥ pure p =
    map₂ (fun x1 x2 ↦ x1 • x2) atTop (𝓝 v) +ᵥ pure p

Tactic:
map₂_map_right,

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
v : V
c : k
hc : 0 < c
p : P
⊢ map₂ (fun a b ↦ a • c • b) atTop (𝓝 v) +ᵥ pure p = map₂ (fun x1 x2 ↦ x1 • x2) atTop (𝓝 v) +ᵥ pure p
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
h₁ : c • v +ᵥ p ∈ s
h₂ : c • u +ᵥ p ∈ s
⊢ ((c * a) • v + (c * b) • u) +ᵥ p ∈ [c • v +ᵥ p -[k] c • u +ᵥ p]

Tactic:
rw [← affineSegment_eq_segment, mem_vadd_const_affineSegment, affineSegment_eq_segment]

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
h₁ : c • v +ᵥ p ∈ s
h₂ : c • u +ᵥ p ∈ s
⊢ (c * a) • v + (c * b) • u ∈ [c • v -[k] c • u]
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:
apply hs.ne (a₁ := ⟨(i₁, i₂), h₁₂lt⟩) (a₂ := ⟨(i₄, i₃), h₄₃lt⟩)

Goal state after:
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₃
⊢ ⟨(i₁, i₂), h₁₂lt⟩ ≠ ⟨(i₄, i₃), h₄₃lt⟩
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
⊢ Gamma s ≠ 0

Tactic:
have : sin (↑π * s) ≠ 0 := by
      rw [Complex.sin_ne_zero_iff]
      intro k
      apply_fun im
      rw [im_ofReal_mul, ← ofReal_intCast, ← ofReal_mul, ofReal_im]
      exact mul_ne_zero Real.pi_pos.ne' h_im
    have A := div_ne_zero (ofReal_ne_zero.mpr Real.pi_pos.ne') this
    rw [← Complex.Gamma_mul_Gamma_one_sub s, mul_ne_zero_iff] at A
    exact A.1

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

Goal state before:
pp: s : ℝ
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π

Tactic:
rw [← ofReal_inj]
  simpa only [← Gamma_ofReal, ofReal_cpow zero_le_two, ofReal_mul, ofReal_add, ofReal_div,
    ofReal_sub] using! Complex.Gamma_mul_Gamma_add_half ↑s

Goal state after:
Module: Mathlib.Analysis.Polynomial.Factorization

Goal state before:
pp: case inl
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
have hg₂ := of_mul_left hd₁ <| (show 2 + n = 1 + (n + 1) by lia) ▸ hf
    obtain ⟨p₁, p₂, hp₁ | hp₂, h'⟩ := hg₂.eq_isMonicOfDegree_one_or_two_mul
    · rw [h', ← mul_assoc] at h hf
      exact ⟨g₁ * p₁, p₂, hd₁.mul hp₁, (hd₁.mul hp₁).of_mul_left hf, h⟩
    · rw [h', mul_left_comm] at h hf
      exact ⟨p₁, g₁ * p₂, hp₂, of_mul_left hp₂ hf, h⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedField F
inst✝ : NormedAlgebra ℝ F
⊢ Algebra.IsAlgebraic ℝ F

Tactic:
refine ⟨fun x ↦ ?_⟩

Goal state after:
F : Type u_2
inst✝¹ : NormedField F
inst✝ : NormedAlgebra ℝ F
x : F
⊢ IsAlgebraic ℝ x
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedField F
inst✝ : NormedAlgebra ℝ F
this : Algebra.IsAlgebraic ℝ F
⊢ Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ)

Tactic:
exact _root_.Real.nonempty_algEquiv_or F

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk.mk
R : Type u_1
inst✝ : NonUnitalRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
mul_le'✝¹ :
  ∀ (x y : R), toAddGroupSeminorm✝¹.toFun (x * y) ≤ toAddGroupSeminorm✝¹.toFun x * toAddGroupSeminorm✝¹.toFun y
toAddGroupSeminorm✝ : AddGroupSeminorm R
mul_le'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) ≤ toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, mul_le' := mul_le'✝¹ } =
    (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ }
⊢ toAddGroupSeminorm✝¹ = toAddGroupSeminorm✝

Tactic:
ext x

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonUnitalRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
mul_le'✝¹ :
  ∀ (x y : R), toAddGroupSeminorm✝¹.toFun (x * y) ≤ toAddGroupSeminorm✝¹.toFun x * toAddGroupSeminorm✝¹.toFun y
toAddGroupSeminorm✝ : AddGroupSeminorm R
mul_le'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) ≤ toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, mul_le' := mul_le'✝¹ } =
    (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ }
x : R
⊢ toAddGroupSeminorm✝¹ x = toAddGroupSeminorm✝ x