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)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis * bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis = 1
⊢ ‖(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‖

Tactic:
rw [← Matrix.det_comm' h1 h2, ← Matrix.mul_assoc, Matrix.det_mul, norm_mul]

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)
h1 : bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis = 1
h2 : (stdOrthonormalBasis 𝕜 U).toBasis.toMatrix ⇑bu.toBasis * bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis = 1
⊢ ‖(bu.toBasis.toMatrix ⇑(stdOrthonormalBasis 𝕜 U).toBasis * h.some.toBasis.toMatrix ⇑bv.toBasis).det‖ *
      ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖ =
    ‖((toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : r < dimH s
⊢ ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t

Tactic:
contrapose! h

Goal state after:
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, dimH t ≤ r
⊢ dimH s ≤ r
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
x : ι → ℝ
r : ℝ
hr : 0 < r
h✝ : Nonempty ι
⊢ μH[↑(Fintype.card ι)] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr]

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
inst✝ : CompleteSpace V
K : Matrix X X (V →L[𝕜] V)
this : ∀ {h p1 p2 p3 : Prop}, (h → [p1, p2, p3].TFAE) → [h ∧ p1, h ∧ p2, h ∧ p3].TFAE
hHerm : K.IsHermitian
x✝ : Nontrivial V
v : V
hv : v ≠ 0
tfae_1_to_2 :
  (∀ (x : X →₀ V →L[𝕜] V) (x_1 : V),
      0 ≤ RCLike.re (x.sum fun i a ↦ x.sum fun i_1 a_1 ↦ ⟪(K i i_1) (a_1 x_1), a x_1⟫_𝕜)) →
    ∀ (f : X × V →₀ 𝕜),
      0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)
h :
  ∀ (f : X × V →₀ 𝕜),
    0 ≤ RCLike.re (f.sum fun xv z ↦ f.sum fun xv' w ↦ (starRingEnd 𝕜) z * w * ⟪(K xv'.1 xv.1) xv.2, xv'.2⟫_𝕜)
vv : X →₀ V
⊢ 0 ≤ RCLike.re (vv.sum fun x w ↦ vv.sum fun x' w' ↦ ⟪(K x' x) w, w'⟫_𝕜)

Tactic:
by
    simpa [add_mul, Finsupp.sum_sum_index] using (h (vv.sum fun x v ↦ .single ⟨x, v⟩ 1))

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

Goal state before:
pp: case refine_1
ι : Type u_4
inst✝ : Fintype ι
a b : ι → ℚ
H : ∀ (i : ι), a i < b i
I : ∀ (i : ι), 0 ≤ ↑(b i) - ↑(a i)
γ : ℕ → Type u_4 := fun n ↦ (i : ι) → Fin ⌈(↑(b i) - ↑(a i)) * ↑n⌉₊
t : (n : ℕ) → γ n → Set (ι → ℝ) := fun n f ↦ univ.pi fun i ↦ Icc (↑(a i) + ↑↑(f i) / ↑n) (↑(a i) + (↑↑(f i) + 1) / ↑n)
A : Tendsto (fun n ↦ 1 / ↑n) atTop (𝓝 0)
B : ∀ᶠ (n : ℕ) in atTop, ∀ (i : γ n), ediam (t n i) ≤ 1 / ↑n
C : ∀ᶠ (n : ℕ) in atTop, (univ.pi fun i ↦ Ioo ↑(a i) ↑(b i)) ⊆ ⋃ i, t n i
i : ι
x✝ : i ∈ Finset.univ
⊢ Tendsto (fun n ↦ ↑⌈(↑(b i) - ↑(a i)) * ↑n⌉₊ / ↑n) atTop (𝓝 (ENNReal.ofReal (↑(b i) - ↑(a i))))

Tactic:
apply
          Tendsto.congr' _
            ((ENNReal.continuous_ofReal.tendsto _).comp
              ((tendsto_nat_ceil_mul_div_atTop (I i)).comp tendsto_natCast_atTop_atTop))
        apply eventually_atTop.2 ⟨1, fun n hn => _⟩
        intro n hn
        simp only [ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr hn), comp_apply,
          ENNReal.ofReal_natCast]

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
⊢ Fintype.card (Fin 2) = finrank ℝ E

Tactic:
@Fact.out (finrank ℝ E = 2),

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) = 2
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 y : E
⊢ (o.areaForm x) (o.rightAngleRotation y) = ⟪x, y⟫

Tactic:
← o.inner_rightAngleRotation_left,

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, o.rightAngleRotation y⟫ = ⟪x, y⟫
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: case e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ Fintype.card (Fin 2) = finrank ℝ E

Tactic:
@Fact.out (finrank ℝ E = 2),

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) = 2
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁹ : NormedField 𝕜₁
inst✝⁸ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜₂ F
x : E
y : F⋆
⊢ Continuous[instTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun A ↦ y (A x)

Tactic:
by
  refine (continuous_pi_iff.mp continuous_inducingFn) ⟨x, y⟩

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)
x y : E
⊢ (o.kahler x) (o.rightAngleRotation y) = Complex.I * (o.kahler x) y

Tactic:
simp only [o.areaForm_rightAngleRotation_right, o.inner_rightAngleRotation_right,
    o.kahler_apply_apply, Complex.ofReal_neg, Complex.real_smul]

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.areaForm x) y) + ↑⟪x, y⟫ * Complex.I = Complex.I * (↑⟪x, y⟫ + ↑((o.areaForm x) y) * Complex.I)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_1
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
t : ℝ
ht : t ∈ Ioi (max e 1)
⊢ ContinuousAt (fun t ↦ t ^ (s - 1)) t

Tactic:
exact continuousAt_rpow_const _ _ (Or.inl <| (he'.trans ht).ne')

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

Goal state before:
pp: case h
n : ℕ
⊢ ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ 2 / (↑n + 1) * ‖x ^ (n + 1)‖

Tactic:
filter_upwards [
    eventually_norm_sub_lt 0 one_pos,
    eventually_norm_sub_lt 0 (show 0 < 1 / 2 by simp)] with z hz1 hz12

Goal state after:
n : ℕ
z : ℂ
hz1 : ‖z - 0‖ < 1
hz12 : ‖z - 0‖ < 1 / 2
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / (↑n + 1) * ‖z ^ (n + 1)‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: t : ℝ
⊢ Tendsto (fun x ↦ (1 + t / x) ^ x) atTop (𝓝 (rexp t))

Tactic:
by
  apply tendsto_one_add_rpow_exp_of_tendsto
  apply tendsto_nhds_of_eventually_eq
  filter_upwards [eventually_ne_atTop 0] with x hx0
  exact mul_div_cancel₀ t (mod_cast hx0)

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ ∫ (x : ℝ) in 0..1, ↑x ^ (s - 1) = 1 / s

Tactic:
integral_cpow (Or.inl aux1),

Goal state after:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ (↑1 ^ (s - 1 + 1) - ↑0 ^ (s - 1 + 1)) / (s - 1 + 1) = 1 / s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: A : 0 < 3 / 2
⊢ 1 / 2 ≤ 1

Tactic:
by norm_num

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

Goal state before:
pp: A : 0 < 3 / 2
this : log (Γ (2 + 1 / 2)) ≤ 1 / 2 * log 2
⊢ 2 + 1 / 2 = 3 / 2 + 1

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 1 < 3 / 2

Tactic:
by norm_num

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

Goal state before:
pp: ⊢ 3 / 2 < 2

Tactic:
by norm_num

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

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
⊢ 3 / 2 ∈ Icc 1 2

Tactic:
by norm_num

Goal state after:
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
s : Set P
hs : Bornology.IsBounded s
⊢ asymptoticCone ℝ s ⊆ {0}

Tactic:
intro v h

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Bornology.IsBounded s
v : V
h : v ∈ asymptoticCone ℝ s
⊢ v ∈ {0}
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
⊢ ¬Bornology.IsBounded s ↔ ∃ v, v ≠ 0 ∧ v ∈ asymptoticCone ℝ s

Tactic:
by
  rw [isBounded_iff_asymptoticCone_subset_singleton, Set.subset_singleton_iff, not_forall]
  tauto

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

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
| ∫ (x : ℝ) in 0..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)

Tactic:
enter [1, x, 2, 1]; rw [this x]

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
x : ℝ
| ↑(x / ↑n * ↑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
p : P
⊢ ∀ (x : V), (∃ᶠ (y : V) in 𝓝 x, y ∈ asymptoticCone k s) → x ∈ asymptoticCone k s

Tactic:
intro v h

Goal state after:
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
p : P
v : V
h : ∃ᶠ (y : V) in 𝓝 v, y ∈ asymptoticCone k s
⊢ v ∈ asymptoticCone k s
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
⊢ Convex k (asymptoticCone k s)

Tactic:
intro v hv u hu a b ha hb hab

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
⊢ a • v + b • u ∈ asymptoticCone k s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

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

Tactic:
indicator_of_mem (mem_Ioc.mpr ⟨mem_Ioi.mp hx, hxn⟩),

Goal state after:
case inr
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : x ≤ ↑n
⊢ ‖↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)‖ ≤ rexp (-x) * x ^ (s.re - 1)
Module: Mathlib.Analysis.Polynomial.Factorization

Goal state before:
pp: case inl.inr
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
rw [h', mul_left_comm] at h hf
      exact ⟨p₁, g₁ * p₂, hp₂, of_mul_left hp₂ hf, h⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ 0 < ENNReal.toReal 1

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: 𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹² : SeminormedCommRing S
inst✝¹¹ : SeminormedRing R
inst✝¹⁰ : SeminormedAddCommGroup M
inst✝⁹ : Algebra S R
inst✝⁸ : Module S M
inst✝⁷ : IsBoundedSMul S R
inst✝⁶ : IsBoundedSMul S M
inst✝⁵ : Module R M
inst✝⁴ : IsBoundedSMul R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsBoundedSMul Rᵐᵒᵖ M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝ : NormOneClass R
⊢ ‖fst 1‖ + ‖snd 1‖ = 1

Tactic:
fst_one,

Goal state after:
𝕜 : Type u_1
S : Type u_2
R : Type u_3
M : Type u_4
inst✝¹² : SeminormedCommRing S
inst✝¹¹ : SeminormedRing R
inst✝¹⁰ : SeminormedAddCommGroup M
inst✝⁹ : Algebra S R
inst✝⁸ : Module S M
inst✝⁷ : IsBoundedSMul S R
inst✝⁶ : IsBoundedSMul S M
inst✝⁵ : Module R M
inst✝⁴ : IsBoundedSMul R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : IsBoundedSMul Rᵐᵒᵖ M
inst✝¹ : SMulCommClass R Rᵐᵒᵖ M
inst✝ : NormOneClass R
⊢ ‖1‖ + ‖snd 1‖ = 1
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Goal state before:
pp: case inr.calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ k⁻¹ • ((-1) ^ n * ‖q‖ ^ (2 * n)) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q

Tactic:
rw [smul_smul]

Goal state after:
case inr.calc_2
q : ℍ
hq : q.re = 0
n : ℕ
hq0 : q ≠ 0
hq2 : q ^ 2 = -↑(normSq q)
hqn : ‖q‖ ≠ 0
k : ℝ := ↑(2 * n + 1)!
⊢ (k⁻¹ * ((-1) ^ n * ‖q‖ ^ (2 * n))) • q = ((-1) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
inst✝ : NormedField K
f g : K[X]
ε : ℝ
hε : 0 < ε
a : K
ha : eval a f = 0
hfm : f.Monic
hgm : g.Monic
hdeg : g.natDegree = f.natDegree
hcoeff : ∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε
hg : g.Splits
this✝ : (Multiset.map (fun x ↦ ‖a - x‖) g.roots).prod < (↑f.natDegree + 1) * ε * max ‖a‖ 1 ^ ↑f.natDegree
h✝ : ∀ b ∈ g.roots, ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1 ≤ ‖a - b‖
this :
  ((↑f.natDegree + 1) * ε) ^ ((↑f.natDegree)⁻¹ * ↑f.natDegree) * max ‖a‖ 1 ^ ↑f.natDegree ≤
    (Multiset.map (fun b ↦ ‖a - b‖) g.roots).prod
h : f = 1
⊢ False

Tactic:
simp [h] at ha

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
x✝ : ℕ
⊢ 0 ≤ 1 / ↑(ψ x✝)

Tactic:
by simp only [one_div, inv_nonneg, cast_nonneg]

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

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
E : IntermediateField K L
x : ↥E
⊢ spectralNorm K (↥(normalClosure K (↥E) (AlgebraicClosure ↥E)))
      ((algebraMap ↥E ↥(normalClosure K (↥E) (AlgebraicClosure ↥E))) x) =
    spectralNorm K L ((algebraMap (↥E) L) x)

Tactic:
simp_rw [← spectralNorm.eq_of_tower]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε

Tactic:
rw [max_def]

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
b : ℝ := 1 - a
hb : b = 1 - a
hb_lim : Tendsto ((fun n ↦ ↑(nu n) / ↑n) ∘ ψ) atTop (𝓝 b)
b_in : b ∈ Set.Icc 0 1
hnu_le : ∀ (n : ℕ), nu n ≤ n
hx : limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a
hy : limsup (fun n ↦ μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ y ^ b
hxy :
  limsup (fun n ↦ μ (x ^ mu (ψ n)) ^ (1 / ↑(ψ n)) * μ (y ^ nu (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤
    smoothingFun μ x ^ a * smoothingFun μ y ^ b
ε : ℝ
hε : ε > 0
⊢ smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤
    (if smoothingFun μ x ≤ smoothingFun μ y then smoothingFun μ y else smoothingFun μ x) + ε
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hn : Normal K L
hu : IsUltrametricDist K
x : L
hna : IsNonarchimedean fun x ↦ ‖x‖
f : AlgebraNorm K L := Classical.choose ⋯
hf : f = Classical.choose ⋯
hf_pow : IsPowMul ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ‖x‖
hf_na : IsNonarchimedean ⇑f
⊢ ⨆ σ, f (σ x) = (invariantExtension K L) x

Tactic:
simp only [invariantExtension_apply, algNormOfAlgEquiv_apply, hf]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoEMetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ ((zipWith edist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ =
    ((zipWith edist ⋯ g.ofLp f.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹

Tactic:
simp only [sum, zipWith_apply, edist_comm]
    congr 2
    ext i
    simp [edist_comm]

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

Goal state before:
pp: R : Type u_1
K : Type u
inst✝³ : NontriviallyNormedField K
L : Type v
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1
x : L
hx : x ≠ 0
hx' : (spectralAlgNorm K L) x ≠ 0
k : K
y : L
h_mul :
  ∀ (y : L), spectralNorm K L ((algebraMap K L) k * y) = spectralNorm K L ((algebraMap K L) k) * spectralNorm K L y
⊢ spectralNorm K L ((algebraMap K L) k) = seminormFromConst' x (spectralAlgNorm K L).toRingSeminorm ((algebraMap K L) k)

Tactic:
rw [seminormFromConst_apply_of_isMul h1 hx' spectralAlgNorm_isPowMul h_mul]

Goal state after:
R : Type u_1
K : Type u
inst✝³ : NontriviallyNormedField K
L : Type v
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 : (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1
x : L
hx : x ≠ 0
hx' : (spectralAlgNorm K L) x ≠ 0
k : K
y : L
h_mul :
  ∀ (y : L), spectralNorm K L ((algebraMap K L) k * y) = spectralNorm K L ((algebraMap K L) k) * spectralNorm K L y
⊢ spectralNorm K L ((algebraMap K L) k) = (spectralAlgNorm K L).toRingSeminorm ((algebraMap K L) k)
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: 𝕜 : Type u_7
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type u_8
F : Type u_9
inst✝¹² : TopologicalSpace E
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : IsTopologicalAddGroup E
inst✝⁸ : ContinuousSMul 𝕜 E
inst✝⁷ : TopologicalSpace F
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : IsTopologicalAddGroup F
inst✝³ : ContinuousSMul 𝕜 F
inst✝² : T2Space F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 F
hf : Injective ⇑f
⊢ f.HasLeftInverse

Tactic:
by
  -- An injective linear map has a linear inverse; this inverse is automatically continuous
  -- because its domain is finite-dimensional.
  obtain ⟨g, hg⟩ :=
    f.toLinearMap.exists_leftInverse_of_injective (f.ker_eq_bot_of_injective hf)
  exact ⟨⟨g, LinearMap.continuous_of_finiteDimensional _⟩, fun x ↦ congr($hg x)⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set ↑(sphere 0 r)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x // x ∈ Ioi 0 }
hxU : ↑x ∈ U
this :
  Subtype.val ∘ ⇑(homeomorphSphereProd E r hr₀).symm '' V ×ˢ Ioi 0 ↓∩ U ∈
    𝓝[{0}ᶜ] ↑((homeomorphSphereProd E r hr₀).symm (y, x))
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}ᶜ

Tactic:
exact isOpen_compl_singleton

Goal state after: