mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
inst✝⁹ : Field k
inst✝⁸ : LinearOrder k
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
⊢ asymptoticNhds k V 0 = ⊤

Tactic:
by
  rw [← top_le_iff, ← iSup_pure_eq_top, iSup_le_iff]
  intro v
  rw [← map_const (f := atTop (α := k))]
  have : (fun _ => v) =ᶠ[atTop (α := k)]
      (Function.uncurry (· • ·)) ∘ (fun c => (c, c⁻¹ • v)) := by
    filter_upwards [eventually_ne_atTop 0] with _ h
    simp [h]
  rw [map_congr this, ← map_map, asymptoticNhds_eq_smul, ← map₂_smul, ← map_prod_eq_map₂]
  apply map_mono
  have : Tendsto (fun c => (c, c⁻¹ • v)) (atTop (α := k)) _ :=
    tendsto_id.prodMk <| tendsto_inv_atTop_zero.smul_const v
  simpa

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:
1,

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
| fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
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]

Goal state after:
s : ℂ
hs : 0 < s.re
n : ℕ
hn : n ≠ 0
this : ∀ (x : ℝ), x = x / ↑n * ↑n
x : ℝ
| ↑x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
A : Gamma s * Gamma (1 - s) ≠ 0
⊢ Gamma s ≠ 0

Tactic:
mul_ne_zero_iff

Goal state after:
case neg
s : ℂ
hs : ∀ (m : ℕ), s ≠ -↑m
h_im : ¬s.im = 0
this : sin (↑π * s) ≠ 0
A : Gamma s ≠ 0 ∧ Gamma (1 - s) ≠ 0
⊢ Gamma s ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_2
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma s * Gamma (s + 1 / 2) = (Gamma s)⁻¹⁻¹ * (Gamma (s + 1 / 2))⁻¹⁻¹

Tactic:
inv_inv,

Goal state after:
case e'_2
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma s * (Gamma (s + 1 / 2))⁻¹⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_3
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = (Gamma (2 * s))⁻¹⁻¹ * (2 ^ (2 * s - 1))⁻¹ * (↑√π)⁻¹⁻¹

Tactic:
inv_inv,

Goal state after:
case e'_3
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = Gamma (2 * s) * (2 ^ (2 * s - 1))⁻¹ * (↑√π)⁻¹⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case e'_3
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = Gamma (2 * s) * (2 ^ (2 * s - 1))⁻¹ * (↑√π)⁻¹⁻¹

Tactic:
inv_inv,

Goal state after:
case e'_3
s : ℂ
this : (fun z ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z ↦ (Gamma (2 * z))⁻¹ * 2 ^ (2 * z - 1) / ↑√π
⊢ Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π = Gamma (2 * s) * (2 ^ (2 * s - 1))⁻¹ * ↑√π
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝¹⁵ : CommRing R
inst✝¹⁴ : AddCommGroup M
inst✝¹³ : Algebra ℚ R
inst✝¹² : Module ℚ M
inst✝¹¹ : Module R M
inst✝¹⁰ : Module Rᵐᵒᵖ M
inst✝⁹ : IsCentralScalar R M
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : IsTopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : T2Space R
inst✝¹ : T2Space M
x : tsze R M
inst✝ : Invertible x.fst
⊢ x = x.fst • exp (⅟x.fst • inr x.snd)

Tactic:
rw [← inr_smul, exp_inr, smul_add, ← inl_one, ← inl_smul, ← inr_smul, smul_eq_mul, mul_one,
    smul_smul, mul_invOf_self, one_smul, inl_fst_add_inr_snd_eq]

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

Goal state before:
pp: case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
h' :
  ∀ (i : Fin 3), ∃ c, ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k := fun i ↦ ⋯.choose
hc✝ : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
hc : ¬∏ i, c i = 0
⊢ ∏ i, r i = ∏ i, (1 - r i)

Tactic:
exact mul_left_cancel₀ hc hcr

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

Goal state before:
pp: m : Type u_1
𝔸 : Type u_5
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : CommRing 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : Algebra ℚ 𝔸
inst✝ : T2Space 𝔸
A : Matrix m m 𝔸
⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • Aᵀ ^ n = (∑' (n : ℕ), (↑n.factorial)⁻¹ • A ^ n)ᵀ

Tactic:
transpose_tsum,

Goal state after:
m : Type u_1
𝔸 : Type u_5
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : CommRing 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : Algebra ℚ 𝔸
inst✝ : T2Space 𝔸
A : Matrix m m 𝔸
⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • Aᵀ ^ n = ∑' (x : ℕ), ((↑x.factorial)⁻¹ • A ^ x)ᵀ
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) univ z
H : ∀ (z' : ℂ), ‖x - (algebraMap ℂ F) z'‖ ≠ 0
c : ℂ
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hMdef : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
y w : ℂ
hy : ‖x - (algebraMap ℂ F) y‖ = M
n : ℕ
hn : n > 0
⊢ (C (w - y) ^ n).natDegree < n

Tactic:
by compute_degree!

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

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

Tactic:
Complex.I_sq,

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
⊢ ‖↑0‖₊ ≤ 1

Tactic:
simp only [Nat.cast_zero, nnnorm_zero, zero_le]

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

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

Tactic:
Complex.I_sq,

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

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

Tactic:
rcases le_or_gt ‖x‖ 1 with H | H

Goal state after:
case inl
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : ‖x‖ ≤ 1
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖x + 1‖ ≤ max ‖x‖ 1
Module: Mathlib.Analysis.Normed.Unbundled.AlgebraNorm

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedCommRing R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
f : AlgebraNorm R S
hf1 : f 1 = 1
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
by
  rw [← mul_one ‖a‖, ← hf1]; exact f.smul' _ _

Goal state after:
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
⊢ 0 ≤ a * b

Tactic:
exact mul_nonneg ((le_limsup_of_frequently_le h₁ h₂).trans a_u.le) (v_0.trans x_b.le)

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

Goal state before:
pp: case neg
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
⊢ f (x * y * z) / f z / seminormFromBounded' f y ≤ f (x * z) / f z

Tactic:
rw [div_le_iff₀ (lt_of_le_of_ne' (seminormFromBounded_nonneg f_nonneg f_mul _) hy),
      div_mul_eq_mul_div]

Goal state after:
case neg
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
⊢ f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: 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‖
⊢ ‖(B.repr (x + y)) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖

Tactic:
rw [map_add, Finsupp.coe_add, Pi.add_apply]

Goal state after:
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‖
⊢ ‖(B.repr x) ixy + (B.repr y) ixy‖ ≤ max ‖(B.repr x) ixy‖ ‖(B.repr y) ixy‖
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
⊢ iSup (spectralValueTerms P) ≤ 1

Tactic:
apply ciSup_le (fun n ↦ ?_)
    rw [spectralValueTerms]
    split_ifs with hn
    · apply Real.rpow_le_one (norm_nonneg _) (h n)
      rw [one_div_nonneg, sub_nonneg, Nat.cast_le]
      exact le_of_lt hn
    · exact zero_le_one

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
x : R
⊢ Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x))

Tactic:
by
  by_cases hx : μ x = 0
  · exact tendsto_smoothingFun_of_eq_zero μ hx
  · exact tendsto_smoothingFun_of_ne_zero μ hμ1 hx

Goal state after:
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
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
n : ℕ
⊢ (μ x ^ ↑(s (ψ n))) ^ (1 / ↑(ψ n)) ≤ 1

Tactic:
← rpow_mul (apply_nonneg _ _),

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : μ x ≤ 1
n : ℕ
⊢ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ≤ 1
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
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
n : ℕ
⊢ (μ x ^ ↑(s (ψ n))) ^ (1 / ↑(ψ n)) ≤ μ x

Tactic:
← rpow_mul (apply_nonneg _ _),

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
n : ℕ
⊢ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n))) ≤ μ x
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ : ∀ (n : ℕ), 0 ≤ 1 / ↑(ψ n)
hx : 1 < μ x
⊢ BddAbove (Set.range fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n)))

Tactic:
· use μ x
    simp only [mem_upperBounds, Set.mem_range, forall_exists_index]
    rintro _ n rfl
    apply le_trans (rpow_le_rpow (apply_nonneg _ _) (map_pow_le_pow' hμ1 _ _) (hψ n))
    rw [← rpow_natCast, ← rpow_mul (apply_nonneg _ _), mul_one_div]
    conv_rhs => rw [← rpow_one (μ x)]
    rw [rpow_le_rpow_left_iff hx]
    exact div_le_one_of_le₀ (cast_le.mpr (hs (ψ n))) (cast_nonneg _)

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

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
b : ℕ
⊢ 0 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x

Tactic:
_

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hμx : ¬μ x < 1
b : ℕ
a✝ : 0 ≤ b
⊢ μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x
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ψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : μ x < 1
b : ℕ
⊢ 0 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ 1

Tactic:
_

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : ∀ (x_1 : ℝ) (x_2 : ℕ), (∀ (b : ℕ), x_2 ≤ b → μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ x_1) → c ≤ x_1
hμx : μ x < 1
b : ℕ
a✝ : 0 ≤ b
⊢ μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ 1
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝³ : SeminormedAddCommGroup G
H : Type u_2
inst✝² : SeminormedAddCommGroup H
inst✝¹ : T0Space H
inst✝ : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom (Completion G) H
hg : ∀ (v : G), f v = g ↑v
⊢ f.extension = g

Tactic:
ext v
  rw [NormedAddGroupHom.extension_coe_to_fun,
    Completion.extension_unique f.uniformContinuous g.uniformContinuous fun a => hg a]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: case h_below
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
inst✝ : NontrivialTopology M
N : ℝ
⊢ N ≥ 0 → (∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖) → 1 ≤ N

Tactic:
_

Goal state after:
case h_below
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
inst✝ : NontrivialTopology M
N : ℝ
a✝ : N ≥ 0
⊢ (∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖) → 1 ≤ N
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
inst✝ : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x y : L
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x + y = (algebraMap (↥K⟮x, y⟯) L) (gx + gy)
⊢ spectralNorm K (↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
      ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) (gx + gy)) ≤
    max
      (spectralNorm K (↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) gx))
      (spectralNorm K (↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) gy))

Tactic:
_root_.map_add

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x y : L
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x + y = (algebraMap (↥K⟮x, y⟯) L) (gx + gy)
⊢ spectralNorm K (↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
      ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) gx +
        (algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) gy) ≤
    max
      (spectralNorm K (↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) gx))
      (spectralNorm K (↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) gy))
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case inr
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
n✝ : R
n : ℕ+
hneg : (-1) ^ ↑n = -1
⊢ μ ((-1) ^ ↑n * n✝ ^ ↑n) ^ (1 / ↑↑n) = μ (n✝ ^ ↑n) ^ (1 / ↑↑n)

Tactic:
hneg,

Goal state after:
case inr
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
n✝ : R
n : ℕ+
hneg : (-1) ^ ↑n = -1
⊢ μ (-1 * n✝ ^ ↑n) ^ (1 / ↑↑n) = μ (n✝ ^ ↑n) ^ (1 / ↑↑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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
⊢ smoothingSeminormSeq μ x (m * n) ^ m = smoothingSeminormSeq μ (x ^ m) n

Tactic:
have hm' : (m : ℝ) ≠ 0 := cast_ne_zero.mpr (_root_.ne_of_gt (lt_of_lt_of_le zero_lt_one hm))

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : ↑m ≠ 0
⊢ smoothingSeminormSeq μ x (m * n) ^ m = smoothingSeminormSeq μ (x ^ m) 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
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : ↑m ≠ 0
⊢ μ ((x ^ m) ^ n) ^ (1 / ↑n * (1 / ↑m * ↑m)) = μ ((x ^ m) ^ n) ^ (1 / ↑n)

Tactic:
one_div_mul_cancel hm',

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
m : ℕ
hm : 1 ≤ m
hlim : Tendsto (fun n ↦ smoothingSeminormSeq μ x (m * n)) atTop (𝓝 (smoothingFun μ x))
n : ℕ
hm' : ↑m ≠ 0
⊢ μ ((x ^ m) ^ n) ^ (1 / ↑n * 1) = μ ((x ^ m) ^ n) ^ (1 / ↑n)
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 : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
n : ℕ
hn : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ μ x ^ (↑n * (1 / ↑n)) = μ x

Tactic:
mul_one_div_cancel hn0,

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (n : ℕ), 1 ≤ n → μ (x ^ n) = μ x ^ n
n : ℕ
hn : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ μ x ^ 1 = μ x
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : ¬μ x = 0
h1 : μ 1 = 1
hn0 : ↑n ≠ 0
⊢ μ x ^ (↑n * (1 / ↑n)) = μ x

Tactic:
mul_one_div_cancel hn0,

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
n : ℕ
hn : 1 ≤ n
hx0 : ¬μ x = 0
h1 : μ 1 = 1
hn0 : ↑n ≠ 0
⊢ μ x ^ 1 = μ 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 : ∀ (y : R), μ (x * y) = μ x * μ y
y : R
hlim : Tendsto (fun n ↦ μ x * smoothingSeminormSeq μ y n) atTop (𝓝 (smoothingFun μ x * smoothingFun μ y))
n : ℕ
hn1 : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ μ x ^ (↑n * (1 / ↑n)) * μ (y ^ n) ^ (1 / ↑n) = μ x * μ (y ^ n) ^ (1 / ↑n)

Tactic:
mul_one_div_cancel hn0,

Goal state after:
case h
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : ∀ (y : R), μ (x * y) = μ x * μ y
y : R
hlim : Tendsto (fun n ↦ μ x * smoothingSeminormSeq μ y n) atTop (𝓝 (smoothingFun μ x * smoothingFun μ y))
n : ℕ
hn1 : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ μ x ^ 1 * μ (y ^ n) ^ (1 / ↑n) = μ x * μ (y ^ n) ^ (1 / ↑n)
Module: Mathlib.Analysis.Normed.Module.DoubleDual

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ‖inclusionInDoubleDual 𝕜 E‖ ≤ 1

Tactic:
by
  rw [inclusionInDoubleDual_norm_eq]
  exact ContinuousLinearMap.norm_id_le

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hf : Summable fun i ↦ ‖f i‖
| Multipliable fun i ↦ ‖1 + f i‖

Tactic:
1,

Goal state after:
ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hf : Summable fun i ↦ ‖f i‖
| fun i ↦ ‖1 + f i‖
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝¹ : NormedCommRing R
inst✝ : NormOneClass R
f : ι → R
hf : Summable fun i ↦ ‖f i‖
⊢ Multipliable fun i ↦ ‖1 + f i‖

Tactic:
by
  conv => enter [1, i]; rw [← sub_add_cancel ‖1 + f i‖ 1, add_comm]
  refine Real.multipliable_one_add_of_summable <| hf.of_norm_bounded (fun i ↦ ?_)
  simpa using abs_norm_sub_norm_le (1 + f i) 1

Goal state after: