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

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

Tactic:
borelize F'

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

Goal state before:
pp: F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ eLpNorm u (↑q) μ = eLpNorm u (↑q) (μ.restrict s)

Tactic:
rw [eLpNorm_restrict_eq_of_support_subset h2u]

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ eLpNorm u (↑p') (μ.restrict s) * ↑t = eLpNorm u (↑p') μ * ↑t

Tactic:
rw [eLpNorm_restrict_eq_of_support_subset h2u]

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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
⊢ f.range = ⊤

Tactic:
apply Submodule.eq_of_le_of_finrank_le le_top

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
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 V
this : FiniteDimensional 𝕜 V
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
⊢ finrank 𝕜 ↥⊤ ≤ finrank 𝕜 ↥f.range
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
h : f.ker = ⊥
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet

Tactic:
let bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U

Goal state after:
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
h : f.ker = ⊥
bv : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range
bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U
⊢ (c • f).normDet = ‖c‖ ^ finrank 𝕜 U * f.normDet
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 = ⊥
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet

Tactic:
let bu : OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 U := stdOrthonormalBasis 𝕜 U

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
⊢ (g ∘ₗ f).normDet = (g.domRestrict f.range).normDet * f.normDet
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := ⋯
t : (n : ℕ) → γ n → Set (ι → ℝ) := ⋯
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
⊢ Tendsto (fun n ↦ ∏ i, ↑⌈(↑(b i) - ↑(a i)) * ↑n⌉₊ / ↑n) atTop (𝓝 (∏ x, ENNReal.ofReal (↑(b x) - ↑(a x))))

Tactic:
refine ENNReal.tendsto_finsetProd_of_ne_top _ (fun i _ => ?_) fun i _ => ?_

Goal state after:
case refine_1
ι : 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
⊢ Tendsto (fun n ↦ ↑⌈(↑(b i) - ↑(a i)) * ↑n⌉₊ / ↑n) atTop (𝓝 (ENNReal.ofReal (↑(b i) - ↑(a i))))

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)) ≠ ∞
Module: Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
b a : F
x✝ : F →WOT[𝕜] F
| ⟪x✝ b, a⟫_𝕜

Tactic:
← inner_conj_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
b a : F
x✝ : F →WOT[𝕜] F
| (starRingEnd 𝕜) ⟪a, x✝ b⟫_𝕜
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case e'_2
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
⊢ Fintype.card (Fin 2) = finrank ℝ E

Tactic:
rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]

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

Goal state before:
pp: case e'_3
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 : E
⊢ Fintype.card (Fin 2) = finrank ℝ E

Tactic:
rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]

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

Goal state before:
pp: case neg
𝕜 : 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
i j : n
hij : ¬i = j
⊢ ⟪WithLp.toLp 2 (lowerInv hS j), WithLp.toLp 2 (Sᵀ *ᵥ lowerInv hS i)⟫_𝕜 =
    lowerInv hS i ᵥ* S ⬝ᵥ (lowerInv hS).map star j

Tactic:
← inner_conj_symm,

Goal state after:
case neg
𝕜 : 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
i j : n
hij : ¬i = j
⊢ (starRingEnd 𝕜) ⟪WithLp.toLp 2 (Sᵀ *ᵥ lowerInv hS i), WithLp.toLp 2 (lowerInv hS j)⟫_𝕜 =
    lowerInv hS i ᵥ* S ⬝ᵥ (lowerInv hS).map star j
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
α : Type u_5
l : Filter α
f : α → E →SWOT[σ] F
A : E →SWOT[σ] F
⊢ Tendsto f l (𝓝 A) ↔ ∀ (x : E) (y : F⋆), Tendsto (fun a ↦ y ((f a) x)) l (𝓝 (y (A x)))

Tactic:
by
  simp [isInducing_inducingFn.tendsto_nhds_iff, tendsto_pi_nhds]

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ ∫ (u : ℝ), cexp (↑(-2 * π * (u * (s.im / (2 * π)))) * I) • rexp (-s.re * u) • f (rexp (-u)) =
    𝓕 (fun u ↦ rexp (-s.re * u) • f (rexp (-u))) (s.im / (2 * π))

Tactic:
by
      simp [fourier_eq', mul_comm (_ / _)]

Goal state after:
Module: Mathlib.Analysis.MellinInversion

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : ↑x ≠ 0
⊢ |(2 * π)⁻¹| • ∫ (y : ℝ), (↑x ^ (-↑σ) * ↑x ^ (-(↑y * I))) • f (↑σ + ↑y * I) =
    ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)

Tactic:
mul_smul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : ↑x ≠ 0
⊢ |(2 * π)⁻¹| • ∫ (y : ℝ), ↑x ^ (-↑σ) • ↑x ^ (-(↑y * I)) • f (↑σ + ↑y * I) =
    ↑x ^ (-↑σ) • ∫ (y : ℝ), cexp (2 * ↑π * (↑y * -↑(Real.log x)) * I) • f (↑σ + 2 * ↑π * ↑y * I)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
⊢ mellin (fun t ↦ ↑t ^ a • f t) s = mellin f (s + a)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • (fun t ↦ ↑t ^ a • f t) t = ↑t ^ (s + a - 1) • f t
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f (t ^ a) =
    ∫ (a_1 : ℝ) in Ioi 0, |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • ↑(a_1 ^ a) ^ (s / ↑a - 1) • f (a_1 ^ a)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = |a|⁻¹ • (|a| * t ^ (a - 1)) • ↑(t ^ a) ^ (s / ↑a - 1) • f (t ^ a)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : 1 - z ∈ slitPlane
⊢ log (1 - z)⁻¹ = z * ∫ (t : ℝ) in 0..1, (1 - t • z)⁻¹

Tactic:
rw [sub_eq_add_neg 1 z] at hz ⊢
  rw [log_inv _ <| slitPlane_arg_ne_pi hz, neg_eq_iff_eq_neg, ← neg_mul]
  convert! log_eq_integral hz using 5
  rw [sub_eq_add_neg, smul_neg]

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

Goal state before:
pp: t : ℝ
ht : t ∈ Set.Icc 0 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Tactic:
rw [Set.mem_Icc] at ht
  rw [norm_inv]
  refine inv_anti₀ (by linarith) ?_
  calc 1 - ‖z‖
    _ ≤ 1 - t * ‖z‖ := by
      nlinarith [norm_nonneg z]
    _ = 1 - ‖t * z‖ := by
      rw [norm_mul, Complex.norm_of_nonneg ht.1]
    _ ≤ ‖1 + t * z‖ := by
      rw [← norm_neg (t * z), ← sub_neg_eq_add]
      convert! norm_sub_norm_le 1 (-(t * z))
      exact norm_one.symm

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

Goal state before:
pp: case convert_2
f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
⊢ (fun x ↦ (1 / ↑x)⁻¹ • (f x - (1 + t / ↑x))) =ᶠ[atTop] fun x ↦ ↑x * (f x - 1) - t

Tactic:
filter_upwards [eventually_ne_atTop 0] with n h0

Goal state after:
f : ℕ → ℂ
t : ℂ
hf : (fun n ↦ f n - (1 + t / ↑n)) =o[atTop] fun n ↦ 1 / ↑n
n : ℕ
h0 : n ≠ 0
⊢ (1 / ↑n)⁻¹ • (f n - (1 + t / ↑n)) = ↑n * (f n - 1) - t
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
⊢ f ↑n = f 1 + log ↑(n - 1)!

Tactic:
by
  refine Nat.le_induction (by simp) (fun m hm IH => ?_) n (Nat.one_le_iff_ne_zero.2 hn)
  have A : 0 < (m : ℝ) := Nat.cast_pos.2 hm
  simp only [hf_feq A, Nat.cast_add, Nat.cast_one, Nat.add_succ_sub_one, add_zero]
  rw [IH, add_assoc, ← log_mul (Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)) A.ne', ←
    Nat.cast_mul]
  conv_rhs => rw [← Nat.succ_pred_eq_of_pos hm, Nat.factorial_succ, mul_comm]
  congr
  exact (Nat.succ_pred_eq_of_pos hm).symm

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

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

Tactic:
exact Nat.succ_ne_zero _

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

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

Tactic:
exp_log

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

case refine_2
A : 0 < 3 / 2
this : Γ (3 / 2) ≤ rexp (1 / 2 * log 2 - log (3 / 2))
⊢ 0 < (3 / 2) ^ 2
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
⊢ (support fun i ↦ d i • logDeriv (F i) y) ⊆ ↑hd.toFinset

Tactic:
simp +contextual [-support_mul, -mul_eq_zero, Set.subset_def, not_imp_not]

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
⊢ atTop • 𝓝 v ≤ ⨆ p, atTop • 𝓝 v +ᵥ pure p

Tactic:
apply (le_iSup _ 0).trans'
    simp

Goal state after:
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
s : Set ι
hs : s.Finite
f : ι → Set P
⊢ asymptoticCone k (⋃ i ∈ s, f i) = ⋃ i ∈ s, asymptoticCone k (f i)

Tactic:
induction s, hs using Set.Finite.induction_on <;>
    simp [asymptoticCone_union, *]

Goal state after:
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
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
⊢ ∃ w' fs',
    ∑ j ∈ fs', w' j = 1 ∧
      (Finset.affineCombination k fs' p) w' = p' ∧
        ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑fs' \ {↑i}).indicator w' j

Tactic:
let w' : ι → k := AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩) ri'

Goal state after:
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
p : ι → P
hp : AffineIndependent k p
s : Set ι
fs : ↑s → Finset ι
hfs : ∀ (i : ↑s), ↑i ∈ fs i
w : ↑s → ι → k
hw : ∀ (i : ↑s), ∑ j ∈ fs i, w i j = 1
p' : P
hp' : ∀ (i : ↑s), p' ∈ line[k, p ↑i, (Finset.affineCombination k (fs i) p) (w i)]
hp'' : ∀ (i : ↑s), ∃ r, (Finset.affineCombination k (fs i) p) ((AffineMap.lineMap (Pi.single (↑i) 1) (w i)) r) = p'
i' : ι
hi' : i' ∈ s
ri' : k
hri' :
  (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((AffineMap.lineMap (Pi.single (↑⟨i', hi'⟩) 1) (w ⟨i', hi'⟩)) ri') = p'
w' : ι → k := (AffineMap.lineMap (Pi.single i' 1) (w ⟨i', hi'⟩)) ri'
⊢ ∃ w' fs',
    ∑ j ∈ fs', w' j = 1 ∧
      (Finset.affineCombination k fs' p) w' = p' ∧
        ∀ (i : ↑s), ∃ r, ∀ (j : ι), r * (↑(fs i) \ {↑i}).indicator (w i) j = (↑fs' \ {↑i}).indicator w' j
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
⊢ ∀ (n : ℕ), ∀ᵐ (a : ℝ) ∂volume.restrict (Ioi 0), ‖f n a‖ ≤ rexp (-a) * a ^ (s.re - 1)

Tactic:
intro n
    rw [ae_restrict_iff' measurableSet_Ioi]
    filter_upwards with x hx
    simp only [mem_Ioi, f] at hx ⊢
    rcases lt_or_ge (n : ℝ) x with (hxn | hxn)
    · rw [indicator_of_notMem (notMem_Ioc_of_gt hxn), norm_zero,
        mul_nonneg_iff_right_nonneg_of_pos (exp_pos _)]
      positivity
    · rw [indicator_of_mem (mem_Ioc.mpr ⟨mem_Ioi.mp hx, hxn⟩), norm_mul, Complex.norm_of_nonneg
          (pow_nonneg (sub_nonneg.mpr <| div_le_one_of_le₀ hxn <| by positivity) _),
          norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]
      gcongr
      exact one_sub_div_pow_le_exp_neg hxn

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

Goal state before:
pp: case zero
s : ℂ
hs : ⌊1 - s.re⌋₊ = 0
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
rw [Nat.floor_eq_zero, sub_lt_self_iff] at hs
    apply (approx_Gamma_integral_tendsto_Gamma_integral hs).congr'
    filter_upwards [eventually_ne_atTop 0] with n hn using
      (GammaSeq_eq_approx_Gamma_integral hs hn).symm

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

Goal state before:
pp: E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e ↦ dist (↑e z) z)
R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e ↦ ((e.trans R).trans e.symm).trans R
e : PE ≃ᵢ PE
⊢ dist (e.symm ((pointReflection ℝ z) (e z))) z = 2 * dist (e z) z

Tactic:
← e.dist_eq,

Goal state after:
E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}
this : Nonempty ↑s
h_bdd : BddAbove (range fun e ↦ dist (↑e z) z)
R : PE ≃ᵢ PE := (pointReflection ℝ z).toIsometryEquiv
f : PE ≃ᵢ PE → PE ≃ᵢ PE := fun e ↦ ((e.trans R).trans e.symm).trans R
e : PE ≃ᵢ PE
⊢ dist (e (e.symm ((pointReflection ℝ z) (e z)))) (e z) = 2 * dist (e z) z
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℝ
this : Tendsto (Complex.ofReal ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma ↑s))
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))

Tactic:
exact (Complex.continuous_re.tendsto (Complex.Gamma ↑s)).comp this

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: a : ℝ
⊢ ‖↑a‖ = ‖a‖

Tactic:
by
  rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
⊢ IsUltrametricDist R

Tactic:
refine isUltrametricDist_of_forall_norm_add_le_max_norm (fun x y ↦ ?_)
  rcases eq_or_ne y 0 with rfl | hy
  · simpa only [add_zero] using le_max_left _ _
  · have p : 0 < ‖y‖ := norm_pos_iff.mpr hy
    simpa only [div_add_one hy, norm_div, div_le_iff₀ p, max_mul_of_nonneg _ _ p.le, one_mul,
      div_mul_cancel₀ _ p.ne'] using h (x / y)

Goal state after: