mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set ↑(sphere 0 r)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x // x ∈ Ioi 0 }
hxU : ↑x ∈ U
this : Subtype.val ∘ ⇑(homeomorphSphereProd E r hr₀).symm '' V ×ˢ Ioi 0 ↓∩ U ∈ 𝓝 (↑(y, x).2 • ↑(y, x).1)
⊢ U • Subtype.val '' V ∈ 𝓝 ((fun x1 x2 ↦ x1 • x2) ↑x ↑y)

pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set ↑(sphere 0 r)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x // x ∈ Ioi 0 }
hxU : ↑x ∈ U
this :
  Subtype.val ∘ ⇑(homeomorphSphereProd E r hr₀).symm '' V ×ˢ Ioi 0 ↓∩ U ∈
    𝓝[{0}ᶜ] ↑((homeomorphSphereProd E r hr₀).symm (y, x))
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}ᶜ

pp: case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set ↑(sphere 0 r)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x // x ∈ Ioi 0 }
hxU : ↑x ∈ U
this :
  Subtype.val ∘ ⇑(homeomorphSphereProd E r hr₀).symm '' V ×ˢ Ioi 0 ↓∩ U ∈
    𝓝[{0}ᶜ] ↑((homeomorphSphereProd E r hr₀).symm (y, x))
⊢ ↑((homeomorphSphereProd E r hr₀).symm (y, x)) ∈ {0}ᶜ

Tactic:
· filter_upwards [this]
    rintro _ ⟨⟨a, b⟩, ⟨ha, hb⟩, rfl⟩
    rw [Function.comp_apply, homeomorphSphereProd_symm_apply_coe]
    apply Set.smul_mem_smul
    exacts [hb, mem_image_of_mem _ ha]

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set ↑(sphere 0 r)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x // x ∈ Ioi 0 }
hxU : ↑x ∈ U
this :
  Subtype.val ∘ ⇑(homeomorphSphereProd E r hr₀).symm '' V ×ˢ Ioi 0 ↓∩ U ∈
    𝓝[{0}ᶜ] ↑((homeomorphSphereProd E r hr₀).symm (y, x))
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {0}ᶜ

case ha
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : r ≠ 0
V : Set ↑(sphere 0 r)
hV : IsOpen[instTopologicalSpaceSubtype] V
y : { x // x ∈ sphere 0 r }
hyV : y ∈ V
U : Set ℝ
hU : IsOpen U
hU₀ : 0 ∉ U
hr₀ : 0 < r
x : { x // x ∈ Ioi 0 }
hxU : ↑x ∈ U
this :
  Subtype.val ∘ ⇑(homeomorphSphereProd E r hr₀).symm '' V ×ˢ Ioi 0 ↓∩ U ∈
    𝓝[{0}ᶜ] ↑((homeomorphSphereProd E r hr₀).symm (y, x))
⊢ ↑((homeomorphSphereProd E r hr₀).symm (y, x)) ∈ {0}ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Log.Summable

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : NormedCommRing R
inst✝² : NormOneClass R
f : ι → R
inst✝¹ : CompleteSpace R
inst✝ : NormMulClass R
hf : ∀ (i : ι), 1 + f i ≠ 0
hu : Summable fun x ↦ ‖f x‖
⊢ Multipliable fun i ↦ 1 + f i

Tactic:
· exact multipliable_one_add_of_summable hu

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

Goal state before:
pp: case h
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
⊢ ∀ (x : SeminormedAddCommGroup G) (x_1 : NormedSpace 𝕜 G),
    p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) →
      p ≤ projectiveSeminorm

Tactic:
_

Goal state after:
case h
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
x✝ : SeminormedAddCommGroup G
⊢ ∀ (x : NormedSpace 𝕜 G),
    p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) →
      p ≤ projectiveSeminorm
Module: Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm

Goal state before:
pp: case h
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
x✝ : SeminormedAddCommGroup G
⊢ ∀ (x : NormedSpace 𝕜 G),
    p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) →
      p ≤ projectiveSeminorm

Tactic:
_

Goal state after:
case h
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)
G : Type (max uι u𝕜 uE)
x✝¹ : SeminormedAddCommGroup G
x✝ : NormedSpace 𝕜 G
⊢ p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G) →
    p ≤ projectiveSeminorm
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))
a : ℝ
x : 𝕜
m : (i : ι) → E i
⊢ (x, m) ∈ FreeAddMonoid.toList p → ‖x‖ * ∏ x, ‖m x‖ = a → 0 ≤ a

Tactic:
_

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 : ℝ
x : 𝕜
m : (i : ι) → E i
a✝ : (x, m) ∈ FreeAddMonoid.toList p
⊢ ‖x‖ * ∏ x, ‖m x‖ = a → 0 ≤ a
Module: Mathlib.Topology.Algebra.Order.UpperLower

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsUpperSet (interior s)

Tactic:
← isLowerSet_compl,

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : HasUpperLowerClosure α
s : Set α
h : IsUpperSet s
⊢ IsLowerSet (interior s)ᶜ
Module: Mathlib.Analysis.ODE.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s

Tactic:
IsIntegralCurveAt,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ (∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt γ (v t (γ t)) t) ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s
Module: Mathlib.Analysis.ODE.Basic

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

Tactic:
IsIntegralCurveAt,

Goal state after:
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₀ ε)
Module: Mathlib.Analysis.ODE.Gronwall

Goal state before:
pp: δ K ε x a : ℝ
⊢ HasDerivAt (fun y ↦ gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x

Tactic:
by
  convert! (hasDerivAt_gronwallBound δ K ε _).comp x ((hasDerivAt_id x).sub_const a) using 1
  rw [id, mul_one]

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

Goal state before:
pp: δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
⊢ gronwallBound δ K ε x₁ ≤ gronwallBound δ K ε x₂

Tactic:
unfold gronwallBound

Goal state after:
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
⊢ (if K = 0 then δ + ε * x₁ else δ * rexp (K * x₁) + ε / K * (rexp (K * x₁) - 1)) ≤
    if K = 0 then δ + ε * x₂ else δ * rexp (K * x₂) + ε / K * (rexp (K * x₂) - 1)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x ↦ eval x P) ~[atBot] fun x ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
by
  convert! (P.comp (-X)).isEquivalent_atTop_lead.comp_tendsto tendsto_neg_atBot_atTop using 2
  · simp
  · rw [Function.comp_apply, comp_neg_X_leadingCoeff_eq, ← mul_rotate]
    simp [natDegree_comp, ← mul_pow, mul_comm]

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

Goal state before:
pp: case inr.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
hpq : p + q ≠ 0
i : ℕ
⊢ i ∈ (p + q).support →
    v ((p + q).coeff i) * c ^ i ≤
      max (if h : p.support.Nonempty then p.support.sup' h fun i ↦ v (p.coeff i) * c ^ i else 0)
        (if h : q.support.Nonempty then q.support.sup' h fun i ↦ v (q.coeff i) * c ^ i else 0)

Tactic:
_

Goal state after:
case inr.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
hpq : p + q ≠ 0
i : ℕ
a✝ : i ∈ (p + q).support
⊢ v ((p + q).coeff i) * c ^ i ≤
    max (if h : p.support.Nonempty then p.support.sup' h fun i ↦ v (p.coeff i) * c ^ i else 0)
      (if h : q.support.Nonempty then q.support.sup' h fun i ↦ v (q.coeff i) * c ^ i else 0)
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
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
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
⊢ i ∈ (p * q).support →
    v (∑ x ∈ range i.succ, p.coeff x * q.coeff (i - x)) * c ^ i ≤
      (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) * q.support.sup' ⋯ fun i ↦ v (q.coeff i) * c ^ i

Tactic:
_

Goal state after:
case inr
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
h_supp_p : p.support.Nonempty
h_supp_q : q.support.Nonempty
i : ℕ
a✝ : i ∈ (p * q).support
⊢ v (∑ x ∈ range i.succ, p.coeff x * q.coeff (i - x)) * c ^ i ≤
    (p.support.sup' ⋯ fun i ↦ v (p.coeff i) * c ^ i) * q.support.sup' ⋯ fun i ↦ v (q.coeff i) * c ^ i
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case h.left
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
⊢ {x | eval (circleMap 0 1 x) p ≠ 0} ∈ ae (volume.restrict (Icc 0 (2 * π)))

Tactic:
rw [mem_ae_iff, compl_def, Measure.restrict_apply' (by simp)]
    apply (Finite.of_sdiff _ <| finite_singleton (2 * π)).measure_zero
    simp only [ne_eq, mem_ofPred_eq, Decidable.not_not, inter_sdiff_assoc, Icc_sdiff_right]
    rw [ofPred_inter_eq_sep]
    apply Finite.of_finite_image (f := circleMap 0 1) ((Multiset.finite_toSet p.roots).subset _)
      <| fun _ h _ k l ↦ injOn_circleMap_of_abs_sub_le' one_ne_zero (by linarith) h.1 k.1 l
    simp [hp]

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✝ : ℝ
⊢ y✝ ∈ {x | eval (circleMap 0 1 x) p ≠ 0} → log ‖eval (circleMap 0 1 y✝) p‖ ≤ log (p.sum fun x a ↦ ‖a‖)

Tactic:
_

Goal state after:
case h.right
p : ℂ[X]
hp : ¬p = 0
this : 0 < p.sum fun x a ↦ ‖a‖
y✝ : ℝ
a✝ : y✝ ∈ {x | eval (circleMap 0 1 x) p ≠ 0}
⊢ log ‖eval (circleMap 0 1 y✝) p‖ ≤ log (p.sum fun x a ↦ ‖a‖)
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hx : Germ.Tendsto x atBot
⊢ x < ↑r

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩
  rw [tendsto_ofSeq] at hx
  exact ofSeq_lt_ofSeq.2 <| hx.eventually_mem (Iio_mem_atBot r)

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

Goal state before:
pp: case neg
A : Type u_2
inst✝ : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry ⇑v
hp : ¬p.leadingCoeff = 0
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v

Tactic:
· have hv_ne : v p.leadingCoeff ≠ 0 :=
      fun h ↦ hp <| hv.injective <| h.trans (map_zero _).symm
    have hv_norm : ‖v p.leadingCoeff‖ = ‖p.leadingCoeff‖ := hv.norm_map_of_map_zero (map_zero _) _
    grw [← hv_norm, ← leadingCoeff_map_of_leadingCoeff_ne_zero v hv_ne,
      leadingCoeff_le_mahlerMeasure, mapMahlerMeasure]

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

Goal state before:
pp: x : ℝ*
⊢ (-x).InfinitePos ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0

Tactic:
infinitePos_iff_infinitesimal_inv_pos,

Goal state after:
x : ℝ*
⊢ (-x)⁻¹.Infinitesimal ∧ 0 < (-x)⁻¹ ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
z₁ : 1 + z * I ≠ 0
h₂ : -I = z
⊢ z = -I

Tactic:
exact h₂.symm

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

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ cexp (2 * (z.arctan * I)) = (1 + z * I) / (1 - z * I)

Tactic:
rw [arctan, ← mul_rotate, ← mul_assoc,
      show 2 * (I * (-I / 2)) = 1 by simp [field], one_mul, exp_log]

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
z₁ : 1 + z * I ≠ 0
z₂ : 1 - z * I ≠ 0
⊢ (1 + z * I) / (1 - z * I) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Arcosh

Goal state before:
pp: x : ℝ
hx : 1 ≤ x
⊢ arcosh x = 0 ↔ x = 1

Tactic:
← exp_injective.eq_iff,

Goal state after:
x : ℝ
hx : 1 ≤ x
⊢ rexp (arcosh x) = rexp 0 ↔ x = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
| log ((cos z + sin z * I) / (cos z - sin z * I))

Tactic:
1,

Goal state after:
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
| (cos z + sin z * I) / (cos z - sin z * I)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
⊢ (tan z).arctan = z

Tactic:
by
  have h := cos_ne_zero_of_arctan_bounds h₀ h₁ h₂
  unfold arctan tan
  -- multiply top and bottom by `cos z`
  rw [← mul_div_mul_right (1 + _) _ h, add_mul, sub_mul, one_mul, ← mul_rotate, mul_div_cancel₀ _ h]
  conv_lhs =>
    enter [2, 1, 2]
    rw [sub_eq_add_neg, ← neg_mul, ← sin_neg, ← cos_neg]
  rw [← exp_mul_I, ← exp_mul_I, ← exp_sub, show z * I - -z * I = 2 * (I * z) by ring, log_exp,
    show -I / 2 * (2 * (I * z)) = -(I * I) * z by ring, I_mul_I, neg_neg, one_mul]
  all_goals simp
  · rwa [← div_lt_iff₀' two_pos, neg_div]
  · rwa [← le_div_iff₀' two_pos]

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

Goal state before:
pp: x y : ℝ≥0
| Tendsto (fun t ↦ dist x y / 2 ^ (t + 1)) atTop (𝓝 (0 * (dist x y / 2)))

Tactic:
1,

Goal state after:
x y : ℝ≥0
| fun t ↦ dist x y / 2 ^ (t + 1)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
| ⨅ n, (y.agmSequences x n).2

Tactic:
1,

Goal state after:
x y : ℝ≥0
| fun n ↦ (y.agmSequences x n).2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
| Tendsto (fun x_1 ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1) atTop (𝓝 0)

Tactic:
1,

Goal state after:
x y : ℝ≥0
| fun x_1 ↦ dist (x.agmSequences y x_1).2 (x.agmSequences y x_1).1
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: case inr
x y : ℝ≥0
this : ∀ {x y : ℝ≥0}, x ≤ y → min x y ≤ x.agm y
h : ¬x ≤ y
⊢ min x y ≤ x.agm y

Tactic:
simpa [agm_comm, min_comm] using this (not_le.mp h).le

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 1
⊢ sinh (artanh x) = x / √(1 - x ^ 2)

Tactic:
have : 0 < √((1 + x) / (1 - x)) := sqrt_pos_of_pos <| div_pos (by grind) (by grind)
  rw [← one_pow, sq_sub_sq 1 x, sqrt_mul]
    <;> grind [artanh, sinh_eq, exp_neg, exp_log, sqrt_div]

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

Goal state before:
pp: x : ℝ
hx : x ∈ Ioo (-1) 0
⊢ artanh x < 0

Tactic:
by
  rw [← artanh_zero, artanh_lt_artanh_iff (by grind) (by grind)]
  exact hx.2

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

Goal state before:
pp: q : ℕ
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1

Tactic:
have tendstoBot : Tendsto (fun p ↦ log (q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot := by
    have : (fun p ↦ log (q - 1) + log (1 - p) - log p)
      = (fun p ↦ log (q - 1) + (log (1 - p) - log p)) := by
      ext
      ring
    rw [this]
    apply tendsto_atBot_add_const_left
    exact tendsto_log_one_sub_sub_log_nhdsLT_one_atBot
  apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoBot) nhdsWithin_le_nhds
  · simp only [disjoint_nhds_atBot_iff, not_isBot, not_false_eq_true]
  filter_upwards [Ioo_mem_nhdsLT (show 1 - 2⁻¹ < (1 : ℝ) by norm_num)]
  intros
  apply (deriv_qaryEntropy _ _).symm
  · simp_all only [mem_Ioo, ne_eq]
    linarith [show (1 : ℝ) = 2⁻¹ + 2⁻¹ by norm_num]
  · simp_all only [mem_Ioo, ne_eq]
    linarith [two_inv_lt_one (α := ℝ)]

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

Goal state before:
pp: case neg
A : Type u_1
inst✝⁸ : PartialOrder A
inst✝⁷ : Ring A
inst✝⁶ : StarRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarOrderedRing A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : SeparatelyContinuousMul A
c a b : A
hab : a ≤ b
hc : ¬0 ≤ c
⊢ (conjSqrt c) a ≤ (conjSqrt c) b

Tactic:
simp [conjSqrt_of_not_nonneg hc]

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

Goal state before:
pp: s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
⊢ ‖log x‖ / (‖log x‖ + 1) ≤ 1

Tactic:
rw [div_le_one₀]

Goal state after:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
⊢ ‖log x‖ ≤ ‖log x‖ + 1

s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
x : ℝ
hx : x ∈ s
⊢ 0 < ‖log x‖ + 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
a₁✝ : A
⊢ ∀ ⦃a₂ : A⦄, addl a₁✝ = addl a₂ → a₁✝ = a₂

Tactic:
_

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
a₁✝ a₂✝ : A
⊢ addl a₁✝ = addl a₂✝ → a₁✝ = a₂✝
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≤ y
h : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

Tactic:
simp only [rpowIntegrand₀₁, mem_Ici] at hx h ⊢
    gcongr

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case inl
⊢ eulerMascheroniSeq' (0 + 1) < eulerMascheroniSeq' 0

pp: case inr
n : ℕ
hn : n > 0
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n

Tactic:
· simp [eulerMascheroniSeq']

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = 1 / ↑π * (↑π)⁻¹⁻¹

Tactic:
inv_inv,

Goal state after:
case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = 1 / ↑π * ↑π
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ ∃ μ,
    ∀ x ∈ Ici 0,
      IntegrableOn (fun t ↦ p.rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂μ

Tactic:
let C : ℝ≥0 := .mk (∫ t in Ioi 0, rpowIntegrand₀₁ p t 1)⁻¹
    (by rw [inv_nonneg]; exact le_of_lt <| integral_rpowIntegrand₀₁_one_pos hp)
  refine ⟨C • volume, fun x hx => ⟨?_, ?_⟩⟩
  · unfold IntegrableOn
    rw [Measure.restrict_smul]
    exact Integrable.smul_measure_nnreal <| integrableOn_rpowIntegrand₀₁_Ioi hp hx
  · simp_rw [Measure.restrict_smul, integral_smul_nnreal_measure, rpow_eq_const_mul_integral hp hx,
      NNReal.smul_def, C, NNReal.coe_mk, smul_eq_mul]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun y ↦ y ^ s * rexp (-a * y ^ 2)) atTop (𝓝 0)

Tactic:
exact
    (rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg ha s).tendsto_zero_of_tendsto
      (tendsto_exp_atBot.comp <| tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr one_half_pos))

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ -↑(Nat.clog b ⌈(↑b ^ ↑n)⁻¹⁻¹⌉₊) = -↑n

Tactic:
inv_inv,

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
hb : 1 < b
n : ℕ
⊢ -↑(Nat.clog b ⌈↑b ^ ↑n⌉₊) = -↑n
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
⊢ x ∈ univ → x ∈ logb b '' Iio 0

Tactic:
_

Goal state after:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ x ∈ logb b '' Iio 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
⊢ y ∈ Ici (rexp a⁻¹) → x ≤ y → (fun x ↦ log x / x ^ a) y ≤ (fun x ↦ log x / x ^ a) x

Tactic:
_

Goal state after:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
⊢ x ≤ y → (fun x ↦ log x / x ^ a) y ≤ (fun x ↦ log x / x ^ a) x
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ
⊢ ∫ (x : X), f x ∂μ = ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ

Tactic:
by
  simp only [f.self_eq_nnrealPart_sub_nnrealPart_neg, Pi.sub_apply, integral_sub,
             integrable_of_nnreal]
  simp only [Function.comp_apply]

Goal state after: