mathlib-initiative/mathlib-tactics huggingface dataset:
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) ^ (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)
⊢ L + ε = L + (ε / 2 + ε / 2)

Tactic:
add_halves

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) ^ (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)
⊢ L + ε = L + ε
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

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

Tactic:
rw [← this]

Goal state after:
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
this : (⨆ n, if n = 0 then ‖r‖ else 0) = ‖r‖
⊢ (⨆ n, if n = 0 then ‖X.coeff n - (C r).coeff n‖ ^ (1 - ↑n)⁻¹ else 0) = ⨆ n, if n = 0 then ‖r‖ else 0
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
⊢ ∀ᶠ (c : ℕ) in atTop, 0 ≤ smoothingSeminormSeq μ x c

Tactic:
simpa [eventually_atTop, ge_iff_le] using ⟨1, fun _ _ ↦ by positivity⟩

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 : ℕ
a✝ : 0 ≤ b
⊢ μ x ^ (↑(s (ψ b)) * (1 / ↑(ψ b))) ≤ μ x ^ 1

Tactic:
apply rpow_le_rpow_of_exponent_le (not_lt.mp hμx)

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
⊢ ↑(s (ψ b)) * (1 / ↑(ψ b)) ≤ 1
Module: Mathlib.Analysis.Normed.Group.SeparationQuotient

Goal state before:
pp: case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
this : normedMk x = 0
⊢ mk x = 0

Tactic:
rw [← this]

Goal state after:
case mp
M : Type u_1
inst✝ : SeminormedAddCommGroup M
h : normedMk = 0
x : M
this : normedMk x = 0
⊢ mk x = normedMk x
Module: Mathlib.Analysis.Normed.Group.Tannery

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝ : Nonempty β
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

Tactic:
rcases 𝓕.eq_or_neBot with rfl | _

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
h✝ : Nonempty β
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) ⊥ (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) ⊥ (𝓝 (∑' (k : β), g k))

case inr.inr
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst✝¹ : NormedAddCommGroup G
inst✝ : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun x ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h✝¹ : Nonempty β
h✝ : 𝓕.NeBot
⊢ Tendsto (fun x ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))
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
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x

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
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x

Tactic:
· have hxn : μ (x ^ n) = 0 := by
      apply le_antisymm _ (apply_nonneg μ _)
      apply le_trans (map_pow_le_pow μ x (one_le_iff_ne_zero.mp hn))
      rw [hx0, zero_pow (pos_iff_ne_zero.mp hn)]
    rw [hx0, hxn, zero_rpow (one_div_cast_ne_zero (one_le_iff_ne_zero.mp hn))]

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
⊢ μ (x ^ n) ^ (1 / ↑n) = μ x
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✝ : Algebra.IsAlgebraic K E
a : E
ha : a ∈ ((mapAlg K E) (minpoly K x)).roots
⊢ spectralValue (minpoly K a) = spectralValue (minpoly K ((algebraMap L E) x))

Tactic:
have : (aeval a) (minpoly K ((algebraMap L E) x)) = 0 := by
    simp only [mem_roots', IsRoot.def] at ha
    rw [← ha.2, mapAlg_eq_map, minpoly.algebraMap_eq (algebraMap L E).injective, aeval_def,
      eval_map]

Goal state after:
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✝ : Algebra.IsAlgebraic K E
a : E
ha : a ∈ ((mapAlg K E) (minpoly K x)).roots
this : (aeval a) (minpoly K ((algebraMap L E) x)) = 0
⊢ spectralValue (minpoly K a) = spectralValue (minpoly K ((algebraMap L E) x))
Module: Mathlib.Analysis.Normed.Module.DoubleDual

Goal state before:
pp: 𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : StrongDual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
⊢ ‖x‖ ≤ M

Tactic:
← (inclusionInDoubleDualLi (E := E) 𝕜).norm_map x

Goal state after:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : StrongDual 𝕜 E), ‖f x‖ ≤ M * ‖f‖
⊢ ‖(inclusionInDoubleDualLi 𝕜) x‖ ≤ M
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case refine_1
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ 0 ∈
    {p |
      ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}

Tactic:
simp only [Set.mem_ofPred_eq]

Goal state after:
case refine_1
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ ∃ G x x_1, 0 = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)
Module: Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁵] ↑A
A_cofg : A.CoFG
h_ker : Disjoint (↑u).ker A
range_u : (↑u).range = ⊤
range_u_restr : IsClosed[inst✝²] ↑(↑(u.domRestrict A)).range
S : Submodule 𝕜 E
ker_le_S : (↑u).ker ≤ S
this✝ : FiniteDimensional 𝕜 ↥S
S_compl_A : IsTopCompl S A
uS_compl_uA : IsTopCompl (map (↑u) S) (map (↑u) A)
this : T2Space ↥(map (↑u) S)
uₛ : ↥S →L[𝕜] ↥(map (↑u) S) := u.restrict ⋯
uₐ : ↥A →L[𝕜] ↥(map (↑u) A) := u.restrict ⋯
Φ : (↥S × ↥A) ≃L[𝕜] E := S.prodEquivOfIsTopCompl A S_compl_A
Ψ : (↥(map (↑u) S) × ↥(map (↑u) A)) ≃L[𝕜] F := (map (↑u) S).prodEquivOfIsTopCompl (map (↑u) A) uS_compl_uA
u_eq : ⇑u = ⇑Ψ ∘ ⇑(uₛ.prodMap uₐ) ∘ ⇑Φ.symm
u_restr_eq : ⇑(u.domRestrict A) = ⇑(map (↑u) A).subtypeL ∘ ⇑uₐ
⊢ IsStrictMap ⇑↑(uₛ.prodMap uₐ) ↔ IsStrictMap ⇑↑uₐ

Tactic:
ContinuousLinearMap.coe_prodMap,

Goal state after:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : CompleteSpace 𝕜
E : Type u_2
F : Type u_3
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜 F
u : E →L[𝕜] F
A : Submodule 𝕜 E
A_closed : IsClosed[inst✝⁵] ↑A
A_cofg : A.CoFG
h_ker : Disjoint (↑u).ker A
range_u : (↑u).range = ⊤
range_u_restr : IsClosed[inst✝²] ↑(↑(u.domRestrict A)).range
S : Submodule 𝕜 E
ker_le_S : (↑u).ker ≤ S
this✝ : FiniteDimensional 𝕜 ↥S
S_compl_A : IsTopCompl S A
uS_compl_uA : IsTopCompl (map (↑u) S) (map (↑u) A)
this : T2Space ↥(map (↑u) S)
uₛ : ↥S →L[𝕜] ↥(map (↑u) S) := u.restrict ⋯
uₐ : ↥A →L[𝕜] ↥(map (↑u) A) := u.restrict ⋯
Φ : (↥S × ↥A) ≃L[𝕜] E := S.prodEquivOfIsTopCompl A S_compl_A
Ψ : (↥(map (↑u) S) × ↥(map (↑u) A)) ≃L[𝕜] F := (map (↑u) S).prodEquivOfIsTopCompl (map (↑u) A) uS_compl_uA
u_eq : ⇑u = ⇑Ψ ∘ ⇑(uₛ.prodMap uₐ) ∘ ⇑Φ.symm
u_restr_eq : ⇑(u.domRestrict A) = ⇑(map (↑u) A).subtypeL ∘ ⇑uₐ
⊢ IsStrictMap ⇑((↑uₛ).prodMap ↑uₐ) ↔ IsStrictMap ⇑↑uₐ
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
s : Finset ι
⊢ ∑ x ∈ s, ‖((B x) (↑e x)) (↑f x)‖ ^ r.toReal ≤ (↑K * ‖e‖ * ‖f‖) ^ r.toReal

Tactic:
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: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this✝¹ : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this✝ : IsUnit (adjoint ↑y ∘SL ↑y)
this : (starRingEnd 𝕜) α = α
⊢ α = ↑(RCLike.re α)

Tactic:
RCLike.conj_eq_iff_re,

Goal state after:
𝕜 : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : CompleteSpace V
inst✝² : NormedAddCommGroup W
inst✝¹ : InnerProductSpace 𝕜 W
inst✝ : CompleteSpace W
f : (V →L[𝕜] V) ≃⋆ₐ[𝕜] W →L[𝕜] W
hf : Continuous ⇑f
h✝ : Nontrivial V
y : V ≃L[𝕜] W
hy : ⇑{ toAlgEquiv := f.toAlgEquiv, continuous_toFun := hf, continuous_invFun := ⋯ } = ⇑y.conjContinuousAlgEquiv
this✝¹ : ∀ (x : V →L[𝕜] V), Commute x (adjoint ↑y ∘SL ↑y)
α : 𝕜
hα : α • 1 = adjoint ↑y ∘SL ↑y
this✝ : IsUnit (adjoint ↑y ∘SL ↑y)
this : ↑(RCLike.re α) = α
⊢ α = ↑(RCLike.re α)
Module: Mathlib.Analysis.ODE.Transform

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

Tactic:
by
  simp_rw [isIntegralCurveAt_iff_exists_pos]
  congrm ∃ ε > 0, ?_
  convert! isIntegralCurveOn_comp_add
  simp [neg_add_eq_sub]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha : ‖a‖₊ ≠ 1
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
rcases lt_or_gt_of_ne ha with ha | ha

Goal state after:
case inr.inl
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha✝ : ‖a‖₊ ≠ 1
ha : ‖a‖₊ < 1
⊢ ‖a‖₊ < p.cauchyBound

case inr.inr
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ∑ x ∈ range p.natDegree, ‖a‖₊ ^ x
ha✝ : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ ‖a‖₊ < p.cauchyBound
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos.inl
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
⊢ ⊥ < Q.degree

Tactic:
exact bot_lt_iff_ne_bot.2 fun hQ' => hQ (degree_eq_bot.1 hQ')

Goal state after:
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
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
hpq : p + q ≠ 0
i : ℕ
a✝ : i ∈ (p + q).support
⊢ v ((p + q).coeff i) * c ^ i ≤ max (v (p.coeff i)) (v (q.coeff i)) * c ^ i

Tactic:
rw [coeff_add]

Goal state after:
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
hpq : p + q ≠ 0
i : ℕ
a✝ : i ∈ (p + q).support
⊢ v (p.coeff i + q.coeff i) * c ^ i ≤ max (v (p.coeff i)) (v (q.coeff i)) * c ^ i
Module: Mathlib.Analysis.Polynomial.Norm

Goal state before:
pp: case pos
A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
h : p.support.Nonempty
⊢ p.supNorm = p.support.sup' h (norm ∘ p.coeff)

pp: case neg
A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
h : ¬p.support.Nonempty
⊢ p.supNorm = 0

Tactic:
· simp only [supNorm, gaussNorm, h, ↓reduceDIte, one_pow, mul_one, Function.comp_apply]
    congr

Goal state after:
case neg
A : Type u_1
inst✝ : SeminormedRing A
p : A[X]
h : ¬p.support.Nonempty
⊢ p.supNorm = 0
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) * c ^ (i + j) <
    v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) * c ^ (i + j)

Tactic:
convert_to! v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) <
    v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)

Goal state after:
case e'_3
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff (x, i + j - x).1 * q.coeff (x, i + j - x).2) * c ^ (i + j) =
    v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x))

case e'_4
c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff (i, i + j - i).1 * q.coeff (i, i + j - i).2) * c ^ (i + j) =
    v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)

c✝ : ℝ
R✝ : Type u_3
inst✝¹ : Ring R✝
v✝ : AbsoluteValue R✝ ℝ
c : ℝ
R : Type u_3
inst✝ : Ring R
v : AbsoluteValue R ℝ
hna : IsNonarchimedean ⇑v
hc : 0 < c
p q : R[X]
hc0 : 0 ≤ c
i : ℕ
hi_p : gaussNorm v c p = v (p.coeff i) * c ^ i
hlt_p : ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p
j : ℕ
hj_q : gaussNorm v c q = v (q.coeff j) * c ^ j
hlt_q : ∀ j_1 < j, v (q.coeff j_1) * c ^ j_1 < gaussNorm v c q
hvpq : v (p.coeff i) ≠ 0 ∧ v (q.coeff j) ≠ 0
this✝¹ : v (p.coeff i) ≠ 0
this✝ : v (q.coeff j) ≠ 0
x : ℕ
hx : x ∈ range (i + j).succ
hneq : x ≠ i
this : x + (i + j - x) = i + j
⊢ v (p.coeff x) * c ^ x * (v (q.coeff (i + j - x)) * c ^ (i + j - x)) < v (p.coeff i) * c ^ i * (v (q.coeff j) * c ^ j)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ p.mahlerMeasure ≤ p.sum fun x a ↦ ‖a‖

Tactic:
rw [show (p.sum fun _ a ↦ ‖a‖) = rexp (circleAverage (fun _ ↦ log (p.sum fun _ a ↦ ‖a‖)) 0 1)
    by simp [circleAverage_def, mul_assoc, exp_log this], mahlerMeasure_def_of_ne_zero hp,
    circleAverage_def, smul_eq_mul]

Goal state after:
case neg
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ rexp ((2 * π)⁻¹ * ∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖) ≤
    rexp ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (p.sum fun x a ↦ ‖a‖))
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case neg
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Tactic:
have hlogAe : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)),
      exp (log ‖p.eval (circleMap 0 1 θ)‖) = ‖p.eval (circleMap 0 1 θ)‖ := by
    filter_upwards [this] with θ hθ
    exact exp_log hθ

Goal state after:
case neg
p : ℂ[X]
this✝¹ : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π)))
this✝ : NeZero (volume (uIoc 0 (2 * π)))
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case refine_3
b✝ n✝ b : ℕ
hb0 : 0 < ↑n✝ + 2
hb : 1 < ↑b
n : ℕ
x : ℕ → Fin b
⊢ ‖ofDigitsTerm x n‖ ≤ (↑b)⁻¹ ^ n

Tactic:
· simp only [norm_eq_abs, abs_of_nonneg ofDigitsTerm_nonneg, inv_pow]
      apply ofDigitsTerm_le.trans
      calc
        _ ≤ b * ((b : ℝ) ^ (n + 1))⁻¹ := by
          gcongr
          linarith
        _ = _ := by
          grind

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
hx : Germ.Tendsto x (𝓝 0)
⊢ ArchimedeanClass.mk x ≠ 0

Tactic:
← stdPart_eq_zero,

Goal state after:
x : ℝ*
hx : Germ.Tendsto x (𝓝 0)
⊢ stdPart x = 0
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
r s : ℝ
hxr : x.IsSt r
hys : y.IsSt s
hrs : r < s
⊢ x < y

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩
  rcases ofSeq_surjective y with ⟨g, rfl⟩
  rw [isSt_ofSeq_iff_tendsto] at hxr hys
  exact ofSeq_lt_ofSeq.2 <| hxr.eventually_lt hys hrs

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

Goal state before:
pp: x y : ℝ≥0
⊢ 4 * x * y ≤ (x + y) ^ 2

Tactic:
exact four_mul_le_sq_add ..

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

Goal state before:
pp: x y : ℝ≥0
n m : ℕ
this : ∀ {k : ℕ}, (x.agmSequences y k).1 ≤ (x.agmSequences y k).2
⊢ (x.agmSequences y n).1 ≤ (x.agmSequences y m).2

Tactic:
by
    obtain h | h := le_total n m
    · exact (agmSequences_fst_monotone h).trans this
    · exact this.trans (agmSequences_snd_antitone h)

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

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ (1 + z).arg ∈ Set.Ioo (-(π / 2)) (π / 2)

Tactic:
by
  rw [Set.mem_Ioo, ← abs_lt, abs_arg_lt_pi_div_two_iff, add_re, one_re, ← neg_lt_iff_pos_add']
  exact Or.inl (abs_lt.mp ((abs_re_le_norm z).trans_lt hz)).1

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

Goal state before:
pp: p : ℝ
hp : p < 0
hp' : p < -1
⊢ log p < log (1 - p)

Tactic:
rw [← log_neg_eq_log]

Goal state after:
p : ℝ
hp : p < 0
hp' : p < -1
⊢ log (-p) < log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

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

Tactic:
have hp : 1 - p < 2⁻¹ := by
      rw [sub_lt_comm]; norm_num at *; linarith +splitNe
    rw [← binEntropy_one_sub]
    exact this hp.ne hp

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

Goal state before:
pp: case inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
⊢ Real.log (|z.im| ^ n) ≤ |z.re|

Tactic:
Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _),

Goal state after:
case inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ n ≤ Real.exp z.re
hle : z.re ≤ |z.im|
h₁ : 1 < z.re
H : 1 < |z.im|
⊢ |z.im| ^ n ≤ Real.exp |z.re|