mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℕ
hn : finrank 𝕜 E = n
i : Fin n
⊢ T.singularValues ↑i = √(⋯.eigenvalues hn i)

Tactic:
by
  subst hn
  exact Finsupp.embDomain_apply_self _ _ i

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

Goal state before:
pp: X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : (volume.addHaarScalarFactor μH[↑0] • μH[↑0]) {0} = volume {0}
| volume {0}

Tactic:
heq,

Goal state after:
X : Type u_1
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
basis : OrthonormalBasis (Fin 0) ℝ (EuclideanSpace ℝ (Fin 0)) := EuclideanSpace.basisFun (Fin 0) ℝ
heq : {0} = parallelepiped ⇑basis
h✝ : volume = volume.addHaarScalarFactor μH[↑0] • μH[↑0]
h : (volume.addHaarScalarFactor μH[↑0] • μH[↑0]) {0} = volume {0}
| volume (parallelepiped ⇑basis)
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d d' : ℝ≥0
hsd' : μH[↑d'] s = ∞
hdd' : d < d'
⊢ μH[↑d] s = ∞

Tactic:
← NNReal.coe_lt_coe

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d d' : ℝ≥0
hsd' : μH[↑d'] s = ∞
hdd' : ↑d < ↑d'
⊢ μH[↑d] s = ∞
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d < ↑d
d' : ℝ≥0
hsd' : ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d < ↑d'
hd'd : d' < d
⊢ μH[↑d] s = 0

Tactic:
← NNReal.coe_lt_coe

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d < ↑d
d' : ℝ≥0
hsd' : ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d < ↑d'
hd'd : ↑d' < ↑d
⊢ μH[↑d] s = 0
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
⊢ ⨅ d, ⨅ (_ : μH[↑d] s = 0), ↑d ≤ dimH s

Tactic:
by_contra! h
    rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hdim_lt, hlt⟩
    have h0 : μH[d'] s = 0 := hausdorffMeasure_of_dimH_lt hdim_lt
    exact hlt.not_ge (iInf₂_le d' h0)

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

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ x, limsup dimH (𝓝[s] x).smallSets = dimH s

Tactic:
refine le_antisymm (iSup_le fun x => ?_) ?_

Goal state after:
case refine_1
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
x : X
⊢ limsup dimH (𝓝[s] x).smallSets ≤ dimH s

case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ dimH s ≤ ⨆ x, limsup dimH (𝓝[s] x).smallSets
Module: Mathlib.Analysis.InnerProductSpace.NormDet

Goal state before:
pp: case neg
𝕜 : 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 ι 𝕜 V
this : FiniteDimensional 𝕜 V
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
h : IsUnit ((toMatrix bu.toBasis bv.toBasis) f).det
f' : U ≃ₗ[𝕜] V := LinearEquiv.ofIsUnitDet h
⊢ finrank 𝕜 U = finrank 𝕜 ↥f.range

Tactic:
have hf : f.range = ⊤ := f'.range

Goal state after:
case neg
𝕜 : 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 ι 𝕜 V
this : FiniteDimensional 𝕜 V
hdet : ¬‖((toMatrix bu.toBasis bv.toBasis) f).det‖ = 0
h : IsUnit ((toMatrix bu.toBasis bv.toBasis) f).det
f' : U ≃ₗ[𝕜] V := LinearEquiv.ofIsUnitDet h
hf : f.range = ⊤
⊢ finrank 𝕜 U = finrank 𝕜 ↥f.range
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inl.inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
⊢ μH[d] (f ⁻¹' s) ≤ ↑0 ^ d * μH[d] s

Tactic:
have : f ⁻¹' s = {x} := by
      have : Subsingleton X := hf.subsingleton
      have : (f ⁻¹' s).Subsingleton := subsingleton_univ.anti (subset_univ _)
      exact (subsingleton_iff_singleton hx).1 this

Goal state after:
case inl.inr
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hd : 0 ≤ d
s : Set Y
hf : AntilipschitzWith 0 f
x : X
hx : x ∈ f ⁻¹' s
this : f ⁻¹' s = {x}
⊢ μH[d] (f ⁻¹' s) ≤ ↑0 ^ d * μH[d] s
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case inr.refine_1
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
K : ℝ≥0
d : ℝ
hf : AntilipschitzWith K f
hd : 0 ≤ d
s : Set Y
h0 : K ≠ 0
hKd0 : ↑K ^ d ≠ 0
hKd : ↑K ^ d ≠ ∞
ε : ℝ≥0∞
ε0 : 0 < ε
t : ℕ → Set Y
htε : ∀ (n : ℕ), ediam (t n) ≤ ε / ↑K
hst : f ⁻¹' s ⊆ ⋃ i, f ⁻¹' t i
n : ℕ
⊢ ediam ((fun n ↦ f ⁻¹' t n) n) ≤ ε

Tactic:
exact (hf.ediam_preimage_le _).trans (ENNReal.mul_le_of_le_div' <| htε n)

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

Goal state before:
pp: case h'
ι : 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
n : ℕ
hn : 1 ≤ n
npos : 0 < ↑n
x : ι → ℝ
hx : ∀ (i : ι), ↑(a i) < x i ∧ x i < ↑(b i)
i : ι
⊢ 0 < ↑(b i) - ↑(a i)

Tactic:
simpa only [Rat.cast_lt, sub_pos] using H i

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

Goal state before:
pp: 𝕜 : Type u_4
E : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
d : ℝ
s : Set E
hs : 0 ≤ d
⊢ μH[d] (⇑K.orthogonalProjectionOnto '' s) ≤ μH[d] s

Tactic:
by
  simpa using K.lipschitzWith_orthogonalProjectionOnto.hausdorffMeasure_image_le hs s

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ

Tactic:
let f' : StrongDual 𝕜 (WeakSpace 𝕜 E) :=
    { toLinearMap := (f : E →ₗ[𝕜] 𝕜).comp ((toWeakSpace 𝕜 E).symm : WeakSpace 𝕜 E →ₗ[𝕜] E)
      cont := WeakBilin.eval_continuous (topDualPairing 𝕜 E).flip _ }

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsScalarTower ℝ 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : (toWeakSpace 𝕜 E).toEquiv x ∈ (⇑(toWeakSpace 𝕜 E) '' closure s)ᶜ
this : ContinuousSMul ℝ E
f : StrongDual 𝕜 E
u : ℝ
hus : ∀ a ∈ closure s, RCLike.re (f a) < u
hux : u < RCLike.re (f x)
f' : StrongDual 𝕜 (WeakSpace 𝕜 E) :=
  let __LinearMap := ↑f ∘ₗ ↑(toWeakSpace 𝕜 E).symm;
  { toLinearMap := __LinearMap, cont := ⋯ }
⊢ (toWeakSpace 𝕜 E).toEquiv x ∈ (closure (⇑(toWeakSpace 𝕜 E) '' s))ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: ⊢ ¬ContinuousAt Gamma (-↑0)

Tactic:
case =>

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

Goal state before:
pp: n : ℕ
ih : ¬ContinuousAt Gamma (-↑n)
⊢ ¬ContinuousAt Gamma (-↑(n + 1))

Tactic:
case =>

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

Goal state before:
pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ n) / (2 * z) -
      (↑n - 1) / (2 * z) * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2)) =
    -((Complex.cos ↑x ^ n - (↑n - 1) * (1 - Complex.cos ↑x ^ 2) * Complex.cos ↑x ^ (n - 2)) *
        (-Complex.cos (2 * z * ↑x) / (2 * z)))

Tactic:
←
      mul_div_right_comm,

Goal state after:
case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 :
  ∀ x ∈ uIcc 0 (π / 2),
    HasDerivAt (fun y ↦ ↑(sin y) * ↑(cos y) ^ (n - 1)) (↑(cos x) ^ n - (↑n - 1) * ↑(sin x) ^ 2 * ↑(cos x) ^ (n - 2)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ n) / (2 * z) -
      (↑n - 1) * (Complex.cos (2 * z * ↑x) * Complex.cos ↑x ^ (n - 2)) / (2 * z) =
    -((Complex.cos ↑x ^ n - (↑n - 1) * (1 - Complex.cos ↑x ^ 2) * Complex.cos ↑x ^ (n - 2)) *
        (-Complex.cos (2 * z * ↑x) / (2 * z)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ n = ∫ (x : ℝ) in 0 + π / 2..π / 2 + π / 2, sin x ^ n

Tactic:
rw [← integral_comp_add_right]

Goal state after:
case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ n = ∫ (x : ℝ) in 0..π / 2, sin (x + π / 2) ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e_a
n : ℕ
L : IntervalIntegrable (fun i ↦ sin i ^ n) volume 0 (π / 2)
R : IntervalIntegrable (fun i ↦ sin i ^ n) volume (π / 2) π
⊢ ∫ (x : ℝ) in 0..π / 2, cos x ^ n = ∫ (x : ℝ) in π / 2..π, sin x ^ n

Tactic:
nth_rw 3 [(by ring : π = π / 2 + π / 2)]
    nth_rw 2 [(by ring : π / 2 = 0 + π / 2)]
    rw [← integral_comp_add_right]
    refine integral_congr fun x _ => ?_
    rw [sin_add_pi_div_two]

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

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

Tactic:
rw [id, sub_re, one_re, ofReal_re, sub_pos]; exact hx.2

Goal state after:
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
⊢ (𝓝 v).bind (asymptoticNhds k P) ≤ asymptoticNhds k P v

Tactic:
have ⟨p⟩ : Nonempty P := inferInstance
    eta_expand
    simp_rw [asymptoticNhds_eq_smul_vadd _ p, vadd_pure]
    nth_rw 2 [← nhds_bind_nhds]
    simp only [le_def, mem_map, ← map₂_smul, mem_map₂_iff, mem_bind]
    grind

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

Goal state before:
pp: case hx
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
x : R
⊢ MulOpposite.op (inl x).fst • (inl x).snd = (inl x).fst • (inl x).snd

Tactic:
rw [snd_inl, fst_inl, smul_zero, smul_zero]

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

Goal state before:
pp: q : ℍ
⊢ √(normSq (exp q)) = ‖exp q.re‖

Tactic:
normSq_exp,

Goal state after:
q : ℍ
⊢ √(exp q.re ^ 2) = ‖exp q.re‖
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case refine_2
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
⊢ Tendsto (fun x_1 ↦ ‖x_1.1 • x - (algebraMap ℝ F) x_1.2‖) (cobounded ℝ ×ˢ ⊤) atTop

Tactic:
suffices Tendsto (fun y : ℝ × ℝ ↦ ‖y.1‖ * c) (cobounded ℝ ×ˢ ⊤) atTop by
      refine tendsto_atTop_mono' _ ?_ this
      filter_upwards [prod_mem_prod (isBounded_singleton (x := 0)) univ_mem] with y hy
      calc ‖y.1‖ * c
        _ ≤ ‖y.1‖ * ‖x - algebraMap ℝ F (y.1⁻¹ * y.2)‖ := by gcongr; exact hbd _
        _ = ‖y.1 • x - algebraMap ℝ F y.2‖ := by
          simp only [← norm_smul, smul_sub, smul_smul, Algebra.algebraMap_eq_smul_one]
          simp_all
    rw [tendsto_mul_const_atTop_of_pos hc₀, tendsto_norm_atTop_iff_cobounded]
    exact tendsto_fst

Goal state after:
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
⊢ ‖eval a g‖ ≤ ‖eval a g - eval a f‖ + ‖eval a f‖

Tactic:
by
    convert! norm_add_le (g.eval a - f.eval a) (f.eval a)
    simp

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

Goal state before:
pp: case h₂
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
i : ℕ
hi : i < f.natDegree + 1
⊢ ‖a‖ ^ i ≤ max ‖a‖ 1 ^ f.natDegree

pp: case a0
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
i : ℕ
hi : i < f.natDegree + 1
⊢ 0 ≤ ‖g.coeff i - f.coeff i‖

pp: case d0
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
i : ℕ
hi : i < f.natDegree + 1
⊢ 0 < max ‖a‖ 1 ^ f.natDegree

Tactic:
· refine (pow_le_pow_left₀ (norm_nonneg a) (le_max_left ‖a‖ 1) i).trans ?_
        exact pow_le_pow_right₀ (le_max_right ‖a‖ 1) (Nat.le_of_lt_succ hi)

Goal state after:
case a0
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
i : ℕ
hi : i < f.natDegree + 1
⊢ 0 ≤ ‖g.coeff i - f.coeff i‖

case d0
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
i : ℕ
hi : i < f.natDegree + 1
⊢ 0 < max ‖a‖ 1 ^ f.natDegree
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: case inr
K : Type u_1
L : Type u_2
inst✝⁴ : NormedField K
inst✝³ : Ring L
inst✝² : Algebra K L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
B : Basis ι K L
hna : IsNonarchimedean Norm.norm
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x + y)) i‖) = ‖(B.repr (x + y)) ixy‖
hxy : ‖(B.repr (x + y)) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖
hy : ‖(B.repr (x + y)) ixy‖ ≤ ‖(B.repr y) ixy‖
⊢ ‖(B.repr (x + y)) ixy‖ ≤ max (B.norm x) (B.norm y)

Tactic:
exact le_max_of_le_right (le_trans hy (norm_repr_le_norm B ixy))

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

Goal state before:
pp: 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
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
| f x

Tactic:
rw [← mul_one (f x)]

Goal state after:
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
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
| f x * 1
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : ¬f y = 0
⊢ f (x * y) / f y ≤ f x

Tactic:
· rw [div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hy)]; exact hx _

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

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
x y : L
⊢ (Classical.choose ⋯) (σ (x * y)) ≤ (Classical.choose ⋯) (σ x) * (Classical.choose ⋯) (σ y)

Tactic:
by simp [map_mul σ, map_mul_le_mul]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
h0 : ¬f x = 0
heq : f 1 = 1
⊢ f x = f (x * 1) / f 1

Tactic:
heq,

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y)
h0 : ¬f x = 0
heq : f 1 = 1
⊢ f x = f (x * 1) / 1
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
m n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
heq : m = n
⊢ n - m = 0

Tactic:
heq,

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
m n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
heq : m = n
⊢ n - n = 0
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: case inl
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
m n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
heq : m = n
hnm : n - m = 0
⊢ f (x * c ^ m) * f (c ^ 0) / f c ^ n ≤ f (x * c ^ m) / f c ^ m

Tactic:
heq,

Goal state after:
case inl
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
m n : ℕ
hmn : m ≤ n
hc_pos : 0 < f c
heq : m = n
hnm : n - m = 0
⊢ f (x * c ^ n) * f (c ^ 0) / f c ^ n ≤ f (x * c ^ n) / f c ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: 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
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
heq : L + ε = L + ε / 2 + ε / 2
⊢ (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ L + ε

Tactic:
heq,

Goal state after:
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
hxn' : 0 < μ (x ^ (n % ↑m1))
h : μ (x ^ (↑m1 * (n / ↑m1))) ^ (1 / ↑n) ≤ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n)
hL0' : 0 < L + ε / 2
h1 : (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
h2 : μ (x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ (μ x ^ (n % ↑m1)) ^ (1 / ↑n)
heq : L + ε = L + ε / 2 + ε / 2
⊢ (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ L + ε / 2 + ε / 2
Module: Mathlib.Analysis.Normed.Field.Instances

Goal state before:
pp: F : Type u_1
inst✝ : NormedField F
f : Filter F
hc : f.NeBot ∧ Tendsto (fun p ↦ p.2 - p.1) (f ×ˢ f) (nhds 0)
hn : nhds 0 ⊓ f = ⊥
δ : ℝ
δ_pos : δ > 0
hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖
f_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ ‖x⁻¹‖
h₀ : ∀ᶠ (y : F) in f, y ≠ 0
this : ∀ᶠ (p : F × F) in f ×ˢ f, p.1⁻¹ - p.2⁻¹ = p.1⁻¹ * (p.2 - p.1) * p.2⁻¹
⊢ f.NeBot ∧ Tendsto (fun p ↦ p.1⁻¹ - p.2⁻¹) (f ×ˢ f) (nhds 0)

Tactic:
tendsto_congr' this

Goal state after:
F : Type u_1
inst✝ : NormedField F
f : Filter F
hc : f.NeBot ∧ Tendsto (fun p ↦ p.2 - p.1) (f ×ˢ f) (nhds 0)
hn : nhds 0 ⊓ f = ⊥
δ : ℝ
δ_pos : δ > 0
hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖
f_bdd : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun x ↦ ‖x⁻¹‖
h₀ : ∀ᶠ (y : F) in f, y ≠ 0
this : ∀ᶠ (p : F × F) in f ×ˢ f, p.1⁻¹ - p.2⁻¹ = p.1⁻¹ * (p.2 - p.1) * p.2⁻¹
⊢ f.NeBot ∧ Tendsto (fun x ↦ x.1⁻¹ * (x.2 - x.1) * x.2⁻¹) (f ×ˢ f) (nhds 0)
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : μ x < 1
⊢ {a | ∀ᶠ (n : ℝ) in map (fun n ↦ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}.Nonempty

Tactic:
use 1
    simp only [eventually_map, eventually_atTop, Set.mem_ofPred_eq]
    exact ⟨0, fun _ _ ↦ rpow_le_one (apply_nonneg _ _) (le_of_lt hμx)
      (mul_nonneg (cast_nonneg _) (one_div_nonneg.mpr (cast_nonneg _)))⟩

Goal state after: