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

Goal state before:
pp: case mp
R : Type u_1
V : Type u_2
inst✝⁹ : Field R
inst✝⁸ : AddCommGroup V
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : Module R V
inst✝³ : SeparatingDual R V
W : Type u_3
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : FiniteDimensional R W
f : W →ₗ[R] V
hf : Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)
⊢ Injective ⇑f

pp: case mpr
R : Type u_1
V : Type u_2
inst✝⁹ : Field R
inst✝⁸ : AddCommGroup V
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : Module R V
inst✝³ : SeparatingDual R V
W : Type u_3
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : FiniteDimensional R W
f : W →ₗ[R] V
hf : Injective ⇑f
⊢ Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)

Tactic:
· exact LinearMap.dualMap_surjective_iff.mp hf.of_comp

Goal state after:
case mpr
R : Type u_1
V : Type u_2
inst✝⁹ : Field R
inst✝⁸ : AddCommGroup V
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : Module R V
inst✝³ : SeparatingDual R V
W : Type u_3
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : FiniteDimensional R W
f : W →ₗ[R] V
hf : Injective ⇑f
⊢ Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap)
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝¹⁵ : Field R
inst✝¹⁴ : AddCommGroup V
inst✝¹³ : TopologicalSpace R
inst✝¹² : TopologicalSpace V
inst✝¹¹ : IsTopologicalRing R
inst✝¹⁰ : Module R V
inst✝⁹ : SeparatingDual R V
inst✝⁸ : IsTopologicalAddGroup V
inst✝⁷ : ContinuousSMul R V
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S V
inst✝⁴ : SMulCommClass R S V
inst✝³ : Algebra S R
inst✝² : IsScalarTower S R V
inst✝¹ : ContinuousConstSMul S V
inst✝ : Algebra.IsCentral S R
f : V →L[R] V
hf : f ∈ Subalgebra.center S (V →L[R] V)
⊢ ∃ α ∈ Subalgebra.center S R, f = α • ContinuousLinearMap.id R V

Tactic:
nontriviality V

Goal state after:
R : Type u_1
V : Type u_2
inst✝¹⁵ : Field R
inst✝¹⁴ : AddCommGroup V
inst✝¹³ : TopologicalSpace R
inst✝¹² : TopologicalSpace V
inst✝¹¹ : IsTopologicalRing R
inst✝¹⁰ : Module R V
inst✝⁹ : SeparatingDual R V
inst✝⁸ : IsTopologicalAddGroup V
inst✝⁷ : ContinuousSMul R V
S : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S V
inst✝⁴ : SMulCommClass R S V
inst✝³ : Algebra S R
inst✝² : IsScalarTower S R V
inst✝¹ : ContinuousConstSMul S V
inst✝ : Algebra.IsCentral S R
f : V →L[R] V
hf : f ∈ Subalgebra.center S (V →L[R] V)
a✝ : Nontrivial V
⊢ ∃ α ∈ Subalgebra.center S R, f = α • ContinuousLinearMap.id R V
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
⊢ ⇑g.conjContinuousAlgEquiv = ⇑f.conjContinuousAlgEquiv ↔ ∃ α, f = α • g

Tactic:
funext_iff,

Goal state after:
R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
⊢ (∀ (x : V →L[R] V), g.conjContinuousAlgEquiv x = f.conjContinuousAlgEquiv x) ↔ ∃ α, f = α • g
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case pos
𝕜 : 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, (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b)

Tactic:
have hsep :
        ∃ (f : StrongDual 𝕜 E) (u : ℝ),
          f ≠ 0 ∧ (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b) :=
        geometric_hahn_banach_of_nonempty_interior hs ht hst hsint htne

Goal state after:
case pos
𝕜 : 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
hsep : ∃ f u, f ≠ 0 ∧ (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b)
⊢ ∃ f u, (∀ a ∈ s, re (f a) ≤ u) ∧ ∀ b ∈ t, u ≤ re (f b)
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this : (fun x' ↦ f x' - f x - (x' - x) • derivWithin f (Ici x) x) =o[𝓝[≥] x] fun x' ↦ x' - x
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε

Tactic:
isLittleO_iff

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
ε : ℝ
hε : 0 < ε
x : ℝ
hx : DifferentiableWithinAt ℝ f (Ici x) x
this : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x_1 : ℝ) in 𝓝[≥] x, ‖f x_1 - f x - (x_1 - x) • derivWithin f (Ici x) x‖ ≤ c * ‖x_1 - x‖
⊢ ∃ R > 0, ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ε
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✝ : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : StrongDual 𝕜 E), ∃ y ∈ s✝, re (i x) ≤ re (i y)}
h : x ∉ s✝
l : StrongDual 𝕜 E
s : ℝ
hlA : ∀ a ∈ s✝, re (l a) < s
hl : s < re (l x)
y : E
hy : y ∈ s✝
hxy : re (l x) ≤ re (l y)
⊢ False

Tactic:
exact ((hxy.trans_lt (hlA y hy)).trans hl).false

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

Goal state before:
pp: X : Type u_1
E : Type u_3
inst✝³ : MeasurableSpace X
μ : Measure X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : X → ℝ≥0∞
s : Set X
hf : AEMeasurable f (μ.restrict s)
hf_top : ∀ᵐ (x : X) ∂μ.restrict s, f x < ∞
g : X → E
⊢ ∫ (x : X) in s, g x ∂μ.withDensity f = ∫ (x : X) in s, (f x).toReal • g x ∂μ

Tactic:
by
  rw [restrict_withDensity' s, integral_withDensity_eq_integral_toReal_smul₀ hf hf_top]

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

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

Tactic:
revert hint
  refine Nat.le_induction ?_ ?_ n hmn
  · simp
  · intro p hp IH h
    exact (IH fun k hk => h k (Ico_subset_Ico_right p.le_succ hk)).trans (h p (by simp [hp]))

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
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
⊢ ∫ (x : ℝ) in Icc t u, y ≤ ∫ (w : ℝ) in t..u, (G' w).toReal

Tactic:
intervalIntegral.integral_of_le hu.1.le,

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
⊢ ∫ (x : ℝ) in Icc t u, y ≤ ∫ (x : ℝ) in Ioc t u, (G' x).toReal ∂volume
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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

Tactic:
ext p

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s t : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
K : Set (E →L[𝕜] F)
H : IsOpen[instTopologicalSpaceProd] (⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s t})
p : α × E
⊢ p ∈ {p | p.2 ∈ B (f p.1) K r s t} ↔ p ∈ ⋃ L ∈ K, {p | p.2 ∈ A (f p.1) L r t ∧ p.2 ∈ A (f p.1) L s 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)
A : ∀ᶠ (δ : ℝ) in 𝓝[>] 0, δ ∈ Ioo 0 1
B : ∀ᶠ (δ : ℝ) in 𝓝 0, Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
C : ∀ᶠ (δ : ℝ) in 𝓝 0, (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
δ : ℝ
hδ : δ ∈ Ioo 0 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
⊢ ∃ δ,
    0 < δ ∧
      δ < 1 ∧ Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b ∧ (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε

Tactic:
exact ⟨δ, hδ.1, hδ.2, h'δ, h''δ⟩

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 ℝ
hf : IntegrableOn f (Ici a) μ
hab : a ≤ b
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in Ico a b, f x ∂μ

Tactic:
have ha : IntegrableOn f (Ici b) μ := hf.mono_set (Ici_subset_Ici.2 hab)

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ici a) μ
hab : a ≤ b
ha : IntegrableOn f (Ici b) μ
⊢ ∫ (x : ℝ) in Ici a, f x ∂μ - ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ) in Ico a b, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: f : ℝ → ℝ
a b : ℝ
hfi : IntervalIntegrable f volume a b
hpos : ∀ x ∈ Ioo a b, 0 < f x
hab : a < b
hsupp : Ioo a b ⊆ support f ∩ Ioc a b
⊢ ∀ᵐ (x : ℝ), x ∈ Ioo a b → 0 x ≤ f x

Tactic:
filter_upwards with x hx using (hpos x hx).le

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 : ℤ
⊢ ContinuousAt (uncurry f ∘ Prod.map id fract) (s, ↑n)

Tactic:
rw [ContinuousAt, nhds_prod_eq, ← nhdsLT_sup_nhdsGE (n : α), prod_sup, tendsto_sup]
    constructor
    · refine (((h (s, 1) ⟨trivial, zero_le_one, le_rfl⟩).tendsto.mono_left ?_).comp
        (tendsto_id.prodMap (tendsto_fract_left _))).mono_right (le_of_eq ?_)
      · rw [nhdsWithin_prod_eq, nhdsWithin_univ, ← nhdsWithin_Ico_eq_nhdsLT one_pos]
        exact Filter.prod_mono le_rfl (nhdsWithin_mono _ Ico_subset_Icc_self)
      · simp [hf]
    · refine (((h (s, 0) ⟨trivial, le_rfl, zero_le_one⟩).tendsto.mono_left <| le_of_eq ?_).comp
        (tendsto_id.prodMap (tendsto_fract_right _))).mono_right (le_of_eq ?_) <;>
        simp [nhdsWithin_prod_eq, nhdsWithin_univ]

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

Goal state before:

Tactic:
max a₁ a₂
      _ ≤ t + n₂ * T := by linarith [(div_le_iff₀ hT).1 hn₂]
      _ ≤ max (t - n₁ * T) (t + n₂ * T) := by apply le_max_right

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 (Ioi a₀) μ
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀) a₀

Tactic:
by
  simp_rw [← integral_indicator measurableSet_Ioi]
  apply tendsto_integral_filter_of_dominated_convergence ((Ioi a₀).indicator (norm ∘ f))
  · filter_upwards [self_mem_nhdsWithin] with a ha
    rw [aestronglyMeasurable_indicator_iff measurableSet_Ioi]
    exact (hf.mono_set (Ioi_subset_Ioi 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 (Ioi_subset_Ioi (by grind)) (fun a ↦ norm_nonneg (f a))
  · simpa [integrable_indicator_iff measurableSet_Ioi] using! hf.norm
  · refine ae_of_all _ fun x ↦ ?_
    simp only [indicator_apply, mem_Ioi]
    by_cases hx : a₀ < x <;> apply tendsto_const_nhds.congr'
    · filter_upwards [mem_nhdsWithin_of_mem_nhds (Iio_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.Integral.Prod

Goal state before:
pp: case pos
α : 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 ν)
hE : CompleteSpace E
⊢ ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ

Tactic:
revert f

Goal state after:
case pos
α : 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 μ
hE : CompleteSpace E
⊢ ∀ (f : α × β → E), Integrable f (μ.prod ν) → ∫ (z : α × β), f z ∂μ.prod ν = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (↑x + ↑y * I)) 1 - (f' (↑x + ↑y * I)) I

Tactic:
have he : ∀ x y : ℝ, ↑x + ↑y * I = e (x, y) := fun x y => (mk_eq_add_mul_I x y).symm

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he : ∀ (x y : ℝ), ↑x + ↑y * I = e (x, y)
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (↑x + ↑y * I)) 1 - (f' (↑x + ↑y * I)) I
Module: Mathlib.MeasureTheory.Integral.Prod

Goal state before:
pp: case neg
α : 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 μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (fun z ↦ f z.1 • g z.2) (μ.prod ν)
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν

Tactic:
have H : ¬Integrable f μ ∨ ¬Integrable g ν := by
    contrapose! h
    exact h.1.smul_prod h.2

Goal state after:
case neg
α : 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 μ
𝕜 : Type u_5
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hE : CompleteSpace E
h : ¬Integrable (fun z ↦ f z.1 • g z.2) (μ.prod ν)
H : ¬Integrable f μ ∨ ¬Integrable g ν
⊢ ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν
Module: Mathlib.Analysis.Complex.CauchyIntegral

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p ↦ f' (e p) ∘SL ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
htd : ∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t, HasFDerivAt F (F' p) p
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        ∫ (x : ℝ) in z.im..w.im, I • f (e (w.re, x))) -
      ∫ (x : ℝ) in z.im..w.im, I • f (e (z.re, x)) =
    ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I

Tactic:
intervalIntegral.integral_symm w.im z.im,

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
f' : ℂ → ℂ →L[ℝ] E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[w.im, z.im]])
Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min w.im z.im) (max w.im z.im) \ s, HasFDerivAt f (f' x) x
Hi : IntegrableOn (fun z ↦ I • (f' z) 1 - (f' z) I) ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) volume
e : (ℝ × ℝ) ≃L[ℝ] ℂ := equivRealProdCLM.symm
he₁ : e (1, 0) = 1
he₂ : e (0, 1) = I
he : ∀ (x y : ℝ), True
F : ℝ × ℝ → E := f ∘ ⇑e
F' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fun p ↦ f' (e p) ∘SL ↑e
hF' : ∀ (p : ℝ × ℝ), (-(I • F' p)) (1, 0) + (F' p) (0, 1) = -(I • (f' (e p)) 1 - (f' (e p)) I)
R : Set (ℝ × ℝ) := [[z.re, w.re]] ×ˢ [[w.im, z.im]]
t : Set (ℝ × ℝ) := ⇑e ⁻¹' s
hR : ⇑e ⁻¹' ([[z.re, w.re]] ×ℂ [[w.im, z.im]]) = R
htc : ContinuousOn F R
htd : ∀ p ∈ Ioo (min z.re w.re) (max z.re w.re) ×ˢ Ioo (min w.im z.im) (max w.im z.im) \ t, HasFDerivAt F (F' p) p
⊢ (((∫ (x : ℝ) in z.re..w.re, f (e (x, z.im))) - ∫ (x : ℝ) in z.re..w.re, f (e (x, w.im))) +
        -∫ (x : ℝ) in w.im..z.im, I • f (e (w.re, x))) -
      -∫ (x : ℝ) in w.im..z.im, I • f (e (z.re, x)) =
    ∫ (x : ℝ) in z.re..w.re, -∫ (y : ℝ) in w.im..z.im, I • (f' (e (x, y))) 1 - (f' (e (x, y))) I
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)
this✝ : Fact (μ U < ∞)
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (ν V < ∞)
⊢ ∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ = ∫ (y : Y) in V, ∫ (x : X) in U, f x y ∂μ ∂ν

Tactic:
by
    apply integral_integral_swap
    apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
    refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
    obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
    exact .of_bounded (C := C) (.of_forall hC)

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
ϕ : Gal(E/F)
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ϕ ↑((rootsEquivRoots p E) ((rootsEquivRoots p E).symm x)) = ϕ ↑x

Tactic:
Equiv.apply_symm_apply (rootsEquivRoots p E)

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
ϕ : Gal(E/F)
x : ↑(p.rootSet E)
ψ : p.SplittingField ≃ₐ[F] ↥(IsScalarTower.toAlgHom F p.SplittingField E).range :=
  AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F p.SplittingField E)
⊢ ϕ ↑x = ϕ ↑x