mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

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

Tactic:
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_mul_sub f (inv_ne_zero hc) d

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

Goal state before:
pp: g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
x : ℝ
hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal
h'x : x ∈ Ioc t (min v b)
⊢ ({t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty

Tactic:
refine ⟨x, ?_, Ioc_subset_Ioc le_rfl (min_le_left _ _) h'x⟩

Goal state after:
g' g φ : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt g (g' x) (Ioi x) x
φint : IntegrableOn φ (Icc a b) volume
hφg : ∀ x ∈ Ico a b, g' x ≤ φ x
ε : ℝ
εpos : 0 < ε
G' : ℝ → EReal
f_lt_G' : ∀ (x : ℝ), ↑(φ x) < G' x
G'cont : LowerSemicontinuous G'
G'int : Integrable (fun x ↦ (G' x).toReal) (volume.restrict (Icc a b))
G'lt_top : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc a b), G' x < ⊤
hG' : ∫ (x : ℝ) in Icc a b, (G' x).toReal < (∫ (x : ℝ) in Icc a b, φ x) + ε
s : Set ℝ := {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Icc a b
s_closed : IsClosed s
t : ℝ
ht : t ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ico a b
v : ℝ
t_lt_v : v ∈ Ioi t
y : ℝ
g'_lt_y' : ↑(g' t) < ↑y
y_lt_G' : ↑y < G' t
I1 : ∀ᶠ (u : ℝ) in 𝓝[>] t, (u - t) * y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I2 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ (u - t) * y
I3 : ∀ᶠ (u : ℝ) in 𝓝[>] t, g u - g t ≤ ∫ (w : ℝ) in t..u, (G' w).toReal
I4 : ∀ᶠ (u : ℝ) in 𝓝[>] t, u ∈ Ioc t (min v b)
x : ℝ
hx : g x - g t ≤ ∫ (w : ℝ) in t..x, (G' w).toReal
h'x : x ∈ Ioc t (min v b)
⊢ x ∈ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal}
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε

Tactic:
obtain ⟨δ, δpos, hδ, h'δ, h''δ⟩ : ∃ (δ : ℝ), 0 < δ ∧ δ < 1 ∧ Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b ∧
      (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε := by
    have A : ∀ᶠ δ in 𝓝[>] (0 : ℝ), δ ∈ Ioo 0 1 := Ioo_mem_nhdsGT zero_lt_one
    have B : ∀ᶠ δ in 𝓝 0, Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b := by
      have I : Tendsto (fun δ ↦ b₀ - δ) (𝓝 0) (𝓝 (b₀ - 0)) := tendsto_const_nhds.sub tendsto_id
      have J : Tendsto (fun δ ↦ b₀ + δ) (𝓝 0) (𝓝 (b₀ + 0)) := tendsto_const_nhds.add tendsto_id
      simp only [sub_zero, add_zero] at I J
      filter_upwards [(tendsto_order.1 I).1 _ a_lt.2, (tendsto_order.1 J).2 _ lt_b.2] with δ hδ h'δ
      exact Icc_subset_Icc hδ.le h'δ.le
    have C : ∀ᶠ δ in 𝓝 0,
        (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε := by
      suffices Tendsto
        (fun δ ↦ (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b))
          (𝓝 0) (𝓝 ((M + 1) * (0 : ℝ≥0∞).toReal + 0 * μ.real (Icc a b))) by
        simp only [toReal_zero, mul_zero, zero_mul, add_zero] at this
        exact (tendsto_order.1 this).2 _ εpos
      apply Tendsto.add (Tendsto.mul tendsto_const_nhds _)
        (Tendsto.mul tendsto_id tendsto_const_nhds)
      exact (tendsto_toReal zero_ne_top).comp (tendsto_measure_Icc _ _)
    rcases (A.and ((B.and C).filter_mono nhdsWithin_le_nhds)).exists with ⟨δ, hδ, h'δ, h''δ⟩
    exact ⟨δ, hδ.1, hδ.2, h'δ, h''δ⟩

Goal state after:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
⊢ ∀ᶠ (x : X × ℝ) in 𝓝 (q, b₀),
    dist (∫ (t : ℝ) in a₀..x.2, f x.1 t ∂μ) (∫ (t : ℝ) in a₀..(q, b₀).2, f (q, b₀).1 t ∂μ) < ε
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
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : StrongDual ℝ E
⊢ ∫ (x : ℝ) in a..b, g (f' x) = g (f b) - g (f a)

Tactic:
exact integral_eq_sub_of_hasDeriv_right_of_le_real hab (g.continuous.comp_continuousOn hcont)
    (fun x hx => g.hasFDerivAt.comp_hasDerivWithinAt x (hderiv x hx))
    (g.integrable_comp ((intervalIntegrable_iff_integrableOn_Icc_of_le hab enorm_ne_top).1 f'int))

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: α : Type u_1
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
inst✝³ : FloorRing α
inst✝² : TopologicalSpace α
inst✝¹ : IsStrictOrderedRing α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑⌈x⌉ < x + 1

Tactic:
exact ceil_lt_add_one _

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (𝓝 (s, ↑n)) (𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n)))

Tactic:
nhds_prod_eq,

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ Tendsto (uncurry f ∘ Prod.map id fract) (𝓝 s ×ˢ 𝓝 ↑n) (𝓝 ((uncurry f ∘ Prod.map id fract) (s, ↑n)))
Module: Mathlib.Topology.Algebra.Order.Floor

Goal state before:
pp: case inl.left.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 s ×ˢ 𝓝[<] 1 ≤ 𝓝 s ×ˢ 𝓝[Icc 0 1] 1

Tactic:
← nhdsWithin_Ico_eq_nhdsLT one_pos

Goal state after:
case inl.left.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : FloorRing α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsStrictOrderedRing α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α → γ
h : ContinuousOn (uncurry f) (univ ×ˢ Icc 0 1)
hf : ∀ (s : β), f s 0 = f s 1
s : β
n : ℤ
⊢ 𝓝 s ×ˢ 𝓝[Ico 0 1] 1 ≤ 𝓝 s ×ˢ 𝓝[Icc 0 1] 1
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case neg
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ¬ε < T / 2
⊢ volume (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))

Tactic:
· simp [I, hε, min_eq_left (by linarith : T ≤ 2 * ε)]

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

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T t : ℝ
h₁f : Periodic f T
hT✝ : T ≠ 0
h₂f : IntervalIntegrable f volume (t + T + -T) (t + T)
a₁ a₂ : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T t : ℝ},
    Periodic f T →
      T ≠ 0 → IntervalIntegrable f volume t (t + T) → ∀ (a₁ a₂ : ℝ), 0 < T → IntervalIntegrable f volume a₁ a₂
hT : ¬0 < T
h : T < 0
hnT : 0 < -T
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
apply this h₁f.neg hnT.ne' h₂f.symm _ _ hnT

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

Goal state before:
pp: case hF
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : TendstoUniformlyOn f g l (sphere c R)
⊢ ∀ᶠ (i : ι) in l, ContinuousOn (fun x ↦ deriv (circleMap c R) x • (fun z ↦ f i z) (circleMap c R x)) [[0, 2 * π]]

Tactic:
refine hf.mono fun i hi ↦ .smul ?_ (hi.comp ?_ ?_)
    · rw [funext (deriv_circleMap _ _)]
      fun_prop
    · fun_prop
    · simp [hR, MapsTo]

Goal state after:
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
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ y ∈ Box.Icc (I.face i),
    ‖f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤ 2 * ε * diam (Box.Icc I)
⊢ ‖(∏ 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)‖ =
    ‖integral (I.face i) ⊥
        (fun x ↦ f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) x) - f (e (I.lower i) x)))
        BoxAdditiveMap.volume‖

Tactic:
rw [← integral_sub (Hi _ Hu) (Hi _ Hl), ← Box.volume_face_mul i, mul_smul, ← Box.volume_apply,
        ← BoxAdditiveMap.toSMul_apply, ← integral_const, ← BoxAdditiveMap.volume,
        ← integral_sub (integrable_const _) ((Hi _ Hu).sub (Hi _ Hl))]
      simp only [(· ∘ ·), Pi.sub_def, ← f'.map_smul, ← Pi.single_smul', smul_eq_mul, mul_one]

Goal state after:
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
e : ℝ → (Fin n → ℝ) → Fin (n + 1) → ℝ := i.insertNth
Hl : I.lower i ∈ Set.Icc (I.lower i) (I.upper i)
Hu : I.upper i ∈ Set.Icc (I.lower i) (I.upper i)
Hi : ∀ x ∈ Set.Icc (I.lower i) (I.upper i), Integrable (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume
this :
  ∀ y ∈ Box.Icc (I.face i),
    ‖f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤ 2 * ε * diam (Box.Icc I)
⊢ (volume ↑(I.face i)).toReal * (2 * ε * ↑c * (I.upper i - I.lower i)) = 2 * ε * ↑c * ∏ j, (I.upper j - I.lower j)

Tactic:
rw [← measureReal_def, ← Measure.toBoxAdditive_apply, Box.volume_apply,
        ← I.volume_face_mul i]
      ac_rfl

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

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ≥0
n : ℕ
hR : ↑R ^ n ≠ 0
⊢ ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖) * (↑R)⁻¹ ^ n * ↑R ^ n ≤
    (2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, ‖f (circleMap c (↑R) θ)‖

Tactic:
rw [inv_pow]
    have : (R : ℝ) ^ n ≠ 0 := by norm_cast at hR ⊢
    rw [inv_mul_cancel_right₀ this]

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 ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

Tactic:
by_cases hE : CompleteSpace E; swap; · simp only [integral, dif_neg hE]
  revert f
  apply Integrable.induction
  · intro c s hs h2s
    simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp_def,
      integral_indicator (measurable_prodMk_left hs), setIntegral_const, integral_smul_const,
      measureReal_def,
      integral_toReal (measurable_measure_prodMk_left hs).aemeasurable
        (ae_measure_lt_top hs h2s.ne)]
    rw [Measure.prod_apply hs]
  · rintro f g - i_f i_g hf hg
    simp_rw [integral_add' i_f i_g, integral_integral_add' i_f i_g, hf, hg]
  · exact isClosed_eq continuous_integral continuous_integral_integral
  · rintro f g hfg - hf; convert! hf using 1
    · exact integral_congr_ae hfg.symm
    · apply integral_congr_ae
      filter_upwards [ae_ae_of_ae_prod hfg] with x hfgx using integral_congr_ae (ae_eq_symm hfgx)

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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
hle : rexp a ≤ R
hd : ∀ z ∈ (ball c R \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c R \ ball c (rexp a)
hc : ContinuousOn f A
⊢ ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z

Tactic:
obtain ⟨b, rfl⟩ : ∃ b, Real.exp b = R := ⟨Real.log R, Real.exp_log (h0.trans_le hle)⟩

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
a : ℝ
h0 : 0 < rexp a
b : ℝ
hle : rexp a ≤ rexp b
hd : ∀ z ∈ (ball c (rexp b) \ closedBall c (rexp a)) \ s, DifferentiableAt ℂ f z
A : Set ℂ := closedBall c (rexp b) \ ball c (rexp a)
hc : ContinuousOn f A
⊢ ∮ (z : ℂ) in C(c, rexp b), (z - c)⁻¹ • f z = ∮ (z : ℂ) in C(c, rexp a), (z - c)⁻¹ • f z
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 ∈ (Finsupp.single (∑ i ∈ s, Finsupp.single i 1) 1).support →
      a ∉ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support

Tactic:
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 ∉ (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support
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:
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 σ
this : (⇑Finsupp.toMultiset ∘ fun t ↦ ∑ i ∈ t, Finsupp.single i 1) = val
⊢ (esymm σ R n).degrees = univ.val

Tactic:
degrees_def,

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).support.sup fun s ↦ Finsupp.toMultiset s) = univ.val
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (-1) ^ k * x.prod

Tactic:
(mem_powersetCard.mp hx).right.symm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
s : Multiset R
k : ℕ
x : Multiset R
hx : x ∈ powersetCard k s
⊢ (prod ∘ map Neg.neg) x = (-1) ^ x.card * x.prod
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
den : ℕ
hden✝ : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).num *
      ↑m
hden :
  den =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).den *
      m
| den • x

Tactic:
rw [hden, mul_comm, ← smul_smul]

Goal state after:
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : LinearOrder M
inst✝¹ : IsOrderedAddMonoid M
inst✝ : One M
num : ℤ
den : ℕ
hden✝ : den ≠ 0
x : M
m : ℕ
hm0 : m ≠ 0
hnum :
  num =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).num *
      ↑m
hden :
  den =
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).den *
      m
| m •
    (Decidable.rec (fun h ↦ (fun den_nz ↦ Rat.normalize num den den_nz) h)
          (fun h ↦
            (fun den_nz ↦ { num := 0, den_nz := instInhabitedRat._proof_1, reduced := instInhabitedRat._proof_2 }) h)
          (instDecidableEqNat den 0)).den •
      x
Module: Mathlib.Topology.MetricSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y z : X
h : dist x y ≠ dist y z
⊢ dist x z = max (dist x y) (dist y z)

Tactic:
apply le_antisymm (dist_triangle_max x y z)
  rcases h.lt_or_gt with h | h
  · rw [max_eq_right h.le]
    apply (le_max_iff.mp <| dist_triangle_max y x z).resolve_left
    simpa only [not_le, dist_comm x y] using h
  · rw [max_eq_left h.le, dist_comm x y, dist_comm x z]
    apply (le_max_iff.mp <| dist_triangle_max y z x).resolve_left
    simpa only [not_le, dist_comm x y] using h

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑(toLex d) = φ.lexOrder
hφ : φ ≠ 0
ne : (⇑toLex '' Function.support φ).Nonempty
hφ' : toLex d = ⋯.min (⇑toLex '' Function.support φ) ne
this : d ∈ Function.support φ
⊢ (coeff d) φ ≠ 0

Tactic:
apply this

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
h✝ : n = 0
⊢ (constantCoeff φ)⁻¹ = (coeff n) 0

Tactic:
simp only [h, map_zero, zero_mul, inv_zero, neg_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Inverse

Goal state before:
pp: case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : constantCoeff φ = 0
n : σ →₀ ℕ
h✝ : ¬n = 0
⊢ (-(constantCoeff φ)⁻¹ * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff x.1) φ * (coeff x.2) φ⁻¹ else 0) = (coeff n) 0

Tactic:
simp only [h, map_zero, zero_mul, inv_zero, neg_zero]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := (weightedOrder w f).toNat
hp : ↑p = weightedOrder w f
q : ℕ := (weightedOrder w g).toNat
hq : ↑q = weightedOrder w g
this : (weightedHomogeneousComponent w (p + q)) (f * g) ≠ 0
H : ↑(p + q) < weightedOrder w (f * g)
⊢ False

Tactic:
apply this

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
w : σ → ℕ
f g : MvPowerSeries σ R
hf : weightedOrder w f < ⊤
hg : weightedOrder w g < ⊤
p : ℕ := ⋯
hp : ↑p = weightedOrder w f
q : ℕ := ⋯
hq : ↑q = weightedOrder w g
this : (weightedHomogeneousComponent w (p + q)) (f * g) ≠ 0
H : ↑(p + q) < weightedOrder w (f * g)
⊢ (weightedHomogeneousComponent w (p + q)) (f * g) = 0
Module: Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors

Goal state before:
pp: case cons
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : weightedOrder w (∏ i ∈ s, f i) = ∑ i ∈ s, weightedOrder w (f i)
⊢ weightedOrder w (∏ i ∈ Finset.cons a s ha, f i) = weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x)

Tactic:
Finset.prod_cons ha,

Goal state after:
case cons
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
ι : Type u_4
w : σ → ℕ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih : weightedOrder w (∏ i ∈ s, f i) = ∑ i ∈ s, weightedOrder w (f i)
⊢ weightedOrder w (f a * ∏ x ∈ s, f x) = weightedOrder w (f a) + ∑ x ∈ s, weightedOrder w (f x)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.negMap ⟦P⟧ = ⟦![0, 1, 0]⟧

Tactic:
negMap_eq,

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ ⟦W.neg P⟧ = ⟦![0, 1, 0]⟧