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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s✝ t✝ : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : StrongDual 𝕜 E
s t : ℝ
hs : ∀ a ∈ t✝, re (f a) < s
st : s < t
ht : ∀ b ∈ s✝, t < re (f b)
⊢ ∀ b ∈ t✝, -s < re ((-f) b)

Tactic:
simpa using hs

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

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ∫ (x : X), ↑(re (f x)) ∂μ + (∫ (x : X), ↑(im (f x)) ∂μ) * I = ∫ (x : X), f x ∂μ

Tactic:
by
  rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add]
  · congr
    ext1 x
    rw [smul_eq_mul, mul_comm, RCLike.re_add_im]
  · exact hf.re.ofReal
  · exact hf.im.ofReal.smul (𝕜 := 𝕜) (β := 𝕜) RCLike.I

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

Goal state before:
pp: case pos.refine_2
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))
⊢ ∀ ⦃f_1 g : X → E⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Integrable f_1 (μ.withDensity fun x ↦ ↑(f x)) →
        Integrable g (μ.withDensity fun x ↦ ↑(f x)) →
          (∫ (x : X), f_1 x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • f_1 x ∂μ →
            (∫ (x : X), g x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • g x ∂μ →
              (∫ (x : X), (f_1 + g) x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • (f_1 + g) x ∂μ

Tactic:
intro u u' _ u_int u'_int h h'
    change
      (∫ x : X, u x + u' x ∂μ.withDensity fun x : X => ↑(f x)) = ∫ x : X, f x • (u x + u' x) ∂μ
    simp_rw [smul_add]
    rw [integral_add u_int u'_int, h, h', integral_add]
    · exact (integrable_withDensity_iff_integrable_smul f_meas).1 u_int
    · exact (integrable_withDensity_iff_integrable_smul f_meas).1 u'_int

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

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
inst✝ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b) μ

Tactic:
by
  rw [uIoc_eq_union, integrableOn_union, IntervalIntegrable]

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

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst✝ : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hp : m ≤ p
IH : (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a p)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ p ∈ Ico m (p + 1)

Tactic:
simp [hp]

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

Goal state before:
pp: case pos.h_lim
ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : Countable ι
f : ι → C(ℝ, E)
hf_sum : Summable fun i ↦ ‖ContinuousMap.restrict (↑{ carrier := [[a, b]], isCompact' := ⋯ }) (f i)‖
hE : CompleteSpace E
⊢ ∀ᵐ (t : ℝ), t ∈ Ι a b → HasSum (fun n ↦ (f n) t) (∑' (i : ι), (f i) t)

Tactic:
refine ae_of_all _ fun x hx => Summable.hasSum ?_
    let x : (⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ) := ⟨x, ⟨hx.1.le, hx.2⟩⟩
    have := hf_sum.of_norm
    simpa only [Compacts.coe_mk, ContinuousMap.restrict_apply]
      using ContinuousMap.summable_apply this x

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
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
⊢ Measurable fun x ↦ derivWithin f (Ici x) x

Tactic:
refine measurable_of_isClosed fun s hs => ?_

Goal state after:
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
f : ℝ → F
inst✝² : CompleteSpace F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
s : Set F
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ MeasurableSet ((fun x ↦ derivWithin f (Ici x) x) ⁻¹' s)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case pos.refine_3
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
t : ι
⊢ ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - μ.real (Ioc (u t) (v t)) • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
    ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)

Tactic:
simp_rw [intervalIntegral]

Goal state after:
case pos.refine_3
ι : Type u_1
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst✝¹ : l'.IsMeasurablyGenerated
inst✝ : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  (fun i ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) =o[lt] fun i ↦ μ.real (Ioc (u i) (v i))
B :
  (fun i ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) =o[lt] fun i ↦ μ.real (Ioc (v i) (u i))
t : ι
⊢ ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - μ.real (Ioc (u t) (v t)) • c -
      (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
    ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - ∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ -
      (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: case pos
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 1 • ∫ (x : ℝ) in Ι a b, f x ∂μ

Tactic:
simp only [integral_of_le h, uIoc_of_le h, one_smul]

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

Goal state before:
pp: E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝ : FTCFilter a (𝓝[s] a) (𝓝[t] a)
hmeas : StronglyMeasurableAtFilter f (𝓝[t] a) volume
ha : Tendsto f (𝓝[t] a ⊓ ae volume) (𝓝 c)
⊢ HasDerivWithinAt (fun u ↦ ∫ (x : ℝ) in u..b, f x) (-c) s a

Tactic:
simp only [integral_symm b]
  exact (integral_hasDerivWithinAt_of_tendsto_ae_right hf.symm hmeas ha).neg

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
H : IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
⊢ IsOpen[instTopologicalSpaceProd] {p | p.2 ∈ B (f p.1) K r s t}

Tactic:
convert! H; ext p; simp [B]

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) μ
⊢ (fun x ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ

Tactic:
ext x

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntegrableOn f (Icc a b) μ
x : ℝ
⊢ ∫ (t : ℝ) in Icc a x, f t ∂μ = ∫ (t : ℝ) in Ioc a x, f t ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
uIoc_comm,

Goal state after:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᵐ[μ.restrict (Ι b a)] f
hfi : IntervalIntegrable f μ a b
hba : b ≤ a
⊢ 0 ≤ ∫ (x : ℝ) in Ioc b a, f x ∂μ
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
⊢ Tendsto (fun n ↦ a * c ^ n / ↑(n - d)!) atTop (𝓝 0)

Tactic:
rw [tendsto_order]
  constructor
  all_goals
    intro ε hε
    filter_upwards [eventually_mul_pow_lt_factorial_sub (a * ε⁻¹) c d] with n h
    rw [mul_right_comm, ← div_eq_mul_inv] at h
  · rw [div_lt_iff_of_neg hε] at h
    rwa [lt_div_iff₀' (Nat.cast_pos.mpr (Nat.factorial_pos _))]
  · rw [div_lt_iff₀ hε] at h
    rwa [div_lt_iff₀' (Nat.cast_pos.mpr (Nat.factorial_pos _))]

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
⊢ ENNReal.ofReal (min T (2 * (2 * ε))) ≤ ↑(Real.toNNReal 2) * ENNReal.ofReal (min T (2 * ε))

Tactic:
ENNReal.ofNNReal_toNNReal 2,

Goal state after:
T : ℝ
hT : Fact (0 < T)
ε : ℝ
x : AddCircle T
⊢ ENNReal.ofReal (min T (2 * (2 * ε))) ≤ ENNReal.ofReal 2 * ENNReal.ofReal (min T (2 * ε))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
h : Measurable ⇑(measurableEquivIoc T a)
s : Set ↑(Ioc a (a + T))
hs : MeasurableSet s
⊢ MeasurableSet (⇑(equivIoc T a) ⁻¹' s)

Tactic:
exact h hs

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

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
a : ℝ
h : Measurable ⇑(measurableEquivIoc T a)
s : Set ↑(Ioc a (a + T))
hs : MeasurableSet s
⊢ QuotientAddGroup.mk ⁻¹' ⇑(equivIoc T a) ⁻¹' s ∩ Ioc a (a + T) = Subtype.val '' s

Tactic:
ext x

Goal state after:
T : ℝ
hT : Fact (0 < T)
a : ℝ
h : Measurable ⇑(measurableEquivIoc T a)
s : Set ↑(Ioc a (a + T))
hs : MeasurableSet s
x : ℝ
⊢ x ∈ QuotientAddGroup.mk ⁻¹' ⇑(equivIoc T a) ⁻¹' s ∩ Ioc a (a + T) ↔ x ∈ Subtype.val '' s
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case hF_meas
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, AEStronglyMeasurable ((Ioi n).indicator f) μ

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
⊢ AEStronglyMeasurable ((Ioi a).indicator f) μ
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case h_bound
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Ioi n).indicator f a‖ ≤ (Ioi a₀).indicator (norm ∘ f) a

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
⊢ ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Ioi a).indicator f a_1‖ ≤ (Ioi a₀).indicator (norm ∘ f) a_1
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case hF_meas
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, AEStronglyMeasurable ((Iio n).indicator f) μ

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ AEStronglyMeasurable ((Iio a).indicator f) μ
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case h_bound
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Iio n).indicator f a‖ ≤ (Iio a₀).indicator (norm ∘ f) a

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
a : ℝ
ha : a ∈ Iic a₀
⊢ ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Iio a).indicator f a_1‖ ≤ (Iio a₀).indicator (norm ∘ f) a_1
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
ν : Measure β
p : ℝ≥0∞
f : β → ε
hf : MemLp f p ν
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : SFinite ν
⊢ MemLp (fun x ↦ f x.2) p (μ.prod ν)

Tactic:
have hf' : MemLp f p (μ .univ • ν) := hf.smul_measure (by simp)
  change MemLp (f ∘ Prod.snd) p (μ.prod ν)
  rw [← memLp_map_measure_iff ?_ (by fun_prop)]
  · simpa using hf'
  · simpa using hf'.1

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : SFinite μ
inst✝ : SFinite ν
f : β × α → X
hf : AEStronglyMeasurable f (ν.prod μ)
⊢ AEStronglyMeasurable (fun z ↦ f z.swap) (μ.prod ν)

Tactic:
rw [← prod_swap] at hf
  exact hf.comp_measurable measurable_swap

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

Goal state before:
pp: c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
this : ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹ = 2 * ↑π * I
⊢ HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹) (2 * ↑π * I)

Tactic:
refine this ▸ hasSum_single _ fun n hn => ?_

Goal state after:
c w : ℂ
R : ℝ
hw : w ∈ ball c R
hR : 0 < R
H : ∀ (n : ℕ), n ≠ 0 → ∮ (z : ℂ) in C(c, R), (z - c) ^ (-↑n - 1) = 0
this : ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ 0 * (z - c)⁻¹ = 2 * ↑π * I
n : ℕ
hn : n ≠ 0
⊢ ∮ (z : ℂ) in C(c, R), ((w - c) / (z - c)) ^ n * (z - c)⁻¹ = 0
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
⊢ ∀ ⦃a : σ →₀ ℕ⦄, a ∈ {∑ i ∈ s, Finsupp.single i 1} → a ∉ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support

Tactic:
rw [Finsupp.support_single _ one_ne_zero]

Goal state after:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
s t : Finset σ
hst : s ≠ t
⊢ ∀ ⦃a : σ →₀ ℕ⦄, a ∈ {∑ i ∈ s, Finsupp.single i 1} → a ∉ {∑ i ∈ t, Finsupp.single i 1}
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ (esymm σ R n).degrees = univ.val

Tactic:
have :
      (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i ∈ t, Finsupp.single i 1) = val := by
      funext
      simp

Goal state after:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (⇑Finsupp.toMultiset ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) = val
⊢ (esymm σ R n).degrees = univ.val
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case h
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
⊢ eval α (map (algebraMap F p.SplittingField) p) = 0

Tactic:
eval_rootOfSplits

Goal state after:
case h
F : Type u_1
inst✝¹ : Field F
p : F[X]
inst✝ : CharZero F
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
hp : p.degree ≠ 0
α : p.SplittingField := rootOfSplits ⋯ ⋯
hα : IsIntegral F α
⊢ 0 = 0
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {a : R}, a ≠ 0 → f (C a * X).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (C a * X))) l atTop

pp: case refine_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p * X).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p * X))) l atTop

pp: case refine_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]} {a : R},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p + C a).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p + C a))) l atTop

Tactic:
· rintro _ - hc
    rw [leadingCoeff_mul_X, leadingCoeff_C] at hc
    simpa [abv_mul abv] using hz.const_mul_atTop ((abv_pos abv).2 hc)

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p * X).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p * X))) l atTop

case refine_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Ring S
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsStrictOrderedRing k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]} {a : R},
    0 < p.degree →
      (f p.leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) p)) l atTop) →
        f (p + C a).leadingCoeff ≠ 0 → Tendsto (fun x ↦ abv (eval₂ f (z x) (p + C a))) l atTop
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| fun t ↦ X - C t

pp: case a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| s

Tactic:
ext x

Goal state after:
case a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
x : R
| X - C x

case a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
| s
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: case a.a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| fun t ↦ X - C t

pp: case a.a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| s

pp: case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| k

Tactic:
ext x

Goal state after:
case a.a.f
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
x : R
| X - C x

case a.a.s
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| s

case a
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
h : k ≤ s.card
| k
Module: Mathlib.RingTheory.Valuation.Archimedean

Goal state before:
pp: case refine_4
F : Type u_1
Γ₀ : Type u_2
O : Type u_3
inst✝⁴ : Field F
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : CommRing O
inst✝¹ : Algebra O F
v : Valuation F Γ₀
inst✝ : Nontrivial (↥(MonoidHom.mrange v))ˣ
hv : v.Integers O
h : {x | x ≤ 1}.WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ ∀ a ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)),
    ∀ b ∈ Set.range (⇑v ∘ ⇑(algebraMap O F)),
      a > b → ((fun x1 x2 ↦ x1 > x2) on fun x ↦ if hx : x ∈ MonoidHom.mrange v then ⟨x, hx⟩ else 1) a b

Tactic:
simp [Function.onFun]

Goal state after:
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case h0
p : ℚ[X]
p_irr : Irreducible p
p_deg : Nat.Prime p.natDegree
p_roots : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
h1 : Fintype.card ↑(p.rootSet ℂ) = p.natDegree
conj' : p.Gal := ⋯
x : Equiv.Perm ↑(p.rootSet ℂ)
⊢ Nat.Prime (Fintype.card ↑(p.rootSet ℂ))

Tactic:
rwa [h1]

Goal state after:
Module: Mathlib.RingTheory.Valuation.RankOne

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H' : ∀ (x : K), v x ≠ 0 → v x = 1
x : (ofClass v).ValueGroup₀ˣ
k : K
h0 : v k ≠ 0
hk : v k = embedding ↑x
hx : ↑x ≠ ↑1
h : v k = 1
⊢ False

Tactic:
apply_fun embedding at hx using embedding_injective (f := .ofClass v)

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
K : Type u_3
inst✝¹ : DivisionRing K
v : Valuation K Γ₀
inst✝ : v.RankLeOne
H' : ∀ (x : K), v x ≠ 0 → v x = 1
x : (ofClass v).ValueGroup₀ˣ
k : K
h0 : v k ≠ 0
hk : v k = embedding ↑x
h : v k = 1
hx : embedding ↑x ≠ embedding ↑1
⊢ False
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
s : Set (ℝ × ℝ)
hs : s.Countable
a₁ b₁ : ℝ
h₁ : a₁ ≤ b₁
a₂ b₂ : ℝ
h₂ : a₂ ≤ b₂
Hcf : ContinuousOn f (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hcg : ContinuousOn g (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂)
Hdf : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a₁ b₁ ×ˢ Set.Ioo a₂ b₂ \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂) volume
⊢ ∫ (x : ℝ × ℝ) in Set.Icc a₁ b₁ ×ˢ Set.Icc a₂ b₂, (f' x) (1, 0) + (g' x) (0, 1) =
    (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) -
      ∫ (y : ℝ) in a₂..b₂, f (a₁, y)

Tactic:
by
      rw [Icc_prod_Icc] at *
      apply integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le f g f' g'
        (a₁, a₂) (b₁, b₂) ⟨h₁, h₂⟩ s <;> assumption

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case refine_1.inr
K : Type u_1
hK : NormedField K
inst✝ : IsUltrametricDist K
U : Set K
ε : ℝ
hε : ε > 0
h : Metric.ball 0 ε ⊆ U
H : ∀ {γ : ℝ≥0}, γ ≠ 0 → ∃ x, x ≠ 0 ∧ (RankLeOne.hom' valuation) (valuation.restrict x) < γ
⊢ ∃ γ, {x | valuation.restrict x < ↑γ} ⊆ U

Tactic:
· obtain ⟨x, hx, hxy⟩ := H (γ := ⟨ε, le_of_lt hε⟩) (pos_iff_ne_zero.mp hε)
          use Units.mk0 (valuation.restrict x) (by simp [Valuation.restrict_def, hx])
          intro y hy
          apply h
          simp only [Metric.mem_ball, dist_zero_right]
          simp only [Units.val_mk0, mem_ofPred_eq, restrict_lt_iff, ← NNReal.coe_lt_coe] at hy
          apply lt_trans hy
          simpa [RankLeOne.hom', valuation.restrict_def] using! hxy

Goal state after: