mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : G ≃ₗᵢ[𝕜] E
f : E → F
x : G
i : ℕ
⊢ ‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ (g x)‖

Tactic:
apply g.norm_iteratedFDerivWithin_comp_right f uniqueDiffOn_univ (mem_univ (g x)) i

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : ↑m ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m) f (insert a s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
t : Set E
ht : t ⊆ s ∩ U
⊢ HasFTaylorSeriesUpToOn (↑m) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)

Tactic:
insert_eq_of_mem ha

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ∞ω
f : E → F
s : Set E
a : E
h : ContDiffWithinAt 𝕜 n f s a
hs : UniqueDiffOn 𝕜 s
ha : a ∈ s
m : ℕ
hm : ↑m ≤ n
U : Set E
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
haU : a ∈ U
hfU : ContDiffOn 𝕜 (↑m) f (s ∩ U)
this : ∀ᶠ (t : Set E) in (𝓝[s] a).smallSets, t ⊆ s ∩ U
t : Set E
ht : t ⊆ s ∩ U
⊢ HasFTaylorSeriesUpToOn (↑m) f (ftaylorSeriesWithin 𝕜 f s) (s ∩ U)
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}
ht : ∃ a, ∀ (b : ℕ), a ≤ b → f b ∈ t
⊢ ∃ i, ∀ j ≥ i, ‖f j - f i‖ < ε

Tactic:
obtain ⟨N, hN⟩ := ht

Goal state after:
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
⊢ ∃ i, ∀ j ≥ i, ‖f j - f i‖ < ε
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: case cons
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
    iteratedFDerivWithin 𝕜 i (fun x ↦ ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ∀ j ∈ Finset.cons a u ha, ContDiffWithinAt 𝕜 (↑i) (f j) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x ↦ ∑ j ∈ Finset.cons a u ha, f j x) s x =
    ∑ j ∈ Finset.cons a u ha, iteratedFDerivWithin 𝕜 i (f j) s x

Tactic:
simp only [Finset.mem_cons, forall_eq_or_imp] at h

Goal state after:
case cons
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
    iteratedFDerivWithin 𝕜 i (fun x ↦ ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffWithinAt 𝕜 (↑i) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i) (f a) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x ↦ ∑ j ∈ Finset.cons a u ha, f j x) s x =
    ∑ j ∈ Finset.cons a u ha, iteratedFDerivWithin 𝕜 i (f j) s x
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
f g : 𝕜 → F
hf : ContDiffAt 𝕜 (↑n) f x
hg : ContDiffAt 𝕜 (↑n) g x
⊢ iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x

Tactic:
by
  simpa only [iteratedDerivWithin_univ] using
    iteratedDerivWithin_sub (Set.mem_univ _) uniqueDiffOn_univ hf hg

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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : {x | (fun x ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∉ s
⊢ ↑(f x) < (fun x ↦ g0 x + g1 x) x

Tactic:
have : f x = fmeas.mk f x := by rw [Set.compl_subset_comm] at hs; exact hs h

Goal state after:
case neg
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this✝ : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : {x | (fun x ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∉ s
this : f x = AEMeasurable.mk f fmeas x
⊢ ↑(f x) < (fun x ↦ g0 x + g1 x) x
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
S : Submodule R M := { carrier := ↑C - ↑C, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ x ∈ ↑C - ↑C

Tactic:
have hCS : (C : Set M) ⊆ S := fun x hx ↦
    let ⟨c, hc⟩ := hne; ⟨x + c, C.add_mem hx hc, c, hc, add_sub_cancel_right x c⟩

Goal state after:
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
S : Submodule R M := { carrier := ↑C - ↑C, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hCS : ↑C ⊆ ↑S
⊢ x ∈ ↑C - ↑C
Module: Mathlib.Geometry.Convex.Cone.Pointed

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
s : Set (Submodule R E)
⊢ ↑(sSup s) = ⨆ S ∈ s, ↑S

Tactic:
ofSubmodule_sSup,

Goal state after:
R : Type u_1
E : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
s : Set (Submodule R E)
⊢ sSup (ofSubmodule '' s) = ⨆ S ∈ s, ↑S
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case refine_1
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ (HAdd.hAdd 1 / HSub.hSub 1) y ≠ 0

pp: case refine_2
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ 1 / 2 * ((1 * (1 - y) - (1 + y) * -1) / (1 - y) ^ 2 / (HAdd.hAdd 1 / HSub.hSub 1) y) -
      ∑ i ∈ Finset.range n, ↑(2 * i + 1) * y ^ (2 * i + 1 - 1) / (2 * ↑i + 1) =
    (y ^ 2) ^ n / (1 - y ^ 2)

Tactic:
· simp only [div_ne_zero_iff, Pi.div_apply]; grind

Goal state after:
case refine_2
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ 1 / 2 * ((1 * (1 - y) - (1 + y) * -1) / (1 - y) ^ 2 / (HAdd.hAdd 1 / HSub.hSub 1) y) -
      ∑ i ∈ Finset.range n, ↑(2 * i + 1) * y ^ (2 * i + 1 - 1) / (2 * ↑i + 1) =
    (y ^ 2) ^ n / (1 - y ^ 2)
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
⊢ r • (r⁻¹ • x + y) ∈ s

Tactic:
smul_add,

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
f : E →ₗ.[ℝ] ℝ
nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x
dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
c : ℝ
le_c : ∀ (x : ↥f.domain), -↑x - y ∈ s → ↑f x ≤ c
c_le : ∀ (x : ↥f.domain), ↑x + y ∈ s → c ≤ ↑f x
x : E
hx : x ∈ f.domain
r : ℝ
hy' : r • y ∈ (LinearPMap.mkSpanSingleton y (-c) ⋯).domain
hz : x + r • y ∈ (f.supSpanSingleton y (-c) hy).domain
hzs : x + r • y ∈ s
hr : 0 < r
⊢ r • r⁻¹ • x + r • y ∈ s
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
⊢ x ∈ {x | gauge s x ≤ a} ↔ ∀ (i : ℝ), a < i → x ∈ i • s

Tactic:
Set.mem_ofPred_eq

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
⊢ gauge s x ≤ a ↔ ∀ (i : ℝ), a < i → x ∈ i • s
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr.mpr
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
α : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : MulActionWithZero α ℝ
inst✝² : IsStrictOrderedModule α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s

Tactic:
have := smul_pos ha' hr

Goal state after:
case inr.mpr
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℝ E
α : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : MulActionWithZero α ℝ
inst✝² : IsStrictOrderedModule α ℝ
inst✝¹ : MulActionWithZero α E
inst✝ : IsScalarTower α ℝ (Set E)
s : Set E
a : α
ha : 0 ≤ a
x : E
ha' : 0 < a
r : ℝ
hr : 0 < r
hx : x ∈ r • s
this : 0 < a • r
⊢ 0 < a • r ∧ (a • r)⁻¹ • a • x ∈ s
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_2
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
this : ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ gauge s x
⊢ ∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1

pp: case refine_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
⊢ ∀ (x : ↥f.domain), ↑f x ≤ gauge s ↑x

Tactic:
· obtain ⟨φ, hφ₁, hφ₂⟩ := this
    have hφ₃ : φ x₀ = 1 := by
      rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁,
        LinearPMap.mkSpanSingleton'_apply_self]
    have hφ₄ : ∀ x ∈ s, φ x < 1 := fun x hx =>
      (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_isOpen hs₂ hx)
    refine ⟨⟨φ, ?_⟩, hφ₃, hφ₄⟩
    refine
      φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩)
        (vadd_set_subset_iff.mpr fun x hx => ?_)
    change φ (-x₀ + x) ≠ 0
    rw [map_add, map_neg]
    specialize hφ₄ x hx
    linarith

Goal state after:
case refine_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : x₀ ∉ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 ⋯
⊢ ∀ (x : ↥f.domain), ↑f x ≤ gauge s ↑x
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
hr' : 0 < r
⊢ gauge (closedBall 0 r) x = ‖x‖ / r

Tactic:
· apply le_antisymm
    · rw [← gauge_ball hr]
      exact gauge_mono (absorbent_ball_zero hr') ball_subset_closedBall x
    · suffices ∀ᶠ R in 𝓝[>] r, ‖x‖ / R ≤ gauge (closedBall 0 r) x by
        refine le_of_tendsto ?_ this
        exact tendsto_const_nhds.div inf_le_left hr'.ne'
      filter_upwards [self_mem_nhdsWithin] with R hR
      rw [← gauge_ball (hr.trans hR.out.le)]
      refine gauge_mono ?_ (closedBall_subset_ball hR) _
      exact (absorbent_ball_zero hr').mono ball_subset_closedBall

Goal state after:
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, f a < u
hf₂ : ∀ b ∈ V, u < f b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (⇑f) s x
this : f x < u
a : E
ha : a ∈ s
⊢ f a < (f x + u) / 2

Tactic:
have := hx₂ ha

Goal state after:
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s t : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : s.Nonempty
_ht : t.Nonempty
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : StrongDual ℝ E
u : ℝ
hf₁ : ∀ a ∈ U, f a < u
hf₂ : ∀ b ∈ V, u < f b
x : E
hx₁ : x ∈ s
hx₂ : IsMaxOn (⇑f) s x
this✝ : f x < u
a : E
ha : a ∈ s
this : a ∈ {x_1 | (fun x_2 ↦ f x_2 ≤ f x) x_1}
⊢ f a < (f x + u) / 2
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case pos.refine_1
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
f_meas : Measurable f
g : X → E
hE : CompleteSpace E
hg : Integrable g (μ.withDensity fun x ↦ ↑(f x))
⊢ ∀ (c : E) ⦃s : Set X⦄,
    MeasurableSet s →
      (μ.withDensity fun x ↦ ↑(f x)) s < ∞ →
        (∫ (x : X), s.indicator (fun x ↦ c) x ∂μ.withDensity fun x ↦ ↑(f x)) =
          ∫ (x : X), f x • s.indicator (fun x ↦ c) x ∂μ

Tactic:
intro c s s_meas hs
    rw [integral_indicator s_meas]
    simp_rw [← Set.indicator_smul_apply, integral_indicator s_meas]
    simp only [s_meas, integral_const, Measure.restrict_apply', Set.univ_inter, withDensity_apply,
      measureReal_def]
    rw [lintegral_coe_eq_integral, ENNReal.toReal_ofReal, ← integral_smul_const]
    · rfl
    · exact integral_nonneg fun x => NNReal.coe_nonneg _
    · refine ⟨f_meas.coe_nnreal_real.aemeasurable.aestronglyMeasurable, ?_⟩
      simpa [withDensity_apply _ s_meas, hasFiniteIntegral_iff_enorm] using hs

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
h_int : IntegrableOn f [[a, b]] μ
⊢ ContinuousOn (fun x ↦ ∫ (t : ℝ) in x..b, f t ∂μ) [[a, b]]

Tactic:
rw [uIcc_comm a b] at h_int ⊢
  simp only [integral_symm b]
  exact (continuousOn_primitive_interval h_int).neg

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

Goal state before:
pp: case hf
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn f (Ioo a b) μ

pp: case hg
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn g (Ioo a b) μ

pp: case hs
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ MeasurableSet (Ioo a b)

pp: case h
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∀ x ∈ Ioo a b, f x ≤ g x

Tactic:
· apply hf.1.mono Ioo_subset_Ioc_self le_rfl

Goal state after:
case hg
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ IntegrableOn g (Ioo a b) μ

case hs
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ MeasurableSet (Ioo a b)

case h
f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
inst✝ : NullSingletonClass μ
h : ∀ x ∈ Ioo a b, f x ≤ g x
⊢ ∀ x ∈ Ioo a b, f x ≤ g x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic

Goal state before:
pp: case e'_2
T : ℝ
hT : Fact (0 < T)
t : ℝ
f : AddCircle T → ℝ≥0∞
m : MeasurableSet (Ioc t (t + T))
this : ∫⁻ (a : AddCircle T), f a ∂Measure.map (fun x ↦ ↑↑x) volume = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a
⊢ ∫⁻ (a : ℝ), f ↑a ∂Measure.map Subtype.val (Measure.comap Subtype.val volume) = ∫⁻ (a : ↑(Ioc t (t + T))), f ↑↑a

Tactic:
exact MeasurableEmbedding.lintegral_map (MeasurableEmbedding.subtype_coe m) _

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

Goal state before:
pp: case left
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst✝ : NullSingletonClass μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
h_split : ∀ b ∈ Icc a₀ a, ∫ (x : ℝ) in Ioi b, f x ∂μ = ∫ (x : ℝ) in Ioi a₀, f x ∂μ - ∫ (x : ℝ) in a₀..b, f x ∂μ
h_cwa : ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in a₀..b, f x ∂μ) (Icc a₀ a) a
⊢ ContinuousWithinAt (fun b ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Icc a₀ a) a

Tactic:
exact (continuousWithinAt_const.sub h_cwa).congr h_split (h_split a (right_mem_Icc.2 ha))

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

Goal state before:
pp: case hbc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 < R
hc : ContinuousOn f (sphere c R)
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
θ₀ : ℝ
hmem : θ₀ ∈ Ioc 0 (2 * π)
hlt : ‖f (circleMap c R θ₀)‖ < C
θ : ℝ
x✝ : θ ∈ Ioc 0 (2 * π)
⊢ ‖f (circleMap c R θ)‖ ≤ C

Tactic:
exact hf _ <| circleMap_mem_sphere _ hR.le _

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
F : Type u_4
G : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
⊢ ∫⁻ (z : α × β), ‖op (f z.1) (g z.2)‖ₑ ∂μ.prod ν ≤ ∫⁻ (z : α × β), ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ ∂μ.prod ν

Tactic:
by
      gcongr with z
      simp only [enorm_eq_nnnorm, ENNReal.ofReal, ← ENNReal.coe_mul, ENNReal.coe_le_coe,
        ← NNReal.coe_le_coe, NNReal.coe_mul, coe_nnnorm]
      refine (hC _ _).trans ?_
      gcongr
      apply le_coe_toNNReal

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

Goal state before:
pp: case pos
n : ℤ
hn : n ≠ -1
c w : ℂ
R : ℝ
H : w ∈ sphere c |R| ∧ n < -1
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

Tactic:
rcases H with ⟨hw, hn⟩

Goal state after:
case pos
n : ℤ
hn✝ : n ≠ -1
c w : ℂ
R : ℝ
hw : w ∈ sphere c |R|
hn : n < -1
⊢ ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
φ : k →+* ℂ
this : Algebra k ℂ := φ.toAlgebra
⊢ IsAlgClosed.lift.comp (algebraMap k K) = φ

Tactic:
AlgHom.toRingHom_eq_coe,

Goal state after:
K : Type u_1
inst✝³ : Field K
k : Type u_2
inst✝² : Field k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsAlgebraic k K
φ : k →+* ℂ
this : Algebra k ℂ := φ.toAlgebra
⊢ (↑IsAlgClosed.lift).comp (algebraMap k K) = φ
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: case mp
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a ∈ ratLt (x + y)
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a

Tactic:
Set.mem_ofPred_eq

Goal state after:
case mp
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
⊢ ∃ x_1 ∈ ratLt x, ∃ y_1 ∈ ratLt y, x_1 + y_1 = a
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
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • (x + y) - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1

Tactic:
smul_add,

Goal state after:
M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
a : ℚ
h : a.num • 1 < a.den • (x + y)
k : ℕ
hk : 1 + 1 ≤ k • (a.den • x + a.den • y - a.num • 1)
hk0 : k ≠ 0
hka0 : k * a.den ≠ 0
m : ℤ
right✝ : ∀ (y : ℤ), (fun m ↦ 0 + m • 1 ∈ Set.Ico (k • a.den • x - 1) (k • a.den • x - 1 + 1)) y → y = m
hm1 : k • a.den • x - 1 ≤ 0 + m • 1
hm2 : 0 + m • 1 < k • a.den • x - 1 + 1
⊢ 1 + (k • a.num • 1 - k • a.den • y) ≤ k • a.den • x - 1