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
x : E
n : ℕ∞ω
s : Set E
f : E → F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ (f x, g x)) s x

Tactic:
match n with
  | ω =>
    obtain ⟨u, hu, p, hp, h'p⟩ := hf
    obtain ⟨v, hv, q, hq, h'q⟩ := hg
    refine ⟨u ∩ v, Filter.inter_mem hu hv, _,
      (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right), fun i ↦ ?_⟩
    change AnalyticOn 𝕜 (fun x ↦ ContinuousMultilinearMap.prodL _ _ _ _ (p x i, q x i)) (u ∩ v)
    apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn _ (Set.mapsTo_univ _ _)
    exact ((h'p i).mono inter_subset_left).prod ((h'q i).mono inter_subset_right)
  | (n : ℕ∞) =>
    intro m hm
    rcases hf m hm with ⟨u, hu, p, hp⟩
    rcases hg m hm with ⟨v, hv, q, hq⟩
    exact ⟨u ∩ v, Filter.inter_mem hu hv, _,
      (hp.mono inter_subset_left).prodMk (hq.mono inter_subset_right)⟩

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft

Goal state before:
pp: case refine_1
𝕜 : 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 : E → F
f : F → G
h : E → G
g' : E →L[𝕜] F
f' : F →L[𝕜] G
a : E
hg : ContinuousAt g a
hf : HasFDerivAt f f' (g a)
hf' : Topology.IsEmbedding ⇑f'
hh : HasFDerivAt h (f' ∘SL g') a
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ Tendsto (Prod.map g g) (𝓝 a ×ˢ pure a) (𝓝 (g a) ×ˢ pure (g a))

Tactic:
exact hg.tendsto.prodMap (by simp)

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : AccPt x (𝓟 s)
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : ¬AccPt x (𝓟 s)
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x

Tactic:
· rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
      iteratedFDerivWithin_eq_equiv_comp,
      LinearIsometryEquiv.comp_fderivWithin _ hxs.uniqueDiffWithinAt, derivWithin]
    change ((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜
      (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) : (Fin n → 𝕜) → F) fun _ : Fin n => 1) =
      (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1
    simp

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
hxs : ¬AccPt x (𝓟 s)
⊢ iteratedDerivWithin (n + 1) f s x = derivWithin (iteratedDerivWithin n f s) s x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
m : Fin c.length
⊢ StrictMono
    (if h : m = m then
      have this := ⋯;
      (fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast this
    else
      have this := ⋯;
      succ ∘ c.emb m ∘ Fin.cast this)

Tactic:
suffices ∀ (a' b' : Fin (c.partSize m + 1)), a' < b' →
          (cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb m)) a' <
          (cases (motive := fun _ ↦ Fin (n + 1)) 0 (succ ∘ c.emb m)) b' by
        simp only [↓reduceDIte]
        intro a b hab
        exact this _ _ hab

Goal state after:
case inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
m : Fin c.length
⊢ ∀ (a' b' : Fin (c.partSize m + 1)), a' < b' → cases 0 (succ ∘ c.emb m) a' < cases 0 (succ ∘ c.emb m) b'
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q✝ : F → FormalMultilinearSeries 𝕜 F G
p✝ : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
m : Fin c.length
q q' : E [×c.partSize m]→L[𝕜] F
⊢ c.compAlongOrderedFinpartition f (update p m (q + q')) =
    c.compAlongOrderedFinpartition f (update p m q) + c.compAlongOrderedFinpartition f (update p m q')

Tactic:
by
        ext v
        simp [applyOrderedFinpartition_update_left]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q✝ : F → FormalMultilinearSeries 𝕜 F G
p✝ : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
m : Fin c.length
a : 𝕜
q : E [×c.partSize m]→L[𝕜] F
⊢ c.compAlongOrderedFinpartition f (update p m (a • q)) = a • c.compAlongOrderedFinpartition f (update p m q)

Tactic:
by
        ext v
        simp [applyOrderedFinpartition_update_left]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×m]→L[𝕜] G :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : ↑c.length ≤ ↑m
cp : ∀ (i : Fin c.length), ↑(c.partSize i) ≤ ↑m
I : ∀ (i : Fin c.length), HasFDerivWithinAt (fun x ↦ p x (c.partSize i)) (p x (c.partSize i).succ).curryLeft s x
J : HasFDerivWithinAt (fun x ↦ q x c.length) (q (f x) c.length.succ).curryLeft t (f x)
⊢ HasFDerivWithinAt (fun y ↦ (B (q (f y) c.length)) fun i ↦ p y (c.partSize i))
    (∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x

Tactic:
have K : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x :=
        hf.hasFDerivWithinAt hm.ne_bot hx

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : (F [×c.length]→L[𝕜] G) →L[𝕜] (E [×c.partSize i]→L[𝕜] F) [×c.length]→L[𝕜] E [×m]→L[𝕜] G :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : ↑c.length ≤ ↑m
cp : ∀ (i : Fin c.length), ↑(c.partSize i) ≤ ↑m
I : ∀ (i : Fin c.length), HasFDerivWithinAt (fun x ↦ p x (c.partSize i)) (p x (c.partSize i).succ).curryLeft s x
J : HasFDerivWithinAt (fun x ↦ q x c.length) (q (f x) c.length.succ).curryLeft t (f x)
K : HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x
⊢ HasFDerivWithinAt (fun y ↦ (B (q (f y) c.length)) fun i ↦ p y (c.partSize i))
    (∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMinOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
⊢ 0 ≤ f' y

Tactic:
by
  simpa using h.neg.hasFDerivWithinAt_nonpos hf.neg hy

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ deriv f (-x) ≠ 0

Tactic:
mem_Ioo

Goal state after:
f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : -a < x ∧ x < -b
⊢ deriv f (-x) ≠ 0
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
⊢ C.Salient ↔ ¬C.Flat

Tactic:
simp [Salient, Flat]

Goal state after:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case pos
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : 0 ∈ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

pp: case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : 0 ∉ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

Tactic:
· simp only [smul_zero, sep_true, h, csInf_Ioi]

Goal state after:
case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : 0 ∉ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}

Tactic:
· convert! convex_empty (𝕜 := ℝ)
    exact eq_empty_iff_forall_notMem.2 fun x hx => ha <| (gauge_nonneg _).trans hx

Goal state after:
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: case refine_1
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
g : ↥⊤ →ₗ[ℝ] ℝ
hfg : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g }.domain⦄, ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y
hgs : ∀ (x : ↥{ domain := ⊤, toFun := g }.domain), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x
⊢ ∀ (x : ↥f.domain), (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) ↑x = ↑f x

pp: case refine_2
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
g : ↥⊤ →ₗ[ℝ] ℝ
hfg : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g }.domain⦄, ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y
hgs : ∀ (x : ↥{ domain := ⊤, toFun := g }.domain), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x
⊢ ∀ x ∈ s, 0 ≤ (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) x

Tactic:
· exact fun x => (hfg rfl).symm

Goal state after:
case refine_2
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
g : ↥⊤ →ₗ[ℝ] ℝ
hfg : ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥{ domain := ⊤, toFun := g }.domain⦄, ↑x = ↑y → ↑f x = ↑{ domain := ⊤, toFun := g } y
hgs : ∀ (x : ↥{ domain := ⊤, toFun := g }.domain), ↑x ∈ s → 0 ≤ ↑{ domain := ⊤, toFun := g } x
⊢ ∀ x ∈ s, 0 ≤ (g ∘ₗ LinearMap.codRestrict ⊤ LinearMap.id ⋯) x
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Absorbent ℝ s
hr : 0 ≤ r
hsr : s ⊆ closedBall 0 r
⊢ ‖x‖ / r ≤ gauge s x

Tactic:
← gauge_closedBall hr

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : Absorbent ℝ s
hr : 0 ≤ r
hsr : s ⊆ closedBall 0 r
⊢ gauge (closedBall 0 r) x ≤ gauge s x
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
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + ((G y)⁻¹ * G z) • (x - y) + (G z + ((G y)⁻¹ * G z - (G y)⁻¹ * G z * G y)) • (y - x) = z

Tactic:
mul_comm _ (G y),

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
x y : V
hx : x ≠ 0
hy : y ≠ 0
G : StrongDual R V
Gx : G x = 1
Gy : G y ≠ 0
z : V
⊢ z + ((G y)⁻¹ * G z) • (x - y) + (G z + ((G y)⁻¹ * G z - G y * ((G y)⁻¹ * G z))) • (y - x) = z
Module: Mathlib.Analysis.Calculus.TangentCone.Prod

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
x : E
s : Set E
y : F
t : Set F
hs : x ∈ closure[inst✝⁷] s
⊢ ⇑(LinearMap.inr 𝕜 E F) '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Tactic:
rw [← tangentConeAt_closure (s := s ×ˢ t), closure_prod_eq]
  rintro _ ⟨z, hz, rfl⟩
  rcases exists_fun_of_mem_tangentConeAt hz with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩
  refine mem_tangentConeAt_of_seq l c (fun n ↦ (0, d n)) (tendsto_const_nhds.prodMk_nhds hd₀)
    (hds.mono fun n hn ↦ by simp [hs, subset_closure hn]) ?_
  simpa using tendsto_const_nhds.prodMk_nhds hcd

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

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞
this :
  ∀ {a b : ℝ},
    IntervalIntegrable f volume a b →
      ‖f (min a b)‖ₑ ≠ ∞ →
        ‖f (min (a - c) (b - c) + c)‖ₑ ≠ ∞ → a ≤ b → IntervalIntegrable (fun x ↦ f (x + c)) volume (a - c) (b - c)
hab : ¬a ≤ b
⊢ ‖f (min (b - c) (a - c) + c)‖ₑ ≠ ∞

Tactic:
· rw [min_comm]; exact 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 c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ + -∫ (x : ℝ) in a..c, f x ∂μ = 0

Tactic:
← integral_symm,

Goal state after:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
⊢ ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ + ∫ (x : ℝ) in c..a, f x ∂μ = 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : StrongDual ℝ E
⊢ g (∫ (y : ℝ) in a..b, f' y) = g (f b - f a)

Tactic:
rw [← g.intervalIntegral_comp_comm f'int, g.map_sub]

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
inst✝ : CompleteSpace E
f f' : ℝ → E
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : StrongDual ℝ E
⊢ ∫ (x : ℝ) in a..b, g (f' x) = g (f b) - g (f a)
Module: Mathlib.Analysis.SpecialFunctions.NonIntegrable

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
⊢ ¬IntegrableOn g k volume

Tactic:
let a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
f : ℝ → E
g : ℝ → F
k : Set ℝ
l : Filter ℝ
inst✝¹ : l.NeBot
inst✝ : TendstoIxxClass Icc l l
hl : k ∈ l
hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x
hf : Tendsto (fun x ↦ ‖f x‖) l atTop
hfg : deriv f =O[l] g
a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
⊢ ¬IntegrableOn g k volume
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)
  have h : IntegrableOn f (Ico a b) μ := hf.mono_set Ico_subset_Ici_self
  rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h, union_comm,
    Ico_union_Ici_eq_Ici hab]

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)
δ : ℝ
δ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 a₀..s, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f p t ∂μ‖ +
      ‖∫ (t : ℝ) in a₀..b₀, f p t ∂μ - ∫ (t : ℝ) in a₀..b₀, f q t ∂μ‖ =
    ‖∫ (t : ℝ) in b₀..s, f p t ∂μ‖ + ‖∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ‖

Tactic:
by
      congr 2
      · rw [integral_interval_sub_left (J _ _ _) (J _ _ _)]
      · rw [integral_sub (J _ _ _) (J _ _ _)]

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

Goal state before:
pp: F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x ↦ (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun x ↦ Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun x ↦ ‖Real.log (x - c)‖) (𝓝[≠] c) atTop

Tactic:
refine tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsNE_zero.comp ?_)

Goal state after:
F : Type u_2
inst✝ : NormedAddCommGroup F
f : ℝ → F
a b c : ℝ
hf : (fun x ↦ (x - c)⁻¹) =O[𝓝[≠] c] f
hne : a ≠ b
hc : c ∈ [[a, b]]
A : ∀ᶠ (x : ℝ) in 𝓝[≠] c, HasDerivAt (fun x ↦ Real.log (x - c)) (x - c)⁻¹ x
⊢ Tendsto (fun x ↦ x - c) (𝓝[≠] c) (𝓝[≠] 0)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: f g : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
h : f ≤ᵐ[μ] g
⊢ ∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ

Tactic:
simpa only [integral_of_le hab] using setIntegral_mono_ae hf.1 hg.1 h

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

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

Tactic:
exact le_ceil _

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

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_1 : NormedSpace ℝ E],
    Periodic f T → ∀ (t s : ℝ), 0 < T → ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
hT✝ : ¬0 < T
hT : T < 0
⊢ -∫ (x : ℝ) in t..t + T, f x = -∫ (x : ℝ) in s..s + T, f x

Tactic:
← integral_symm,

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
inst✝ : NormedSpace ℝ E
hf : Periodic f T
t s : ℝ
this :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_1 : NormedSpace ℝ E],
    Periodic f T → ∀ (t s : ℝ), 0 < T → ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
hT✝ : ¬0 < T
hT : T < 0
⊢ ∫ (x : ℝ) in t + T..t, f x = -∫ (x : ℝ) in s..s + T, f x
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

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

Tactic:
Metric.tendstoUniformlyOn_iff

Goal state after:
case h_lim
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
ι : Type u_2
f : ι → ℂ → E
g : ℂ → E
c : ℂ
R : ℝ
l : Filter ι
inst✝ : l.IsCountablyGenerated
hR : 0 ≤ R
hf : ∀ᶠ (i : ι) in l, ContinuousOn (f i) (sphere c R)
h : ∀ ε > 0, ∀ᶠ (n : ι) in l, ∀ x ∈ sphere c R, dist (g x) (f n x) < ε
⊢ ∀ ε > 0,
    ∀ᶠ (n : ι) in l,
      ∀ x ∈ [[0, 2 * π]],
        dist (deriv (circleMap c R) x • (fun z ↦ g z) (circleMap c R x))
            (deriv (circleMap c R) x • (fun z ↦ f n z) (circleMap c R x)) <
          ε
Module: Mathlib.MeasureTheory.Integral.CircleIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z = ∮ (z : ℂ) in C(c, R), f z

Tactic:
rcases eq_or_ne R 0 with (rfl | hR)

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
⊢ ∮ (z : ℂ) in C(c, 0), (z - w)⁻¹ • (z - w) • f z = ∮ (z : ℂ) in C(c, 0), f z

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c w : ℂ
R : ℝ
hR : R ≠ 0
⊢ ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z = ∮ (z : ℂ) in C(c, R), f z