mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.GaussSum

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
| ∑ i, ∑ j, χ i * ψ i * (φ j * ψ j) = ∑ t, ∑ x, χ x * φ (t - x) * ψ t

Tactic:
enter [1, 2, x, 2, x_1]; rw [mul_mul_mul_comm]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Fintype R
R' : Type v
inst✝ : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x x_1 : R
| χ x * φ x_1 * (ψ x * ψ x_1)
Module: Mathlib.Data.Finset.Grade

Goal state before:
pp: α : Type u_1
⊢ ∀ ⦃x : Multiset α⦄, x ∈ Set.range val → ∀ ⦃y : Multiset α⦄, y ∈ Set.range val → Set.Icc x y ⊆ Set.range val

Tactic:
rintro _ _ _ ⟨s, rfl⟩ t ht; exact ⟨⟨t, Multiset.nodup_of_le ht.2 s.2⟩, rfl⟩

Goal state after:
Module: Mathlib.Data.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(Iio s) = 2 ^ #s - 1

Tactic:
by
  rw [Iio_eq_ssubsets, ssubsets, card_erase_of_mem (mem_powerset_self _), card_powerset]

Goal state after:
Module: Mathlib.Analysis.Hofer

Goal state before:
pp: X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / 2 ^ m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
⊢ d (u (n + 1)) x ≤ 2 * ε

Tactic:
rw [dist_comm]

Goal state after:
X : Type u_1
inst✝¹ : MetricSpace X
inst✝ : CompleteSpace X
x : X
ε : ℝ
ε_pos : 0 < ε
ϕ : X → ℝ
cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ϕ
nonneg : ∀ (y : X), 0 ≤ ϕ y
reformulation : ∀ (x' : X) (k : ℕ), ε * ϕ x ≤ ε / 2 ^ k * ϕ x' ↔ 2 ^ k * ϕ x ≤ ϕ x'
this : Nonempty X
F : ℕ → X → X
hF : ∀ (k : ℕ) (x' : X), d x' x ≤ 2 * ε ∧ 2 ^ k * ϕ x ≤ ϕ x' → d x' (F k x') ≤ ε / 2 ^ k ∧ 2 * ϕ x' < ϕ (F k x')
u : ℕ → X := fun n ↦ Nat.recOn n x F
hu :
  ∀ (n : ℕ), d (u n) x ≤ 2 * ε ∧ 2 ^ n * ϕ x ≤ ϕ (u n) → d (u n) (u (n + 1)) ≤ ε / 2 ^ n ∧ 2 * ϕ (u n) < ϕ (u (n + 1))
n : ℕ
IH : ∀ m ≤ n, d (u m) (u (m + 1)) ≤ ε / 2 ^ m ∧ 2 * ϕ (u m) < ϕ (u (m + 1))
⊢ d x (u (n + 1)) ≤ 2 * ε
Module: Mathlib.Analysis.InnerProductSpace.Coalgebra

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ ↑(assocIsometry 𝕜 E E E).toLinearEquiv ∘ₗ
      adjoint (LinearMap.rTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) =
    adjoint (LinearMap.lTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)

Tactic:
← (assocIsometry 𝕜 _ _ _).symm_symm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : FiniteDimensional 𝕜 E
A : Type u_3
inst✝³ : Ring A
inst✝² : Module 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
e : E ≃ₗ[𝕜] A
⊢ ↑(assocIsometry 𝕜 E E E).symm.symm.toLinearEquiv ∘ₗ
      adjoint (LinearMap.rTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e) =
    adjoint (LinearMap.lTensor E (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)) ∘ₗ adjoint (↑e.symm ∘ₗ mul' 𝕜 A ∘ₗ map ↑e ↑e)
Module: Mathlib.Analysis.InnerProductSpace.Positive

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ 0 ≤ re ⟪(T + S) x, x⟫

Tactic:
add_apply,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsPositive
hS : S.IsPositive
x : E
⊢ 0 ≤ re ⟪T x + S x, x⟫
Module: Mathlib.Analysis.InnerProductSpace.Semisimple

Goal state before:
pp: case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
suffices q ⊔ qᗮ = ⊤ by rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]

Goal state after:
case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ = ⊤
Module: Mathlib.Analysis.InnerProductSpace.LaxMilgram

Goal state before:
pp: V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ (↑(continuousLinearMapOfBilin B)).range = ⊤

Tactic:
have := coercive.isClosed_range.completeSpace_coe

Goal state after:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
this : CompleteSpace ↑↑(↑(continuousLinearMapOfBilin B)).range
⊢ (↑(continuousLinearMapOfBilin B)).range = ⊤
Module: Mathlib.Topology.Algebra.Module.LinearPMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ (fun a ↦ a.swap) '' closure[instTopologicalSpaceProd] ↑f.graph =
    closure[instTopologicalSpaceProd] ((fun a ↦ a.swap) '' ↑f.graph)

Tactic:
apply (image_closure_subset_closure_image continuous_swap).antisymm

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module R E
inst✝⁷ : Module R F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
f : E →ₗ.[R] F
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousAdd F
inst✝² : TopologicalSpace R
inst✝¹ : ContinuousSMul R E
inst✝ : ContinuousSMul R F
hf : f.toFun.ker = ⊥
hf' : f.IsClosable
hcf : f.closure.toFun.ker = ⊥
⊢ closure[instTopologicalSpaceProd] (Prod.swap '' ↑f.graph) ⊆ Prod.swap '' closure[instTopologicalSpaceProd] ↑f.graph
Module: Mathlib.Dynamics.BirkhoffSum.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
f : α → α
x : α
h : IsFixedPt f x
g : α → M
n : ℕ
⊢ birkhoffSum f g n x = n • g x

Tactic:
simp [birkhoffSum, (h.iterate _).eq]

Goal state after:
Module: Mathlib.Dynamics.BirkhoffSum.Average

Goal state before:
pp: R : Type u_1
α : Type u_2
M : Type u_3
inst✝⁷ : DivisionSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_4
F : Type u_5
N : Type u_6
inst✝⁴ : DivisionSemiring S
inst✝³ : AddCommMonoid N
inst✝² : Module S N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
g' : F
f : α → α
g : α → M
n : ℕ
x : α
⊢ g' (birkhoffAverage R f g n x) = birkhoffAverage S f (⇑g' ∘ g) n x

Tactic:
by
  simp only [birkhoffAverage, map_inv_natCast_smul g' R S, map_birkhoffSum]

Goal state after:
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}
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
have Ssep (n) : Metric.AreSeparated (S n) t :=
    ⟨n⁻¹, ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _),
      fun x hx y hy ↦ hx.2.trans <| infEDist_le_edist_of_mem hy⟩

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
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s
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
f₂ : H →L[𝕜] E
x✝ : G ⊗[𝕜] H
⊢ (lTensor G (f₁ ∘SL f₂)) x✝ = (lTensor G f₁ ∘SL lTensor G f₂) x✝

Tactic:
simp [LinearMap.lTensor_comp]

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

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

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

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

Goal state before:
pp: case refine_2
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 < d
x : X
ε : ℝ≥0∞
x✝¹ : 0 < ε
x✝ : ℕ
⊢ ediam ((fun x_1 ↦ {x}) x✝) ≤ ε

Tactic:
simp only [ediam_singleton, zero_le]

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

Goal state before:
pp: case inl
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d : ℝ
hd : 0 ≤ d
hs : ∅.Subsingleton
⊢ μH[d] ∅ ≤ 1

pp: case inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ μH[d] s ≤ 1

Tactic:
· simp only [measure_empty, zero_le]

Goal state after:
case inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
hs : s.Subsingleton
d : ℝ
hd : 0 ≤ d
x : X
hx : x ∈ s
⊢ μH[d] s ≤ 1
Module: Mathlib.Analysis.InnerProductSpace.OfNorm

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : I * I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ -
        I * 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖) =
    4⁻¹ *
      (-I *
        (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
          I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖))

Tactic:
have h₂ : ‖-x + y‖ = ‖x - y‖ := by rw [← neg_sub, norm_neg, sub_eq_neg_add]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
hI : ¬I = 0
x y : E
hI' : I * I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
⊢ 4⁻¹ *
      (𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ - 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖ + I * 𝓚 ‖-x + y‖ * 𝓚 ‖-x + y‖ -
        I * 𝓚 ‖-x - y‖ * 𝓚 ‖-x - y‖) =
    4⁻¹ *
      (-I *
        (𝓚 ‖x + y‖ * 𝓚 ‖x + y‖ - 𝓚 ‖x - y‖ * 𝓚 ‖x - y‖ + I * 𝓚 ‖I • x + y‖ * 𝓚 ‖I • x + y‖ -
          I * 𝓚 ‖I • x - y‖ * 𝓚 ‖I • x - y‖))
Module: Mathlib.Analysis.InnerProductSpace.StarOrder

Goal state before:
pp: case mp
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p

Tactic:
obtain ⟨p, hp₁, -, hp₃⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts
        h.isSelfAdjoint h.spectrumRestricts

Goal state after:
case mp
𝕜 : Type u_1
H : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
inst✝² : Algebra ℝ (H →L[𝕜] H)
inst✝¹ : IsScalarTower ℝ 𝕜 (H →L[𝕜] H)
inst✝ : ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint
f g : H →L[𝕜] H
h : (g - f).IsPositive
p : H →L[𝕜] H
hp₁ : IsSelfAdjoint p
hp₃ : p * p = g - f
⊢ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), g = f + p
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr
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
⊢ μH[1] ((fun x ↦ ‖v‖ • x) '' ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s

Tactic:
have iso_smul : Isometry (LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) := by
    refine AddMonoidHomClass.isometry_of_norm _ fun x => (norm_smul _ _).trans ?_
    rw [norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn, mul_one, LinearMap.id_apply]

Goal state after:
case inr
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
iso_smul : Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))
⊢ μH[1] ((fun x ↦ ‖v‖ • x) '' ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr
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
iso_smul : Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))
⊢ μH[1] ((fun x ↦ ‖v‖ • x) '' ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s

Tactic:
Set.image_smul,

Goal state after:
case inr
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
iso_smul : Isometry ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v))
⊢ μH[1] (‖v‖ • ⇑(LinearMap.toSpanSingleton ℝ E (‖v‖⁻¹ • v)) '' s) = ‖v‖₊ • μH[1] s
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ μH[d] ((fun x ↦ c • x) '' ⇑(IsometryEquiv.vaddConst x).symm '' s) = ‖c‖₊ ^ d • μH[d] s

Tactic:
Set.image_smul,

Goal state after:
𝕜 : Type u_4
E : Type u_5
P : Type u_6
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : MeasurableSpace P
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor E P
inst✝ : BorelSpace P
d : ℝ
hd : 0 ≤ d
x : P
c : 𝕜
hc : c ≠ 0
s : Set P
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ μH[d] (c • ⇑(IsometryEquiv.vaddConst x).symm '' s) = ‖c‖₊ ^ d • μH[d] 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)
x : E
⊢ ∀ (v : E), ⟪v, o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)⟫ = ⟪v, -x⟫

Tactic:
intro y

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪y, o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)⟫ = ⟪y, -x⟫
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
⊢ ∀ (v : E), ⟪(-o).rightAngleRotation x, v⟫ = ⟪-o.rightAngleRotation x, v⟫

Tactic:
intro y

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪(-o).rightAngleRotation x, y⟫ = ⟪-o.rightAngleRotation x, y⟫
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)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x : F
⊢ ∀ (v : F), ⟪((map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x, v⟫ = ⟪φ (o.rightAngleRotation (φ.symm x)), v⟫

Tactic:
intro y

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ⟪((map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x, y⟫ = ⟪φ (o.rightAngleRotation (φ.symm x)), y⟫
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
⊢ rexp (-x) * x ^ (u - 1) = (rexp (-c * x) * x ^ (c * (u - 1))) ^ (1 / c)

Tactic:
rw [mul_rpow (exp_pos _).le ((rpow_nonneg hx.le) _), ← exp_mul, ← rpow_mul hx.le]

Goal state after:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
⊢ rexp (-x) * x ^ (u - 1) = rexp (-c * x * (1 / c)) * x ^ (c * (u - 1) * (1 / c))
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case hbc.inl
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))
h2 : IntegrableOn (F s) (Ioi 0) volume
h3 : AEStronglyMeasurable (F' s) (volume.restrict (Ioi 0))
t : ℝ
ht : t ∈ Ioi 0
z : ℂ
hz : z ∈ Metric.ball s v
h : 1 ≤ t
⊢ t ^ (z - 1).re ≤ t ^ (s.re + v - 1) + t ^ (s.re - v - 1)

Tactic:
refine le_add_of_le_of_nonneg (rpow_le_rpow_of_exponent_le h ?_)
        (by positivity)
      rw [sub_re, one_re, sub_le_sub_iff_right]
      rw [mem_ball_iff_norm] at hz
      have hz' := (re_le_norm _).trans hz.le
      rwa [sub_re, sub_le_iff_le_add'] at hz'

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

Goal state before:
pp: case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) = ↑a ^ (s - 1) * ↑(x / a) ^ (s - 1)

Tactic:
← mul_cpow_ofReal_nonneg ha.le (div_pos hx.1 ha).le,

Goal state after:
case e_a
s t : ℂ
a : ℝ
ha : 0 < a
ha' : ↑a ≠ 0
A : ↑a ^ (s + t - 1) = ↑a * (↑a ^ (s - 1) * ↑a ^ (t - 1))
x : ℝ
hx : x ∈ Ioc 0 a
⊢ ↑x ^ (s - 1) = (↑a * ↑(x / a)) ^ (s - 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

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

Tactic:
Nat.cast_add_one n

Goal state after:
x : ℝ
n : ℕ
this : ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) = ∑ k ∈ Finset.range (n + 1), log (x + ↑(k + 1))
⊢ (x + 1) * log ↑n + log ↑n ! - ∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) =
    x * log (↑n + 1) + (log (↑n + 1) + log ↑n !) - (∑ m ∈ Finset.range (n + 1), log (x + 1 + ↑m) + log x) + log x -
      (x + 1) * (log (↑n + 1) - log ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ y ∈ Icc 0 (π / 2), y ≠ 0 → cos y < cos 0
c_nonneg : ∀ x ∈ Icc 0 (π / 2), 0 ≤ cos x
c_zero_pos : 0 < cos 0
⊢ 0 ∈ closure (interior (Icc 0 (π / 2)))

Tactic:
interior_Icc,

Goal state after:
f : ℝ → ℂ
hf : ContinuousOn f (Icc 0 (π / 2))
c_lt : ∀ y ∈ Icc 0 (π / 2), y ≠ 0 → cos y < cos 0
c_nonneg : ∀ x ∈ Icc 0 (π / 2), 0 ≤ cos x
c_zero_pos : 0 < cos 0
⊢ 0 ∈ closure (Ioo 0 (π / 2))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
⊢ ∀ {y : ℝ}, 0 < y → (log ∘ f) (y + 1) = (log ∘ f) y + log y

Tactic:
intro y

Goal state after:
case refine_1
f : ℝ → ℝ
hf_conv : ConvexOn ℝ (Ioi 0) (log ∘ f)
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = y * f y
hf_pos : ∀ {y : ℝ}, 0 < y → 0 < f y
hf_one : f 1 = 1
x : ℝ
hx : x ∈ Ioi 0
y : ℝ
⊢ 0 < y → (log ∘ f) (y + 1) = (log ∘ f) y + log y
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
⊢ ¬asymptoticCone ℝ s ⊆ {0} ↔ ∃ v, v ≠ 0 ∧ v ∈ asymptoticCone ℝ s

Tactic:
Set.subset_singleton_iff,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set P
⊢ (¬∀ y ∈ asymptoticCone ℝ s, y = 0) ↔ ∃ v, v ≠ 0 ∧ v ∈ asymptoticCone ℝ s
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
hs : Convex k s
⊢ Convex k (asymptoticCone k s)

Tactic:
by
  wlog hs' : IsClosed s generalizing s
  · rw [← asymptoticCone_closure]; exact this hs.closure isClosed_closure
  rcases s.eq_empty_or_nonempty with rfl | ⟨p, hp⟩
  · rw [asymptoticCone_empty]; exact convex_empty
  intro v hv u hu a b ha hb hab
  rw [mem_asymptoticCone_iff]
  refine tendsto_id.atTop_smul_const_tendsto_asymptoticNhds _ |>.asymptoticNhds_vadd_const p
    |>.frequently (Eventually.frequently ?_)
  filter_upwards [eventually_ge_atTop 0] with c hc
  simp_rw [id, smul_add, smul_smul]
  have h₁ : c • v +ᵥ p ∈ s := hs.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone hs' hc hv hp
  have h₂ : c • u +ᵥ p ∈ s := hs.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone hs' hc hu hp
  apply hs.segment_subset h₁ h₂
  rw [← affineSegment_eq_segment, mem_vadd_const_affineSegment, affineSegment_eq_segment]
  exists a, b, ha, hb, hab
  module

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

Goal state before:
pp: z : ℂ
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

Tactic:
have pi_ne : (π : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr pi_ne_zero

Goal state after:
z : ℂ
pi_ne : ↑π ≠ 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)