mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜₁ E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜₂ F
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h : ∀ (x : E) (y : F⋆), y (A x) = y (B x)
⊢ ∀ (x : E), (ContinuousLinearMap.coeLM 𝕜₂).flip (A x) = (ContinuousLinearMap.coeLM 𝕜₂).flip (B x)

Tactic:
LinearMap.ext_iff

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜₁ E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜₂ F
H : SeparatingDual 𝕜₂ F
A B : E →SWOT[σ] F
h : ∀ (x : E) (y : F⋆), y (A x) = y (B x)
⊢ ∀ (x : E) (x_1 : F →L[𝕜₂] 𝕜₂),
    ((ContinuousLinearMap.coeLM 𝕜₂).flip (A x)) x_1 = ((ContinuousLinearMap.coeLM 𝕜₂).flip (B x)) x_1
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁ : Type u_5
𝕜₂ : Type u_6
E : Type u_9
F : Type u_10
inst✝⁷ : NormedField 𝕜₁
inst✝⁶ : NormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜₁ E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜₂ F
f : E →SWOT[σ₁₂] F
⊢ (ContinuousLinearMapWOT.id 𝕜₂ F).comp f = f

Tactic:
by simp [comp]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₂ : Type u_6
𝕜₃ : Type u_7
F : Type u_10
G : Type u_11
inst✝⁷ : NormedField 𝕜₂
inst✝⁶ : NormedField 𝕜₃
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : Module 𝕜₂ F
inst✝² : AddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : Module 𝕜₃ G
g : F →SWOT[σ₂₃] G
⊢ g.comp (ContinuousLinearMapWOT.id 𝕜₂ F) = g

Tactic:
by simp [comp]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
⊢ x = 0 ∨ y = 0

Tactic:
have : ‖x‖ * ‖y‖ = 0 := by simpa [hx] using (o.norm_kahler x y).symm

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : (o.kahler x) y = 0
this : ‖x‖ * ‖y‖ = 0
⊢ x = 0 ∨ y = 0
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x ↦ ↑(a * x) ^ (s - 1) • f (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t ↦ ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ ↑a ^ (s - 1) ≠ 0

Tactic:
Ne,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x ↦ ↑(a * x) ^ (s - 1) • f (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t ↦ ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t ↦ ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t ↦ ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ ¬↑a ^ (s - 1) = 0
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁✝ : Type u_1
𝕜₂✝ : Type u_2
inst✝³¹ : NormedField 𝕜₁✝
inst✝³⁰ : NormedField 𝕜₂✝
σ : 𝕜₁✝ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
inst✝²⁹ : AddCommGroup E✝
inst✝²⁸ : TopologicalSpace E✝
inst✝²⁷ : Module 𝕜₁✝ E✝
inst✝²⁶ : AddCommGroup F✝
inst✝²⁵ : TopologicalSpace F✝
inst✝²⁴ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : AddCommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
f : E →SWOT[σ₁₂] F
⊢ ∀ (x y : F →SWOT[σ₂₃] G), (x + y).comp f = x.comp f + y.comp f

Tactic:
by simp [comp]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ MellinConvergent (fun t ↦ f (a * t)) s ↔ MellinConvergent f s

Tactic:
have := integrableOn_Ioi_comp_mul_left_iff (fun t : ℝ => (t : ℂ) ^ (s - 1) • f t) 0 ha
  rw [mul_zero] at this
  have h1 : EqOn (fun t : ℝ => (↑(a * t) : ℂ) ^ (s - 1) • f (a * t))
      ((a : ℂ) ^ (s - 1) • fun t : ℝ => (t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0) := fun t ht ↦ by
    simp only [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), mul_smul, Pi.smul_apply]
  have h2 : (a : ℂ) ^ (s - 1) ≠ 0 := by
    rw [Ne, cpow_eq_zero_iff, not_and_or, ofReal_eq_zero]
    exact Or.inl ha.ne'
  rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi,
    IntegrableOn, IntegrableOn, integrable_smul_iff h2]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁✝ : Type u_1
𝕜₂✝ : Type u_2
inst✝³¹ : NormedField 𝕜₁✝
inst✝³⁰ : NormedField 𝕜₂✝
σ : 𝕜₁✝ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
inst✝²⁹ : AddCommGroup E✝
inst✝²⁸ : TopologicalSpace E✝
inst✝²⁷ : Module 𝕜₁✝ E✝
inst✝²⁶ : AddCommGroup F✝
inst✝²⁵ : TopologicalSpace F✝
inst✝²⁴ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²³ : NormedField 𝕜₁
inst✝²² : NormedField 𝕜₂
inst✝²¹ : NormedField 𝕜₃
inst✝²⁰ : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁸ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁶ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : TopologicalSpace E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : AddCommGroup G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : AddCommGroup H
inst✝⁵ : TopologicalSpace H
inst✝⁴ : Module 𝕜₄ H
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousConstSMul 𝕜₂ F
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜₃ G
f : E →SWOT[σ₁₂] F
⊢ ∀ (m : 𝕜₃) (x : F →SWOT[σ₂₃] G), (m • x).comp f = (RingHom.id 𝕜₃) m • x.comp f

Tactic:
by simp [comp]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁✝ : Type u_1
𝕜₂✝ : Type u_2
inst✝³³ : NormedField 𝕜₁✝
inst✝³² : NormedField 𝕜₂✝
σ : 𝕜₁✝ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
inst✝³¹ : AddCommGroup E✝
inst✝³⁰ : TopologicalSpace E✝
inst✝²⁹ : Module 𝕜₁✝ E✝
inst✝²⁸ : AddCommGroup F✝
inst✝²⁷ : TopologicalSpace F✝
inst✝²⁶ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²⁵ : NormedField 𝕜₁
inst✝²⁴ : NormedField 𝕜₂
inst✝²³ : NormedField 𝕜₃
inst✝²² : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝²¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝²⁰ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : TopologicalSpace E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : TopologicalSpace F
inst✝¹² : Module 𝕜₂ F
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : Module 𝕜₃ G
inst✝⁸ : AddCommGroup H
inst✝⁷ : TopologicalSpace H
inst✝⁶ : Module 𝕜₄ H
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
⊢ ∀ (x y : E →SWOT[σ₁₂] F), g.comp (x + y) = g.comp x + g.comp y

Tactic:
by simp [comp]

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.WeakOperatorTopology

Goal state before:
pp: 𝕜₁✝ : Type u_1
𝕜₂✝ : Type u_2
inst✝³³ : NormedField 𝕜₁✝
inst✝³² : NormedField 𝕜₂✝
σ : 𝕜₁✝ →+* 𝕜₂✝
E✝ : Type u_3
F✝ : Type u_4
inst✝³¹ : AddCommGroup E✝
inst✝³⁰ : TopologicalSpace E✝
inst✝²⁹ : Module 𝕜₁✝ E✝
inst✝²⁸ : AddCommGroup F✝
inst✝²⁷ : TopologicalSpace F✝
inst✝²⁶ : Module 𝕜₂✝ F✝
𝕜₁ : Type u_5
𝕜₂ : Type u_6
𝕜₃ : Type u_7
𝕜₄ : Type u_8
E : Type u_9
F : Type u_10
G : Type u_11
H : Type u_12
inst✝²⁵ : NormedField 𝕜₁
inst✝²⁴ : NormedField 𝕜₂
inst✝²³ : NormedField 𝕜₃
inst✝²² : NormedField 𝕜₄
σ₁₂ : 𝕜₁ →+* 𝕜₂
σ₁₃ : 𝕜₁ →+* 𝕜₃
σ₁₄ : 𝕜₁ →+* 𝕜₄
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₃₄ : 𝕜₃ →+* 𝕜₄
inst✝²¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝²⁰ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹⁹ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁸ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : TopologicalSpace E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : TopologicalSpace F
inst✝¹² : Module 𝕜₂ F
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : Module 𝕜₃ G
inst✝⁸ : AddCommGroup H
inst✝⁷ : TopologicalSpace H
inst✝⁶ : Module 𝕜₄ H
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousConstSMul 𝕜₂ F
inst✝³ : IsTopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomIsometric σ₂₃
g : F →SWOT[σ₂₃] G
⊢ ∀ (m : 𝕜₂) (x : E →SWOT[σ₁₂] F), g.comp (m • x) = σ₂₃ m • g.comp x

Tactic:
by simp [comp]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑a ^ (s - 1) ≠ 0

Tactic:
Ne,

Goal state after:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : t ∈ Ioi 0
⊢ ¬↑a ^ (s - 1) = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case succ
n : ℕ
ih : logTaylor n 0 = 0
⊢ logTaylor (n + 1) 0 = 0

Tactic:
simpa [logTaylor_succ, ih] using ne_or_eq n 0

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

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖↑t * z‖ ≤ ‖1 + ↑t * z‖

Tactic:
by
      rw [← norm_neg (t * z), ← sub_neg_eq_add]
      convert! norm_sub_norm_le 1 (-(t * z))
      exact norm_one.symm

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
hd' : ∀ᶠ (x : ℝ) in 𝓝 0, x ∈ Ioi 0 → ‖f x‖ ≤ d * ‖x ^ (-b)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume

Tactic:
Metric.eventually_nhds_iff,

Goal state after:
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
hd' : ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ ∃ c, 0 < c ∧ IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c) volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ↑s ≠ ↑(-↑m)

Tactic:
Ne,

Goal state after:
s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ¬↑s = ↑(-↑m)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
⊢ ENNReal.ofReal (1 / c) ≠ 0

Tactic:
Ne,

Goal state after:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
⊢ ¬ENNReal.ofReal (1 / c) = 0
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun x ↦ ↑(x * g x)) atTop (𝓝 ↑t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ Tendsto (fun x ↦ ↑(x * log (1 + g x))) atTop (𝓝 ↑t)

Tactic:
push_cast at hg ⊢

Goal state after:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
⊢ Tendsto (fun x ↦ ↑x * ↑(log (1 + g x))) atTop (𝓝 ↑t)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun x ↦ ↑(x * g x)) atTop (𝓝 ↑t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ Tendsto (fun x ↦ ↑((1 + g x) ^ x)) atTop (𝓝 ↑(rexp t))

Tactic:
push_cast at hg ⊢

Goal state after:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun x ↦ ↑x * ↑(g x)) atTop (𝓝 ↑t)
⊢ Tendsto (fun x ↦ ↑((1 + g x) ^ x)) atTop (𝓝 (Complex.exp ↑t))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hg
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ ContinuousOn (fun x ↦ (1 - ↑x) ^ (v - 1)) (uIcc 0 (1 / 2))

Tactic:
apply continuousOn_of_forall_continuousAt

Goal state after:
case hg
u : ℂ
hu : 0 < u.re
v : ℂ
⊢ ∀ x ∈ uIcc 0 (1 / 2), ContinuousAt (fun x ↦ (1 - ↑x) ^ (v - 1)) x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
⊢ f ↑(m + 1) = f 1 + log ↑(m + 1 - 1)!

Tactic:
have A : 0 < (m : ℝ) := Nat.cast_pos.2 hm

Goal state after:
f : ℝ → ℝ
n : ℕ
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : n ≠ 0
m : ℕ
hm : 1 ≤ m
IH : f ↑m = f 1 + log ↑(m - 1)!
A : 0 < ↑m
⊢ f ↑(m + 1) = f 1 + log ↑(m + 1 - 1)!
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hn : 2 ≤ n
hx : 0 < x
⊢ f ↑n + x * log (↑n - 1) ≤ f (↑n + x)

Tactic:
have npos : 0 < (n : ℝ) - 1 := by rw [← Nat.cast_one, sub_pos, Nat.cast_lt]; lia
  have c :=
    (convexOn_iff_slope_mono_adjacent.mp <| hf_conv).2 npos (by linarith : 0 < (n : ℝ) + x)
      (by linarith : (n : ℝ) - 1 < (n : ℝ)) (by linarith)
  rw [add_sub_cancel_left, sub_sub_cancel, div_one] at c
  have : f (↑n - 1) = f n - log (↑n - 1) := by
    rw [eq_sub_iff_add_eq, ← hf_feq npos, sub_add_cancel]
  rwa [this, le_div_iff₀ hx, sub_sub_cancel, le_sub_iff_add_le, mul_comm _ x, add_comm] at c

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
F : ι → 𝕜 → 𝕜'
hF : (mulSupport F).Finite
h : ∀ (i : ι), Meromorphic (F i)
h' : ∀ (i : ι) (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤
⊢ logDeriv (∏ᶠ (i : ι), F i) =ᶠ[codiscrete 𝕜] ∑ᶠ (i : ι), logDeriv (F i)

Tactic:
apply MeromorphicOn.logDeriv_finprod_eventuallyEq hF (fun i ↦ meromorphicOn_univ.mpr (h i))

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
ι : Type u_3
F : ι → 𝕜 → 𝕜'
hF : (mulSupport F).Finite
h : ∀ (i : ι), Meromorphic (F i)
h' : ∀ (i : ι) (x : 𝕜), meromorphicOrderAt (F i) x ≠ ⊤
⊢ ∀ (i : ι), ∀ x ∈ univ, meromorphicOrderAt (F i) x ≠ ⊤
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case hg
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
F : ℝ → ℂ := fun x ↦ ↑x ^ u * (1 - ↑x) ^ v
hu' : 0 < (u + 1).re
hv' : 0 < (v + 1).re
hc : ContinuousOn F (Icc 0 1)
hder : ∀ x ∈ Ioo 0 1, HasDerivAt F (u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) x
h_int : IntervalIntegrable (fun x ↦ u * (↑x ^ (u - 1) * (1 - ↑x) ^ v) - v * (↑x ^ u * (1 - ↑x) ^ (v - 1))) volume 0 1
int_ev : ∫ (y : ℝ) in 0..1, u * (↑y ^ (u - 1) * (1 - ↑y) ^ v) - v * (↑y ^ u * (1 - ↑y) ^ (v - 1)) = 0
hF0 : F 0 = 0
hF1 : F 1 = 0
⊢ IntervalIntegrable (fun y ↦ v * (↑y ^ u * (1 - ↑y) ^ (v - 1))) volume 0 1

Tactic:
apply IntervalIntegrable.const_mul
    convert! betaIntegral_convergent hu' hv; ring

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ hd.toFinset, F i y ≠ 0
h₀ : ∏ᶠ (i : ι), F i ^ d i = ∏ i ∈ hd.toFinset, F i ^ d i
hsub : (support fun i ↦ d i • logDeriv (F i) y) ⊆ ↑hd.toFinset
⊢ logDeriv (∏ᶠ (i : ι), F i ^ d i) y = logDeriv (fun z ↦ ∏ i ∈ hd.toFinset, (F i ^ d i) z) y

Tactic:
h₀,

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
hA : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
hN : ∀ᶠ (y : 𝕜) in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0
y : 𝕜
h₁y : ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y
h₂y : ∀ i ∈ hd.toFinset, F i y ≠ 0
h₀ : ∏ᶠ (i : ι), F i ^ d i = ∏ i ∈ hd.toFinset, F i ^ d i
hsub : (support fun i ↦ d i • logDeriv (F i) y) ⊆ ↑hd.toFinset
⊢ logDeriv (∏ i ∈ hd.toFinset, F i ^ d i) y = logDeriv (fun z ↦ ∏ i ∈ hd.toFinset, (F i ^ d i) z) y
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case inr.inl
x : ℝ
hx : x ∈ Icc 1 2
hmin : IsMinOn Γ (Icc 1 2) x
h1 : Γ (3 / 2) < Γ 1
h2 : Γ (3 / 2) < Γ 2
h3half : Γ x ≤ Γ (3 / 2)
y : ℝ
x✝ : y ∈ Ioi 0
hy : y ∈ Icc 1 2
⊢ y ∈ {x_1 | (fun x_2 ↦ Γ x ≤ Γ x_2) x_1}

Tactic:
exact hmin hy

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : LinearOrder k
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : AddTorsor V P
inst✝⁵ : TopologicalSpace V
inst✝⁴ : TopologicalSpace k
inst✝³ : OrderTopology k
inst✝² : IsStrictOrderedRing k
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul k V
s : Set P
⊢ 0 ∈ asymptoticCone k s ↔ s.Nonempty

Tactic:
refine ⟨Function.mtr ?_, fun _ => ?_⟩
  · simp +contextual [Set.not_nonempty_iff_eq_empty]
  · simpa [mem_asymptoticCone_iff]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.ContinuousAffineMap

Goal state before:

Tactic:
‖f.comp g 0‖ = ‖f (g 0)‖ := by simp
      _ = ‖f.contLinear (g 0) + f 0‖ := by rw [f.decomp]; simp
      _ ≤ ‖f.contLinear‖ * ‖g 0‖ + ‖f 0‖ := by grw [norm_add_le, f.contLinear.le_opNorm]
      _ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ := by grw [f.norm_contLinear_le, g.norm_image_zero_le]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.MazurUlam

Goal state before:
pp: E : Type u_1
PE : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MetricSpace PE
inst✝ : NormedAddTorsor E PE
x y : PE
z : PE := midpoint ℝ x y
s : Set (PE ≃ᵢ PE) := {e | e x = x ∧ e y = y}
this : Nonempty ↑s
e : PE ≃ᵢ PE
hx : e x = x
right✝ : e y = y
⊢ dist (e z) x + dist x z = dist (e x) (e z) + dist x z

Tactic:
by rw [hx, dist_comm]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: z : ℂ
pi_ne : ↑π ≠ 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

Tactic:
by_cases hs : sin (↑π * z) = 0

Goal state after:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
hs : sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)

case neg
z : ℂ
pi_ne : ↑π ≠ 0
hs : ¬sin (↑π * z) = 0
⊢ Gamma z * Gamma (1 - z) = ↑π / sin (↑π * z)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case pos
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : -z * ↑π = ↑k * ↑π
⊢ Gamma z * Gamma (1 - z) = 0

Tactic:
mul_eq_mul_right_iff,

Goal state after:
case pos
z : ℂ
pi_ne : ↑π ≠ 0
k : ℤ
hk : -z = ↑k ∨ ↑π = 0
⊢ Gamma z * Gamma (1 - z) = 0
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ inl (exp (inr m).fst) + inr (exp (inr m).fst • m) = 1 + inr m

pp: case hx
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ MulOpposite.op (inr m).fst • (inr m).snd = (inr m).fst • (inr m).snd

Tactic:
fst_inr,

Goal state after:
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ inl (exp 0) + inr (exp 0 • m) = 1 + inr m

case hx
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ MulOpposite.op (inr m).fst • (inr m).snd = (inr m).fst • (inr m).snd
Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

Goal state before:
pp: case hx
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ MulOpposite.op (inr m).fst • m = (inr m).fst • m

Tactic:
fst_inr,

Goal state after:
case hx
R : Type u_3
M : Type u_4
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : IsTopologicalAddGroup M
inst✝⁵ : ContinuousSMul R M
inst✝⁴ : ContinuousSMul Rᵐᵒᵖ M
inst✝³ : Algebra ℚ R
inst✝² : Module ℚ M
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ MulOpposite.op 0 • m = 0 • m