mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : α → α
g : α → M
h : g ∘ f = g
n : ℕ
hn : ↑n ≠ 0
⊢ birkhoffAverage R f g n = g

Tactic:
by
  funext x
  suffices (n : R)⁻¹ • n • g x = g x by simpa [birkhoffAverage, birkhoffSum_of_comp_eq h]
  rw [← Nat.cast_smul_eq_nsmul (R := R), ← mul_smul, inv_mul_cancel₀ hn, one_smul]

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

Goal state before:
pp: case hg_ker.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (↑f - 1).rangeᗮ
⊢ RCLike.re ⟪↑f x, ↑1 x⟫ = ‖↑1 x‖ ^ 2

Tactic:
have : ∀ y, ⟪f y, x⟫ = ⟪y, x⟫ := by
        simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx
      simp [this]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
i : ℕ
⊢ 0 ≤ if h : ∃ a, Fin.valEmbedding a = i then (Finsupp.ofSupportFinite (fun i ↦ √(⋯.eigenvalues ⋯ i)) ⋯) h.choose else 0

Tactic:
Finsupp.ofSupportFinite_coe

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
i : ℕ
⊢ 0 ≤ if h : ∃ a, Fin.valEmbedding a = i then √(⋯.eigenvalues ⋯ h.choose) else 0
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
⊢ T.singularValues j ^ 2 ≤ T.singularValues i ^ 2

Tactic:
T.sq_singularValues_fin rfl ⟨j, hj⟩,

Goal state after:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
⊢ ⋯.eigenvalues ⋯ ⟨j, hj⟩ ≤ T.singularValues i ^ 2
Module: Mathlib.Analysis.InnerProductSpace.SingularValues

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : FiniteDimensional 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : FiniteDimensional 𝕜 F
T : E →ₗ[𝕜] F
i j : ℕ
hij : i ≤ j
hj : j < finrank 𝕜 E
⊢ ⋯.eigenvalues ⋯ ⟨j, hj⟩ ≤ ⋯.eigenvalues ⋯ ⟨i, ⋯⟩

Tactic:
exact T.isSymmetric_adjoint_comp_self.eigenvalues_antitone rfl hij

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))⁻¹
H : p'⁻¹ ≤ q⁻¹
⊢ q ≤ p'

Tactic:
rwa [inv_le_inv₀] at H

Goal state after:
case ha
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))⁻¹
H : p'⁻¹ ≤ q⁻¹
⊢ 0 < p'

case hb
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))⁻¹
H : p'⁻¹ ≤ q⁻¹
⊢ 0 < q
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
s : Set ι
hs : s.Countable
t : ι → Set X
⊢ dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)

Tactic:
have := hs.toEncodable
  rw [biUnion_eq_iUnion, dimH_iUnion, ← iSup_subtype'']

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

Goal state before:
pp: E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ μH[↑d] = 0

Tactic:
rw [← measure_univ_eq_zero]

Goal state after:
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ μH[↑d] univ = 0
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inl.inr.inl
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
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this : f '' s = {f x}
hd : 0 ≤ 0
⊢ μH[0] {f x} ≤ ↑0 ^ 0 * μH[↑r * 0] s

Tactic:
simp only [ENNReal.rpow_zero, one_mul, mul_zero]

Goal state after:
case inl.inr.inl
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
r : ℝ≥0
f : X → Y
s : Set X
hr : 0 < r
h : HolderOnWith 0 r f s
x : X
hx : x ∈ s
this : f '' s = {f x}
hd : 0 ≤ 0
⊢ μH[0] {f x} ≤ μH[0] s
Module: Mathlib.Analysis.InnerProductSpace.StandardSubspace

Goal state before:
pp: case mpr
H : Type u_1
inst✝ : NormedAddCommGroup H
ipc : InnerProductSpace ℂ H
S : ClosedSubmodule ℝ H
x : H
⊢ x ∈ S → x ∈ S.mulI.mulI

Tactic:
intro h
    rw [← SetLike.forall_smul_mem_iff] at h
    simpa [← smul_assoc, Units.smul_def] using (h (-1 : ℝ))

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
inst✝¹ : InnerProductSpaceable E
inst✝ : NormedSpace ℝ E
⊢ UniformConvexSpace E

Tactic:
by
  cases nonempty_innerProductSpace ℝ E; infer_instance

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

Goal state before:
pp: 𝕜 : 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
⊢ (fun s ↦ star s * s) p = p ^ 2

Tactic:
by simp only [hp₁.star_eq, sq]

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

Goal state before:
pp: case pos
𝕜 : 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
⊢ diag hS i j = (lowerInv hS * S * (lowerInv hS)ᴴ) i j

Tactic:
simp only [diag, diagEntries, EuclideanSpace.inner_toLp_toLp, star_star, hij,
      diagonal_apply_eq, Matrix.mul_assoc, dotProduct_comm]
    rfl

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d : ℝ
hd' : ∀ᶠ (x : ℝ) in atTop, ‖f x‖ ≤ d * ‖x ^ (-a)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c) volume

Tactic:
eventually_atTop

Goal state after:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d : ℝ
hd' : ∃ a_1, ∀ (b : ℝ), a_1 ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c) volume
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖z‖ ≤ 1 - t * ‖z‖

Tactic:
nlinarith [norm_nonneg z]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ HasFiniteIntegral (fun t ↦ t ^ (s - 1) * f t) (volume.restrict (Ioi (max e 1)))

Tactic:
have : ∀ᵐ t : ℝ ∂volume.restrict (Ioi <| max e 1),
        ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d := by
      refine (ae_restrict_mem measurableSet_Ioi).mono fun t ht => ?_
      have ht' : 0 < t := he'.trans ht
      rw [norm_mul, rpow_add ht', ← norm_of_nonneg (rpow_nonneg ht'.le (-a)), mul_assoc,
        mul_comm _ d, norm_of_nonneg (rpow_nonneg ht'.le _)]
      gcongr
      exact he t ((le_max_left e 1).trans_lt ht).le
    refine (HasFiniteIntegral.mul_const ?_ _).mono' this
    exact (integrableOn_Ioi_rpow_of_lt (by linarith) he').hasFiniteIntegral

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioo 0 ε), ‖a ^ (s - 1) * f a‖ ≤ d * a ^ (s - b - 1)

Tactic:
refine (ae_restrict_iff' measurableSet_Ioo).mpr (Eventually.of_forall fun t ht => ?_)

Goal state after:
case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
⊢ ‖t ^ (s - 1) * f t‖ ≤ d * t ^ (s - b - 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ (1 - ‖z‖)⁻¹ ≤ 2

Tactic:
inv_eq_one_div,

Goal state after:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 1 / (1 - ‖z‖) ≤ 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖logTaylor n z - log (1 + z)‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖‖z‖ ^ n‖

Tactic:
norm_sub_rev,

Goal state after:
z : ℂ
hz : ‖z‖ < 1
n : ℕ
⊢ ‖log (1 + z) - logTaylor n z‖ ≤ max ‖log (1 + z)‖ (1 - ‖z‖)⁻¹ * ‖‖z‖ ^ n‖
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

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

Tactic:
rw [logGammaSeq, ← add_sub_assoc, le_sub_iff_add_le, ← f_add_nat_eq (@hf_feq) hx, add_comm x]
  refine (f_add_nat_le hf_conv (@hf_feq) (Nat.add_one_ne_zero n) hx hx').trans (le_of_eq ?_)
  rw [f_nat_eq @hf_feq (by lia : n + 1 ≠ 0), Nat.add_sub_cancel, Nat.cast_add_one]
  ring

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

Goal state before:
pp: 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
A : HasDerivAt (fun x ↦ x ^ v) (v * (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun y ↦ 1 - y) (-1) ↑x

Tactic:
apply HasDerivAt.const_sub

Goal state after:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := ⋯
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
A : HasDerivAt (fun x ↦ x ^ v) (v * (1 - ↑x) ^ (v - 1) * 1) (1 - ↑x)
⊢ HasDerivAt (fun x ↦ x) 1 ↑x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (log (Γ x)))

Tactic:
have : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1 := by
    simp_rw [Function.comp_apply, Gamma_one, log_one, sub_zero]

Goal state after:
x : ℝ
hx : 0 < x
this : log (Γ x) = (log ∘ Γ) x - (log ∘ Γ) 1
⊢ Tendsto (logGammaSeq x) atTop (𝓝 (log (Γ x)))
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
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
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P
⊢ ((𝓝 v).bind fun v ↦ map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)) ≤ map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)

Tactic:
nth_rw 2 [← nhds_bind_nhds]

Goal state after:
case a
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
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P
⊢ ((𝓝 v).bind fun v ↦ map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)) ≤ map (fun x ↦ x +ᵥ p) (atTop • (𝓝 v).bind 𝓝)
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case a
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
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P
⊢ ((𝓝 v).bind fun v ↦ map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)) ≤ map (fun x ↦ x +ᵥ p) (atTop • (𝓝 v).bind 𝓝)

Tactic:
simp only [le_def, mem_map, ← map₂_smul, mem_map₂_iff, mem_bind]

Goal state after:
case a
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
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
v : V
p : P
⊢ ∀ (x : Set P),
    (∃ s ∈ atTop,
        ∃ t, (∃ t_1 ∈ 𝓝 v, ∀ x ∈ t_1, t ∈ 𝓝 x) ∧ Set.image2 (fun x1 x2 ↦ x1 • x2) s t ⊆ (fun x ↦ x +ᵥ p) ⁻¹' x) →
      ∃ t ∈ 𝓝 v, ∀ x_1 ∈ t, ∃ s ∈ atTop, ∃ t ∈ 𝓝 x_1, Set.image2 (fun x1 x2 ↦ x1 • x2) s t ⊆ (fun x ↦ x +ᵥ p) ⁻¹' x
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case inr
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✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • v + b • u ∈ asymptoticCone k s

Tactic:
rw [mem_asymptoticCone_iff]

Goal state after:
case inr
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✝ s : Set V
hs : Convex k s
hs' : IsClosed[inst✝²] s
p : V
hp : p ∈ s
v : V
hv : v ∈ asymptoticCone k s
u : V
hu : u ∈ asymptoticCone k s
a b : k
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ᶠ (p : V) in asymptoticNhds k V (a • v + b • u), p ∈ s
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ max ‖(f.comp g) 0‖ ‖(f.comp g).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
max_le_iff

Goal state after:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ ∧ ‖(f.comp g).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖
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
⊢ ∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z

Tactic:
have h_bdd : BddAbove (range fun e : s => dist ((e : PE ≃ᵢ PE) z) z) := by
    refine ⟨dist x z + dist x z, forall_mem_range.2 <| Subtype.forall.2 ?_⟩
    rintro e ⟨hx, _⟩
    calc
      dist (e z) z ≤ dist (e z) x + dist x z := dist_triangle (e z) x z
      _ = dist (e x) (e z) + dist x z := by rw [hx, dist_comm]
      _ = dist x z + dist x z := by rw [e.dist_eq x z]

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)
⊢ ∀ (e : PE ≃ᵢ PE), e x = x → e y = y → e z = z
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg.convert_4.convert_5
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun x ↦ z * ∏ j ∈ Finset.range x, (1 - z ^ 2 / (↑j + 1) ^ 2)) atTop (𝓝 (sin (↑π * z) / ↑π))

Tactic:
rw [← tendsto_mul_iff_of_ne_zero tendsto_const_nhds pi_ne, div_mul_cancel₀ _ pi_ne]

Goal state after:
case neg.convert_4.convert_5
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
this✝ : ↑π / sin (↑π * z) = 1 * (↑π / sin (↑π * z))
this : ↑π / sin (↑π * z) = 1 / (sin (↑π * z) / ↑π)
⊢ Tendsto (fun n ↦ (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) * ↑π) atTop (𝓝 (sin (↑π * z)))
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.swap 0 j) = ⇑x ∘ s.points
⊢ 1 ≠ 0

Tactic:
by simp [hn]

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

Goal state before:
pp: 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : ¬i = 1
x : P ≃ᵢ P
hx : s.points ∘ ⇑(Equiv.trans (Equiv.swap 0 i) (Equiv.swap 1 j)) = ⇑x ∘ s.points
⊢ 1 ≠ 0

Tactic:
by simp [hn]

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

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

Tactic:
Complex.sin,

Goal state after:
z : ℂ
⊢ HasSum (fun n ↦ (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((cexp (-z * I) - cexp (z * I)) * I / 2)
Module: Mathlib.Analysis.Normed.Ring.Ultra

Goal state before:
pp: case ofNat
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
a✝ : ℕ
⊢ ‖↑(Int.ofNat a✝)‖₊ ≤ 1

Tactic:
simpa only [Int.ofNat_eq_natCast, Int.cast_natCast, Int.cast_negSucc, Nat.cast_one, nnnorm_neg]
    using nnnorm_natCast_le_one _ _

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

Goal state before:
pp: case negSucc
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
a✝ : ℕ
⊢ ‖↑(Int.negSucc a✝)‖₊ ≤ 1

Tactic:
simpa only [Int.ofNat_eq_natCast, Int.cast_natCast, Int.cast_negSucc, Nat.cast_one, nnnorm_neg]
    using nnnorm_natCast_le_one _ _

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x + 1‖ ≤ max ‖x‖ 1
x y : R
hy : y ≠ 0
⊢ ‖x + y‖ ≤ max ‖x‖ ‖y‖

Tactic:
· 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:
Module: Mathlib.Analysis.Normed.Field.Ultra

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

Tactic:
by
  have (x : R) (hx : ‖x‖ ≤ 1) : ‖x + 1‖ ≤ 1 := by
    simpa only [← neg_add', norm_neg] using h (-x) (norm_neg x ▸ hx)
  exact isUltrametricDist_of_forall_norm_add_one_of_norm_le_one this

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
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
r : ℝ
⊢ √M ^ 2 ≤ ‖x - (algebraMap ℝ F) r‖ ^ 2

Tactic:
Real.sq_sqrt (norm_nonneg _),

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
r : ℝ
⊢ ‖φ x z‖ ≤ ‖x - (algebraMap ℝ F) r‖ ^ 2
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_4
inst✝⁷ : ConditionallyCompleteLinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : AddCommSemigroup R
inst✝³ : Sub R
inst✝² : ContinuousSub R
inst✝¹ : OrderedSub R
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ f
cobdd : ∃ b, ∀ (a : R), b ≥ a
⊢ sInf Set.univ = c - sSup Set.univ

Tactic:
rcases cobdd with ⟨x, hx⟩

Goal state after:
case inl
ι : Type u_1
R : Type u_4
inst✝⁷ : ConditionallyCompleteLinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : AddCommSemigroup R
inst✝³ : Sub R
inst✝² : ContinuousSub R
inst✝¹ : OrderedSub R
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
⊢ sInf Set.univ = c - sSup Set.univ
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ f
a : R
cobdd : ∃ b, ∀ (a : R), b ≤ a
⊢ BddBelow Set.univ

Tactic:
rcases cobdd with ⟨x, hx⟩

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : AddCommSemigroup R
inst✝² : Sub R
inst✝¹ : ContinuousSub R
inst✝ : OrderedSub R
f : ι → R
c : R
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ f
a x : R
hx : ∀ (a : R), x ≤ a
⊢ BddBelow Set.univ