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 : ℝ
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:
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
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
⊢ ContinuousAt (fun p ↦ ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)

Tactic:
have : ∀ᶠ p : X × ℝ in 𝓝 (x₀, b₀),
      ∫ s in a₀..p.2, F p.1 s ∂μ =
        ∫ s in a₀..b₀, F p.1 s ∂μ + ∫ s in b₀..p.2, F x₀ s ∂μ +
          ∫ s in b₀..p.2, F p.1 s - F x₀ s ∂μ := by
    rw [nhds_prod_eq]
    refine (h_bound.prod_mk Ioo_nhds).mono ?_
    rintro ⟨x, t⟩ ⟨hx : ∀ᵐ t : ℝ ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t, ht : t ∈ Ioo a b⟩
    dsimp
    have hiF : ∀ {x a₀ b₀},
        (∀ᵐ t : ℝ ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b →
          IntervalIntegrable (F x) μ a₀ b₀ := fun {x a₀ b₀} hx ha₀ hb₀ ↦
      (bound_integrable.mono_set_ae <| Eventually.of_forall <| hsub ha₀ hb₀).mono_fun'
        ((hF_meas x).mono_set <| hsub ha₀ hb₀)
        (ae_restrict_of_ae_restrict_of_subset (hsub ha₀ hb₀) hx)
    rw [intervalIntegral.integral_sub, add_assoc, add_sub_cancel,
      intervalIntegral.integral_add_adjacent_intervals]
    · exact hiF hx ha₀ hb₀
    · exact hiF hx hb₀ ht
    · exact hiF hx hb₀ ht
    · exact hiF hx₀ hb₀ ht

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
this :
  ∀ᶠ (p : X × ℝ) in 𝓝 (x₀, b₀),
    ∫ (s : ℝ) in a₀..p.2, F p.1 s ∂μ =
      ∫ (s : ℝ) in a₀..b₀, F p.1 s ∂μ + ∫ (s : ℝ) in b₀..p.2, F x₀ s ∂μ + ∫ (s : ℝ) in b₀..p.2, F p.1 s - F x₀ s ∂μ
⊢ ContinuousAt (fun p ↦ ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case h
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
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
C1 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), G' x < ↑∞
C2 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), x ∈ Icc t u
⊢ (fun x ↦ y) ≤ᵐ[volume.restrict (Icc t u)] fun x ↦ (G' x).toReal

Tactic:
filter_upwards [C1, C2] with x G'x hx

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
B : ∀ᶠ (u : ℝ) in 𝓝 t, ↑y < G' u
m M : ℝ
H : Ioo m M ⊆ {x | (fun u ↦ ↑y < G' u) x}
hm : m < t
hM : t < M
this : Ioo t (min M b) ∈ 𝓝[>] t
u : ℝ
hu : u ∈ Ioo t (min M b)
I : Icc t u ⊆ Icc a b
C1 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), G' x < ↑∞
C2 : ∀ᵐ (x : ℝ) ∂volume.restrict (Icc t u), x ∈ Icc t u
x : ℝ
G'x : G' x < ↑∞
hx : x ∈ Icc t u
⊢ y ≤ (G' x).toReal
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 (d - x / c) = c • ∫ (x : ℝ) in d - b / c..d - a / c, f x

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

Goal state after:
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)
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, δ ∈ Ioo 0 1
B : ∀ᶠ (δ : ℝ) in 𝓝 0, Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε

Tactic:
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

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)
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, δ ∈ Ioo 0 1
B : ∀ᶠ (δ : ℝ) in 𝓝 0, Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
⊢ Tendsto (fun δ ↦ (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b)) (𝓝 0)
    (𝓝 ((M + 1) * ENNReal.toReal 0 + 0 * μ.real (Icc a b)))
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this✝ : QuotientGroup.mk ⁻¹' (fun x ↦ g • x) ⁻¹' A = (fun x ↦ g * x) ⁻¹' π_preA
this : ν ((fun x ↦ g * x) ⁻¹' π_preA ∩ 𝓕) = ν (π_preA ∩ (fun x ↦ g⁻¹ * x) ⁻¹' 𝓕)
⊢ ν ((fun x ↦ g * x) ⁻¹' π_preA ∩ 𝓕) = ν (π_preA ∩ g • 𝓕)

Tactic:
rw [this, ← preimage_smul_inv]

Goal state after:
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst✝⁷ : QuotientMeasureEqMeasurePreimage ν μ
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
inst✝³ : PolishSpace G
inst✝² : T2Space (G ⧸ Γ)
inst✝¹ : SecondCountableTopology (G ⧸ Γ)
inst✝ : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this✝ : QuotientGroup.mk ⁻¹' (fun x ↦ g • x) ⁻¹' A = (fun x ↦ g * x) ⁻¹' π_preA
this : ν ((fun x ↦ g * x) ⁻¹' π_preA ∩ 𝓕) = ν (π_preA ∩ (fun x ↦ g⁻¹ * x) ⁻¹' 𝓕)
⊢ ν (π_preA ∩ (fun x ↦ g⁻¹ * x) ⁻¹' 𝓕) = ν (π_preA ∩ (fun x ↦ g⁻¹ • x) ⁻¹' 𝓕)
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
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
⊢ μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U

Tactic:
let μ' : Measure (G ⧸ Γ) := (ν.restrict s).map π

Goal state after:
G : Type u_1
inst✝¹⁴ : Group G
inst✝¹³ : MeasurableSpace G
inst✝¹² : TopologicalSpace G
inst✝¹¹ : IsTopologicalGroup G
inst✝¹⁰ : BorelSpace G
inst✝⁹ : PolishSpace G
Γ : Subgroup G
inst✝⁸ : Γ.Normal
inst✝⁷ : T2Space (G ⧸ Γ)
inst✝⁶ : SecondCountableTopology (G ⧸ Γ)
μ : Measure (G ⧸ Γ)
ν : Measure G
inst✝⁵ : ν.IsMulLeftInvariant
inst✝⁴ : Countable ↥Γ
inst✝³ : ν.IsMulRightInvariant
inst✝² : SigmaFinite ν
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SigmaFinite μ
s : Set G
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
V : Set (G ⧸ Γ)
meas_V : MeasurableSet V
neZeroV : μ V ≠ 0
hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)
neTopV : μ V ≠ ∞
U : Set (G ⧸ Γ)
a✝ : MeasurableSet U
meas_π : Measurable QuotientGroup.mk
μ' : Measure (G ⧸ Γ) := map QuotientGroup.mk (ν.restrict s)
⊢ μ U = (map (Quotient.mk (MulAction.orbitRel (↥Γ.op) G)) (ν.restrict s)) U
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: T : ℝ
hT : 0 < T
t : ℝ
μ : Measure ℝ
x : ℝ
this : Bijective (codRestrict (fun n ↦ n • T) ↑(zmultiples T) ⋯)
⊢ ∃! x_1, codRestrict (fun n ↦ n • T) ↑(zmultiples T) ⋯ x_1 +ᵥ x ∈ Ioc t (t + T)

Tactic:
simpa only [add_comm x] using! existsUnique_add_zsmul_mem_Ioc hT x t

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : a₀ < x
⊢ (fun x_1 ↦ if a₀ < x then f x else 0) =ᶠ[𝓝[≥] a₀] fun n ↦ if n < x then f x else 0

Tactic:
filter_upwards [mem_nhdsWithin_of_mem_nhds (Iio_mem_nhds hx)] with a ha using by grind

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a₀

Tactic:
by
  simp_rw [← integral_indicator measurableSet_Iio]
  apply tendsto_integral_filter_of_dominated_convergence ((Iio a₀).indicator (norm ∘ f))
  · filter_upwards [self_mem_nhdsWithin] with a ha
    rw [aestronglyMeasurable_indicator_iff measurableSet_Iio]
    exact (hf.mono_set (Iio_subset_Iio ha)).aestronglyMeasurable
  · filter_upwards [self_mem_nhdsWithin] with a ha
    refine ae_of_all _ fun x ↦ ?_
    rw [norm_indicator_eq_indicator_norm]
    apply indicator_le_indicator_of_subset (Iio_subset_Iio (by grind)) (fun a ↦ norm_nonneg (f a))
  · simpa [integrable_indicator_iff measurableSet_Iio] using! hf.norm
  · refine ae_of_all _ fun x ↦ ?_
    simp only [indicator_apply, mem_Iio]
    by_cases hx : x < a₀ <;> apply tendsto_const_nhds.congr'
    · filter_upwards [mem_nhdsWithin_of_mem_nhds (Ioi_mem_nhds hx)] with a ha using by grind
    · filter_upwards [self_mem_nhdsWithin] with a ha using by grind

Goal state after:
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 ν
⊢ MemLp (fun x ↦ f x.1) p (μ.prod ν)

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

Goal state after:
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 : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg (LT.lt.ne' hT) h_int
ε : ℝ := Int.fract (t / T) * T
⊢ (∫ (x : ℝ) in 0..ε, g x) + ∫ (x : ℝ) in ε..Int.fract (t / T) * T + ⌊t / T⌋ • T, g x ≤
    sSup ((fun t ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0..T, g x

Tactic:
rw [hg.intervalIntegral_add_zsmul_eq ⌊t / T⌋ ε h'_int, hg.intervalIntegral_add_eq ε 0, zero_add,
    add_le_add_iff_right]

Goal state after:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
hT : 0 < T
t : ℝ
h'_int : ∀ (a₁ a₂ : ℝ), IntervalIntegrable g volume a₁ a₂ := intervalIntegrable₀ hg (LT.lt.ne' hT) h_int
ε : ℝ := Int.fract (t / T) * T
⊢ ∫ (x : ℝ) in 0..ε, g x ≤ sSup ((fun t ↦ ∫ (x : ℝ) in 0..t, g x) '' Icc 0 T)
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ ∮ (z : ℂ) in C(c, R), f₁ z = ∮ (z : ℂ) in C(c, R), f₂ z

Tactic:
apply intervalIntegral.integral_congr_ae_restrict
  apply ae_restrict_le_codiscreteWithin measurableSet_uIoc
  simp only [deriv_circleMap, smul_eq_mul, mul_eq_mul_left_iff, mul_eq_zero,
    circleMap_eq_center_iff, hR, Complex.I_ne_zero, or_self, or_false]
  exact codiscreteWithin_mono (by tauto) (circleMap_preimage_codiscrete hR hf)

Goal state after:
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (map (algebraMap F E) p).Splits
hp : Irreducible p
x y : ↑(p.rootSet E)
hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)
⊢ ∃ g, g • x = y

Tactic:
have hy := minpoly.eq_of_irreducible hp (mem_rootSet.mp ((rootsEquivRoots p E).symm y).2).2

Goal state after:
F : Type u_1
inst✝³ : Field F
p : F[X]
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Fact (map (algebraMap F E) p).Splits
hp : Irreducible p
x y : ↑(p.rootSet E)
hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)
hy : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm y)
⊢ ∃ g, g • x = y
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map
        (fun a ↦
          (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t))
              (powersetCard a s)).sum)
        (range (s.card + 1))).sum =
    ∑ j ∈ Finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j)

Tactic:
Finset.sum_eq_multiset_sum,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Multiset R
⊢ (map
        (fun a ↦
          (map ((fun p ↦ (map (fun r ↦ X) p.1).prod * (map (⇑C) p.2).prod) ∘ fun t ↦ (s - t, t))
              (powersetCard a s)).sum)
        (range (s.card + 1))).sum =
    (map (fun j ↦ C (s.esymm j) * X ^ (s.card - j)) (Finset.range (s.card + 1)).val).sum
Module: Mathlib.Topology.Algebra.Polynomial

Goal state before:
pp: R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < p.degree
⊢ ∀ (y : R), ‖eval (p.coeff 0) p‖ ≤ ‖eval y p‖

Tactic:
rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]; simp

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Vieta

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ p.leadingCoeff * (map (fun a ↦ X - C a) p.roots).prod.coeff k =
    p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
mul_assoc

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
⊢ p.leadingCoeff * (map (fun a ↦ X - C a) p.roots).prod.coeff k =
    p.leadingCoeff * ((-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: case refine_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑((finrank ℚ K).choose (finrank ℚ K / 2))⌉₊
this :
  (⋃ f,
      ⋃ (_ : f.natDegree ≤ finrank ℚ K ∧ ∀ (i : ℕ), f.coeff i ∈ Icc (-↑C) ↑C),
        ↑(map (algebraMap ℤ K) f).roots.toFinset).Finite
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ (minpoly ℚ x).natDegree ≤ finrank ℚ K

Tactic:
exact minpoly.natDegree_le x

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

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

Goal state after:
case inr
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a₁ a₂ b₁ b₂ : ℝ
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]])
Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume
this :
  ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
    ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) →
      (∀ x ∈ Set.Ioo (min a₁ b₁) (max b₁ a₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x) →
        (∀ x ∈ Set.Ioo (min a₁ b₁) (max b₁ a₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x) →
          IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]]) volume →
            b₁ ≤ a₁ →
              ∫ (x : ℝ) in b₁..a₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) =
                (((∫ (x : ℝ) in b₁..a₁, g (x, b₂)) - ∫ (x : ℝ) in b₁..a₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (a₁, y)) -
                  ∫ (y : ℝ) in a₂..b₂, f (b₁, y)
h₁ : ¬a₁ ≤ b₁
⊢ ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (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)
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₀ˣ
hx : x ≠ 1
k : K
hk : (restrict₀ (ofClass v)) k = ↑x
h0 : v k ≠ 0
⊢ False

Tactic:
have h1 : v k ≠ 1 := by
      apply_fun embedding at hk
      simp only [embedding_restrict₀, MonoidWithZeroHom.coe_ofClass] at hk
      apply_fun Units.val at hx using
          Units.val_injective (α := (MonoidWithZeroHom.ofClass v).ValueGroup₀)
      intro h
      apply_fun embedding at hx using embedding_injective (f := .ofClass v)
      simp [← hk, h] at hx

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₀ˣ
hx : x ≠ 1
k : K
hk : (restrict₀ (ofClass v)) k = ↑x
h0 : v k ≠ 0
h1 : v k ≠ 1
⊢ False
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case empty
M : Type u_1
ι : Type u_2
inst✝² : SeminormedCommGroup M
inst✝¹ : IsUltrametricDist M
inst✝ : Nonempty ι
f : ι → M
inhabited_h : Inhabited ι
⊢ ∃ i, (0 ≠ 0 → i ∈ 0) ∧ ‖(Multiset.map f 0).prod‖ ≤ ‖f i‖

Tactic:
| empty =>

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
⊢ ‖∏' (i : ι), f i‖₊ ≤ ⨆ i, ‖f i‖₊

Tactic:
by
  simpa only [← NNReal.coe_le_coe, coe_nnnorm', coe_iSup] using norm_tprod_le f

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case empty
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
hs : (↑∅).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
⊢ ‖∏ i ∈ ∅, f i‖₊ = ∅.sup fun i ↦ ‖f i‖₊

Tactic:
| empty =>

Goal state after: