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

Goal state before:
pp: case pos
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
⊢ eLpNorm u (↑p') μ ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
eLpNorm_nnreal_eq_lintegral hp'0,

Goal state after:
case pos
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
⊢ (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑p') ≤ ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ
Module: Mathlib.Analysis.InnerProductSpace.LinearPMap

Goal state before:
pp: case h
𝕜 : 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
x : F × E
h : ∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ = ⟪a, x.2⟫
hx : x.1 ∈ T†.domain
⊢ ↑T† ⟨x.1, ⋯⟩ = x.2

Tactic:
apply hT.eq_of_inner_right 𝕜

Goal state after:
case h
𝕜 : 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
x : F × E
h : ∀ (a : E) (a_1 : a ∈ T.domain), ⟪↑T ⟨a, ⋯⟩, x.1⟫ = ⟪a, x.2⟫
hx : x.1 ∈ T†.domain
⊢ ∀ v ∈ ↑T.domain, ⟪v, ↑T† ⟨x.1, ⋯⟩⟫ = ⟪v, x.2⟫
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
y : F
⊢ ‖x ⊗ₜ[𝕜] y‖₊ = ‖x‖₊ * ‖y‖₊

Tactic:
by simp [← NNReal.coe_inj]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E ⊗[𝕜] 𝕜
⊢ ‖(TensorProduct.rid 𝕜 E) x‖₊ = ‖x‖₊

Tactic:
by simp [← NNReal.coe_inj]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤ RCLike.re (∑ x, ∑ x_1, ∑ x_2, A x x_2 * inner 𝕜 (g x_2) (g x_1) * star (A x x_1))

Tactic:
← starRingEnd_self_apply (A _ _),

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ∀ (i j : Fin n),
    ‖f‖ ^ 2 • inner 𝕜 (e i) (e j) - (∑ i, Matrix.vecMulVec (A i) (star (A i))) i j = inner 𝕜 (f (e i)) (f (e j))
⊢ 0 ≤
    RCLike.re
      (∑ x,
        ∑ x_1,
          ∑ x_2,
            (starRingEnd 𝕜) ((starRingEnd 𝕜) (A x x_2)) * inner 𝕜 (g x_2) (g x_1) *
              star ((starRingEnd 𝕜) ((starRingEnd 𝕜) (A x x_1))))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
x : X
hxs : x ∈ s
hxt : x ∉ t
⊢ x ∈ ⋃ n, S n

Tactic:
mem_iff_infEDist_zero_of_closed ht

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
x : X
hxs : x ∈ s
hxt : ¬infEDist x t = 0
⊢ x ∈ ⋃ n, S n
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
s t : Set X
⊢ dimH (s ∪ t) = max (dimH s) (dimH t)

Tactic:
rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond]

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
⊢ normDet 0 = 0 ^ finrank 𝕜 U

Tactic:
nontriviality U

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
a✝ : Nontrivial U
⊢ normDet 0 = 0 ^ finrank 𝕜 U
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case pos
𝕜 : 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
c : 𝕜
hc : c = 0
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet

Tactic:
nontriviality U

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
c : 𝕜
hc : c = 0
a✝ : Nontrivial U
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
ε : ℝ≥0∞
hε : id ε > 0
h_mono : Monotone m
s t : { s // s.Nonempty }
hst : s ≤ t
ht : ediam ↑t ≤ ε
⊢ ⨅ (_ : ediam ↑s ≤ ε), m (ediam ↑s) ≤ m (ediam ↑s)

Tactic:
simp only [(ediam_mono hst).trans ht, le_refl, ciInf_pos]

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

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
⊢ (map f) (mkMetric m) = (restrict (range f)) (mkMetric m)

Tactic:
← isometry_comap_mkMetric _ hf H,

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
m : ℝ≥0∞ → ℝ≥0∞
f : X → Y
hf : Isometry f
H : Monotone m ∨ Surjective f
⊢ (map f) ((comap f) (mkMetric m)) = (restrict (range f)) (mkMetric m)
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: 𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
h : ¬f.ker = ⊥
h0 : (Matrix.gram 𝕜 fun x ↦ f.rangeRestrict (b x)).det ≠ 0
⊢ finrank 𝕜 U ≤ finrank 𝕜 ↥f.range

Tactic:
finrank_eq_card_basis b.toBasis

Goal state after:
𝕜 : Type u_1
U : Type u_2
V : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup U
inst✝⁵ : InnerProductSpace 𝕜 U
inst✝⁴ : FiniteDimensional 𝕜 U
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace 𝕜 V
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
h : ¬f.ker = ⊥
h0 : (Matrix.gram 𝕜 fun x ↦ f.rangeRestrict (b x)).det ≠ 0
⊢ Fintype.card ι ≤ finrank 𝕜 ↥f.range
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)
ε : ℝ≥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

Tactic:
refine le_of_forall_gt_imp_ge_of_dense fun c hc => ?_

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 < ε
c : ℝ≥0∞
hc : liminf (fun n ↦ ∑' (i : ι n), m (ediam (t n i))) l < c
⊢ ⨅ t, ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ ε), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n)) ≤ c
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.mulIᗮ

Tactic:
by
  rw [mulI_orthogonal_eq_symplComp]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Goal state before:
pp: case refine_2
𝕜 : 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
⊢ ∀ (i' : ℕ), True → c ^ i' • b i' ∈ 𝓝 0

Tactic:
intro n _
      simpa using smul_mem_nhds_smul₀ (pow_ne_zero n c_ne) (bE1 n).1

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

Goal state before:
pp: ⊢ Measure.map ⇑(MeasurableEquiv.funUnique Unit ℝ) μH[1] =
    Measure.map ⇑(MeasurableEquiv.funUnique Unit ℝ) μH[↑(Fintype.card Unit)]

Tactic:
Fintype.card_unit,

Goal state after:
⊢ Measure.map ⇑(MeasurableEquiv.funUnique Unit ℝ) μH[1] = Measure.map ⇑(MeasurableEquiv.funUnique Unit ℝ) μH[↑1]
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:
rw [LDL.lower, conjTranspose_nonsing_inv, Matrix.mul_assoc,
    Matrix.inv_mul_eq_iff_eq_mul_of_invertible (LDL.lowerInv hS),
    Matrix.mul_inv_eq_iff_eq_mul_of_invertible]
  exact LDL.diag_eq_lowerInv_conj hS

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u ↦ rexp (-σ * u) • f (rexp (-u))
hf : Integrable (fun x ↦ cexp (-↑σ * ↑x) • f (rexp (-x))) volume
⊢ Integrable g volume

Tactic:
norm_cast at hf

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

Goal state before:
pp: case pos
s : ℂ
hs : s ≠ 0
h : ∃ m, s = -↑m
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s

pp: case neg
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -↑m
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s

Tactic:
· obtain ⟨m, rfl⟩ := h
    rw [← sub_neg_eq_add, ← neg_sub', ← Nat.cast_one, ← Nat.cast_sub,
      deriv_zero_of_not_differentiableAt (not_differentiableAt_Gamma_neg_nat m),
      deriv_zero_of_not_differentiableAt (not_differentiableAt_Gamma_neg_nat (m - 1)),
      Gamma_neg_nat_eq_zero, zero_add, mul_zero]
    rwa [neg_ne_zero, Nat.cast_ne_zero, ← Nat.one_le_iff_ne_zero] at hs

Goal state after:
case neg
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -↑m
⊢ deriv Gamma (s + 1) = Gamma s + s * deriv Gamma s
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case e'_4
z : ℂ
hz : ‖z‖ < 1
⊢ 2 = ↑1 + 1

Tactic:
· norm_num

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

Goal state before:
pp: case e'_9.e_a
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 = Complex.cos ↑x * Complex.cos ↑x ^ (n - 1)

Tactic:
rw [← pow_succ', Nat.sub_add_cancel (by lia : 1 ≤ n)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

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

Tactic:
apply ((continuous_exp.tendsto _).comp (tendsto_mul_log_one_add_of_tendsto hg)).congr'

Goal state after:
g : ℝ → ℂ
t : ℂ
hg : Tendsto (fun x ↦ ↑x * g x) atTop (𝓝 t)
⊢ (cexp ∘ fun x ↦ ↑x * log (1 + g x)) =ᶠ[atTop] fun x ↦ (1 + g x) ^ ↑x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_4
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ (1 - ↑(-x)) ^ (v - 1) * ↑(-x) ^ (u - 1) = ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)

Tactic:
congr 2 <;> · push_cast; ring

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

Goal state before:
pp: case e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -(1 / 2) = 1 / 2 - 1

pp: case e'_7
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -1 = 0 - 1

Tactic:
· norm_num

Goal state after:
case e'_7
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -1 = 0 - 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: n : ℕ
⊢ (∫ (x : ℝ) in 0..π / 2, cos x ^ n) / 1 * 2 = ∫ (x : ℝ) in 0..π, sin x ^ n

Tactic:
div_one,

Goal state after:
n : ℕ
⊢ (∫ (x : ℝ) in 0..π / 2, cos x ^ n) * 2 = ∫ (x : ℝ) in 0..π, sin x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ cos x ^ n = sin (x + π / 2) ^ n

Tactic:
sin_add_pi_div_two

Goal state after:
case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ cos x ^ n = cos x ^ n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

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

Tactic:
rw [sub_add_cancel, Nat.sub_add_cancel hn] at this

Goal state after:
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
m : ℕ
x : ℝ
hm : Tendsto (logGammaSeq (x - 1)) atTop (𝓝 (f (x - 1) - f 1))
hx : 0 < x
hy : ↑m < x - 1
hy' : x - 1 ≤ ↑m + 1
n : ℕ
hn : 1 ≤ n
this : logGammaSeq x (n - 1) = logGammaSeq (x - 1) n + log (x - 1) - x * (log (↑(n - 1) + 1) - log ↑(n - 1))
⊢ logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
n : ℕ
⊢ u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)

Tactic:
induction n generalizing u with

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

Tactic:
← pow_two

Goal state after:
z : ℂ
n : ℕ
hn : n ≠ 0
aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)
⊢ ↑n ^ z * ↑n ^ (1 - z) * ↑n ! ^ 2 /
      ((∏ 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.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg.convert_3
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ Tendsto (fun n ↦ ↑n / (↑n + 1 - z)) atTop (𝓝 1)

Tactic:
convert! tendsto_natCast_div_add_atTop (1 - z) using 1

Goal state after:
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
⊢ (fun n ↦ ↑n / (↑n + 1 - z)) = fun n ↦ ↑n / (↑n + (1 - z))
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inr.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:
· rw [dist_comm]
    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 inr
⊢ (Gamma 0)⁻¹ = 0 * (Gamma (0 + 1))⁻¹

Tactic:
· rw [zero_add, Gamma_zero, inv_zero, zero_mul]

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

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

Tactic:
exact ⟨g₁ * p₁, p₂, hd₁.mul hp₁, (hd₁.mul hp₁).of_mul_left hf, h⟩

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

Goal state before:
pp: case hx
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ MulOpposite.op (inr m).fst • (inr m).snd = (inr m).fst • (inr m).snd

Tactic:
rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]

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

Goal state before:
pp: m : Type u_1
𝔸 : Type u_5
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
A : Matrix m m 𝔸
⊢ exp (-A) = (exp A)⁻¹

Tactic:
rw [nonsing_inv_eq_ringInverse]
  open scoped Norms.Operator in exact (Ring.inverse_exp A).symm

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

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto (fun x_1 ↦ φ x x_1) (cobounded (ℝ × ℝ)) (cobounded F)

Tactic:
by
  simp_rw [φ, sub_add]
  refine tendsto_const_sub_cobounded _ |>.comp ?_
  rw [← tendsto_norm_atTop_iff_cobounded]
  -- split into statements involving each of the two components separately.
  refine Tendsto.coprod_of_prod_top_right (α := ℝ) (fun s hs ↦ ?_) ?_
    -- the first component is bounded and the second one is unbounded
  · rw [← isCobounded_def, ← isBounded_compl_iff] at hs
    obtain ⟨M, hM_pos, hM⟩ : ∃ M > 0, ∀ y ∈ sᶜ, ‖y‖ ≤ M := hs.exists_pos_norm_le
    suffices Tendsto (‖algebraMap ℝ F ·.2‖ - M * ‖x‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop by
      refine tendsto_atTop_mono' _ ?_ this
      filter_upwards [prod_mem_prod (mem_principal_self sᶜ) univ_mem] with w hw
      rw [norm_sub_rev]
      refine le_trans ?_ (norm_sub_norm_le ..)
      specialize hM _ (Set.mem_prod.mp hw).1
      simp only [norm_algebraMap', norm_smul]
      gcongr
    simp only [norm_algebraMap', sub_eq_add_neg]
    exact tendsto_atTop_add_const_right _ _ <| tendsto_norm_atTop_iff_cobounded.mpr tendsto_snd
    -- the first component is unbounded and the second one is arbitrary
  · suffices Tendsto (fun y : ℝ × ℝ ↦ ‖y.1‖ * c) (cobounded ℝ ×ˢ ⊤) atTop by
      refine tendsto_atTop_mono' _ ?_ this
      filter_upwards [prod_mem_prod (isBounded_singleton (x := 0)) univ_mem] with y hy
      calc ‖y.1‖ * c
        _ ≤ ‖y.1‖ * ‖x - algebraMap ℝ F (y.1⁻¹ * y.2)‖ := by gcongr; exact hbd _
        _ = ‖y.1 • x - algebraMap ℝ F y.2‖ := by
          simp only [← norm_smul, smul_sub, smul_smul, Algebra.algebraMap_eq_smul_one]
          simp_all
    rw [tendsto_mul_const_atTop_of_pos hc₀, tendsto_norm_atTop_iff_cobounded]
    exact tendsto_fst

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

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

Tactic:
simp only [map_add, map_add_le_add]

Goal state after: