mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1 + 1)) (∑ j ∈ Finset.range (n + 1), (-1) ^ j * z ^ j) z

Tactic:
rw [logTaylor_succ]
    simp only [Nat.cast_add, Nat.cast_one,
      Finset.sum_range_succ]
    refine HasDerivAt.add ih ?_
    simp only [mul_div_assoc]
    have : HasDerivAt (fun x : ℂ ↦ (x ^ (n + 1) / (n + 1))) (z ^ n) z := by
      simp_rw [div_eq_mul_inv]
      convert! HasDerivAt.mul_const (hasDerivAt_pow (n + 1) z) (((n : ℂ) + 1)⁻¹) using 1
      simp [field]
    convert! HasDerivAt.const_mul _ this using 2
    ring

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

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
simp only [H, norm_mul]

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
⊢ ‖z‖ * ‖∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 1 ≤ m

Tactic:
rwa [neg_ne_zero, Nat.cast_ne_zero, ← Nat.one_le_iff_ne_zero] at hs

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

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

Tactic:
by
  have help : IntervalIntegrable (fun t : ℝ ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1 :=
    IntervalIntegrable.mul_const (Continuous.intervalIntegrable (by fun_prop) 0 1) (1 - ‖z‖)⁻¹
  let f (z : ℂ) : ℂ := log (1 + z) - logTaylor (n + 1) z
  let f' (z : ℂ) : ℂ := (-z) ^ n * (1 + z)⁻¹
  have hderiv : ∀ t ∈ Set.Icc (0 : ℝ) 1, HasDerivAt f (f' (0 + t * z)) (0 + t * z) := by
    intro t ht
    rw [zero_add]
    exact hasDerivAt_log_sub_logTaylor n <|
      StarConvex.add_smul_mem starConvex_one_slitPlane (mem_slitPlane_of_norm_lt_one hz) ht.1 ht.2
  have hcont : ContinuousOn (fun t : ℝ ↦ f' (0 + t * z)) (Set.Icc 0 1) := by
    simp only [zero_add]
    exact (Continuous.continuousOn (by fun_prop)).mul <|
      continuousOn_one_add_mul_inv <| mem_slitPlane_of_norm_lt_one hz
  have H : f z = z * ∫ t in (0 : ℝ)..1, (-(t * z)) ^ n * (1 + t * z)⁻¹ := by
    convert! (integral_unitInterval_deriv_eq_sub hcont hderiv).symm using 1
    · simp only [f, zero_add, add_zero, log_one, logTaylor_at_zero, sub_self, sub_zero]
    · simp only [f', real_smul, zero_add,
        smul_eq_mul]
  unfold f at H
  simp only [H, norm_mul]
  simp_rw [neg_pow (_ * z) n, mul_assoc, intervalIntegral.integral_const_mul, mul_pow,
    mul_comm _ (z ^ n), mul_assoc, intervalIntegral.integral_const_mul, norm_mul, norm_pow,
    norm_neg, norm_one, one_pow, one_mul, ← mul_assoc, ← pow_succ', mul_div_assoc]
  gcongr _ * ?_
  calc ‖∫ t in (0 : ℝ)..1, (t : ℂ) ^ n * (1 + t * z)⁻¹‖
    _ ≤ ∫ t in (0 : ℝ)..1, t ^ n * (1 - ‖z‖)⁻¹ := by
      refine intervalIntegral.norm_integral_le_of_norm_le zero_le_one ?_ help
      filter_upwards with t ⟨ht₀, ht₁⟩
      rw [norm_mul, norm_pow, Complex.norm_of_nonneg ht₀.le]
      gcongr
      exact norm_one_add_mul_inv_le ⟨ht₀.le, ht₁⟩ hz
    _ = (1 - ‖z‖)⁻¹ / (n + 1) := by
      rw [intervalIntegral.integral_mul_const, mul_comm, integral_pow]
      simp [field]

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

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

Tactic:
log_inv _ <| slitPlane_arg_ne_pi <| mem_slitPlane_of_norm_lt_one <| (norm_neg z).symm ▸ hz,

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

Goal state before:
pp: case succ
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + ↑n) = f x + ∑ m ∈ Finset.range n, log (x + ↑m)
⊢ f (x + ↑(n + 1)) = f x + ∑ m ∈ Finset.range (n + 1), log (x + ↑m)

Tactic:
have : x + n.succ = x + n + 1 := by push_cast; ring

Goal state after:
case succ
f : ℝ → ℝ
x : ℝ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
n : ℕ
hn : f (x + ↑n) = f x + ∑ m ∈ Finset.range n, log (x + ↑m)
this : x + ↑n.succ = x + ↑n + 1
⊢ f (x + ↑(n + 1)) = f x + ∑ m ∈ Finset.range (n + 1), log (x + ↑m)
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
v : V
p : P
⊢ ⨆ i, map (fun x ↦ x +ᵥ p) (map (fun x ↦ x +ᵥ i) (atTop • 𝓝 v)) = ⨆ p, map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)

Tactic:
map_map,

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
v : V
p : P
⊢ ⨆ i, map ((fun x ↦ x +ᵥ p) ∘ fun x ↦ x +ᵥ i) (atTop • 𝓝 v) = ⨆ p, map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)
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
v : V
hv : v ≠ 0
p : P
⊢ Tendsto (fun x ↦ dist (id x) p) (map (fun x ↦ x +ᵥ p) (map (fun p ↦ p.1 • p.2) (atTop ×ˢ 𝓝 v))) atTop

Tactic:
map_map,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
hv : v ≠ 0
p : P
⊢ Tendsto (fun x ↦ dist (id x) p) (map ((fun x ↦ x +ᵥ p) ∘ fun p ↦ p.1 • p.2) (atTop ×ˢ 𝓝 v)) atTop
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ x = x / ↑n * ↑n

Tactic:
rw [div_mul_cancel₀]

Goal state after:
case h
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ ↑n ≠ 0
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
v : V
p : P → Prop
⊢ (∀ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (x : V) in 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P x, p y

Tactic:
← map_snd_prod (atTop (α := k)) (𝓝 v)

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
v : V
p : P → Prop
⊢ (∀ᶠ (a : k × V) in atTop ×ˢ 𝓝 v, ∀ᶠ (y : P) in asymptoticNhds k P (a.1 • a.2), p y) ↔
    ∀ᶠ (x : V) in map Prod.snd (atTop ×ˢ 𝓝 v), ∀ᶠ (y : P) in asymptoticNhds k P x, p y
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
⊢ asymptoticCone k Set.univ = Set.univ

Tactic:
by
  rw [← AffineSubspace.top_coe k, asymptoticCone_affineSubspace Set.univ_nonempty,
    AffineSubspace.direction_top, Submodule.top_coe, closure_univ]

Goal state after:
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:
rw [indicator_of_mem (mem_Ioc.mpr ⟨mem_Ioi.mp hx, hxn⟩), norm_mul, Complex.norm_of_nonneg
          (pow_nonneg (sub_nonneg.mpr <| div_le_one_of_le₀ hxn <| by positivity) _),
          norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]
      gcongr
      exact one_sub_div_pow_le_exp_neg hxn

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

Goal state before:
pp: s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ Gamma s ≠ 0

Tactic:
by_cases h_im : s.im = 0

Goal state after:
case pos
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : s.im = 0
⊢ Gamma s ≠ 0

case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
⊢ Gamma s ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: n : ℕ
ihn : ∀ (s : ℂ), -s.re < ↑n → DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < ↑(n + 1)
⊢ -(s + 1).re < ↑n

Tactic:
rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ]

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

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (fun x ↦ ‖f x‖) univ x
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : w ∈ {y | ‖f y‖ = M}
u : X
hu : ‖f u - f w‖ / M < 1
this : Tendsto (fun n ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * (1 + 0)))
⊢ ‖f u‖ ≤ M

Tactic:
refine ge_of_tendsto (by simpa) ?_

Goal state after:
X : Type u_1
E : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (fun x ↦ ‖f x‖) univ x
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y w : X
hw : w ∈ {y | ‖f y‖ = M}
u : X
hu : ‖f u - f w‖ / M < 1
this : Tendsto (fun n ↦ M * (1 + (‖f u - f w‖ / M) ^ n)) atTop (𝓝 (M * (1 + 0)))
⊢ ∀ᶠ (c : ℕ) in atTop, ‖f u‖ ≤ M * (1 + (‖f u - f w‖ / M) ^ c)
Module: Mathlib.Analysis.Normed.Algebra.QuaternionExponential

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

Tactic:
by rw [pow_succ, pow_mul, hq2]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), 1

Tactic:
gcongr with i hi

Goal state after:
case h
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ‖x‖ ^ i ≤ 1
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
⊢ ∑ k ∈ Finset.range (m + 1), ‖x‖ ^ k ≤ ∑ _x ∈ Finset.range (m + 1), ‖x‖ ^ m

Tactic:
gcongr with i hi

Goal state after:
case ha
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖

case hmn
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m
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 y ↦ ‖y.1‖ * c) (cobounded ℝ ×ˢ ⊤) atTop

Tactic:
tendsto_mul_const_atTop_of_pos hc₀,

Goal state after:
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 y ↦ ‖y.1‖) (cobounded ℝ ×ˢ ⊤) atTop
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case pos
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 : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
hxz : f (x * z) = 0
⊢ f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)

Tactic:
rw [mul_comm x y, mul_assoc, mul_comm y, map_mul_zero_of_map_zero f_nonneg f_mul hxz y]

Goal state after:
case pos
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 : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
hxz : f (x * z) = 0
⊢ 0 ≤ seminormFromBounded' f y * f (x * z)
Module: Mathlib.Analysis.Normed.Field.Approximation

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : NormedField L
inst✝ : Algebra K L
hd : DenseRange ⇑(algebraMap K L)
f : L[X]
hf : f.Monic
ε : ℝ
hε : ε > 0
h : ¬f.natDegree = 0
c : ℕ → K
hc : ∀ (i : ℕ), dist (f.coeff i) ((algebraMap K L) (c i)) < ε
⊢ (C 1 * X ^ f.natDegree).natDegree = f.natDegree

Tactic:
by
        simp

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
hna : IsNonarchimedean f
x y z : R
hf : f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y

Tactic:
rcases hf with hfx | hfy
    · exact Or.inl <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z hfx
    · exact Or.inr <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) z hfy

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

Goal state before:
pp: case h.h
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
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝¹ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy_def : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖) = ‖(B.repr (x * y)) ixy‖
hna' : IsNonarchimedean ⇑(NormedField.toMulRingNorm K)
k : ι
hk :
  ‖∑ i, ((B.repr x) i • ∑ i_1, (B.repr y) i_1 • B.repr (B i * B i_1)) ixy‖ ≤
    ‖((B.repr x) k • ∑ j, (B.repr y) j • B.repr (B k * B j)) ixy‖
⊢ ‖(∑ x_1, (B.repr x) x_1 • ∑ x, (B.repr y) x • B.repr (B x_1 * B x)) ixy‖ ≤
    B.norm (B c.1 * B c.2) * B.norm x * B.norm y

Tactic:
simp only [Finsupp.coe_smul, Finsupp.coe_finsetSum, Pi.smul_apply, Finset.sum_apply,
      smul_eq_mul, norm_mul] at hk ⊢

Goal state after:
case h.h
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
i : ι
hBi : B i = 1
hna : IsNonarchimedean Norm.norm
c : ι × ι
left✝¹ : c ∈ univ
hc : (univ.sup' ⋯ fun i ↦ B.norm (B i.1 * B i.2)) = B.norm (B c.1 * B c.2)
x y : L
ixy : ι
left✝ : ixy ∈ univ
hixy_def : (univ.sup' ⋯ fun i ↦ ‖(B.repr (x * y)) i‖) = ‖(B.repr (x * y)) ixy‖
hna' : IsNonarchimedean ⇑(NormedField.toMulRingNorm K)
k : ι
hk :
  ‖∑ x_1, (B.repr x) x_1 * ∑ x, (B.repr y) x * (B.repr (B x_1 * B x)) ixy‖ ≤
    ‖(B.repr x) k‖ * ‖∑ x, (B.repr y) x * (B.repr (B k * B x)) ixy‖
⊢ ‖∑ x_1, (B.repr x) x_1 * ∑ x, (B.repr y) x * (B.repr (B x_1 * B x)) ixy‖ ≤
    B.norm (B c.1 * B c.2) * B.norm x * B.norm y
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
⊢ (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖

Tactic:
apply ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun n ↦ ?_)
      (fun _ hx ↦ ⟨0, by simp only [if_true, hx]⟩)

Goal state after:
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
n : ℕ
⊢ (if n = 0 then ‖r‖ else 0) ≤ ‖r‖
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
⊢ ∃ x, eval x f = 0

Tactic:
let a := rootOfSplits (SplittingField.splits f)
      (by simpa using degree_ne_of_natDegree_ne fnatdeg0)

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
⊢ ∃ x, eval x f = 0
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 + y) - ε ≤ max (smoothingFun μ x) (smoothingFun μ y)

Tactic:
sub_le_iff_le_add

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 + y) ≤ max (smoothingFun μ x) (smoothingFun μ y) + ε
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hf : ∀ (x : M), ‖x‖ = 0 → f x = 0
⊢ ∃ C, ∀ (v : SeparationQuotient M), ‖(liftContinuousAddMonoidHom ↑f ⋯) v‖ ≤ C * ‖v‖

Tactic:
by
    refine ⟨‖f‖, fun v ↦ ?_⟩
    obtain ⟨v, rfl⟩ := surjective_mk v
    exact le_opNorm f v

Goal state after:
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝¹² : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E'
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module R E'
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace F'
inst✝¹ : AddCommMonoid F'
inst✝ : Module R F'
f : E →L[R] F
g : E' →L[R] F'
hf : f.HasLeftInverse
hg : g.HasLeftInverse
⊢ (f.prodMap g).HasLeftInverse

Tactic:
obtain ⟨finv, hfinv⟩ := hf

Goal state after:
R : Type u_1
inst✝¹² : Semiring R
E : Type u_2
E' : Type u_3
F : Type u_4
F' : Type u_5
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module R E
inst✝⁸ : TopologicalSpace E'
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : Module R E'
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
inst✝² : TopologicalSpace F'
inst✝¹ : AddCommMonoid F'
inst✝ : Module R F'
f : E →L[R] F
g : E' →L[R] F'
hg : g.HasLeftInverse
finv : F →L[R] E
hfinv : LeftInverse ⇑finv ⇑f
⊢ (f.prodMap g).HasLeftInverse
Module: Mathlib.Analysis.Normed.Module.ContinuousInverse

Goal state before:
pp: R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
hg : g.HasLeftInverse
hf : f.HasLeftInverse
⊢ (g ∘SL f).HasLeftInverse

Tactic:
obtain ⟨finv, hfinv⟩ := hf

Goal state after:
R : Type u_1
inst✝⁹ : Semiring R
E : Type u_2
F : Type u_4
G : Type u_6
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommMonoid E
inst✝⁶ : Module R E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommMonoid F
inst✝³ : Module R F
f : E →L[R] F
inst✝² : TopologicalSpace G
inst✝¹ : AddCommMonoid G
inst✝ : Module R G
g : F →L[R] G
hg : g.HasLeftInverse
finv : F →L[R] E
hfinv : LeftInverse ⇑finv ⇑f
⊢ (g ∘SL f).HasLeftInverse