mathlib-initiative/mathlib-tactics huggingface dataset:
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
y : L
hy✝ : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hy : -y = (algebraMap (↥K⟮y⟯) L) (-g)
⊢ spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (-g)) =
    spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)

Tactic:
map_neg,

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
y : L
hy✝ : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hy : -y = (algebraMap (↥K⟮y⟯) L) (-g)
⊢ spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (-(algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g) =
    spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)
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
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
⊢ spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y

Tactic:
set gy := IntermediateField.AdjoinPair.gen₂ K x y

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
x y : L
hx : IsAlgebraic K x
hy : IsAlgebraic K y
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
⊢ spectralNorm K L (x * y) ≤ spectralNorm K L x * spectralNorm K L y
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
⊢ spectralNorm K L (x + y) ≤ max (spectralNorm K L x) (spectralNorm K L y)

Tactic:
set gy := IntermediateField.AdjoinPair.gen₂ K x y

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
⊢ spectralNorm K L (x + y) ≤ max (spectralNorm K L x) (spectralNorm K L y)
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
s : Finset ι := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
⊢ (zipWith edist ⋯ f.ofLp h.ofLp).support ⊆ s

Tactic:
grind [support_zipWith]

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
s : Finset ι := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
⊢ (zipWith edist ⋯ f.ofLp g.ofLp).support ⊆ s

Tactic:
grind [support_zipWith]

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
s : Finset ι := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
⊢ (zipWith edist ⋯ g.ofLp h.ofLp).support ⊆ s

Tactic:
grind [support_zipWith]

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

Goal state before:
pp: case pos
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
hxn : μ (x ^ n) = 0
⊢ μ (x ^ n) ^ (1 / ↑n) = 0

Tactic:
hxn,

Goal state after:
case pos
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
hxn : μ (x ^ n) = 0
⊢ 0 ^ (1 / ↑n) = 0
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✝ : MetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ edist f g = ENNReal.ofReal (((zipWith dist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹)

Tactic:
rw [edist_dist, dist_def]

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

Goal state before:
pp: case neg
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
x y : L
hx : ¬x = 0
hx' : (spectralAlgNorm K L) x ≠ 0
hf1 : (spectralAlgNorm K L) 1 ≤ 1
f : AlgebraNorm K L := algNormFromConst hf1 hx
hf : f = algNormFromConst hf1 hx
⊢ (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y

Tactic:
have hf_pow : IsPowMul f := seminormFromConst_isPowMul hf1 hx' isPowMul_spectralNorm

Goal state after:
case neg
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
x y : L
hx : ¬x = 0
hx' : (spectralAlgNorm K L) x ≠ 0
hf1 : (spectralAlgNorm K L) 1 ≤ 1
f : AlgebraNorm K L := algNormFromConst hf1 hx
hf : f = algNormFromConst hf1 hx
hf_pow : IsPowMul ⇑f
⊢ (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
this : ∀ᶠ (a : Finset ι) in (unconditional ι).filter, ∏ b ∈ a, v b ≤ r₁
⊢ ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁

Tactic:
rw [unconditional, eventually_atTop] at this

Goal state after:
ι : Type u_1
v : ι → ℝ
hv : Multipliable v
r₁ : ℝ
hr₁ : 0 < r₁ ∧ ∏' (i : ι), v i < r₁
this : ∃ a, ∀ (b : Finset ι), a ⊆ b → ∏ b ∈ b, v b ≤ r₁
⊢ ∃ r₁ > 0, ∃ s₁, ∀ (t : Finset ι), s₁ ⊆ t → ∏ i ∈ t, v i ≤ r₁
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)
⊢ HasProdUniformlyOn f (fun x ↦ ∏' (i : ι), f i x) s

Tactic:
simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn]
  obtain ⟨r, hr⟩ := hf.exists
  suffices H : TendstoUniformlyOn (fun s x ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s by
    refine H.congr_right (hr.tsum_eqOn.comp_left.symm.trans ?_)
    exact fun x hx ↦ (cexp_tsum_eq_tprod (hfn x hx) (hf.summable hx))
  refine (hr.tendstoUniformlyOn.comp_cexp ?_).congr ?_
  · simpa +contextual [← hr.tsum_eqOn _] using hg
  · filter_upwards with s i hi using by simp [exp_sum, fun y ↦ exp_log (hfn i hi y)]

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

Goal state before:
pp: ι : Type uι
inst✝⁵ : Fintype ι
𝕜 : Type u𝕜
inst✝⁴ : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : ⨂[𝕜] (i : ι), E i
⊢ ‖(toDualContinuousMultilinearMap F) x‖ ≤ ‖x‖

Tactic:
by
  simp only [toDualContinuousMultilinearMap, LinearMap.coe_mk, AddHom.coe_mk]
  apply LinearMap.mkContinuous_norm_le _ (by positivity)

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✝ : NormedField 𝕜
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
⊢ 0 ≤ projectiveSeminormAux p

Tactic:
refine List.sum_nonneg fun a ↦ ?_

Goal state after:
ι : Type u_1
inst✝² : Fintype ι
𝕜 : Type u_2
E : ι → Type u_3
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : NormedField 𝕜
p : FreeAddMonoid (𝕜 × ((i : ι) → E i))
a : ℝ
⊢ a ∈ List.map (fun p ↦ ‖p.1‖ * ∏ i, ‖p.2 i‖) (FreeAddMonoid.toList p) → 0 ≤ a
Module: Mathlib.Analysis.Normed.Lp.lpHolder

Goal state before:
pp: ι : 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)
⊢ ‖((holderₗ r B hBK) e) f‖ ≤ ↑K * ‖e‖ * ‖f‖

Tactic:
by
    obtain ⟨(rfl | hp), (rfl | hq)⟩ := And.intro p.dichotomy q.dichotomy
    · obtain rfl : r = ⊤ := ENNReal.HolderTriple.unique ∞ ∞ r ∞
      refine norm_le_of_forall_le (by positivity) fun i ↦ ?_
      refine (B i).le_of_opNorm₂_le_of_le (hBK i) ?_ ?_
      all_goals exact norm_apply_le_norm (by simp) ..
    · 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
    · obtain rfl : r = p := ENNReal.HolderTriple.unique p ∞ r p
      refine norm_le_of_forall_sum_le (zero_lt_one.trans_le hp) (by positivity) fun s ↦ ?_
      rw [mul_right_comm, Real.mul_rpow (by positivity) (by positivity)]
      refine Memℓp.holder_top_right_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 hp) e
    · have hpqr := hpqr.toReal r (zero_lt_one.trans_le hp) (zero_lt_one.trans_le hq)
      have hp := hpqr.pos
      have hq := hpqr.symm.pos
      refine norm_le_of_forall_sum_le hpqr.pos' (by positivity) fun s ↦ ?_
      simp only [holderₗ_apply_apply_coe]
      calc
        _ ≤ K ^ r.toReal * (‖e‖ ^ p.toReal) ^ (r.toReal / p.toReal) *
          (‖f‖ ^ q.toReal) ^ (r.toReal / q.toReal) :=
          Memℓp.holder_gen_bound r hp hq B hBK (by positivity) (by positivity)
            (sum_rpow_le_norm_rpow hp e) (sum_rpow_le_norm_rpow hq f) s
        _ ≤ _ := by
          rw [← Real.rpow_mul, ← Real.rpow_mul]
          · simp only [← mul_div_assoc, ne_eq, hp.ne', not_false_eq_true, mul_div_cancel_left₀,
            hq.ne', fieldLe]
            rw [Real.mul_rpow, Real.mul_rpow]
            all_goals positivity
          all_goals positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv

Goal state before:
pp: case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
⊢ ∃ U, ∀ (x : V →L[𝕜] V), f x ∘SL ↑U = ↑U ∘SL x

Tactic:
have hT x : T x = f (smulRight v x) z := rfl

Goal state after:
case neg
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : SeminormedAddCommGroup W
inst✝³ : NormedSpace 𝕜 V
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeparatingDual 𝕜 V
inst✝ : SeparatingDual 𝕜 W
f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : StrongDual 𝕜 V
huv : v u ≠ 0
z : W
hz : ¬(f (smulRight v u)) z = 0 z
T : V →L[𝕜] W := (apply' W (RingHom.id 𝕜)) z ∘SL (↑f).toContinuousLinearMap ∘SL (smulRightL 𝕜 V V) v
hT : ∀ (x : V), T x = (f (smulRight v x)) z
⊢ ∃ U, ∀ (x : V →L[𝕜] V), f x ∘SL ↑U = ↑U ∘SL x
Module: Mathlib.Analysis.PSeriesComplex

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

Tactic:
by
  rw [← Real.summable_one_div_nat_rpow, ← summable_nat_add_iff 1 (G := ℝ),
    ← summable_nat_add_iff 1 (G := ℂ), ← summable_norm_iff]
  simp only [norm_div, norm_one, ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos
    (Nat.cast_pos.mpr <| Nat.succ_pos _)]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Fourier

Goal state before:
pp: p : ℂ[X]
this :
  ∑ x ∈ p.support, ‖p.coeff x‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
h1 :
  ∫ (t : AddCircle (2 * π)), ‖(toAddCircle p) t‖ ^ 2 ∂haarAddCircle =
    ∫ (t : AddCircle (2 * π)), ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
⊢ (2 * π)⁻¹ • ∫ (t : AddCircle (2 * π)), ‖(toAddCircle p) t‖ ^ 2 = Real.circleAverage (fun θ ↦ ‖eval θ p‖ ^ 2) 0 1

Tactic:
Real.circleAverage,

Goal state after:
p : ℂ[X]
this :
  ∑ x ∈ p.support, ‖p.coeff x‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
h1 :
  ∫ (t : AddCircle (2 * π)), ‖(toAddCircle p) t‖ ^ 2 ∂haarAddCircle =
    ∫ (t : AddCircle (2 * π)), ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
⊢ (2 * π)⁻¹ • ∫ (t : AddCircle (2 * π)), ‖(toAddCircle p) t‖ ^ 2 =
    (2 * π)⁻¹ • ∫ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ ^ 2
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
⊢ (fun x ↦ eval x P) =o[cobounded R] fun x ↦ eval x Q

Tactic:
· refine isEquivalent_cobounded_leading_monomial.trans_isLittleO <|
      ((IsLittleO.const_mul_right ?_ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm
    · exact leadingCoeff_ne_zero.mpr (ne_zero_of_degree_gt h)
    · exact isLittleO_pow_pow_cobounded_of_lt (natDegree_lt_natDegree hP h)

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

Goal state before:
pp: case inr
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
p q : R[X]
h✝ : p ≠ 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

Tactic:
rcases eq_or_ne q 0 with hq | _

Goal state after:
case inr.inl
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
p q : R[X]
h✝ : p ≠ 0
hq : q = 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)

case inr.inr
R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
hna : IsNonarchimedean ⇑v
c : ℝ
hc : 0 ≤ c
p q : R[X]
h✝¹ : p ≠ 0
h✝ : q ≠ 0
⊢ gaussNorm v c (p + q) ≤ max (gaussNorm v c p) (gaussNorm v c q)
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: case inl
R : Type u_1
F : Type u_2
inst✝⁴ : Semiring R
inst✝³ : FunLike F R ℝ
v : F
c : ℝ
inst✝² : ZeroHomClass F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
hna : IsNonarchimedean ⇑v
p q : R[X]
hc : 0 ≤ c
hpq : p * q = 0
⊢ gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

Tactic:
simp [hpq, hc, gaussNorm_nonneg, mul_nonneg]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Order

Goal state before:
pp: case neg
P : ℝ[X]
x : ℝ
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
hroots : eval x P ≤ 0
⊢ ∃ y, P.IsRoot y ∧ x ≤ y

Tactic:
obtain ⟨z, hz⟩ := Filter.Eventually.exists_forall_of_atTop <|
    (P.tendsto_atTop_of_leadingCoeff_nonneg hdeg hlc.le).eventually_gt_atTop 0

Goal state after:
case neg
P : ℝ[X]
x : ℝ
hlc : 0 < P.leadingCoeff
hdeg : 0 < P.degree
hroots : eval x P ≤ 0
z : ℝ
hz : ∀ (b : ℝ), z ≤ b → 0 < eval b P
⊢ ∃ y, P.IsRoot y ∧ x ≤ y
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: case inl
α : Type u_3
S : Type u_4
inst✝¹ : LinearOrder S
inst✝ : AddCommGroup α
f : α → S
na : IsNonarchimedean f
Neg : ∀ (a : α), f a = f (-a)
a b : α
hne : f a ≠ f b
hab : f a > f b
h : f (a + b + -b) ≤ f (a + b)
⊢ max (f a) (f b) ≤ f (a + b)

Tactic:
simpa [max_eq_left (le_of_lt hab)] using h

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
h : p.degree = 1
⊢ p.mahlerMeasure = max ‖p.coeff 1‖ ‖p.coeff 0‖

Tactic:
by
  rw [eq_X_add_C_of_degree_le_one (le_of_eq h)]
  simp [mahlerMeasure_C_mul_X_add_C (show p.coeff 1 ≠ 0 by exact coeff_ne_zero_of_eq_degree h)]

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case h.right
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ ∀ y ∈ {x | eval (circleMap 0 1 x) p ≠ 0}, log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun x a ↦ ‖a‖)

Tactic:
intro _ _
    gcongr
    rw [eval_eq_sum]
    apply norm_sum_le_of_le p.support
    simp

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))

Tactic:
rw [uIoc_of_le (by positivity)]

Goal state after:
p : ℂ[X]
⊢ IsFiniteMeasure (volume.restrict (Ioc 0 (2 * π)))
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: n : ℕ
⊢ n • |ArchimedeanOrder.val (ArchimedeanOrder.of 1)| < |ArchimedeanOrder.val (ArchimedeanOrder.of ω)|

Tactic:
by simpa using! coe_lt_omega n

Goal state after:
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0

Tactic:
Int.cast_ne_zero

Goal state after:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ m ≠ 0
Module: Mathlib.NumberTheory.Real.Irrational

Goal state before:
pp: m : ℤ
x : ℝ
⊢ ↑m ≠ 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x

Tactic:
Int.cast_ne_zero

Goal state after:
m : ℤ
x : ℝ
⊢ m ≠ 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ x - y ≠ 0

Tactic:
← zero_lt_iff,

Goal state after:
x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ 0 < x - y
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ}, p ≠ 2⁻¹ → p < 2⁻¹ → binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ 1 - 2⁻¹ < p

Tactic:
norm_num at *

Goal state after:
p : ℝ
h : ¬p = 1 / 2
this : ∀ {p : ℝ}, ¬p = 1 / 2 → p < 1 / 2 → binEntropy p < log 2
hp : 1 / 2 ≤ p
⊢ 1 / 2 < p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p✝ p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) = log 2

Tactic:
rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two] <;> positivity

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: p : ℝ
⊢ binEntropy p < log 2 ↔ p ≠ 2⁻¹

Tactic:
refine ⟨?_, fun h ↦ ?_⟩
  · rintro h rfl
    simp at h
  wlog hp : p < 2⁻¹
  · have hp : 1 - p < 2⁻¹ := by
      rw [sub_lt_comm]; norm_num at *; linarith +splitNe
    rw [← binEntropy_one_sub]
    exact this hp.ne hp
  obtain hp₀ | hp₀ := le_or_gt p 0
  · exact (binEntropy_nonpos_of_nonpos hp₀).trans_lt <| log_pos <| by simp
  have hp₁ : 0 < 1 - p := sub_pos.2 <| hp.trans <| by norm_num
  calc
  _ < log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) :=
    strictConcaveOn_log_Ioi.2 (inv_pos.2 hp₀) (inv_pos.2 hp₁)
      (by simpa [eq_sub_iff_add_eq, ← two_mul, mul_comm, mul_eq_one_iff_eq_inv₀]) hp₀ hp₁ (by simp)
  _ = log 2 := by rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two] <;> positivity

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: case inl
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z

Tactic:
rcases k.eq_zero_or_pos with rfl | hk

Goal state after:
case inl.inl
p : ℤ[X]
a : ℤ
hp : p.natDegree ≤ 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ 0 = ↑z

case inl.inr
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
hk : k > 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order

Goal state before:
pp: case pos.inr
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p : ℝ≥0
a b : A
hab : a ≤ b
ha : 0 ≤ a
hb : 0 ≤ b
hIcc : Icc 0 1 = Ioo 0 1 ∪ {0} ∪ {1}
hp : p ∈ {1}
⊢ (fun a ↦ a ^ p) a ≤ (fun a ↦ a ^ p) b

Tactic:
simp_all [mem_singleton_iff, nnrpow_one a, nnrpow_one b]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ (∫ (x : ℝ) in a * ε..a * r, x⁻¹ • f x) - ∫ (x : ℝ) in ε..r, x⁻¹ • f (b * x) =
    (∫ (y : ℝ) in a * ε..a * r, u y) - ∫ (y : ℝ) in b * ε..b * r, u y

Tactic:
integral_comp_mul_inv_smul hb.ne'

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ (∫ (x : ℝ) in a * ε..a * r, x⁻¹ • f x) - ∫ (x : ℝ) in b * ε..b * r, x⁻¹ • f x =
    (∫ (y : ℝ) in a * ε..a * r, u y) - ∫ (y : ℝ) in b * ε..b * r, u y
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
hx : 0 ≤ x
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
by rw [rpowIntegrand₀₁_eq_pow_div hp (le_of_lt ht) hx]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 0) volume

Tactic:
rw [← Set.Ioc_union_Ioi_eq_Ioi zero_le_one]
  exact IntegrableOn.union (integrableOn_rpowIntegrand₀₁_Ioc hp hx)
    (integrableOn_rpowIntegrand₀₁_Ioi_one hp hx)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case inl
p : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ 0
⊢ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 0 = 0 ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1

pp: case inr
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
⊢ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x = x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1

Tactic:
· simp [rpowIntegrand₀₁, Real.zero_rpow hp.1.ne']

Goal state after:
case inr
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
⊢ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x = x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case succ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ ¬s = -↑(m + 1) + 1

Tactic:
convert! hs m using 2

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
m : ℕ
⊢ -↑(m + 1) + 1 = -↑m