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

Goal state before:
pp: d : ℕ
⊢ μH[↑d].IsAddHaarMeasure

Tactic:
by
  simpa using MeasureTheory.isAddHaarMeasure_hausdorffMeasure (E := EuclideanSpace ℝ (Fin d))

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
⊢ dimH (f '' s) ≤ dimH s

Tactic:
have : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t := by
    simpa only [holderOnWith_one] using hf
  simpa only [ENNReal.coe_one, div_one] using dimH_image_le_of_locally_holder_on zero_lt_one this

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:

Tactic:
dimH s ≤ dimH (univ : Set E) := dimH_mono (subset_univ s)
  _ = finrank ℝ E := dimH_univ_eq_finrank E
  _ < ⊤ := by simp

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

Goal state before:
pp: X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
⊢ ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : s ⊆ iUnion t),
            ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) ≤
    liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l

Tactic:
refine iSup₂_le fun ε hε => ?_

Goal state after:
X : Type u_2
inst✝³ : EMetricSpace X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
β : Type u_4
ι : β → Type u_5
inst✝ : ∀ (n : β), Countable (ι n)
s : Set X
l : Filter β
r : β → ℝ≥0∞
hr : Tendsto r l (𝓝 0)
t : (n : β) → ι n → Set X
ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), ediam (t n i) ≤ r n
hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i
m : ℝ≥0∞ → ℝ≥0∞
this : (n : β) → Encodable (ι n)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) ≤
    liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
𝕜 : 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
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hgf : (g ∘ₗ f).ker = ⊥
bw : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g ∘ₗ f).range
bw' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g.domRestrict f.range).range :=
  bw.map (LinearIsometryEquiv.ofEq (g ∘ₗ f).range (g.domRestrict f.range).range ⋯)
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet

Tactic:
rw [(g ∘ₗ f).normDet_eq_norm_det_toMatrix_rangeRestrict bu bw,
        f.normDet_eq_norm_det_toMatrix_rangeRestrict bu bv,
        (g.domRestrict f.range).normDet_eq_norm_det_toMatrix_rangeRestrict bv bw']

Goal state after:
case pos
𝕜 : 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
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
hf : f.ker = ⊥
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
hgf : (g ∘ₗ f).ker = ⊥
bw : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g ∘ₗ f).range
bw' : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥(g.domRestrict f.range).range :=
  bw.map (LinearIsometryEquiv.ofEq (g ∘ₗ f).range (g.domRestrict f.range).range ⋯)
⊢ ‖((toMatrix bu.toBasis bw.toBasis) (g ∘ₗ f).rangeRestrict).det‖ =
    ‖((toMatrix bv.toBasis bw'.toBasis) (g.domRestrict f.range).rangeRestrict).det‖ *
      ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inl.inr
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
this : 0 < ↑c ^ (d₂ - d₁)⁻¹
hr₀ : 0 ≤ ↑0
hrc : ↑0 < ↑c ^ (d₂ - d₁)⁻¹
h₂ : d₂ ≤ 0
⊢ ↑0 ^ d₂ / ↑0 ^ d₁ ≤ ↑c

Tactic:
simp only [h.trans_le h₂, ENNReal.div_top, zero_le, ENNReal.zero_rpow_of_neg,
        ENNReal.coe_zero]

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
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
x✝ : Nontrivial V
v : V
hv : v ≠ 0
tfae_1_to_2 :
  (∀ (x : X →₀ V →L[𝕜] V) (x_1 : V),
      0 ≤ RCLike.re (x.sum fun i a ↦ x.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 x_1), a x_1⟫_𝕜)) →
    ∀ (f : X × V →₀ 𝕜),
      0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)
h :
  ∀ (f : X × V →₀ 𝕜),
    0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)
vv : X →₀ V
⊢ 0 ≤ RCLike.re (vv.sum fun x w ↦ vv.sum fun x' w' ↦ ⟪(K x' x) w, w'⟫_𝕜)

Tactic:
simpa [add_mul, Finsupp.sum_sum_index] using (h (vv.sum fun x v ↦ .single ⟨x, v⟩ 1))

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

Goal state before:
pp: case inr.refine_2
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
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / ↑K
hst : f ⁻¹' s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
hft : ((fun n ↦ f ⁻¹' t n) n).Nonempty
⊢ ediam (f ⁻¹' t n) ^ d ≤ ↑K ^ d * ediam (t n) ^ d

Tactic:
rw [← ENNReal.mul_rpow_of_nonneg _ _ hd]

Goal state after:
case inr.refine_2
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
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / ↑K
hst : f ⁻¹' s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
hft : ((fun n ↦ f ⁻¹' t n) n).Nonempty
⊢ ediam (f ⁻¹' t n) ^ d ≤ (↑K * ediam (t n)) ^ d
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 Y
hs : MeasurableSet s
⊢ μH[d] (f ⁻¹' s) = (μH[d].restrict (range f)) s

Tactic:
Measure.restrict_apply hs,

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 Y
hs : MeasurableSet s
⊢ μH[d] (f ⁻¹' s) = μH[d] (s ∩ range f)
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)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ (o.areaForm (φ x)) (φ y) = (o.areaForm x) y

Tactic:
by
  convert! o.areaForm_map φ (φ x) (φ y)
  · symm
    rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
    rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]
  · simp
  · simp

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 : E
K : Submodule ℝ E := ℝ ∙ x
⊢ finrank ℝ ↥K ≤ {x}.card

Tactic:
← Set.toFinset_singleton

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
⊢ finrank ℝ ↥K ≤ {x}.toFinset.card
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 : E
⊢ o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x) = -x

Tactic:
apply ext_inner_left ℝ
  intro y
  have : ⟪o.rightAngleRotationAux₁ y, o.rightAngleRotationAux₁ x⟫ = ⟪y, x⟫ :=
    LinearIsometry.inner_map_map o.rightAngleRotationAux₂ y x
  rw [o.inner_rightAngleRotationAux₁_right, ← o.inner_rightAngleRotationAux₁_left, this,
    inner_neg_right]

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ cexp (-↑x) ^ (1 + (s - 1)) • f = cexp (-s * ↑x) • f

Tactic:
cpow_def_of_ne_zero (Complex.exp_ne_zero _),

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ cexp (Complex.log (cexp (-↑x)) * (1 + (s - 1))) • f = cexp (-s * ↑x) • f
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin (fun t ↦ f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

Tactic:
by_cases hE : CompleteSpace E

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : CompleteSpace E
⊢ mellin (fun t ↦ f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)

case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : ¬CompleteSpace E
⊢ mellin (fun t ↦ f (t ^ 0)) s = |0|⁻¹ • mellin f (s / ↑0)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_2
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 : ℝ) in 0..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) =
    ∫ (x : ℝ) in 0..π / 2, ↑(sin x) * ↑(cos x) ^ (n - 1) * Complex.sin (2 * z * ↑x)

pp: case e'_3
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
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    ↑(sin (π / 2)) * ↑(cos (π / 2)) ^ (n - 1) * (-Complex.cos (2 * z * ↑(π / 2)) / (2 * z)) -
        ↑(sin 0) * ↑(cos 0) ^ (n - 1) * (-Complex.cos (2 * z * ↑0) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))

pp: case convert_1
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
⊢ IntervalIntegrable (fun x ↦ ↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) volume 0 (π / 2)

pp: case convert_2
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
⊢ IntervalIntegrable (fun x ↦ Complex.sin (2 * z * ↑x)) volume 0 (π / 2)

Tactic:
· refine integral_congr fun x _ => ?_
    ring_nf

Goal state after:
case e'_3
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
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) -
      (↑n - 1) / (2 * z) * ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (n - 2) =
    ↑(sin (π / 2)) * ↑(cos (π / 2)) ^ (n - 1) * (-Complex.cos (2 * z * ↑(π / 2)) / (2 * z)) -
        ↑(sin 0) * ↑(cos 0) ^ (n - 1) * (-Complex.cos (2 * z * ↑0) / (2 * z)) -
      ∫ (x : ℝ) in 0..π / 2,
        (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) * (-Complex.cos (2 * z * ↑x) / (2 * z))

case convert_1
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
⊢ IntervalIntegrable (fun x ↦ ↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) volume 0 (π / 2)

case convert_2
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
⊢ IntervalIntegrable (fun x ↦ Complex.sin (2 * z * ↑x)) volume 0 (π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

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

Tactic:
cpow_add 1 _ ha',

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

Goal state before:
pp: case succ
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + ↑n) = f x + ∑ m ∈ Finset.range n, log (x + ↑m)
this : x + ↑n.succ = x + ↑n + 1
⊢ f x + ∑ m ∈ Finset.range n, log (x + ↑m) + log (x + ↑n) = f x + ∑ m ∈ Finset.range (n + 1), log (x + ↑m)

Tactic:
rw [Finset.range_add_one, Finset.sum_insert Finset.notMem_range_self]

Goal state after:
case succ
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + ↑n) = f x + ∑ m ∈ Finset.range n, log (x + ↑m)
this : x + ↑n.succ = x + ↑n + 1
⊢ f x + ∑ m ∈ Finset.range n, log (x + ↑m) + log (x + ↑n) =
    f x + (log (x + ↑n) + ∑ x_1 ∈ Finset.range n, log (x + ↑x_1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))

Tactic:
refine this ⌈x - 1⌉₊ ?_ ?_

Goal state after:
case refine_1
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ ↑⌈x - 1⌉₊ < x

case refine_2
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
this : ∀ (m : ℕ), ↑m < x → x ≤ ↑m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 (f x - f 1))
⊢ x ≤ ↑⌈x - 1⌉₊ + 1
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
s : Finset ι
F : ι → 𝕜 → 𝕜'
h : ∀ i ∈ s, MeromorphicOn (F i) U
h' : ∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ s, F i y ≠ 0
⊢ logDeriv (∏ i ∈ s, F i) y = ∑ c ∈ s, logDeriv (F c) y

Tactic:
Finset.prod_fn

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
s : Finset ι
F : ι → 𝕜 → 𝕜'
h : ∀ i ∈ s, MeromorphicOn (F i) U
h' : ∀ i ∈ s, ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ s, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ s, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ s, F i y ≠ 0
⊢ logDeriv (fun a ↦ ∏ c ∈ s, F c a) y = ∑ c ∈ s, logDeriv (F c) y
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
s : Finset ι
F : ι → 𝕜 → 𝕜'
h : ∀ i ∈ s, Meromorphic (F i)
h' : ∀ i ∈ s, ∀ (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤
⊢ logDeriv (∏ i ∈ s, F i) =ᶠ[codiscrete 𝕜] ∑ i ∈ s, logDeriv (F i)

Tactic:
by
  apply MeromorphicOn.logDeriv_prod_eventuallyEq (fun i hi ↦ meromorphicOn_univ.mpr (h i hi))
  aesop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ hd.toFinset, F i y ≠ 0
h₀ : ∏ᶠ (i : ι), F i ^ d i = ∏ i ∈ hd.toFinset, F i ^ d i
⊢ logDeriv (∏ᶠ (i : ι), F i ^ d i) y = ∑ᶠ (i : ι), d i • logDeriv (F i) y

Tactic:
have hsub : support (fun i ↦ d i • logDeriv (F i) y) ⊆ hd.toFinset := by
    simp +contextual [-support_mul, -mul_eq_zero, Set.subset_def, not_imp_not]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ hd.toFinset, F i y ≠ 0
h₀ : ∏ᶠ (i : ι), F i ^ d i = ∏ i ∈ hd.toFinset, F i ^ d i
hsub : (support fun i ↦ d i • logDeriv (F i) y) ⊆ ↑hd.toFinset
⊢ logDeriv (∏ᶠ (i : ι), F i ^ d i) y = ∑ᶠ (i : ι), d i • logDeriv (F i) y
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ hd.toFinset, F i y ≠ 0
h₀ : ∏ᶠ (i : ι), F i ^ d i = ∏ i ∈ hd.toFinset, F i ^ d i
hsub : (support fun i ↦ d i • logDeriv (F i) y) ⊆ ↑hd.toFinset
⊢ logDeriv (∏ i ∈ hd.toFinset, F i ^ d i) y = logDeriv (fun z ↦ ∏ i ∈ hd.toFinset, (F i ^ d i) z) y

Tactic:
Finset.prod_fn

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ hd.toFinset, F i y ≠ 0
h₀ : ∏ᶠ (i : ι), F i ^ d i = ∏ i ∈ hd.toFinset, F i ^ d i
hsub : (support fun i ↦ d i • logDeriv (F i) y) ⊆ ↑hd.toFinset
⊢ logDeriv (fun a ↦ ∏ c ∈ hd.toFinset, (F c ^ d c) a) y = logDeriv (fun z ↦ ∏ i ∈ hd.toFinset, (F i ^ d i) z) y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
n : ℕ
hn : n ≠ 0
| ↑n / (↑n + 1 + s) * (↑n ^ s * ↑n ! / ((∏ k ∈ Finset.range n, (s + ↑(k + 1))) * s))

Tactic:
div_mul_div_comm,

Goal state after:
s : ℂ
n : ℕ
hn : n ≠ 0
| ↑n * (↑n ^ s * ↑n !) / ((↑n + 1 + s) * ((∏ k ∈ Finset.range n, (s + ↑(k + 1))) * s))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ (↑n ^ z * ↑n ! / ∏ j ∈ Finset.range (n + 1), (z + ↑j)) *
      (↑n ^ (1 - z) * ↑n ! / ∏ j ∈ Finset.range (n + 1), (1 - z + ↑j)) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))

Tactic:
div_mul_div_comm,

Goal state after:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ ↑n ^ z * ↑n ! * (↑n ^ (1 - z) * ↑n !) /
      ((∏ j ∈ Finset.range (n + 1), (z + ↑j)) * ∏ j ∈ Finset.range (n + 1), (1 - z + ↑j)) =
    ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k Finset.univ p) (w i)]
⊢ ∃ w',
    ∑ j, w' j = 1 ∧
      (Finset.affineCombination k Finset.univ p) w' = p' ∧
        ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j

Tactic:
by
  classical
  obtain ⟨w'', fs'', hw'', hw''p', hi⟩ := hp.exists_affineCombination_eq_smul_eq hs hw hp'
  refine ⟨Set.indicator fs'' w'', ?_, ?_, ?_⟩
  · rw [← hw'']
    exact Finset.sum_indicator_subset _ (by simp)
  · rw [← hw''p']
    exact (Finset.affineCombination_indicator_subset _ _ (by simp)).symm
  · intro i
    obtain ⟨r, hr⟩ := hi i
    refine ⟨r, fun j ↦ ?_⟩
    convert! hr j using 1
    · simp [Set.indicator_apply]
    · by_cases hj : j = (i : ι) <;> simp [Set.indicator_apply, hj]

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, s.points ∘ ⇑σ = ⇑x ∘ s.points

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, (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points

Tactic:
· rcases h ((e.symm.trans σ).trans e) with ⟨x, hx⟩
    refine ⟨x, ?_⟩
    ext i
    simpa using congrFun hx (e i)

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, (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: z : ℂ
⊢ (fun n ↦ (-1) ^ n * (z ^ 2) ^ n * (z / ↑(2 * n + 1)!)) = fun n ↦ (z ^ 2) ^ n * z * (-1) ^ n * (I / ↑(2 * n + 1)! / I)

Tactic:
div_right_comm,

Goal state after:
z : ℂ
⊢ (fun n ↦ (-1) ^ n * (z ^ 2) ^ n * (z / ↑(2 * n + 1)!)) = fun n ↦ (z ^ 2) ^ n * z * (-1) ^ n * (I / I / ↑(2 * n + 1)!)
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case pos.refine_1
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : DecidableEq R
x y : R
h : x * y = 0
⊢ 0 ≤ AddGroupSeminorm.toFun 1 x

Tactic:
change _ ≤ ite _ _ _
              split_ifs
              exacts [le_rfl, zero_le_one]

Goal state after: