mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : s ∈ 𝓝 0
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε

Tactic:
rw [← set_smul_mem_nhds_zero_iff hε.ne'] at hs

Goal state after:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
ε : ℝ
hs : ε • s ∈ 𝓝 0
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝 0, gauge s x ∈ Icc 0 ε
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs : s ∈ 𝓝 0
⊢ Tendsto (gauge s) (𝓝 0) (𝓝[≥] 0)

Tactic:
refine nhdsGE_basis_Icc.tendsto_right_iff.2 fun ε hε ↦ ?_
  rw [← set_smul_mem_nhds_zero_iff hε.ne'] at hs
  filter_upwards [hs] with x hx
  exact ⟨gauge_nonneg _, gauge_le_of_mem hε.le hx⟩

Goal state after:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr.symmetric
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr✝ : 0 ≤ r
x : E
hr : 0 < r
⊢ ∀ (x : E), ‖x‖ < 1 → ‖x‖ < 1

Tactic:
exact fun _ => id

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

Goal state before:
pp: case h_ind
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
e : E
s : Set X
⊢ MeasurableSet s → μ s < ∞ → ∫ (x : X), L (s.indicator (fun x ↦ e) x) ∂μ = L (∫ (x : X), s.indicator (fun x ↦ e) x ∂μ)

Tactic:
s_meas

Goal state after:
case h_ind
X : Type u_1
E : Type u_3
F : Type u_4
inst✝¹¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
𝕜' : Type u_7
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : RCLike 𝕜'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
inst✝⁴ : NormedSpace ℝ F
σ : 𝕜 →+* 𝕜'
inst✝³ : RingHomIsometric σ
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x
L : E →SL[σ] F
φ : X → E
φ_int : Integrable φ μ
e : E
s : Set X
s_meas : MeasurableSet s
⊢ μ s < ∞ → ∫ (x : X), L (s.indicator (fun x ↦ e) x) ∂μ = L (∫ (x : X), s.indicator (fun x ↦ e) x ∂μ)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
e p q e' p' q' : ℕ
hp : n e ≤ p
hq : n e ≤ q
hp' : n e' ≤ p'
hq' : n e' ≤ q'
he' : e ≤ e'
r : ℕ := max (n e) (n e')
I : (1 / 2) ^ e' ≤ (1 / 2) ^ e
J1 : ‖L e p q - L e p r‖ ≤ 4 * (1 / 2) ^ e
J2 : ‖L e p r - L e' p' r‖ ≤ 4 * (1 / 2) ^ e
J3 : ‖L e' p' r - L e' p' q'‖ ≤ 4 * (1 / 2) ^ e
⊢ ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e

Tactic:
calc
      ‖L e p q - L e' p' q'‖ =
          ‖L e p q - L e p r + (L e p r - L e' p' r) + (L e' p' r - L e' p' q')‖ := by
        congr 1; abel
      _ ≤ ‖L e p q - L e p r‖ + ‖L e p r - L e' p' r‖ + ‖L e' p' r - L e' p' q'‖ := by
        grw [norm_add_le, norm_add_le]
      _ ≤ 4 * (1 / 2) ^ e + 4 * (1 / 2) ^ e + 4 * (1 / 2) ^ e := by gcongr
      _ = 12 * (1 / 2) ^ e := by ring

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

Goal state before:
pp: case pos.refine_1
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))
c : E
s : Set X
⊢ MeasurableSet s →
    (μ.withDensity fun x ↦ ↑(f x)) s < ∞ →
      (∫ (x : X), s.indicator (fun x ↦ c) x ∂μ.withDensity fun x ↦ ↑(f x)) =
        ∫ (x : X), f x • s.indicator (fun x ↦ c) x ∂μ

Tactic:
s_meas

Goal state after:
case pos.refine_1
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))
c : E
s : Set X
s_meas : MeasurableSet s
⊢ (μ.withDensity fun x ↦ ↑(f x)) s < ∞ →
    (∫ (x : X), s.indicator (fun x ↦ c) x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • s.indicator (fun x ↦ c) x ∂μ
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: α : Type u_1
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → α → G
inst✝ : IsFiniteMeasure μ
f : α → G
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∃ C, ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ C
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun n ↦ F n ω) l (𝓝 (f ω))
⊢ Tendsto (fun n ↦ ∫ (ω : α), F n ω ∂μ) l (𝓝 (∫ (ω : α), f ω ∂μ))

Tactic:
by
  simp only [integral_eq_setToFun]
  exact tendsto_setToFun_filter_of_norm_le_const _ h_meas h_bound h_lim

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
s : Set F
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
this :
  (fun x ↦ derivWithin f (Ici x) x) ⁻¹' s =
    {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s}
⊢ MeasurableSet
    ({x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x | 0 ∈ s})

Tactic:
exact
    (measurableSet_of_differentiableWithinAt_Ici_of_isComplete _ hs.isComplete).union
      ((measurableSet_of_differentiableWithinAt_Ici _).compl.inter (MeasurableSet.const _))

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 ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable (fun x ↦ f (x + c)) volume (a - c) (b - c)

Tactic:
have h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ⊤ := by
    rw [min_sub_sub_right, sub_add, sub_self, sub_zero]
    exact h
  wlog hab : a ≤ b generalizing a b
  · apply IntervalIntegrable.symm (this hf.symm ?_ ?_ (le_of_not_ge hab))
    · rw [min_comm]; exact h
    · rw [min_comm]; exact h'
  rw [intervalIntegrable_iff' h] at hf
  rw [intervalIntegrable_iff' h'] at ⊢
  have A : MeasurableEmbedding fun x => x + c :=
    (Homeomorph.addRight c).isClosedEmbedding.measurableEmbedding
  rw [← map_add_right_eq_self volume c] at hf
  convert! (MeasurableEmbedding.integrableOn_map_iff A).mp hf using 1
  rw [preimage_add_const_uIcc]

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

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
⊢ ∫ (x : ℝ) in a..b, f (-x) = ∫ (x : ℝ) in -b..-a, f x

Tactic:
simpa only [zero_sub] using integral_comp_sub_left f 0

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

Tactic:
have aux : (fun x => ∫ t in Icc a x, f t ∂μ) = fun x => ∫ t in Ioc a x, f t ∂μ := by
    ext x
    exact integral_Icc_eq_integral_Ioc

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) μ
aux : (fun x ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x ↦ ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x ↦ ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)
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
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
hK : IsComplete K
⊢ MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}

Tactic:
have : {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
          = {p : α × E | p.2 ∈ D (f p.1) K} := by simp [← differentiable_set_eq_D K hK]
  rw [this]
  simp only [D, mem_iInter, mem_iUnion]
  simp only [ofPred_forall, ofPred_exists]
  refine MeasurableSet.iInter (fun _ ↦ ?_)
  refine MeasurableSet.iUnion (fun _ ↦ ?_)
  refine MeasurableSet.iInter (fun _ ↦ ?_)
  refine MeasurableSet.iInter (fun _ ↦ ?_)
  refine MeasurableSet.iInter (fun _ ↦ ?_)
  refine MeasurableSet.iInter (fun _ ↦ ?_)
  have : ProperSpace E := .of_locallyCompactSpace 𝕜
  exact (isOpen_B_with_param hf K).measurableSet

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

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
⊢ ∫ (y : ℝ) in a..b, f' y = fb - fa

Tactic:
set F : ℝ → E := update (update f a fa) b fb
  have Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x := by
    refine fun x hx => (hderiv x hx).congr_of_eventuallyEq ?_
    filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy
    unfold F
    rw [update_of_ne hy.2.ne, update_of_ne hy.1.ne']
  have hcont : ContinuousOn F (Icc a b) := by
    rw [continuousOn_update_iff, continuousOn_update_iff, Icc_sdiff_right, Ico_sdiff_left]
    refine ⟨⟨fun z hz => (hderiv z hz).continuousAt.continuousWithinAt, ?_⟩, ?_⟩
    · exact fun _ => ha.mono_left (nhdsWithin_mono _ Ioo_subset_Ioi_self)
    · rintro -
      refine (hb.congr' ?_).mono_left (nhdsWithin_mono _ Ico_subset_Iio_self)
      filter_upwards [Ioo_mem_nhdsLT hab] with _ hz using (update_of_ne hz.1.ne' _ _).symm
  simpa [F, hab.ne, hab.ne'] using integral_eq_sub_of_hasDerivAt_of_le hab.le hcont Fderiv hint

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
⊢ 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)

Tactic:
by
  rcases lt_or_ge a b with hab | hba
  · rw [uIoc_of_le hab.le] at hf
    simp only [hab, true_and, integral_of_le hab.le,
      setIntegral_pos_iff_support_of_nonneg_ae hf hfi.1]
  · suffices (∫ x in a..b, f x ∂μ) ≤ 0 by simp only [this.not_gt, hba.not_gt, false_and]
    rw [integral_of_ge hba, neg_nonpos]
    rw [uIoc_comm, uIoc_of_le hba] at hf
    exact integral_nonneg_of_ae hf

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

Goal state before:
pp: case refine_1
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b) volume
A : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ IntegrableOn F (Icc a b) volume

Tactic:
integrableOn_Icc_iff_integrableOn_Ioo

Goal state after:
case refine_1
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable g' (volume.restrict (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, ↑‖g' x‖₊
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), f x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ ⇑f
hf : ENNReal.ofReal (g b - g a) < ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
intF : IntegrableOn F (Ioo a b) volume
A : ∫⁻ (x : ℝ) in Ioo a b, ↑(f x) = ENNReal.ofReal (∫ (x : ℝ) in Ioo a b, F x)
⊢ IntegrableOn F (Ioo a b) volume
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
⊢ MeasurableSet s → (map π (μ.restrict 𝓕)) s = 0 → (map π μ) s = 0

Tactic:
s_meas

Goal state after:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
s : Set (G ⧸ Γ)
s_meas : MeasurableSet s
⊢ (map π (μ.restrict 𝓕)) s = 0 → (map π μ) s = 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
⊢ ∫ (x : ℝ) in 0..t, g x ≤ sSup ((fun t ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0..T, g x

Tactic:
let h'_int := hg.intervalIntegrable₀ hT.ne' h_int
  let ε := Int.fract (t / T) * T
  conv_lhs =>
    rw [← Int.fract_div_mul_self_add_zsmul_eq T t hT.ne', ←
      integral_add_adjacent_intervals (h'_int 0 ε) (h'_int _ _)]
  rw [hg.intervalIntegral_add_zsmul_eq ⌊t / T⌋ ε h'_int, hg.intervalIntegral_add_eq ε 0, zero_add,
    add_le_add_iff_right]
  exact (continuous_primitive h'_int 0).continuousOn.le_sSup_image_Icc
    (mem_Icc_of_Ico (Int.fract_div_mul_self_mem_Ico T t hT))

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ HasSum (fun n ↦ ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Tactic:
have hR : 0 < R := (norm_nonneg w).trans_lt hw
  have hwR : ‖w‖ / R ∈ Ico (0 : ℝ) 1 :=
    ⟨div_nonneg (norm_nonneg w) hR.le, (div_lt_one hR).2 hw⟩
  refine intervalIntegral.hasSum_integral_of_dominated_convergence
      (fun n θ => ‖f (circleMap c R θ)‖ * (‖w‖ / R) ^ n) (fun n => ?_) (fun n => ?_) ?_ ?_ ?_
  · simp only [deriv_circleMap]
    apply_rules [AEStronglyMeasurable.smul, hf.def'.1] <;> apply Measurable.aestronglyMeasurable
    · fun_prop
    · fun_prop
    · fun_prop
  · simp [norm_smul, abs_of_pos hR, mul_left_comm R, inv_mul_cancel_left₀ hR.ne', mul_comm ‖_‖]
  · exact Eventually.of_forall fun _ _ => (summable_geometric_of_lt_one hwR.1 hwR.2).mul_left _
  · simpa only [tsum_mul_left, tsum_geometric_of_lt_one hwR.1 hwR.2] using
      hf.norm.mul_continuousOn continuousOn_const
  · refine Eventually.of_forall fun θ _ => HasSum.const_smul _ ?_
    simp only [smul_smul]
    refine HasSum.smul_const ?_ _
    have : ‖w / (circleMap c R θ - c)‖ < 1 := by simpa [abs_of_pos hR] using hwR.2
    convert! (hasSum_geometric_of_norm_lt_one this).mul_right _ using 1
    simp [← sub_sub, ← mul_inv, sub_mul, div_mul_cancel₀ _ (circleMap_ne_center hR.ne')]

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

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ ∫ (x : ℝ) in a..b, ∫ (y : ℝ) in c..d, F x y = ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y

Tactic:
rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, ← intervalIntegral_integral_swap,
    ← intervalIntegral.integral_smul]

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ ∫ (x : ℝ) in c..d, (if a ≤ b then 1 else -1) • ∫ (y : ℝ) in uIoc a b, F y x ∂volume =
    ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y

E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
F : ℝ → ℝ → E
a b c d : ℝ
h : IntegrableOn (uncurry F) (uIoc a b ×ˢ uIoc c d) volume
⊢ Integrable (uncurry fun y x ↦ F x y) ((volume.restrict (uIoc c d)).prod (volume.restrict (uIoc a b)))
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : (map (algebraMap F q₁.SplittingField) p₁).Splits
h₂ : (map (algebraMap F q₂.SplittingField) p₂).Splits
⊢ (map (algebraMap F (q₁ * q₂).SplittingField) p₁ * map (algebraMap F (q₁ * q₂).SplittingField) p₂).Splits

Tactic:
apply Splits.mul

Goal state after:
case hf
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : (map (algebraMap F q₁.SplittingField) p₁).Splits
h₂ : (map (algebraMap F q₂.SplittingField) p₂).Splits
⊢ (map (algebraMap F (q₁ * q₂).SplittingField) p₁).Splits

case hg
F : Type u_1
inst✝ : Field F
p₁ q₁ p₂ q₂ : F[X]
hq₁ : q₁ ≠ 0
hq₂ : q₂ ≠ 0
h₁ : (map (algebraMap F q₁.SplittingField) p₁).Splits
h₂ : (map (algebraMap F q₂.SplittingField) p₂).Splits
⊢ (map (algebraMap F (q₁ * q₂).SplittingField) p₂).Splits
Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs

Goal state before:
pp: σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
⊢ esymm σ R n = ∑ t ∈ powersetCard n univ, (monomial (∑ i ∈ t, Finsupp.single i 1)) 1

Tactic:
simp_rw [monomial_sum_one, esymm, ← X_pow_eq_monomial, pow_one]

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
⊢ P p₂ → P (p₁ * p₂)

Tactic:
hp₂

Goal state after:
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
⊢ P (p₁ * p₂)
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : ¬p₂.comp q = 0
⊢ P (p₁ * p₂)

Tactic:
have key := mul_splits_in_splittingField_of_mul h₁ h₂ hp₁ hp₂

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
p q : F[X]
hq : q.natDegree ≠ 0
P : F[X] → Prop := fun r ↦ (map (algebraMap F (r.comp q).SplittingField) r).Splits
key1 : ∀ {r : F[X]}, Irreducible r → P r
p₁ p₂ : F[X]
hp₁ : P p₁
hp₂ : P p₂
h₁ : ¬p₁.comp q = 0
h₂ : ¬p₂.comp q = 0
key : (map (algebraMap F (p₁.comp q * p₂.comp q).SplittingField) (p₁ * p₂)).Splits
⊢ P (p₁ * p₂)
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c ↑R
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ x ∈ ball c ↑R \ s, DifferentiableAt ℂ f x
hR : 0 < ↑R
this : w ∈ closure (ball c ↑R \ s)
A : ContinuousAt (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) w
⊢ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z = f w

Tactic:
have B : ContinuousAt f w := hc.continuousAt (closedBall_mem_nhds_of_mem hw)

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
R : ℝ≥0
hw : w ∈ ball c ↑R
hc : ContinuousOn f (closedBall c ↑R)
hd : ∀ x ∈ ball c ↑R \ s, DifferentiableAt ℂ f x
hR : 0 < ↑R
this : w ∈ closure (ball c ↑R \ s)
A : ContinuousAt (fun w ↦ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) w
B : ContinuousAt f w
⊢ (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z = f w
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ ∏ i, (Polynomial.X + Polynomial.C (X i)) =
    ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)

Tactic:
let s := Finset.univ.val.map fun i : σ => (MvPolynomial.X i : MvPolynomial σ R)

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun i ↦ X i) univ.val
⊢ ∏ i, (Polynomial.X + Polynomial.C (X i)) =
    ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: case mp
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
⊢ AnalyticAt ℂ f c → ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z

Tactic:
intro fa

Goal state after:
case mp
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
fa : AnalyticAt ℂ f c
⊢ ∀ᶠ (z : ℂ) in 𝓝 c, DifferentiableAt ℂ f z
Module: Mathlib.Analysis.Complex.Polynomial.Basic

Goal state before:
pp: case pos
p : ℚ[X]
hp : p = 0
this : IsEmpty ↑(p.rootSet ℂ)
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card

Tactic:
simp_rw [(galActionHom p ℂ _).support.eq_empty_of_isEmpty, hp, rootSet_zero,
      Set.toFinset_empty, Finset.card_empty]

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

Goal state before:
pp: case neg
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
⊢ (p.rootSet ℂ).toFinset.card =
    (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card

Tactic:
rw [← Finset.card_image_of_injective _ Subtype.coe_injective, ←
    Finset.card_image_of_injective _ inj]

Goal state after:
case neg
p : ℚ[X]
hp : ¬p = 0
inj : Function.Injective ⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)
⊢ (p.rootSet ℂ).toFinset.card =
    (Finset.image (⇑(IsScalarTower.toAlgHom ℚ ℝ ℂ)) (p.rootSet ℝ).toFinset).card +
      (Finset.image (fun a ↦ ↑a) ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support).card
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
⊢ (∀ x_1 ∈ ratLt' 0, x_1 ≤ x) → 0 ≤ x

Tactic:
suffices (∀ (y : ℚ), y.num • (1 : M) < 0 → y ≤ x) → 0 ≤ x by simpa using this

Goal state after:
case a
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x : ℝ
⊢ (∀ (y : ℚ), y.num • 1 < 0 → ↑y ≤ x) → 0 ≤ x