mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Unbundled.FiniteExtension

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
⊢ ∃ f, IsPowMul ⇑f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean ⇑f

Tactic:
have hg_add : ∀ a b : L, g (a + b) ≤ g a + g b :=
    fun _ _ ↦ IsNonarchimedean.add_le hg_nonneg hg_na

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : Field L
inst✝ : Algebra K L
hfd : FiniteDimensional K L
hna : IsNonarchimedean norm
h1 : LinearIndepOn K id {1}
ι : Type u_2 := { x // x ∈ h1.extend ⋯ }
B : Basis ι K L := Basis.extend h1
hfin : Fintype ι := FiniteDimensional.fintypeBasisIndex B
hem : Nonempty ι
h1L : 1 ∈ h1.extend ⋯
hB1 : B ⟨1, h1L⟩ = 1
g : L → ℝ := B.norm
hg0 : g 0 = 0
hg_nonneg : ∀ (x : L), 0 ≤ g x
hg_ext : ∀ (x : K), g ((algebraMap K L) x) = ‖x‖
hg_na : IsNonarchimedean g
hg_add : ∀ (a b : L), g (a + b) ≤ g a + g b
⊢ ∃ f, IsPowMul ⇑f ∧ (∀ (x : K), f ((algebraMap K L) x) = ‖x‖) ∧ IsNonarchimedean ⇑f
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝² : Ring α
inst✝¹ : FunLike F α ℝ
inst✝ : RingSeminormClass F α ℝ
f g : F
hfpm : IsPowMul ⇑f
hgpm : IsPowMul ⇑g
hfg : ∃ r, ∃ (_ : 0 < r), ∀ (a : α), f a ≤ r * g a
hgf : ∃ r, ∃ (_ : 0 < r), ∀ (a : α), g a ≤ r * f a
⊢ f = g

Tactic:
by
  obtain ⟨r, hr0, hr⟩ := hfg
  obtain ⟨s, hs0, hs⟩ := hgf
  have hle : RingHom.IsBoundedWrt f g (RingHom.id _) := ⟨s, hs0, hs⟩
  have hge : RingHom.IsBoundedWrt g f (RingHom.id _) := ⟨r, hr0, hr⟩
  rw [← Function.Injective.eq_iff DFunLike.coe_injective]
  ext x
  exact le_antisymm (contraction_of_isPowMul_of_boundedWrt g hfpm hge x)
    (contraction_of_isPowMul_of_boundedWrt f hgpm hle x)

Goal state after:
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
⊢ Tendsto (seminormFromConst_seq c f 0) atTop (𝓝 0)

Tactic:
by simpa [seminormFromConst_seq_zero c (map_zero _)] using! tendsto_const_nhds

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
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) < (L + ε / 2) ^ ↑↑m1
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
hm10 : ↑↑m1 ≠ 0
⊢ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) < (L + ε / 2) ^ (↑n / ↑n) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))

Tactic:
nth_rw 3 [← div_add_mod n m1]

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) < (L + ε / 2) ^ ↑↑m1
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
hm10 : ↑↑m1 ≠ 0
⊢ (μ (x ^ ↑m1) ^ (n / ↑m1)) ^ (1 / ↑n) <
    (L + ε / 2) ^ (↑(↑m1 * (n / ↑m1) + n % ↑m1) / ↑n) * (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n))
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
this : (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖
n : ℕ
hn : n = 0
⊢ ‖0 - (C r).coeff 0‖ ^ 1⁻¹ = ‖r‖

Tactic:
coeff_C_zero,

Goal state after:
case pos
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
this : (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖
n : ℕ
hn : n = 0
⊢ ‖0 - r‖ ^ 1⁻¹ = ‖r‖
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : n = 0
⊢ ‖p.coeff 0‖ * f 1 < f x ^ p.natDegree

Tactic:
← Nat.sub_zero p.natDegree,

Goal state after:
case pos
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : n = 0
⊢ ‖p.coeff 0‖ * f 1 < f x ^ (p.natDegree - 0)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : n = 0
⊢ f (p.coeff n • x ^ n) < f (x ^ p.natDegree)

pp: case neg
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : ¬n = 0
⊢ f (p.coeff n • x ^ n) < f (x ^ p.natDegree)

Tactic:
· rw [hn0, pow_zero, map_smul_eq_mul, hf_pm _ (succ_le_iff.mpr h_deg),
            ← Nat.sub_zero p.natDegree, ← hn0]
          exact (mul_le_of_le_one_right (norm_nonneg _) hf_pm.map_one_le_one).trans_lt (hn_lt n hn)

Goal state after:
case neg
K : Type u_2
inst✝² : NormedField K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
p : K[X]
hp : p.Monic
x : L
hx : (aeval x) p = 0
hx0 : ¬f x = 0
h_ge : ¬f x ≤ spectralValue p
hn_lt : ∀ n < p.natDegree, ‖p.coeff n‖ < f x ^ (p.natDegree - n)
h_deg : 0 < p.natDegree
n : ℕ
hn : n < p.natDegree
hn0 : ¬n = 0
⊢ f (p.coeff n • x ^ n) < f (x ^ p.natDegree)
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
inst✝ : NontrivialTopology M
⊢ ‖normedMk‖ = 1

Tactic:
apply NormedAddGroupHom.opNorm_eq_of_bounds _ zero_le_one

Goal state after:
case h_above
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
inst✝ : NontrivialTopology M
⊢ ∀ (x : M), ‖normedMk x‖ ≤ 1 * ‖x‖

case h_below
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
inst✝ : NontrivialTopology M
⊢ ∀ N ≥ 0, (∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖) → 1 ≤ N
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

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

Tactic:
obtain ⟨x, _⟩ := exists_norm_ne_zero M

Goal state after:
case h_below
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
inst✝ : NontrivialTopology M
N : ℝ
a✝ : N ≥ 0
hle : ∀ (x : M), ‖normedMk x‖ ≤ N * ‖x‖
x : M
h✝ : ‖x‖ ≠ 0
⊢ 1 ≤ N
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : SeminormedAddCommGroup M
⊢ (∀ (x : M), ‖x‖ = 0) → normedMk = 0

Tactic:
· intro h
    ext x
    simpa [← norm_eq_zero] using h x

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

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝ : Field E :=
  id
    (have this := inferInstance;
    this)
this : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
a : E
⊢ spectralNorm K L ↑(id2 (-a)) = spectralNorm K L ↑(id2 a)

Tactic:
by simp [map_neg, NegMemClass.coe_neg, ← spectralAlgNorm_def, map_neg_eq_map]

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

Goal state before:
pp: K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
⊢ (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).natDegree

Tactic:
rw [mapAlg_eq_map, natDegree_map]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (fun i x ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove ((fun x ↦ (∑' (i : ι), log (f i x)).re) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun i x ↦ log (f i x)) r s
⊢ TendstoUniformlyOn (fun s x ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s

Tactic:
refine (hr.tendstoUniformlyOn.comp_cexp ?_).congr ?_

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (fun i x ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove ((fun x ↦ (∑' (i : ι), log (f i x)).re) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun i x ↦ log (f i x)) r s
⊢ BddAbove ((fun x ↦ (r x).re) '' s)

case refine_2
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (fun i x ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove ((fun x ↦ (∑' (i : ι), log (f i x)).re) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun i x ↦ log (f i x)) r s
⊢ ∀ᶠ (n : Finset ι) in atTop, Set.EqOn (cexp ∘ fun x2 ↦ ∑ i ∈ n, log (f i x2)) (fun x ↦ ∏ i ∈ n, f i x) s
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)
E' : ι → Type u_5
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E' i)
f : (i : ι) → E i →L[𝕜] E' i
⊢ ‖mapL f‖ ≤ ∏ i, ‖f i‖

Tactic:
by
  refine (ContinuousLinearMap.opNorm_le_iff (by positivity)).mpr fun x ↦ ?_
  apply le_trans (norm_eval_le_projectiveSeminorm ..) (mul_le_mul_of_nonneg_right _ (norm_nonneg x))
  refine (ContinuousMultilinearMap.opNorm_le_iff (by positivity)).mpr fun m ↦ ?_
  apply le_trans (projectiveSeminorm_tprod_le fun i ↦ f i (m i))
  rw [← Finset.prod_mul_distrib]
  gcongr
  exact ContinuousLinearMap.le_opNorm _ _

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

Goal state before:
pp: case inl.inr
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
q r : ℝ≥0∞
inst✝² : Fact (1 ≤ q)
inst✝¹ : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
f : ↥(lp F q)
hpqr : ∞.HolderTriple q r
inst✝ : Fact (1 ≤ ∞)
e : ↥(lp E ∞)
hq : 1 ≤ q.toReal
⊢ ‖((holderₗ r B hBK) e) f‖ ≤ ↑K * ‖e‖ * ‖f‖

Tactic:
obtain rfl : r = q := ENNReal.HolderTriple.unique ∞ q r q
      refine norm_le_of_forall_sum_le (zero_lt_one.trans_le hq) (by positivity) fun s ↦ ?_
      rw [Real.mul_rpow (by positivity) (by positivity)]
      refine Memℓp.holder_top_left_bound B hBK
        (by positivity) (by positivity) (norm_apply_le_norm (by simp) _) ?_ s
      exact sum_rpow_le_norm_rpow (zero_lt_one.trans_le hq) f

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

Goal state before:
pp: case inr.inr
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ q)
inst✝ : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
e : ↥(lp E p)
f : ↥(lp F q)
hp✝ : 1 ≤ p.toReal
hq✝ : 1 ≤ q.toReal
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
⊢ ‖((holderₗ r B hBK) e) f‖ ≤ ↑K * ‖e‖ * ‖f‖

Tactic:
refine norm_le_of_forall_sum_le hpqr.pos' (by positivity) fun s ↦ ?_

Goal state after:
case inr.inr
ι : Type u_1
𝕜 : Type u_2
E : ι → Type u_3
F : ι → Type u_4
G : ι → Type u_5
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → NormedAddCommGroup (F i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (F i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (G i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (G i)
p q r : ℝ≥0∞
hpqr✝ : p.HolderTriple q r
inst✝² : Fact (1 ≤ p)
inst✝¹ : Fact (1 ≤ q)
inst✝ : Fact (1 ≤ r)
B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i
K : ℝ≥0
hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K
e : ↥(lp E p)
f : ↥(lp F q)
hp✝ : 1 ≤ p.toReal
hq✝ : 1 ≤ q.toReal
hpqr : p.toReal.HolderTriple q.toReal r.toReal
hp : 0 < p.toReal
hq : 0 < q.toReal
s : Finset ι
⊢ ∑ i ∈ s, ‖↑(((holderₗ r B hBK) e) f) i‖ ^ r.toReal ≤ (↑K * ‖e‖ * ‖f‖) ^ r.toReal
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 α
h : IsUpperSet s
x y : α
hxy : x ≤ y
hx : x ∈ closure s
⊢ y ∈ closure ((y / x) • s)

Tactic:
rw [closure_smul]
      exact ⟨x, hx, div_mul_cancel _ _⟩

Goal state after:
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 α
h : IsLowerSet s
x y : α
hxy : y ≤ x
hx : x ∈ closure s
⊢ y ∈ closure ((y / x) • s)

Tactic:
rw [closure_smul]
      exact ⟨x, hx, div_mul_cancel _ _⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ nndist (y₂ i) (y i) ≤ nndist (y₁ i) (y i)

Tactic:
rw [Real.nndist_eq', Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₂ i ≤ y i)),
    Real.nndist_eq', Real.nnabs_of_nonneg (sub_nonneg_of_le (‹_ ≤ y› i : y₁ i ≤ y i))]

Goal state after:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Iic y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Iic y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ (y i - y₂ i).toNNReal ≤ (y i - y₁ i).toNNReal
Module: Mathlib.Analysis.Normed.Order.UpperLower

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
δ : ℝ
hs : IsLowerSet s
hx : x ∈ closure s
hδ : 0 < δ
⊢ ∃ y, closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s

Tactic:
refine ⟨x - const _ (3 / 4 * δ), closedBall_subset_closedBall' ?_, ?_⟩
  · grw [dist_self_sub_left, ← const_def, pi_norm_const_le]
    apply le_of_eq
    simp [abs_of_nonneg, hδ.le]
    ring
  obtain ⟨y, hy, hxy⟩ := Metric.mem_closure_iff.1 hx _ (div_pos hδ zero_lt_four)
  refine fun z hz => hs.mem_interior_of_forall_lt (subset_closure hy) fun i => ?_
  rw [mem_closedBall, dist_eq_norm'] at hz
  rw [dist_eq_norm] at hxy
  replace hxy := (norm_le_pi_norm _ i).trans hxy.le
  replace hz := (norm_le_pi_norm _ i).trans hz
  dsimp at hxy hz
  rw [abs_sub_le_iff] at hxy hz
  linarith

Goal state after:
Module: Mathlib.Analysis.ODE.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ (∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt γ (v t (γ t)) t) ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
Metric.eventually_nhds_iff_ball

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ (∃ ε > 0, ∀ y ∈ Metric.ball t₀ ε, HasDerivAt γ (v y (γ y)) y) ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
Module: Mathlib.Analysis.ODE.Transform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun x ↦ x + dt) (v ∘ fun x ↦ x + dt) ↔ IsIntegralCurve γ v

Tactic:
simp_rw [← isIntegralCurveOn_univ]
  convert! isIntegralCurveOn_comp_add
  simp

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
inst✝ : CompleteSpace E
⊢ IsClosed {a | a t₀ ∈ closedBall x₀ ↑r}

Tactic:
simp_rw [mem_closedBall_iff_norm]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ : E
a r L : ℝ≥0
inst✝ : CompleteSpace E
⊢ IsClosed {a | ‖a t₀ - x₀‖ ≤ ↑r}
Module: Mathlib.Analysis.PSeriesComplex

Goal state before:
pp: p : ℂ
⊢ (Summable fun n ↦ 1 / ↑(n + 1) ^ p) ↔ Summable fun n ↦ 1 / ↑(n + 1) ^ p.re

Tactic:
← summable_norm_iff

Goal state after:
p : ℂ
⊢ (Summable fun x ↦ ‖1 / ↑(x + 1) ^ p‖) ↔ Summable fun n ↦ 1 / ↑(n + 1) ^ p.re
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
t₁ t₂ : ↑(Icc tmin tmax)
⊢ ‖(x + ∫ (τ : ℝ) in ↑t₀..↑t₁, f τ (α.compProj τ)) - (x + ∫ (τ : ℝ) in ↑t₀..↑t₂, f τ (α.compProj τ))‖ ≤ ↑L * dist t₁ t₂

Tactic:
add_sub_add_left_eq_sub,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
t₁ t₂ : ↑(Icc tmin tmax)
⊢ ‖(∫ (τ : ℝ) in ↑t₀..↑t₁, f τ (α.compProj τ)) - ∫ (τ : ℝ) in ↑t₀..↑t₂, f τ (α.compProj τ)‖ ≤ ↑L * dist t₁ t₂
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ ‖(x + ∫ (τ : ℝ) in ↑t₀..↑t, f τ (((next hf hx)^[n] α).compProj τ)) -
        (x + ∫ (τ : ℝ) in ↑t₀..↑t, f τ (((next hf hx)^[n] β).compProj τ))‖ ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
add_sub_add_left_eq_sub,

Goal state after:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ ‖(∫ (τ : ℝ) in ↑t₀..↑t, f τ (((next hf hx)^[n] α).compProj τ)) -
        ∫ (τ : ℝ) in ↑t₀..↑t, f τ (((next hf hx)^[n] β).compProj τ)‖ ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R ℝ
v : F
c : ℝ
p : R[X]
inst✝ : ZeroHomClass F R ℝ
⊢ ∃ i, gaussNorm v c p = v (p.coeff i) * c ^ i

Tactic:
by_cases h_supp : p.support.Nonempty
  · simp only [gaussNorm, h_supp]
    obtain ⟨i, hi1, hi2⟩ := Finset.exists_mem_eq_sup' h_supp fun i ↦ (v (p.coeff i) * c ^ i)
    exact ⟨i, hi2⟩
  · simp_all

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) f)
⊢ v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i ≤ v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i

Tactic:
exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inl
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) f)
this :
  max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) =
    v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤ v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i

Tactic:
exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) g)
⊢ v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i ≤ v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i

Tactic:
exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inr
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
t : σ →₀ ℕ
hv : v ((coeff t) f + (coeff t) g) ≤ max (v ((coeff t) f)) (v ((coeff t) g))
h : max (v ((coeff t) f)) (v ((coeff t) g)) = v ((coeff t) g)
this :
  max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) =
    v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i
⊢ v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤ v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i

Tactic:
exact mul_le_mul_of_nonneg (by aesop) (by aesop) (by aesop) (H t)

Goal state after: