mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace

Goal state before:
pp: case hab
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → α
g : α → E
n : ℕ
x y : α
⊢ dist (birkhoffSum f g n x) (birkhoffSum f g n y) ≤ ∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))

Tactic:
apply dist_birkhoffSum_birkhoffSum_le

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

Goal state before:
pp: case mp
𝕜 : 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
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
h : End.HasEigenvalue (adjoint T ∘ₗ T) 0
i : Fin (finrank 𝕜 E)
hi : ↑(⋯.eigenvalues ⋯ i) = 0
⊢ ∃ i < finrank 𝕜 E, T.singularValues i ≤ 0

Tactic:
use i, i.isLt

Goal state after:
case right
𝕜 : 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
this : (adjoint T ∘ₗ T).ker = ⊥ ↔ ¬End.HasEigenvalue (adjoint T ∘ₗ T) 0
h : End.HasEigenvalue (adjoint T ∘ₗ T) 0
i : Fin (finrank 𝕜 E)
hi : ↑(⋯.eigenvalues ⋯ i) = 0
⊢ T.singularValues ↑i ≤ 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
⊢ singularValues 0 = 0

Tactic:
by
  ext1 i
  rw [Finsupp.zero_apply, singularValues_eq_zero_iff_le_finrank_range, range_zero]
  simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
f : E →L[𝕜] F
⊢ ↑↑(commIsometry 𝕜 G F) ∘SL lTensor G f ∘SL ↑↑(commIsometry 𝕜 E G) = rTensor G f

Tactic:
ext; simp [lTensor]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
f : E →L[𝕜] F
⊢ lTensor G f ∘SL ↑↑(commIsometry 𝕜 E G) = ↑↑(commIsometry 𝕜 F G) ∘SL rTensor G f

Tactic:
ext; simp [lTensor]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
g : E →L[𝕜] F
⊢ rTensor G g ∘SL ↑↑(commIsometry 𝕜 G E) = ↑↑(commIsometry 𝕜 G F) ∘SL lTensor G g

Tactic:
ext; simp [lTensor]

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

Goal state before:
pp: case e_f
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
⊢ volume (Prod.mk x ⁻¹' ⇑(s.direction.measurableEquivProd ↑p).symm ⁻¹' t) =
    μHE[finrank ℝ ↥s.directionᗮ] (t ∩ ↑(mk' (↑((IsometryEquiv.vaddConst p) x)) s.directionᗮ))

Tactic:
have hrank : finrank ℝ s.directionᗮ = finrank ℝ (mk' (x +ᵥ p).val s.directionᗮ).direction := by
    rw [direction_mk']

Goal state after:
case e_f
V : Type u_3
P : Type u_4
inst✝⁸ : NormedAddCommGroup V
inst✝⁷ : InnerProductSpace ℝ V
inst✝⁶ : MeasurableSpace V
inst✝⁵ : BorelSpace V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : MetricSpace P
inst✝² : MeasurableSpace P
inst✝¹ : BorelSpace P
inst✝ : NormedAddTorsor V P
s : AffineSubspace ℝ P
hs : Nonempty ↥s
t : Set P
ht : MeasurableSet t
p : ↥s
x : ↥s.direction
u : Set ↥(mk' (↑(x +ᵥ p)) s.directionᗮ) := Subtype.val ⁻¹' (t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ))
hu : MeasurableSet u
hinter : t ∩ ↑(mk' (↑(x +ᵥ p)) s.directionᗮ) = Subtype.val '' u
hxp : ↑(x +ᵥ p) ∈ mk' (↑(x +ᵥ p)) s.directionᗮ
hrank : finrank ℝ ↥s.directionᗮ = finrank ℝ ↥(mk' (↑(x +ᵥ p)) s.directionᗮ).direction
⊢ volume (Prod.mk x ⁻¹' ⇑(s.direction.measurableEquivProd ↑p).symm ⁻¹' t) =
    μHE[finrank ℝ ↥s.directionᗮ] (t ∩ ↑(mk' (↑((IsometryEquiv.vaddConst p) x)) s.directionᗮ))
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
m : ℝ≥0∞ → ℝ≥0∞
s : Set X
⊢ (mkMetric m) s =
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : s ⊆ iUnion t), ⨅ (_ : ∀ (n : ℕ), ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (ediam (t n))

Tactic:
simp only [← OuterMeasure.coe_mkMetric, OuterMeasure.mkMetric, OuterMeasure.mkMetric',
    OuterMeasure.iSup_apply, OuterMeasure.mkMetric'.pre, OuterMeasure.boundedBy_apply, extend]
  refine
    surjective_id.iSup_congr id fun r =>
      iSup_congr_Prop Iff.rfl fun _ =>
        surjective_id.iInf_congr _ fun t => iInf_congr_Prop Iff.rfl fun ht => ?_
  dsimp
  by_cases htr : ∀ n, ediam (t n) ≤ r
  · rw [iInf_eq_if, if_pos htr]
    congr 1 with n : 1
    simp only [iInf_eq_if, htr n, if_true]
  · rw [iInf_eq_if, if_neg htr]
    push Not at htr; rcases htr with ⟨n, hn⟩
    refine ENNReal.tsum_eq_top_of_eq_top ⟨n, ?_⟩
    rw [iSup_eq_if, if_pos, iInf_eq_if, if_neg]
    · exact hn.not_ge
    rcases ediam_pos_iff.1 hn.pos with ⟨x, hx, -⟩
    exact ⟨x, hx⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
x y : X
⊢ ‖kernel H x y‖ ^ 2 ≤ ‖kernel H x x‖ * ‖kernel H y y‖

Tactic:
norm_kernel_le

Goal state after:
𝕜 : Type u_1
inst✝⁷ : RCLike 𝕜
X : Type u_2
V : Type u_3
inst✝⁶ : NormedAddCommGroup V
inst✝⁵ : InnerProductSpace 𝕜 V
H : Type u_4
inst✝⁴ : NormedAddCommGroup H
inst✝³ : InnerProductSpace 𝕜 H
inst✝² : RKHS 𝕜 H X V
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace V
x y : X
⊢ (√‖kernel H x x‖ * √‖kernel H y y‖) ^ 2 ≤ ‖kernel H x x‖ * ‖kernel H y y‖
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
d₁ d₂ : ℝ
h✝ : d₁ ≤ d₂
s : Set X
h : d₁ < d₂
⊢ μH[d₂] s ≤ μH[d₁] s

Tactic:
rcases hausdorffMeasure_zero_or_top h s with hs | hs <;> simp [hs]

Goal state after:
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
⊢ (map (Fin 2) φ.toLinearEquiv) o = o

Tactic:
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ

Goal state after:
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
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
⊢ (map (Fin 2) φ.toLinearEquiv) o = o

Tactic:
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ

Goal state after:
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
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: 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)

Tactic:
ofReal_sub,

Goal state after:
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: 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|⁻¹ • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s / ↑a - 1) • f t

Tactic:
conv_rhs => rw [← integral_comp_rpow_Ioi _ ha, ← integral_smul]

Goal state after:
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)
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) + ↑a * (s / ↑a - 1)) • f (t ^ a)

Tactic:
ofReal_sub,

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.SpecialFunctions.Gamma.BohrMollerup

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

Tactic:
have hn' : 0 < (n : ℝ) := Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)

Goal state after:
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
hx : 0 < x
hx' : x ≤ 1
hn' : 0 < ↑n
⊢ f (↑n + x) ≤ f ↑n + x * log ↑n
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
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
x✝ : V
⊢ (∃ᶠ (p : P) in (asymptoticNhds k V x✝).bind (asymptoticNhds k P), p ∈ s) ↔ ∃ᶠ (p : P) in asymptoticNhds k P x✝, p ∈ s

Tactic:
asymptoticNhds_bind_asymptoticNhds

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case refine_3.refine_1
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'
i : ↑s
r : k
hr :
  (Finset.affineCombination k (fs i) p) ((1 - r) • Pi.single (↑i) 1 + r • w i) =
    (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩)
⊢ ∑ i_1 ∈ fs i, ((1 - r) • Pi.single (↑i) 1 + r • w i) i_1 = 1

Tactic:
simp [Finset.sum_add_distrib, ← Finset.mul_sum, hw, hfs]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: case refine_3.refine_2
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'
i : ↑s
r : k
hr :
  (Finset.affineCombination k (fs i) p) ((1 - r) • Pi.single (↑i) 1 + r • w i) =
    (Finset.affineCombination k (fs ⟨i', hi'⟩) p) ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩)
⊢ ∑ i ∈ fs ⟨i', hi'⟩, ((1 - ri') • Pi.single i' 1 + ri' • w ⟨i', hi'⟩) i = 1

Tactic:
simp [Finset.sum_add_distrib, ← Finset.mul_sum, hw, hfs]

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

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
k : ℤ
⊢ π * s.im ≠ 0

Tactic:
exact mul_ne_zero Real.pi_pos.ne' h_im

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

Goal state before:
pp: s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (↑(Real.Gamma (2 * t)))⁻¹ * 2 ^ (-↑(1 - 2 * t)) * (↑√π)⁻¹ = (↑(Real.Gamma (2 * t)))⁻¹ * 2 ^ (↑(2 * t) - 1) / ↑√π

Tactic:
ofReal_sub,

Goal state after:
s : ℂ
h1 : AnalyticOnNhd ℂ (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (↑(Real.Gamma (2 * t)))⁻¹ * 2 ^ (-(↑1 - ↑(2 * t))) * (↑√π)⁻¹ = (↑(Real.Gamma (2 * t)))⁻¹ * 2 ^ (↑(2 * t) - 1) / ↑√π
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case succ
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]}, p.IsMonicOfDegree (2 * n) → M ^ n ≤ ‖(aeval x) p‖
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n + 2)
f₁ f₂ : ℝ[X]
hf₁ : f₁.IsMonicOfDegree 2
hf₂ : f₂.IsMonicOfDegree (2 * n)
H : p = f₁ * f₂
a b : ℝ
hab : f₁ = X ^ 2 - C a * X + C b
⊢ M ^ (n + 1) ≤ ‖(aeval x) p‖

Tactic:
H,

Goal state after:
case succ
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]}, p.IsMonicOfDegree (2 * n) → M ^ n ≤ ‖(aeval x) p‖
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n + 2)
f₁ f₂ : ℝ[X]
hf₁ : f₁.IsMonicOfDegree 2
hf₂ : f₂.IsMonicOfDegree (2 * n)
H : p = f₁ * f₂
a b : ℝ
hab : f₁ = X ^ 2 - C a * X + C b
⊢ M ^ (n + 1) ≤ ‖(aeval x) (f₁ * f₂)‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: case e'_6
z : ℂ
this :
  HasSum
    (fun x ↦
      ((-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! - (z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) * I / 2)
    ((NormedSpace.exp (-z * I) - NormedSpace.exp (z * I)) * I / 2)
k : ℕ
⊢ (z ^ 2) ^ k * ((I ^ 2) ^ k * (z * I)) / ↑(2 * k + 1)! / I =
    -((z ^ 2) ^ k * ((I ^ 2) ^ k * (z * I)) / ↑(2 * k + 1)! * I)

Tactic:
Complex.div_I

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
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
⊢ ((q w - q u) ^ n).natDegree < 2 * n

Tactic:
hsub

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
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2
hdvd : q u ∣ q w ^ n - (q w - q u) ^ n
⊢ (((C u.1 - C w.1) * X + C w.2 - C u.2) ^ n).natDegree < 2 * n
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
hy : 0 y < f y
⊢ f (x * y) / f y ≤ c * f x

Tactic:
· rw [div_le_iff₀ hy]
    apply f_mul

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h : f x = 0
⊢ seminormFromBounded' f x = 0

Tactic:
have hf : seminormFromBounded' f x ≤ c * f x :=
      seminormFromBounded_le f_nonneg f_mul x

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h : f x = 0
hf : seminormFromBounded' f x ≤ c * f x
⊢ seminormFromBounded' f x = 0
Module: Mathlib.Topology.Algebra.Order.LiminfLimsup

Goal state before:
pp: case inl
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ u x * v x
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
u_0 : u x < 0
⊢ u x * v x ≤ a * b

Tactic:
apply (mul_nonpos_of_nonpos_of_nonneg u_0.le v_0).trans

Goal state after:
case inl
ι : Type u_1
f : Filter ι
u v : ι → ℝ
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ u x * v x
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u * v)
a : ℝ
a_u : a > limsup u f
b : ℝ
b_v : b > limsup v f
c : ℝ
c_ab : c > a * b
x : ι
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
u_0 : u x < 0
⊢ 0 ≤ a * b
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
⊢ Tendsto (fun n ↦ (L + ε) ^ (-(↑(n % m1) / ↑n)) * (μ x ^ (n % m1)) ^ (1 / ↑n)) atTop (𝓝 1)

Tactic:
rw [← mul_one (1 : ℝ)]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
⊢ Tendsto (fun n ↦ (L + ε) ^ (-(↑(n % m1) / ↑n)) * (μ x ^ (n % m1)) ^ (1 * 1 / ↑n)) atTop (𝓝 (1 * 1))
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n ↦ ↑(n % m1) / ↑n) atTop (𝓝 0)
h0 : Tendsto (fun t ↦ -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ (L + ε) ^ (-(↑(x % m1) / ↑x))) atTop (𝓝 ((L + ε) ^ 0))

Tactic:
apply Tendsto.rpow tendsto_const_nhds h0

Goal state after:
case hf
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
L : ℝ
hL : 0 ≤ L
ε : ℝ
hε : 0 < ε
m1 : ℕ
hm1 : 0 < m1
x : R
hx : μ x ≠ 0
h_exp : Tendsto (fun n ↦ ↑(n % m1) / ↑n) atTop (𝓝 0)
h0 : Tendsto (fun t ↦ -(↑(t % m1) / ↑t)) atTop (𝓝 0)
⊢ L + ε ≠ 0 ∨ 0 < 0
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: case h
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
h : (C ^ (1 / ↑n)) ^ n = C
⊢ nα (x ^ n) ≤ nα x ^ n

Tactic:
exact map_pow_le_pow _ _ (Nat.one_le_iff_ne_zero.mp hn)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq : ∀ (y : S), ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥R[y]), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
⊢ f₁ x = f₂ x

Tactic:
set g₁ : AlgebraNorm R R[(x : S)] := AlgebraNorm.restriction _ f₁

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : NormedCommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f₁ : AlgebraNorm R S
hf₁_pm : IsPowMul ⇑f₁
f₂ : AlgebraNorm R S
hf₂_pm : IsPowMul ⇑f₂
h_eq : ∀ (y : S), ∃ C₁ C₂, ∃ (_ : 0 < C₁) (_ : 0 < C₂), ∀ (x : ↥R[y]), f₁ ↑x ≤ C₁ * f₂ ↑x ∧ f₂ ↑x ≤ C₂ * f₁ ↑x
x : S
g₁ : AlgebraNorm R ↥R[x] := AlgebraNorm.restriction R[x] f₁
⊢ f₁ x = f₂ x
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
⊢ smoothingSeminormSeq μ x n < L + ε

Tactic:
by_cases hxn : μ (x ^ (n % m1)) = 0

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : μ (x ^ (n % ↑m1)) = 0
⊢ smoothingSeminormSeq μ x n < L + ε

case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
hL_le : L ≤ smoothingSeminormSeq μ x n
hxn : ¬μ (x ^ (n % ↑m1)) = 0
⊢ smoothingSeminormSeq μ x n < L + ε
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedRing R
p : R[X]
n : ℕ
⊢ 0 ≤ if n < p.natDegree then ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n)) else 0

Tactic:
split_ifs with h

Goal state after:
case pos
R : Type u_1
inst✝ : SeminormedRing R
p : R[X]
n : ℕ
h : n < p.natDegree
⊢ 0 ≤ ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n))

case neg
R : Type u_1
inst✝ : SeminormedRing R
p : R[X]
n : ℕ
h : ¬n < p.natDegree
⊢ 0 ≤ 0