mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m ≤ n
c : OrderedFinpartition m
x✝ : c ∈ Finset.univ
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×m]→L[𝕜] G :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ ContinuousOn (fun x i ↦ p x (c.partSize i)) s

Tactic:
· apply continuousOn_pi.2 (fun i ↦ ?_)
      have : (c.partSize i : WithTop ℕ∞) ≤ m := by
        exact_mod_cast OrderedFinpartition.partSize_le c i
      exact hf.cont _ (this.trans hm)

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : ∃ i < a, ∀ ⦃x : ℝ⦄, x ∈ Ioo i a → deriv f x ∈ Iic (-1)
f' : ℝ → ℝ := f ∘ Neg.neg
⊢ ∃ i, -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x

Tactic:
obtain ⟨b, hb₁, hb₂⟩ := hf

Goal state after:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
⊢ ∃ i, -a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo (-a) i → deriv f' x = (-deriv f ∘ Neg.neg) x
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C✝ C₁ C₂ C : ConvexCone R G
h₁ : C.Pointed
h₂ : C.Salient
a b : G
ab : a ≤ b
ba : b ≤ a
h : ¬a = b
h' : b - a ≠ 0
H : a - b ∉ C
⊢ False

Tactic:
exact H ba

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

Goal state before:
pp: case hf₀'
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ HasDerivAt (↑expPartialHomeomorph) y (↑expPartialHomeomorph.symm y)

pp: case hf
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n (↑expPartialHomeomorph) (↑expPartialHomeomorph.symm y)

Tactic:
· convert! hasDerivAt_exp (log y)
      rw [exp_log hy]

Goal state after:
case hf
n : ℕ∞ω
x : ℝ
hx : x ≠ 0
y : ℝ
hy : 0 < y
⊢ ContDiffAt ℝ n (↑expPartialHomeomorph) (↑expPartialHomeomorph.symm y)
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
⊢ (r * r⁻¹) • x - -r • y ∈ s

Tactic:
mul_inv_cancel₀ hr.ne,

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
⊢ 1 • x - -r • y ∈ s
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_2.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : r * c ≤ r * r⁻¹ * ↑f ⟨x, hx⟩
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩

Tactic:
mul_inv_cancel₀ hr.ne,

Goal state after:
case refine_2.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : r < 0
this : r * c ≤ 1 * ↑f ⟨x, hx⟩
⊢ (RingHom.id ℝ) r • c ≤ ↑f ⟨x, hx⟩
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : r ≤ 0
⊢ r * gauge s x ≤ ‖x‖

pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ r * gauge s x ≤ ‖x‖

Tactic:
· exact (mul_nonpos_of_nonpos_of_nonneg hr <| gauge_nonneg _).trans (norm_nonneg _)

Goal state after:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ r * gauge s x ≤ ‖x‖
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
x : E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
⊢ ∃ f, f ≠ 0 ∧ ∀ a ∈ A, f a ≤ f x

Tactic:
by
  obtain ⟨f, u, hfne, hA', hx'⟩ :=
    geometric_hahn_banach_of_nonempty_interior hA (convex_singleton x)
      (disjoint_singleton_right.2 hxA) hAint (singleton_nonempty x)
  exact ⟨f, hfne, fun a ha => (hA' a ha).trans (hx' x (mem_singleton _))⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this✝ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
m : ℝ
xm : m ∈ Ioi x
hm : Ico x m ⊆ {x_1 | (fun x_2 ↦ ‖f x_2 - f x - (x_2 - x) • derivWithin f (Ici x) x‖ ≤ ε / 2 * ‖x_2 - x‖) x_1}
r : ℝ
hr : r ∈ Ioo 0 (m - x)
this : r ∈ Ioc (r / 2) r
y : ℝ
hy : y ∈ Icc x (x + r)
z : ℝ
hz : z ∈ Icc x (x + r)
⊢ x + r < m

Tactic:
linarith [hr.2]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
inst✝ : Zero X
f : X → R
g : C(X, R)₀
hf : f 0 ≠ 0
⊢ mkD f g = g

Tactic:
simp only [mkD, not_and_of_not_right _ hf, ↓reduceDIte]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case neg
X : Type u_1
inst✝⁴ : MeasurableSpace X
μ : Measure X
A : Type u_8
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : ¬CompleteSpace A
⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ

Tactic:
simp [integral, hA]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case neg
X : Type u_1
inst✝⁴ : MeasurableSpace X
μ : Measure X
A : Type u_8
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
f : X → A
hf : Integrable f μ
c : A
hA : ¬CompleteSpace A
⊢ ∫ (x : X), f x * c ∂μ = (∫ (x : X), f x ∂μ) * c

Tactic:
simp [integral, hA]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_2.hg
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
u u' : X → E
a✝ : Disjoint (Function.support u) (Function.support u')
u_int : Integrable u (μ.withDensity fun x ↦ ↑(f x))
u'_int : Integrable u' (μ.withDensity fun x ↦ ↑(f x))
h : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
h' : (∫ (x : X), u' x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u' x ∂μ
⊢ Integrable (fun x ↦ f x • u' x) μ

Tactic:
exact (integrable_withDensity_iff_integrable_smul f_meas).1 u'_int

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case inr
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
⊢ IntervalIntegrable (fun x ↦ f (c * x)) volume (a / c) (b / c)

Tactic:
intervalIntegrable_iff' h'

Goal state after:
case inr
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntegrableOn f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
⊢ IntegrableOn (fun x ↦ f (c * x)) [[a / c, b / c]] volume
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
⊢ StronglyMeasurable fun x ↦ derivWithin f (Ioi x) x

Tactic:
simpa [derivWithin_Ioi_eq_Ici] using stronglyMeasurable_derivWithin_Ici f

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a✝ b✝ : ℝ
inst✝ : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntervalIntegrable (fun x ↦ f (x + c)) volume (a - c) (b - c)

Tactic:
intervalIntegrable_iff' h'

Goal state after:
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a✝ b✝ : ℝ
inst✝ : PseudoMetrizableSpace ε
c a b : ℝ
hf : IntegrableOn f [[a, b]] volume
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntegrableOn (fun x ↦ f (x + c)) [[a - c, b - c]] volume
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
⊢ ∫ (x : ℝ) in a..b, f x + g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
by
  simp only [intervalIntegral_eq_integral_uIoc, integral_add hf.def' hg.def', smul_add]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntegrableOn f (Icc a b) μ
h : a ≤ b
x : ℝ
x_in : x ∈ Icc a b
⊢ ∫ (t : ℝ) in Ioc a x, f t ∂μ = ∫ (t : ℝ) in a..x, f t ∂μ

Tactic:
simp_rw [integral_of_le x_in.1]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᵐ[μ.restrict (Ι a b)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
this : ∫ (x : ℝ) in a..b, f x ∂μ ≤ 0
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Tactic:
simp only [this.not_gt, hba.not_gt, false_and]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Floor

Goal state before:
pp: case calc_1
K : Type u_1
inst✝³ : Ring K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a * c ^ n| ≤ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n

Tactic:
abs_mul,

Goal state after:
case calc_1
K : Type u_1
inst✝³ : Ring K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ |a| * |c ^ n| ≤ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n
Module: Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
⊢ ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
        (integral (I.face i) ⊥ (f ∘ i.insertNth (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ i.insertNth (I.lower i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j, (I.upper j - I.lower j)

Tactic:
set e : ℝ → (Fin n → ℝ) → (Fin (n + 1) → ℝ) := i.insertNth (α := fun _ ↦ ℝ)

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
n : ℕ
inst✝ : CompleteSpace E
I : Box (Fin (n + 1))
i : Fin (n + 1)
f : (Fin (n + 1) → ℝ) → E
f' : (Fin (n + 1) → ℝ) →L[ℝ] E
hfc : ContinuousOn f (Box.Icc I)
x : Fin (n + 1) → ℝ
hxI : x ∈ Box.Icc I
a : E
ε : ℝ
h0 : 0 < ε
hε : ∀ y ∈ Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖
c : ℝ≥0
hc : I.distortion ≤ c
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
⊢ ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
        (integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
          integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ ≤
    2 * ε * ↑c * ∏ j, (I.upper j - I.lower j)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t₁ t₂ : ℝ
hf : Periodic f T
⊢ IntervalIntegrable f volume t₁ (t₁ + T) ↔ IntervalIntegrable f volume t₂ (t₂ + T)

Tactic:
by
  wlog hT : T ≠ 0
  · simp_all
  exact ⟨(hf.intervalIntegrable hT · t₂ (t₂ + T)), (hf.intervalIntegrable hT · t₁ (t₁ + T))⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case mp
c w : ℂ
R : ℝ
n : ℤ
⊢ CircleIntegrable (fun z ↦ (z - w) ^ n) c R → R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|

pp: case mpr
c w : ℂ
R : ℝ
n : ℤ
⊢ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R| → CircleIntegrable (fun z ↦ (z - w) ^ n) c R

Tactic:
· intro h; contrapose! h; rcases h with ⟨hR, hn, hw⟩
    simp only [circleIntegrable_iff R, deriv_circleMap]
    rw [← image_circleMap_Ioc] at hw; rcases hw with ⟨θ, hθ, rfl⟩
    replace hθ : θ ∈ [[0, 2 * π]] := Icc_subset_uIcc (Ioc_subset_Icc_self hθ)
    refine not_intervalIntegrable_of_sub_inv_isBigO_punctured ?_ Real.two_pi_pos.ne hθ
    set f : ℝ → ℂ := fun θ' => circleMap c R θ' - circleMap c R θ
    have : ∀ᶠ θ' in 𝓝[≠] θ, f θ' ∈ ball (0 : ℂ) 1 \ {0} := by
      suffices ∀ᶠ z in 𝓝[≠] circleMap c R θ, z - circleMap c R θ ∈ ball (0 : ℂ) 1 \ {0} from
        ((differentiable_circleMap c R θ).hasDerivAt.tendsto_nhdsNE
          (deriv_circleMap_ne_zero hR)).eventually this
      filter_upwards [self_mem_nhdsWithin, mem_nhdsWithin_of_mem_nhds (ball_mem_nhds _ zero_lt_one)]
      simp_all [dist_eq, sub_eq_zero]
    refine (((hasDerivAt_circleMap c R θ).isBigO_sub.mono inf_le_left).inv_rev
      (this.mono fun θ' h₁ h₂ => absurd h₂ h₁.2)).trans ?_
    refine IsBigO.of_bound |R|⁻¹ (this.mono fun θ' hθ' => ?_)
    set x := ‖f θ'‖
    suffices x⁻¹ ≤ x ^ n by
      simp only [smul_eq_mul, norm_mul,
        norm_inv, norm_I, mul_one]
      simpa only [norm_circleMap_zero, norm_zpow, Ne, abs_eq_zero.not.2 hR, not_false_iff,
        inv_mul_cancel_left₀] using this
    have : x ∈ Ioo (0 : ℝ) 1 := by simpa [x, and_comm] using hθ'
    rw [← zpow_neg_one]
    refine (zpow_right_strictAnti₀ this.1 this.2).le_iff_ge.2 (Int.lt_add_one_iff.1 ?_); exact hn

Goal state after:
case mpr
c w : ℂ
R : ℝ
n : ℤ
⊢ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R| → CircleIntegrable (fun z ↦ (z - w) ^ n) c R
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f f' : ℂ → E
c : ℂ
R : ℝ
h : ∀ z ∈ sphere c |R|, HasDerivWithinAt f (f' z) (sphere c |R|) z
⊢ ∮ (z : ℂ) in C(c, R), f' z = 0

Tactic:
by_cases hi : CircleIntegrable f' c R
  · rw [← sub_eq_zero.2 ((periodic_circleMap c R).comp f).eq]
    refine intervalIntegral.integral_eq_sub_of_hasDerivAt (fun θ _ => ?_) hi.out
    exact (h _ (circleMap_mem_sphere' _ _ _)).scomp_hasDerivAt θ
      (differentiable_circleMap _ _ _).hasDerivAt (circleMap_mem_sphere' _ _)
  · exact integral_undef hi

Goal state after:
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case neg
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

Tactic:
have hd : ∀ z, z ≠ w ∨ -1 ≤ n →
      HasDerivAt (fun z => (z - w) ^ (n + 1) / (n + 1)) ((z - w) ^ n) z := by
    intro z hne
    convert!
      ((hasDerivAt_zpow (n + 1) _ (hne.imp _ _)).comp z ((hasDerivAt_id z).sub_const w)).div_const
        _ using 1
    · have hn' : (n + 1 : ℂ) ≠ 0 := by
        rwa [Ne, ← eq_neg_iff_add_eq_zero, ← Int.cast_one, ← Int.cast_neg, Int.cast_inj]
      simp [mul_div_cancel_left₀ _ hn']
    exacts [sub_ne_zero.2, neg_le_iff_add_nonneg.1]

Goal state after:
case neg
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z ↦ (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: case neg
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| → -1 ≤ n
hd : ∀ (z : ℂ), z ≠ w ∨ -1 ≤ n → HasDerivAt (fun z ↦ (z - w) ^ (n + 1) / (↑n + 1)) ((z - w) ^ n) z
z : ℂ
hz : z ∈ sphere c |R|
⊢ z ≠ w ∨ -1 ≤ n

Tactic:
exact (ne_or_eq z w).imp_right fun (h : z = w) => H <| h ▸ hz

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : β → E
hf : Integrable (fun x ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
⊢ Integrable f ν

Tactic:
rcases hf with ⟨hf_meas, hf_fin⟩

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : β → E
hμ : μ ≠ 0
hf_meas : AEStronglyMeasurable (fun x ↦ f x.2) (μ.prod ν)
hf_fin : HasFiniteIntegral (fun x ↦ f x.2) (μ.prod ν)
⊢ Integrable f ν
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case pos.h_ind
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
hE : CompleteSpace E
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s < ∞
⊢ ∫ (x : α × β) in s, c ∂μ.prod ν = ∫ (x : α), ∫ (y : β), (Prod.mk x ⁻¹' s).indicator ((fun x ↦ c) ∘ Prod.mk x) y ∂ν ∂μ

Tactic:
Function.comp_def,

Goal state after:
case pos.h_ind
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
hE : CompleteSpace E
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s < ∞
⊢ ∫ (x : α × β) in s, c ∂μ.prod ν = ∫ (x : α), ∫ (y : β), (Prod.mk x ⁻¹' s).indicator (fun x ↦ c) y ∂ν ∂μ
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ ∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

Tactic:
rw [← integral_prod_swap f]; exact integral_prod _ hf.swap

Goal state after:
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z ↦ (z - c)⁻¹) (sphere c r)
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖ =
    ‖∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z - (z - c)⁻¹ • y‖

Tactic:
circleIntegral.integral_sub

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z ↦ (z - c)⁻¹) (sphere c r)
⊢ ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖ =
    ‖(∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) - ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • y‖

case hf
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z ↦ (z - c)⁻¹) (sphere c r)
⊢ CircleIntegrable (fun z ↦ (z - c)⁻¹ • f z) c r

case hg
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → E
y : E
s : Set ℂ
hs : s.Countable
hc : ContinuousOn f (closedBall c R \ {c})
hd : ∀ z ∈ (ball c R \ {c}) \ s, DifferentiableAt ℂ f z
hy : Tendsto f (𝓝[≠] c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
δ : ℝ
δ0 : δ > 0
hδ : ∀ z ∈ closedBall c δ \ {c}, dist (f z) y < ε / (2 * π)
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R \ {c}
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
hc' : ContinuousOn (fun z ↦ (z - c)⁻¹) (sphere c r)
⊢ CircleIntegrable (fun z ↦ (z - c)⁻¹ • y) c r
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x, (Multiset.map (fun x ↦ X (e x)) ↑x).prod = ∑ s, (Multiset.map X ↑s).prod

Tactic:
apply Fintype.sum_equiv (equivCongr e)

Goal state after:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : Fintype σ
inst✝² : Fintype τ
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
e : σ ≃ τ
⊢ ∀ (x : Sym σ n), (Multiset.map (fun x ↦ X (e x)) ↑x).prod = (Multiset.map X ↑((equivCongr e) x)).prod
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
A : Type u_2
inst✝³ : Field A
inst✝² : CharZero A
inst✝¹ : NumberField K
inst✝ : IsAlgClosed A
⊢ Nonempty (K →+* A)

Tactic:
rw [← Fintype.card_pos_iff, NumberField.Embeddings.card K A]
  exact Module.finrank_pos

Goal state after: