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)
⊢ ‖((toMatrix (stdOrthonormalBasis 𝕜 U).toBasis ⋯.some.toBasis) f.rangeRestrict).det‖ =
    ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

Tactic:
← basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix (stdOrthonormalBasis 𝕜 U).toBasis
    bu.toBasis h.some.toBasis bv.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
bu : OrthonormalBasis ι 𝕜 U
bv : OrthonormalBasis ι 𝕜 ↥f.range
hrank : finrank 𝕜 U = finrank 𝕜 ↥f.range
h : Nonempty (OrthonormalBasis (Fin (finrank 𝕜 U)) 𝕜 ↥f.range)
⊢ ‖(h.some.toBasis.toMatrix ⇑bv.toBasis * (toMatrix bu.toBasis bv.toBasis) f.rangeRestrict *
          bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis).det‖ =
    ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f ⁻¹' s) = ∞
⊢ μH[↑d] s = ∞

Tactic:
have := hf.hausdorffMeasure_preimage_le d.coe_nonneg s

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
K : ℝ≥0
f : X → Y
hf : AntilipschitzWith K f
s : Set Y
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f ⁻¹' s) = ∞
this : μH[↑d] (f ⁻¹' s) ≤ ↑K ^ ↑d * μH[↑d] s
⊢ μH[↑d] s = ∞
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
⊢ Monotone m → Monotone fun s ↦ extend (fun s x ↦ m (ediam s)) ↑s

Tactic:
· intro h_mono s t hst
    simp only [extend, le_iInf_iff]
    intro ht
    apply le_trans _ (h_mono (ediam_mono hst))
    simp only [(ediam_mono hst).trans ht, le_refl, ciInf_pos]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
⊢ ‖x‖ ^ 2 =
    4 / (4 * 4 + 0 * 0) *
        (‖x + x‖ * ‖x + x‖ - 0 * 0 - (‖x - x‖ * ‖x - x‖ - 0 * 0) +
            ((0 * ‖I • x + x‖ - im I * 0) * ‖I • x + x‖ - (0 * 0 + im I * ‖I • x + x‖) * 0) -
          ((0 * ‖I • x - x‖ - im I * 0) * ‖I • x - x‖ - (0 * 0 + im I * ‖I • x - x‖) * 0)) -
      -0 / (4 * 4 + 0 * 0) *
        (‖x + x‖ * 0 + 0 * ‖x + x‖ - (‖x - x‖ * 0 + 0 * ‖x - x‖) +
            ((0 * ‖I • x + x‖ - im I * 0) * 0 + (0 * 0 + im I * ‖I • x + x‖) * ‖I • x + x‖) -
          ((0 * ‖I • x - x‖ - im I * 0) * 0 + (0 * 0 + im I * ‖I • x - x‖) * ‖I • x - x‖))

Tactic:
have h₂ : ‖x + x‖ = 2 • ‖x‖ := by convert norm_nsmul 𝕜 2 x; module

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h₁ : ‖x - x‖ = 0
h₂ : ‖x + x‖ = 2 • ‖x‖
⊢ ‖x‖ ^ 2 =
    4 / (4 * 4 + 0 * 0) *
        (‖x + x‖ * ‖x + x‖ - 0 * 0 - (‖x - x‖ * ‖x - x‖ - 0 * 0) +
            ((0 * ‖I • x + x‖ - im I * 0) * ‖I • x + x‖ - (0 * 0 + im I * ‖I • x + x‖) * 0) -
          ((0 * ‖I • x - x‖ - im I * 0) * ‖I • x - x‖ - (0 * 0 + im I * ‖I • x - x‖) * 0)) -
      -0 / (4 * 4 + 0 * 0) *
        (‖x + x‖ * 0 + 0 * ‖x + x‖ - (‖x - x‖ * 0 + 0 * ‖x - x‖) +
            ((0 * ‖I • x + x‖ - im I * 0) * 0 + (0 * 0 + im I * ‖I • x + x‖) * ‖I • x + x‖) -
          ((0 * ‖I • x - x‖ - im I * 0) * 0 + (0 * 0 + im I * ‖I • x - x‖) * ‖I • x - x‖))
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
ι : Type u_5
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f : U →ₗ[𝕜] V
b : OrthonormalBasis ι 𝕜 U
h : f.ker = ⊥
⊢ ↑(f.normDet ^ 2) = (Matrix.gram 𝕜 fun x ↦ f.rangeRestrict (b x)).det

Tactic:
let bv := orthonormalBasis_range h b
    rw [Matrix.gram_eq_conjTranspose_mul bv, Matrix.det_mul, Matrix.det_conjTranspose]
    rw [RCLike.star_def, RCLike.conj_mul, f.normDet_eq_norm_det_toMatrix_rangeRestrict b bv]
    simp only [map_pow]
    congr
    ext i j
    simp [LinearMap.toMatrix_apply]

Goal state after:
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
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
htop : f.range = ⊤
⊢ (g ∘ₗ f).normDet = g.normDet * f.normDet

Tactic:
rw [normDet_comp]

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
inst✝ : FiniteDimensional 𝕜 V
f : U →ₗ[𝕜] V
g : V →ₗ[𝕜] W
h : finrank 𝕜 U = finrank 𝕜 V
htop : f.range = ⊤
⊢ (g.domRestrict f.range).normDet * f.normDet = g.normDet * f.normDet
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
p : Submodule 𝕜 V
f : U →ₗ[𝕜] V
h : ∀ (c : U), f c ∈ p
this : f = p.subtype ∘ₗ codRestrict p f h
⊢ (codRestrict p f h).normDet = (p.subtype ∘ₗ codRestrict p f h).normDet

Tactic:
rw [normDet_comp]

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
p : Submodule 𝕜 V
f : U →ₗ[𝕜] V
h : ∀ (c : U), f c ∈ p
this : f = p.subtype ∘ₗ codRestrict p f h
⊢ (codRestrict p f h).normDet = (p.subtype.domRestrict (codRestrict p f h).range).normDet * (codRestrict p f h).normDet
Module: Mathlib.Analysis.InnerProductSpace.Trace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
x y : E
⊢ (trace 𝕜 E) (↑(ContinuousLinearMap.toSpanSingleton 𝕜 x) ∘ₗ ↑((innerSL 𝕜) y)) = ⟪y, x⟫_𝕜

Tactic:
trace_comp_comm',

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
x y : E
⊢ (trace 𝕜 𝕜) (↑((innerSL 𝕜) y) ∘ₗ ↑(ContinuousLinearMap.toSpanSingleton 𝕜 x)) = ⟪y, x⟫_𝕜
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
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
d : ℝ
hd : 0 ≤ d
⊢ μH[d] (f '' s) ≤ ↑C ^ d * μH[↑r * d] s

Tactic:
by
  -- We start with the trivial case `C = 0`
  rcases eq_zero_or_pos C with (rfl | hC0)
  · rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
    · simp only [measure_empty, nonpos_iff_eq_zero, mul_zero, image_empty]
    have : f '' s = {f x} :=
      have : (f '' s).Subsingleton := by simpa [ediam_eq_zero_iff] using h.ediam_image_le
      (subsingleton_iff_singleton (mem_image_of_mem f hx)).1 this
    rw [this]
    rcases eq_or_lt_of_le hd with (rfl | h'd)
    · simp only [ENNReal.rpow_zero, one_mul, mul_zero]
      rw [hausdorffMeasure_zero_singleton]
      exact one_le_hausdorffMeasure_zero_of_nonempty ⟨x, hx⟩
    · have := nullSingletonClass_hausdorff Y h'd
      simp only [zero_le, measure_singleton]
  -- Now assume `C ≠ 0`
  · have hCd0 : (C : ℝ≥0∞) ^ d ≠ 0 := by simp [hC0.ne']
    have hCd : (C : ℝ≥0∞) ^ d ≠ ∞ := by simp [hd]
    simp only [hausdorffMeasure_apply, ENNReal.mul_iSup, ENNReal.mul_iInf_of_ne hCd0 hCd,
      ← ENNReal.tsum_mul_left]
    refine iSup_le fun R => iSup_le fun hR => ?_
    have : Tendsto (fun d : ℝ≥0∞ => (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0) :=
      ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top hr
    rcases ENNReal.nhds_zero_basis_Iic.eventually_iff.1 (this.eventually (gt_mem_nhds hR)) with
      ⟨δ, δ0, H⟩
    refine le_iSup₂_of_le δ δ0 <| iInf₂_mono' fun t hst ↦
      ⟨fun n => f '' (t n ∩ s), ?_, iInf_mono' fun htδ ↦
        ⟨fun n => (h.ediam_image_inter_le (t n)).trans (H (htδ n)).le, ?_⟩⟩
    · grw [← image_iUnion, ← iUnion_inter, ← hst, inter_self]
    · refine ENNReal.tsum_le_tsum fun n => ?_
      simp only [iSup_le_iff, image_nonempty]
      intro hft
      simp only [Nonempty.mono ((t n).inter_subset_left) hft, ciSup_pos]
      rw [ENNReal.rpow_mul, ← ENNReal.mul_rpow_of_nonneg _ _ hd]
      gcongr
      exact h.ediam_image_inter_le _

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 * ediam (t n)) ^ d

Tactic:
exact ENNReal.rpow_le_rpow (hf.ediam_preimage_le _) hd

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

Goal state before:
pp: E : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
v : E
s : Set ℝ
hv : v ≠ 0
hn : ‖v‖ ≠ 0
this : μH[1] ((fun x ↦ ‖v‖ • x) '' ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s
⊢ μH[1] ((fun r ↦ r • v) '' s) = ‖v‖₊ • μH[1] s

Tactic:
simpa only [Set.image_image, smul_comm (norm _), inv_smul_smul₀ hn,
      LinearMap.toSpanSingleton_apply] using this

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
⊢ ⟪a, x⟫ • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) x

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : a = 0
⊢ ⟪a, x⟫ • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) x

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ⟪a, x⟫ • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) x
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : WeakSpace 𝕜 E
hx : x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
⊢ x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ

Tactic:
obtain ⟨x, -, rfl⟩ := (toWeakSpace 𝕜 E).toEquiv.image_compl (closure s) |>.symm.subset hx

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
⊢ ⟪a, x⟫ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : a = 0
⊢ ⟪a, x⟫ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x

case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ⟪a, x⟫ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x
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
⊢ 0 = lowerInv hS i ⬝ᵥ S *ᵥ ((lowerInv hS)ᵀ.map star)ᵀ j

Tactic:
transpose_map,

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
⊢ 0 = lowerInv hS i ⬝ᵥ S *ᵥ ((lowerInv hS).map star)ᵀᵀ j
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 : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = (t ^ (a - 1) • ↑(t ^ a) ^ (s / ↑a - 1)) • f (t ^ a)

Tactic:
real_smul

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) = (↑(t ^ (a - 1)) * ↑(t ^ a) ^ (s / ↑a - 1)) • f (t ^ a)
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 : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ (s - 1) • f (t ^ a) = (↑t ^ ↑(a - 1) * ↑t ^ (↑a * (s / ↑a - 1))) • f (t ^ a)

Tactic:
←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt 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) = ↑t ^ (↑(a - 1) + ↑a * (s / ↑a - 1)) • f (t ^ a)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume

Tactic:
by
  obtain ⟨d, _, hd'⟩ := hf.exists_pos
  simp_rw [IsBigOWith, eventually_nhdsWithin_iff, Metric.eventually_nhds_iff, gt_iff_lt] at hd'
  obtain ⟨ε, hε, hε'⟩ := hd'
  refine ⟨ε, hε, Iff.mpr integrableOn_Ioc_iff_integrableOn_Ioo ⟨?_, ?_⟩⟩
  · refine AEStronglyMeasurable.mul ?_ (hfc.mono_set Ioo_subset_Ioi_self)
    refine (continuousOn_of_forall_continuousAt fun t ht => ?_).aestronglyMeasurable
      measurableSet_Ioo
    exact continuousAt_rpow_const _ _ (Or.inl ht.1.ne')
  · apply HasFiniteIntegral.mono' (g := fun t => d * t ^ (s - b - 1))
    · refine (Integrable.hasFiniteIntegral ?_).const_mul _
      rw [← IntegrableOn, ← integrableOn_Ioc_iff_integrableOn_Ioo, ←
        intervalIntegrable_iff_integrableOn_Ioc_of_le hε.le]
      exact intervalIntegral.intervalIntegrable_rpow' (by linarith)
    · refine (ae_restrict_iff' measurableSet_Ioo).mpr (Eventually.of_forall fun t ht => ?_)
      rw [mul_comm, norm_mul]
      specialize hε' _ ht.1
      · rw [dist_eq_norm, sub_zero, norm_of_nonneg ht.1.le]
        exact ht.2
      · calc _ ≤ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ := by gcongr
          _ = d * t ^ (s - b - 1) := ?_
        simp_rw [norm_of_nonneg (rpow_nonneg ht.1.le _), mul_assoc]
        rw [← rpow_add ht.1]
        congr 2
        abel

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‖
h1 : ∀ᶠ (z : ℂ) in 𝓝 s, AEStronglyMeasurable (F z) (volume.restrict (Ioi 0))
⊢ IntegrableOn (F s) (Ioi 0) volume

Tactic:
exact mellinConvergent_of_isBigO_rpow hfc hf_top hs_top hf_bot hs_bot

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

Goal state before:
pp: g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
x : ℝ
hg1 : -1 ≤ g x
⊢ ↑x * Complex.log (1 + ↑(g x)) = ↑x * Complex.log (↑1 + ↑(g x))

Tactic:
Complex.ofReal_one

Goal state after:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
x : ℝ
hg1 : -1 ≤ g x
⊢ ↑x * Complex.log (1 + ↑(g x)) = ↑x * Complex.log (1 + ↑(g x))
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
x : ℝ
hg1 : -1 ≤ g x
⊢ (1 + ↑(g x)) ^ ↑x = (↑1 + ↑(g x)) ^ ↑x

Tactic:
Complex.ofReal_one

Goal state after:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
x : ℝ
hg1 : -1 ≤ g x
⊢ (1 + ↑(g x)) ^ ↑x = (1 + ↑(g x)) ^ ↑x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

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

Tactic:
mul_two

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = ∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1))

Tactic:
congr! 2 with m

Goal state after:
case a
x : ℝ
n m : ℕ
a✝ : m ∈ Finset.range (n + 1)
⊢ x + 1 + ↑m = x + ↑(m + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y ↦ y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ 0 < (id (1 - ↑x)).re

Tactic:
rw [id, sub_re, one_re, ofReal_re, sub_pos]

Goal state after:
case refine_1
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
x : ℝ
hx : x ∈ Ioo 0 1
U : HasDerivAt (fun y ↦ y ^ u) (u * ↑x ^ (u - 1)) ↑x
⊢ x < 1
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ HasMellin ((Ioc 0 1).indicator fun x ↦ 1) s (1 / s)

Tactic:
have aux1 : -1 < (s - 1).re := by
    simpa only [sub_re, one_re, sub_eq_add_neg] using! lt_add_of_pos_left _ hs

Goal state after:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
⊢ HasMellin ((Ioc 0 1).indicator fun x ↦ 1) s (1 / s)
Module: Mathlib.Analysis.Normed.Affine.Ceva

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle 𝕜 P
p : Fin 3 → P
p' : P
hp0 : ∀ (i : Fin 3), p i ≠ t.points (i + 2)
hp : ∀ (i : Fin 3), p i ∈ line[𝕜, t.points (i + 1), t.points (i + 2)]
hp' : ∀ (i : Fin 3), p' ∈ line[𝕜, t.points i, p i]
i : Fin 3
⊢ dist (p i) (t.points (i + 2)) ≠ 0

Tactic:
simpa using hp0 i

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

Goal state before:
pp: case inl
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 : Set V
hs : Convex k ∅
hs' : IsClosed[inst✝²] ∅
⊢ Convex k (asymptoticCone k ∅)

Tactic:
asymptoticCone_empty

Goal state after:
case inl
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 : Set V
hs : Convex k ∅
hs' : IsClosed[inst✝²] ∅
⊢ Convex k ∅
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 : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun u ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ c • v +ᵥ p ∈ [-(c • u) +ᵥ c • v +ᵥ p -[k] t • u +ᵥ c • v +ᵥ p]

Tactic:
simp_rw [mem_segment_iff_sameRay, ← vsub_eq_sub]

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 : Set V
c : k
v p : V
hs : Convex k s
hc : 0 ≤ c
hp : s ∈ 𝓝 p
hv : ∃ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, a.1 • a.2 +ᵥ c • v +ᵥ p ∈ s
this : Tendsto (fun u ↦ -(c • u) +ᵥ c • v +ᵥ p) (𝓝 v) (𝓝 p)
t : k
u : V
ht : 0 < t
hu : -(c • u) +ᵥ c • v +ᵥ p ∈ s
h : t • u +ᵥ c • v +ᵥ p ∈ s
⊢ SameRay k ((c • v +ᵥ p) -ᵥ (-(c • u) +ᵥ c • v +ᵥ p)) ((t • u +ᵥ c • v +ᵥ p) -ᵥ (c • v +ᵥ p))