mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_1
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
x✝ : (s.reindex e).Equilateral
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r
i j : Fin (m + 1)
hij : i ≠ j
⊢ dist (s.points i) (s.points j) = r

Tactic:
convert! hr (e i) (e j) (e.injective.ne hij) using 2

Goal state after:
case e'_3
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
x✝ : (s.reindex e).Equilateral
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r
i j : Fin (m + 1)
hij : i ≠ j
⊢ s.points i = (s.reindex e).points (e i)

case e'_4
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
x✝ : (s.reindex e).Equilateral
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r
i j : Fin (m + 1)
hij : i ≠ j
⊢ s.points j = (s.reindex e).points (e j)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₁ x₂ : Fin (2 + 1)
hx : (x₁, x₂).1 < (x₁, x₂).2
y₁ y₂ : Fin (2 + 1)
hy : (y₁, y₂).1 < (y₁, y₂).2
⊢ (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(x₁, x₂), hx⟩ =
      (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(y₁, y₂), hy⟩ →
    ⟨(x₁, x₂), hx⟩ = ⟨(y₁, y₂), hy⟩

Tactic:
hxy

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
t : Triangle R P
x✝ :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
x₁ x₂ : Fin (2 + 1)
hx : (x₁, x₂).1 < (x₁, x₂).2
y₁ y₂ : Fin (2 + 1)
hy : (y₁, y₂).1 < (y₁, y₂).2
hxy :
  (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(x₁, x₂), hx⟩ =
    (fun i ↦ dist (t.points (↑i).1) (t.points (↑i).2)) ⟨(y₁, y₂), hy⟩
⊢ ⟨(x₁, x₂), hx⟩ = ⟨(y₁, y₂), hy⟩
Module: Mathlib.Analysis.Normed.Algebra.MatrixExponential

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

Tactic:
diagonal_pow,

Goal state after:
m : Type u_1
𝔸 : Type u_5
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Ring 𝔸
inst✝³ : TopologicalSpace 𝔸
inst✝² : IsTopologicalRing 𝔸
inst✝¹ : T2Space 𝔸
inst✝ : Algebra ℚ 𝔸
v : m → 𝔸
⊢ ∑' (n : ℕ), (↑n.factorial)⁻¹ • diagonal (v ^ n) = diagonal (∑' (n : ℕ), (↑n.factorial)⁻¹ • v ^ n)
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
inst✝ : Nontrivial F
⊢ Function.Bijective ⇑(ofId ℂ F)

Tactic:
by
    refine ⟨FaithfulSMul.algebraMap_injective ℂ F, fun x ↦ ?_⟩
    obtain ⟨z, hz⟩ := exists_norm_sub_smul_one_eq_zero x
    refine ⟨z, ?_⟩
    rwa [norm_eq_zero, sub_eq_zero, eq_comm, ← ofId_apply] at hz

Goal state after:
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: x : ℍ
⊢ ‖WithLp.toLp 2 ((equivTuple ℝ) x)‖ = ‖x‖

Tactic:
rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, normSq_def', PiLp.inner_apply,
    Fin.sum_univ_four]
  simp_rw [RCLike.inner_apply, starRingEnd_apply, star_trivial, ← sq]
  rfl

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

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

Tactic:
by
  convert! Complex.hasSum_cos' z using 1
  simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]

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

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1)
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
clear HH

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Module: Mathlib.Analysis.Normed.Ring.Ultra

Goal state before:
pp: R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
x : R
⊢ ‖x + 1‖ ≤ max ‖x‖ 1

Tactic:
by
  simpa only [le_max_iff, norm_one] using norm_add_le_max x 1

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

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this : Tendsto (fun x_1 ↦ ‖(algebraMap ℝ F) x_1.2‖ - M * ‖x‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ sᶜ ×ˢ Set.univ
⊢ ‖(algebraMap ℝ F) w.2‖ - M * ‖x‖ ≤ ‖w.1 • x - (algebraMap ℝ F) w.2‖

Tactic:
rw [norm_sub_rev]

Goal state after:
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‖
s : Set ℝ
hs : Bornology.IsBounded sᶜ
M : ℝ
hM_pos : M > 0
hM : ∀ y ∈ sᶜ, ‖y‖ ≤ M
this : Tendsto (fun x_1 ↦ ‖(algebraMap ℝ F) x_1.2‖ - M * ‖x‖) (𝓟 sᶜ ×ˢ cobounded ℝ) atTop
w : ℝ × ℝ
hw : w ∈ sᶜ ×ˢ Set.univ
⊢ ‖(algebraMap ℝ F) w.2‖ - M * ‖x‖ ≤ ‖(algebraMap ℝ F) w.2 - w.1 • x‖
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk
R : Type u_1
inst✝ : NonUnitalRing R
g : RingSeminorm R
toAddGroupSeminorm✝ : AddGroupSeminorm R
mul_le'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) ≤ toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h : (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ } = (fun f ↦ f.toFun) g
⊢ { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonUnitalRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
mul_le'✝¹ :
  ∀ (x y : R), toAddGroupSeminorm✝¹.toFun (x * y) ≤ toAddGroupSeminorm✝¹.toFun x * toAddGroupSeminorm✝¹.toFun y
toAddGroupSeminorm✝ : AddGroupSeminorm R
mul_le'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) ≤ toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, mul_le' := mul_le'✝¹ } =
    (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ }
⊢ { toAddGroupSeminorm := toAddGroupSeminorm✝¹, mul_le' := mul_le'✝¹ } =
    { toAddGroupSeminorm := toAddGroupSeminorm✝, mul_le' := mul_le'✝ }
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk
R : Type u_1
inst✝ : NonUnitalRing R
g : RingNorm R
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonUnitalRing R
toRingSeminorm✝¹ : RingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toRingSeminorm✝¹.toFun x = 0 → x = 0
toRingSeminorm✝ : RingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ { toRingSeminorm := toRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    { toRingSeminorm := toRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk
R : Type u_1
inst✝ : NonAssocRing R
g : MulRingSeminorm R
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : toAddGroupSeminorm✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) = toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toAddGroupSeminorm✝¹ : AddGroupSeminorm R
map_one'✝¹ : toAddGroupSeminorm✝¹.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : R), toAddGroupSeminorm✝¹.toFun (x * y) = toAddGroupSeminorm✝¹.toFun x * toAddGroupSeminorm✝¹.toFun y
toAddGroupSeminorm✝ : AddGroupSeminorm R
map_one'✝ : toAddGroupSeminorm✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : R), toAddGroupSeminorm✝.toFun (x * y) = toAddGroupSeminorm✝.toFun x * toAddGroupSeminorm✝.toFun y
h :
  (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toAddGroupSeminorm := toAddGroupSeminorm✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toAddGroupSeminorm := toAddGroupSeminorm✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm

Goal state before:
pp: case mk
R : Type u_1
inst✝ : NonAssocRing R
g : MulRingNorm R
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toMulRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
R : Type u_1
inst✝ : NonAssocRing R
toMulRingSeminorm✝¹ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝¹ : ∀ (x : R), toMulRingSeminorm✝¹.toFun x = 0 → x = 0
toMulRingSeminorm✝ : MulRingSeminorm R
eq_zero_of_map_eq_zero'✝ : ∀ (x : R), toMulRingSeminorm✝.toFun x = 0 → x = 0
h :
  (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    (fun f ↦ f.toFun) { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
⊢ { toMulRingSeminorm := toMulRingSeminorm✝¹, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝¹ } =
    { toMulRingSeminorm := toMulRingSeminorm✝, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero'✝ }
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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
hf : f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x + seminormFromBounded' f y

Tactic:
by
    exact le_trans hf (add_le_add
      (le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z (le_refl _))
      (le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) z (le_refl _)))

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
hna : IsNonarchimedean f
x y z : R
hz : ¬f z = 0
⊢ f ((x + y) * z) ≤ f (x * z) ∨ f ((x + y) * z) ≤ f (y * z)

Tactic:
add_mul,

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
hna : IsNonarchimedean f
x y z : R
hz : ¬f z = 0
⊢ f (x * z + y * z) ≤ f (x * z) ∨ f (x * z + y * z) ≤ f (y * z)
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

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

Tactic:
rw [mul_pow, h, ← hβ _ hn, ← map_pow]
    apply le_trans (hC (x ^ n))
    rw [mul_le_mul_iff_right₀ hC0]
    exact map_pow_le_pow _ _ (Nat.one_le_iff_ne_zero.mp hn)

Goal state after:
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 : μ 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)
h3 : (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) ≤ L + ε
h4 : 0 < μ (x ^ (n % ↑m1)) ^ (1 / ↑n)
h5 : 0 < (L + ε / 2) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
⊢ μ (x ^ (↑m1 * (n / ↑m1) + n % ↑m1)) ^ (1 / ↑n) < L + ε

Tactic:
calc μ (x ^ ((m1 : ℕ) * (n / (m1 : ℕ)) + n % m1)) ^ (1 / (n : ℝ)) =
          μ (x ^ ((m1 : ℕ) * (n / (m1 : ℕ))) * x ^ (n % m1)) ^ (1 / (n : ℝ)) := by rw [pow_add]
      _ ≤ (μ (x ^ ((m1 : ℕ) * (n / (m1 : ℕ)))) * μ (x ^ (n % m1))) ^ (1 / (n : ℝ)) :=
        (rpow_le_rpow (apply_nonneg μ _) (map_mul_le_mul μ _ _) (one_div_cast_nonneg _))
      _ = μ (x ^ ((m1 : ℕ) * (n / (m1 : ℕ)))) ^ (1 / (n : ℝ)) *
          μ (x ^ (n % m1)) ^ (1 / (n : ℝ)) :=
        (mul_rpow (apply_nonneg μ _) (apply_nonneg μ _))
      _ ≤ (μ (x ^ (m1 : ℕ)) ^ (n / (m1 : ℕ))) ^ (1 / (n : ℝ)) *
            μ (x ^ (n % m1)) ^ (1 / (n : ℝ)) := by gcongr
      _ < (L + ε / 2) * (L + ε / 2) ^ (-(((n % m1 : ℕ) : ℝ) / (n : ℝ))) *
            μ (x ^ (n % m1)) ^ (1 / (n : ℝ)) := by gcongr
      _ ≤ (L + ε / 2) * (L + ε / 2) ^ (-(((n % m1 : ℕ) : ℝ) / (n : ℝ))) *
            (μ x ^ (n % m1)) ^ (1 / (n : ℝ)) := by gcongr
      _ ≤ L + ε := h3

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_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
ha : a = 0
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ limsup (fun n ↦ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop

Tactic:
by
          apply csInf_le_csInf _ (μ_nonempty μ hs_le ψ)
          · intro b hb
            simp only [eventually_map, eventually_atTop, Set.mem_ofPred_eq] at hb ⊢
            obtain ⟨m, hm⟩ := hb
            use m
            intro k hkm
            apply le_trans _ (hm k hkm)
            rw [rpow_mul (apply_nonneg μ x), rpow_natCast]
            gcongr
            exact map_pow_le_pow' hμ1 x _
          · use 0
            simp only [mem_lowerBounds, eventually_map, eventually_atTop,
              Set.mem_ofPred_eq, forall_exists_index]
            exact fun _ m hm ↦ le_trans (by positivity) (hm m (le_refl _))

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 h : WithLp (↑p) (ι →₀ X)
this : 0 < p
⊢ ((zipWith edist ⋯ f.ofLp h.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ ≤
    ((zipWith edist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ +
      ((zipWith edist ⋯ g.ofLp h.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹

Tactic:
let s := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support

Goal state after:
ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoEMetricSpace X
f g h : WithLp (↑p) (ι →₀ X)
this : 0 < p
s : Finset ι := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
⊢ ((zipWith edist ⋯ f.ofLp h.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ ≤
    ((zipWith edist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ +
      ((zipWith edist ⋯ g.ofLp h.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹
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 h : WithLp (↑p) (ι →₀ X)
⊢ ((zipWith edist ⋯ f.ofLp h.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ ≤
    ((zipWith edist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹ +
      ((zipWith edist ⋯ g.ofLp h.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹

Tactic:
classical
    have : 0 < p := zero_lt_one.trans_le Fact.out
    let s := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
    rw [sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*]),
      sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*]),
      sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*])]
    simp only [zipWith_apply, ← one_div]
    grw [← ENNReal.Lp_add_le _ _ _ (mod_cast Fact.out)]
    gcongr
    exact edist_triangle ..

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (↑P + ↑Pᶜ * ↑R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ

Tactic:
add_mul,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P * (↑P + ↑Q * ↑R * ↑Pᶜ) + ↑Pᶜ * ↑R * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
v : ι → ℝ
hv : Multipliable v
⊢ ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁

Tactic:
obtain ⟨r₁, hr₁⟩ := exists_gt (max 0 <| ∏' i, v i)

Goal state after:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : max 0 (∏' (i : ι), v i) < r₁
⊢ ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (↑P + ↑Pᶜ * ↑R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ

Tactic:
rw [add_mul, mul_add, mul_add, (mul_assoc _ (R : M) (↑Q * ↑R * ↑Pᶜ)),
    ← mul_assoc (R : M) (↑Q * ↑R) _, ← coe_inf Q, (Pᶜ.prop.commute R.prop).eq,
    ((Q ⊓ R).prop.commute Pᶜ.prop).eq, (R.prop.commute (Q ⊓ R).prop).eq, coe_inf Q,
    mul_assoc (Q : M), ← mul_assoc, mul_assoc (R : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self,
    zero_mul, mul_zero, zero_add, add_zero, ← mul_assoc, P.prop.proj.eq,
    R.prop.proj.eq, ← coe_inf Q, mul_assoc, ((Q ⊓ R).prop.commute Pᶜ.prop).eq, ← mul_assoc,
    Pᶜ.prop.proj.eq]

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

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑P * ↑R → ↑Q = ↑Q * ↑R → ↑P + (↑Q - ↑P * ↑Q) = (↑P + (↑Q - ↑P * ↑Q)) * ↑R

Tactic:
add_mul,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P = ↑P * ↑R → ↑Q = ↑Q * ↑R → ↑P + (↑Q - ↑P * ↑Q) = ↑P * ↑R + (↑Q - ↑P * ↑Q) * ↑R
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (↑P + ↑Pᶜ * ↑Q) * (↑P + ↑Pᶜ * ↑R) = ↑P + ↑Q * ↑R * ↑Pᶜ

Tactic:
add_mul,

Goal state after:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ ↑P * (↑P + ↑Pᶜ * ↑R) + ↑Pᶜ * ↑Q * (↑P + ↑Pᶜ * ↑R) = ↑P + ↑Q * ↑R * ↑Pᶜ
Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn

Goal state before:
pp: α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove ((fun x ↦ (g x).re) '' K)
v : ℝ
hv : ∀ x ∈ K, (g x).re ≤ v
this : ∀ᶠ (i : ι) in p, ∀ x ∈ K, (f i x).re ≤ v + 1
⊢ ∀ x ∈ K, g x ∈ {x | x.re ≤ v + 1}

Tactic:
exact fun x hx ↦ (hv x hx).trans (lt_add_one v).le

Goal state after:
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x✝ : ↑x.lifts
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts
⊢ ‖(lift f.toMultilinearMap) x‖ ≤ projectiveSeminormAux ↑⟨p, hp⟩ * ‖f‖

Tactic:
← ((mem_lifts_iff x p).mp hp),

Goal state after:
ι : Type u_1
inst✝⁵ : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 E G
x : ⨂[𝕜] (i : ι), E i
x✝ : ↑x.lifts
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
hp : p ∈ x.lifts
⊢ ‖(lift f.toMultilinearMap) (List.map (fun x ↦ x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) (FreeAddMonoid.toList p)).sum‖ ≤
    projectiveSeminormAux ↑⟨p, ⋯⟩ * ‖f‖
Module: Mathlib.Topology.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : Preorder α
inst✝¹ : IsOrderedMonoid α
inst✝ : ContinuousConstSMul α α
s : Set α
hs : IsOpen s
⊢ IsOpen (s * ↑(upperClosure 1))

Tactic:
exact hs.mul_right

Goal state after: