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
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : t.Nonempty
⊢ ∃ f u, f ≠ 0 ∧ (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b)

Tactic:
have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
  obtain ⟨f, u, hfne, hA', hB'⟩ :=
    _root_.geometric_hahn_banach_of_nonempty_interior hs ht hst hsint htne
  refine ⟨f.extendRCLikeₗ, u, fun hzero ↦ ?_, ?_, ?_⟩
  · exact hfne <| (StrongDual.extendRCLikeₗ (𝕜 := 𝕜)).injective (by simpa using hzero)
  · simpa [f.extendRCLikeₗ_apply] using hA'
  · simpa [f.extendRCLikeₗ_apply] using hB'

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
r ε : ℝ
L : F
x : ℝ
hx : x ∈ A f L r ε
y z : ℝ
hy : y ∈ Icc x (x + r / 2)
hz : z ∈ Icc x (x + r / 2)
⊢ ‖f z - f y - (z - y) • L‖ ≤ ε * r

Tactic:
rcases hx with ⟨r', r'mem, hr'⟩
  have A : x + r / 2 ≤ x + r' := by linarith [r'mem.1]
  exact hr' _ ((Icc_subset_Icc le_rfl A) hy) _ ((Icc_subset_Icc le_rfl A) hz)

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁵ : Zero X
inst✝⁴ : Zero Y
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace R
f : C(X, Y)₀
⊢ Continuous fun g ↦ g.comp f

Tactic:
continuous_induced_rng

Goal state after:
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁵ : Zero X
inst✝⁴ : Zero Y
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace R
f : C(X, Y)₀
⊢ Continuous (_root_.toContinuousMap ∘ fun g ↦ g.comp f)
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁵ : Zero X
inst✝⁴ : Zero Y
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace R
g : C(Y, R)₀
⊢ Continuous (_root_.toContinuousMap ∘ g.comp)

Tactic:
exact g.toContinuousMap.continuous_postcomp |>.comp <|
    ContinuousMapZero.isEmbedding_toContinuousMap.continuous

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

Goal state before:
pp: X✝ : Type u_1
R✝ : Type u_2
inst✝⁷ : Zero X✝
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace R✝
X : Type u_3
R : Type u_4
inst✝⁴ : Zero X
inst✝³ : TopologicalSpace X
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous fun a ↦ -a

Tactic:
continuous_induced_rng

Goal state after:
X✝ : Type u_1
R✝ : Type u_2
inst✝⁷ : Zero X✝
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace R✝
X : Type u_3
R : Type u_4
inst✝⁴ : Zero X
inst✝³ : TopologicalSpace X
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous (_root_.toContinuousMap ∘ fun a ↦ -a)
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_4
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⦄,
    f_1 =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g →
      Integrable f_1 (μ.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 ∂μ

Tactic:
· intro u v huv _ hu
    rw [← integral_congr_ae huv, hu]
    apply integral_congr_ae
    filter_upwards [(ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 huv] with x hx
    rcases eq_or_ne (f x) 0 with (h'x | h'x)
    · simp only [h'x, zero_smul]
    · rw [hx _]
      simpa only [Ne, ENNReal.coe_eq_zero] using h'x

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun n ↦ F n x) l (𝓝 (f x))
⊢ Tendsto (fun n ↦ ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))

Tactic:
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc,
    ← ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *

Goal state after:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound x
bound_integrable : IntegrableOn bound (Ι a b) μ
h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Tendsto (fun n ↦ F n x) l (𝓝 (f x))
⊢ Tendsto (fun n ↦ (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, F n x ∂μ) l
    (𝓝 ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ))
Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: case neg
ι : 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
⊢ HasSum (fun i ↦ ∫ (x : ℝ) in a..b, (f i) x) (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x)

Tactic:
simp [intervalIntegral, integral, hE, hasSum_zero]

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
this✝¹ : MeasurableSpace F := borel F
this✝ : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ closure (Ioi x ∩ closure t) ⊆ closure (closure (Ioi x ∩ t))

Tactic:
apply closure_mono
      simpa [inter_comm] using (isOpen_Ioi (a := x)).closure_inter (s := t)

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
μ : Measure ℝ
h : ¬IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0

Tactic:
rw [intervalIntegrable_iff] at h

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntegrableOn f (Ι a b) μ
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Iio b, f x ∂μ - ∫ (x : ℝ) in Iio a, f x ∂μ = ∫ (x : ℝ) in Ico a b, f x ∂μ

Tactic:
have ha : IntegrableOn f (Iio a) μ := hf.mono_set (Iio_subset_Iio hab)
  have h : IntegrableOn f (Ico a b) μ := hf.mono_set Ico_subset_Iio_self
  rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h,
      Iio_union_Ico_eq_Iio hab]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:

Tactic:
‖f d‖ - ‖f c‖ ≤ ‖f d - f c‖ := norm_sub_norm_le _ _
    _ = ‖∫ x in c..d, deriv f x‖ := congr_arg _ (integral_deriv_eq_sub hfd hfi).symm
    _ = ‖∫ x in Ι c d, deriv f x‖ := norm_integral_eq_norm_integral_uIoc _
    _ ≤ ∫ x in Ι c d, ‖deriv f x‖ := norm_integral_le_integral_norm _
    _ ≤ ∫ x in Ι c d, C * ‖g x‖ :=
      setIntegral_mono_on hfi.norm.def' (hgi.mono_set hsub') measurableSet_uIoc hg
    _ ≤ ∫ x in k, C * ‖g x‖ := by
      apply setIntegral_mono_set hgi
        (ae_of_all _ fun x => mul_nonneg hC₀ (norm_nonneg _)) hsub'.eventuallyLE

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

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : FloorRing α
inst✝ : IsStrictOrderedRing α
b : ℤ
⊢ ⌈↑(b - 1)⌉ ≤ b

Tactic:
rw [ceil_intCast]

Goal state after:
α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : FloorRing α
inst✝ : IsStrictOrderedRing α
b : ℤ
⊢ b - 1 ≤ b
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: case ctop
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 ⧸ Γ)
inst✝⁵ : Countable ↥Γ
ν : Measure G
inst✝⁴ : ν.IsHaarMeasure
inst✝³ : ν.IsMulRightInvariant
inst✝² : LocallyCompactSpace G
inst✝¹ : QuotientMeasureEqMeasurePreimage ν μ
inst✝ : IsFiniteMeasure μ
K : PositiveCompacts G
K' : PositiveCompacts (G ⧸ Γ) := ⋯
this : μ.IsMulLeftInvariant
s : Set G
finiteCovol : ν s ≠ ∞
fund_dom_s : IsFundamentalDomain (↥Γ.op) s ν
⊢ ν (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' ↑K' ∩ s) ≠ ∞

Tactic:
· change ν (π ⁻¹' (π '' K) ∩ s) ≠ ⊤
    apply ne_of_lt
    refine lt_of_le_of_lt ?_ finiteCovol.lt_top
    apply measure_mono
    exact inter_subset_right

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Quotient

Goal state before:
pp: case neTopV
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 ⧸ Γ)
inst✝³ : Countable ↥Γ
ν : Measure G
inst✝² : ν.IsHaarMeasure
inst✝¹ : ν.IsMulRightInvariant
inst✝ : SigmaFinite ν
K : PositiveCompacts (G ⧸ Γ)
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_finite : ν 𝓕 ≠ ∞
c : ℝ≥0∞ := ⋯
c_ne_top : c ≠ ∞
μ : Measure (G ⧸ Γ) := ⋯
hμK : μ ↑K = c
this : SigmaFinite μ
⊢ μ ↑K ≠ ∞

Tactic:
rw [hμK]
    exact c_ne_top

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

Goal state before:
pp: E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
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)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
⊢ IntervalIntegrable f volume (a 0) (t + ↑n₂ * T)

Tactic:
(by simp [a] : t + n₂ * T = a (n₁ + n₂))

Goal state after:
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
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)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
⊢ IntervalIntegrable f volume (a 0) (a (n₁ + n₂))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case e'_4
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
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)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ f = fun x ↦ f (x - (↑k - ↑n₁) * T)

pp: case e'_7
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
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)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ a (k + 1) = t + T + (↑k - ↑n₁) * T

Tactic:
· funext x
    simpa using (h₁f.sub_int_mul_eq (k - n₁)).symm

Goal state after:
case e'_7
E✝ : Type u_1
inst✝¹ : NormedAddCommGroup E✝
f✝ : ℝ → E✝
T✝ : ℝ
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)
a₁ a₂ : ℝ
hT : 0 < T
n₁ : ℕ
hn₁ : (t - min a₁ a₂) / T ≤ ↑n₁
n₂ : ℕ
hn₂ : (max a₁ a₂ - t) / T ≤ ↑n₂
this : uIcc a₁ a₂ ⊆ uIcc (t - ↑n₁ * T) (t + ↑n₂ * T)
a : ℕ → ℝ := fun n ↦ t + (↑n - ↑n₁) * T
k : ℕ
hk : k < n₁ + n₂
⊢ a (k + 1) = t + T + (↑k - ↑n₁) * T
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)
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
⊢ ∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ + ∫ (_t : ℝ) in Icc a b, δ ∂μ =
    (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b)

Tactic:
simp [mul_comm]

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 ν
hf' : MemLp f p (ν Set.univ • μ)
⊢ MemLp f p (Measure.map Prod.fst (μ.prod ν))

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 ν
hf' : MemLp f p (ν Set.univ • μ)
⊢ AEStronglyMeasurable f (Measure.map Prod.fst (μ.prod ν))

Tactic:
· simpa using hf'

Goal state after:
α : 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 ν
hf' : MemLp f p (ν Set.univ • μ)
⊢ AEStronglyMeasurable f (Measure.map Prod.fst (μ.prod ν))
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 ν
hf' : MemLp f p (μ Set.univ • ν)
⊢ MemLp f p (Measure.map Prod.snd (μ.prod ν))

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 ν
hf' : MemLp f p (μ Set.univ • ν)
⊢ AEStronglyMeasurable f (Measure.map Prod.snd (μ.prod ν))

Tactic:
· simpa using hf'

Goal state after:
α : 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 ν
hf' : MemLp f p (μ Set.univ • ν)
⊢ AEStronglyMeasurable f (Measure.map Prod.snd (μ.prod ν))
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

Goal state after:
c : ℂ
R : ℝ
f₁ f₂ : ℂ → ℂ
hf : f₁ =ᶠ[codiscreteWithin (sphere c |R|)] f₂
hR : R ≠ 0
⊢ (fun x ↦ deriv (circleMap c R) x • (fun z ↦ f₁ z) (circleMap c R x)) =ᵐ[volume.restrict (Ι 0 (2 * π))] fun x ↦
    deriv (circleMap c R) x • (fun z ↦ f₂ z) (circleMap c R x)
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧ ∫⁻ (a : α), ‖∫ (y : β), ‖f (a, y)‖ ∂ν‖ₑ ∂μ < ∞

Tactic:
have (x : _) : ∀ᵐ y ∂ν, 0 ≤ ‖f (x, y)‖ := by filter_upwards with y using norm_nonneg _

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧ ∫⁻ (a : α), ‖∫ (y : β), ‖f (a, y)‖ ∂ν‖ₑ ∂μ < ∞
Module: Mathlib.MeasureTheory.Integral.Prod

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

Tactic:
exact le_abs_self _

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

Goal state before:
pp: E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
⊢ ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν

Tactic:
have : Fact (μ U < ∞) := ⟨(IsCompact.image h'f continuous_fst).measure_lt_top⟩

Goal state after:
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace X
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace X
inst✝² : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this : Fact (μ U < ∞)
⊢ ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
Module: Mathlib.FieldTheory.PolynomialGaloisGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p * q = 0
⊢ Unique (p * q).Gal

Tactic:
rw [hpq]

Goal state after:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : p * q = 0
⊢ Unique (Gal 0)
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case inl
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

pp: case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a

Tactic:
· simp only [uIcc_of_le hab, min_eq_left hab, max_eq_right hab] at *
    exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi

Goal state after:
case inr
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' : ℝ → E
a b : ℝ
s : Set ℝ
hs : s.Countable
Hc : ContinuousOn f [[a, b]]
Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x
Hi : IntervalIntegrable f' volume a b
hab : b ≤ a
⊢ ∫ (x : ℝ) in a..b, f' x = f b - f a
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
⊢ AnalyticOn ℂ f univ ↔ Differentiable ℂ f

Tactic:
rw [analyticOn_univ]

Goal state after:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f
Module: Mathlib.MeasureTheory.Integral.DivergenceTheorem

Goal state before:
pp: case refine_5
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
x : ℝ × ℝ
⊢ (f' x) (1, 0) + (g' x) (0, 1) = ∑ i, (![f', g'] i x) (e.symm (Pi.single i 1))

Tactic:
rw [Fin.sum_univ_two]

Goal state after:
case refine_5
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ × ℝ → E
f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E
a b : ℝ × ℝ
hle : a ≤ b
s : Set (ℝ × ℝ)
hs : s.Countable
Hcf : ContinuousOn f (Set.Icc a b)
Hcg : ContinuousOn g (Set.Icc a b)
Hdf : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x
Hdg : ∀ x ∈ Set.Ioo a.1 b.1 ×ˢ Set.Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x
Hi : IntegrableOn (fun x ↦ (f' x) (1, 0) + (g' x) (0, 1)) (Set.Icc a b) volume
e : (ℝ × ℝ) ≃L[ℝ] Fin 2 → ℝ := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm
x : ℝ × ℝ
⊢ (f' x) (1, 0) + (g' x) (0, 1) = (![f', g'] 0 x) (e.symm (Pi.single 0 1)) + (![f', g'] 1 x) (e.symm (Pi.single 1 1))