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

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ (fderivWithin ℝ f s a) y = 0

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Goal state after:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y = 0
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case mpr
s : Set ℝ
a : ℝ
h : a ∈ closure (Ioi a ∩ s)
⊢ 1 ∈ posTangentConeAt s a

Tactic:
apply mem_posTangentConeAt_of_frequently_mem

Goal state after:
case mpr
s : Set ℝ
a : ℝ
h : a ∈ closure (Ioi a ∩ s)
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + t • 1 ∈ s
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : 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
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x
⊢ iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x

Tactic:
by
  rw [(by aesop : (∑ j ∈ u, f j) = (fun x ↦ ∑ j ∈ u, f j x))]
  induction u using Finset.cons_induction with
  | empty => simp
  | cons a u ha IH =>
    simp only [Finset.mem_cons, forall_eq_or_imp] at h
    simp only [Finset.sum_cons]
    rw [fun_iteratedFDerivWithin_add_apply h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑i) f
⊢ (iteratedFDeriv 𝕜 i fun z ↦ f (a • z)) = fun x ↦ a ^ i • iteratedFDeriv 𝕜 i f (a • x)

Tactic:
induction i with
  | zero => ext; simp
  | succ i hi =>
    ext v
    rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDeriv_succ_eq_comp_left]
    simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, self_le_add_right, hf.of_le, hi,
      comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply, smul_apply]
    rw [fderiv_fun_const_smul, fderiv_comp_smul, smul_smul, ← pow_succ]
    · simp
    rw [← Function.comp_def (g := (a • ·))]
    apply DifferentiableAt.comp
    · exact hf.contDiffAt.differentiableAt_iteratedFDeriv (Nat.cast_lt.2 i.lt_succ_self)
    · exact differentiableAt_id.const_smul _

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

Goal state before:
pp: case h.refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑f.symm a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : ↑f.symm a ∈ t
x : F
hx : x ∈ f.target ∩ ↑f.symm ⁻¹' t
hxu : ↑f.symm x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑f.symm x)
⊢ HasFDerivAt (↑f.symm) ((inverse ∘ f' ∘ ↑f.symm) x) x

Tactic:
have h_deriv : HasFDerivAt f (e : E →L[𝕜] F) (f.symm x) := by
          rw [he]
          exact hff' (f.symm x) hxu

Goal state after:
case h.refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
h_nhds : {y | ∃ e, ↑e = f' y} ∈ 𝓝 (↑f.symm a)
t : Set E
htu : t ⊆ u ∩ {y | ∃ e, ↑e = f' y}
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
htf : ↑f.symm a ∈ t
x : F
hx : x ∈ f.target ∩ ↑f.symm ⁻¹' t
hxu : ↑f.symm x ∈ u
e : E ≃L[𝕜] F
he : ↑e = f' (↑f.symm x)
h_deriv : HasFDerivAt (↑f) (↑e) (↑f.symm x)
⊢ HasFDerivAt (↑f.symm) ((inverse ∘ f' ∘ ↑f.symm) x) x
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
ε0 : ε ≠ 0
f : α →ₛ ℝ≥0 := piecewise s hs (const α c) (const α 0)
h : ∫⁻ (x : α), ↑(f x) ∂μ = ∞
⊢ ∫⁻ (x : α), ↑((fun x ↦ c) x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
simp only [f, _root_.top_add, le_top, h]

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

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
⊢ False

Tactic:
have hcontra : ∀ᶠ _ in 𝓝[>] a, False := by
      filter_upwards [h₀, h₁, eventually_mem_nhdsWithin] with b hb hslope (hab : a < b)
      have hdiff' : DifferentiableOn ℝ f (Ioc a b) := fun z hz => by
        refine DifferentiableWithinAt.mono (t := Ioi a) ?_ Ioc_subset_Ioi_self
        have : derivWithin f (Ioi a) z ≠ 0 := ne_of_gt <| by
          simp_all only [and_imp, mem_Ioc, max_lt_iff]
        exact differentiableWithinAt_of_derivWithin_ne_zero this
      have hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z := by
        intro z hz''
        refine (hdiff'.continuousOn z hz'').mono_of_mem_nhdsWithin ?_
        have hfinal : 𝓝[Ioc a b] z = 𝓝[Icc a b] z := by
          refine nhdsWithin_eq_nhdsWithin' (s := Ioi a) (Ioi_mem_nhds hz''.1) ?_
          simp only [Ioc_inter_Ioi, le_refl, sup_of_le_left]
          ext y
          exact ⟨fun h => ⟨mem_Icc_of_Ioc h, mem_of_mem_inter_left h⟩, fun ⟨H1, H2⟩ => ⟨H2, H1.2⟩⟩
        rw [← hfinal]
        exact self_mem_nhdsWithin
      have hcont : ContinuousOn f (Icc a b) := by
        intro z hz
        by_cases hz' : z = a
        · rw [hz']
          exact hcont_at_a.mono Icc_subset_Ici_self
        · exact hcont_Ioc z ⟨lt_of_le_of_ne hz.1 (Ne.symm hz'), hz.2⟩
      obtain ⟨x, hx₁, hx₂⟩ :=
        exists_deriv_eq_slope' f hab hcont (hdiff'.mono (Ioo_subset_Ioc_self))
      specialize hb x ⟨hx₁.1, le_of_lt hx₁.2⟩
      replace hx₂ : derivWithin f (Ioi a) x = slope f a b := by
        have : Ioi a ∈ 𝓝 x := by simp [← mem_interior_iff_mem_nhds, hx₁.1]
        rwa [derivWithin_of_mem_nhds this]
      rw [hx₂, max_lt_iff] at hb
      linarith

Goal state after:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
hcontra : ∀ᶠ (x : ℝ) in 𝓝[>] a, False
⊢ False
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
h : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ Tendsto (fun x ↦ -deriv f x) (𝓝[>] a) atTop

Tactic:
exact tendsto_neg_atBot_atTop.comp hf

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
h : C₁ ≤ C₂
hgen : C₁.IsGenerating
⊢ C₂.IsGenerating

Tactic:
rw [IsGenerating, ← top_le_iff] at hgen ⊢
  exact hgen.trans (Submodule.span_mono h)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: f : ℝ → ℝ
x f' : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun y ↦ Real.log (f y)) ((f x)⁻¹ * f') x

Tactic:
exact (hasStrictDerivAt_log hx).comp x hf

Goal state after:
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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
⊢ x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2) ^ n < R :=
    exists_pow_lt_of_lt_one R_pos (by norm_num : (1 : ℝ) / 2 < 1)

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
f : E → F
K : Set (E →L[𝕜] F)
x : E
hx : x ∈ {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (fderiv 𝕜 f x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
⊢ x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
n : ℕ
⊢ |∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)

Tactic:
by
  /- For the proof, we show that the derivative of the function to be estimated is small,
    and then apply the mean value inequality. -/
  let F : ℝ → ℝ := fun x => (∑ i ∈ range n, x ^ (i + 1) / (i + 1)) + log (1 - x)
  let F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
  -- Porting note: In `mathlib3`, the proof used `deriv`/`DifferentiableAt`. `simp` failed to
  -- compute `deriv`, so I changed the proof to use `HasDerivAt` instead
  -- First step: compute the derivative of `F`
  have A : ∀ y ∈ Ioo (-1 : ℝ) 1, HasDerivAt F (F' y) y := fun y hy ↦ by
    have : HasDerivAt F ((∑ i ∈ range n, ↑(i + 1) * y ^ i / (↑i + 1)) + (-1) / (1 - y)) y :=
      .add (.fun_sum fun i _ ↦ (hasDerivAt_pow (i + 1) y).div_const ((i : ℝ) + 1))
        (((hasDerivAt_id y).const_sub _).log <| sub_ne_zero.2 hy.2.ne')
    convert! this using 1
    calc
      -y ^ n / (1 - y) = ∑ i ∈ Finset.range n, y ^ i + -1 / (1 - y) := by
        simp [field, geom_sum_eq hy.2.ne, sub_ne_zero.2 hy.2.ne, sub_ne_zero.2 hy.2.ne']
        ring
      _ = ∑ i ∈ Finset.range n, ↑(i + 1) * y ^ i / (↑i + 1) + -1 / (1 - y) := by
        congr with i
        rw [Nat.cast_succ, mul_div_cancel_left₀ _ (Nat.cast_add_one_pos i).ne']
  -- second step: show that the derivative of `F` is small
  have B : ∀ y ∈ Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|) := fun y hy ↦
    calc
      |F' y| = |y| ^ n / |1 - y| := by simp [F', abs_div]
      _ ≤ |x| ^ n / (1 - |x|) := by
        have : |y| ≤ |x| := abs_le.2 hy
        have : 1 - |x| ≤ |1 - y| := le_trans (by linarith [hy.2]) (le_abs_self _)
        gcongr
  -- third step: apply the mean value inequality
  have C : ‖F x - F 0‖ ≤ |x| ^ n / (1 - |x|) * ‖x - 0‖ := by
    refine Convex.norm_image_sub_le_of_norm_hasDerivWithin_le
      (fun y hy ↦ (A _ ?_).hasDerivWithinAt) B (convex_Icc _ _) ?_ ?_
    · exact Icc_subset_Ioo (neg_lt_neg h) h hy
    · simp
    · simp [le_abs_self x, neg_le.mp (neg_le_abs x)]
  -- fourth step: conclude by massaging the inequality of the third step
  simpa [F, div_mul_eq_mul_div, pow_succ] using C

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
hdom : f.domain ≠ ⊤
y : E
hy : y ∉ f.domain
Sp : Set ℝ := ↑f '' {x | ↑x + y ∈ s}
Sn : Set ℝ := ↑f '' {x | -↑x - y ∈ s}
x : ↥f.domain
hx : -↑(-x) - y ∈ s
⊢ {x | -↑x - y ∈ s}.Nonempty

Tactic:
exact ⟨_, hx⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
h₁ :
  |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)| ≤
    |x| ^ (2 * n + 1) / (1 - x ^ 2)
⊢ 1 / 2 * log ((1 + x) / (1 - x)) ≤ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1) + x ^ (2 * n + 1) / (1 - x ^ 2)

Tactic:
rwa [abs_of_nonneg (sub_nonneg_of_le (sum_range_le_log_div h₀ h n)), abs_of_nonneg h₀,
    sub_le_iff_le_add'] at h₁

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

Goal state before:
pp: case inr
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 | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} = a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}

Tactic:
ext r

Goal state after:
case inr
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 : ℝ
⊢ r ∈ {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} ↔ r ∈ a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
s : PointedCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_eq : ∀ (x : ↥f'.domain), g ↑x = ↑f' x
g_nonneg : ∀ x ∈ s, 0 ≤ g x
⊢ ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x

Tactic:
replace g_eq : ∀ (x : f.domain) (y : ℝ), g (x, y) = y - f x := fun x y ↦
    (g_eq ⟨(x, y), ⟨x.2, trivial⟩⟩).trans (sub_eq_neg_add _ _).symm

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E →ₗ.[ℝ] ℝ
N : E → ℝ
N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x
N_add : ∀ (x y : E), N (x + y) ≤ N x + N y
hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x
N_0 : N 0 = 0
s : PointedCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)
hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x
hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s
g : E × ℝ →ₗ[ℝ] ℝ
g_nonneg : ∀ x ∈ s, 0 ≤ g x
g_eq : ∀ (x : ↥f.domain) (y : ℝ), g (↑x, y) = y - ↑f x
⊢ ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr
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✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
⊢ {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ a • s} = a⁻¹ • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}

Tactic:
ext r

Goal state after:
case inr
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✝² : SMulCommClass α ℝ ℝ
inst✝¹ : IsScalarTower α ℝ ℝ
inst✝ : IsScalarTower α ℝ E
s : Set E
a : α
ha : 0 ≤ a
ha' : 0 < a
x : E
r : ℝ
⊢ r ∈ {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ a • s} ↔ r ∈ a⁻¹ • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
fc : F → 𝕜 := fun x ↦ ↑(fr x) - I * ↑(fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(fr (↑c • x)) = ↑c * ↑(fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
c : 𝕜
x : F
⊢ fc (c • x) = c • fc x

Tactic:
rw [← re_add_im c]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
fc : F → 𝕜 := fun x ↦ ↑(fr x) - I * ↑(fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
A : ∀ (c : ℝ) (x : F), ↑(fr (↑c • x)) = ↑c * ↑(fr x)
smul_ℝ : ∀ (c : ℝ) (x : F), fc (↑c • x) = ↑c * fc x
smul_I : ∀ (x : F), fc (I • x) = I * fc x
c : 𝕜
x : F
⊢ fc ((↑(re c) + ↑(im c) * I) • x) = (↑(re c) + ↑(im c) * I) • fc x
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
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 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ ↑f ⟨y • x₀, hx⟩ ≤ gauge s ↑⟨y • x₀, hx⟩

Tactic:
rw [LinearPMap.mkSpanSingleton'_apply]

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 ⋯
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ (RingHom.id ℝ) y • 1 ≤ gauge s ↑⟨y • x₀, hx⟩
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
L : F
r ε δ : ℝ
h : ε ≤ δ
⊢ A f L r ε ⊆ A f L r δ

Tactic:
by
  rintro x ⟨r', r'r, hr'⟩
  refine ⟨r', r'r, fun y hy z hz => (hr' y hy z hz).trans (mul_le_mul_of_nonneg_right h ?_)⟩
  linarith [hy.1, hy.2, r'r.2]

Goal state after:
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
inst✝ : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c // ∀ y ∈ s, re (l y) ≤ c }
l : ι → StrongDual 𝕜 E := fun lc ↦ lc.fst
c : ι → ℝ := fun lc ↦ ↑lc.snd
hc : ∀ (i : ι), ∀ y ∈ s, re ((l i) y) ≤ c i := fun lc ↦ Subtype.prop lc.snd
this : Nonempty ι
⊢ ∃ l c, ⋂ n, {x | re ((l n) x) ≤ c n} = s

Tactic:
have : ⋂ i : ι, { x | re (l i x) ≤ c i } = s := by
    simpa only [ι, iInter_sigma, iInter_subtype, l, c] using iInter_halfSpaces_eq' hs₁ hs₂

Goal state after:
𝕜 : 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
inst✝ : HereditarilyLindelofSpace E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
ι : Type (max u_1 u_2) := (l : StrongDual 𝕜 E) × { c // ∀ y ∈ s, re (l y) ≤ c }
l : ι → StrongDual 𝕜 E := fun lc ↦ lc.fst
c : ι → ℝ := fun lc ↦ ↑lc.snd
hc : ∀ (i : ι), ∀ y ∈ s, re ((l i) y) ≤ c i := fun lc ↦ Subtype.prop lc.snd
this✝ : Nonempty ι
this : ⋂ i, {x | re ((l i) x) ≤ c i} = s
⊢ ∃ l c, ⋂ n, {x | re ((l n) x) ≤ c n} = s
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
⊢ x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2) ^ n < R :=
    exists_pow_lt_of_lt_one R_pos (by norm_num : (1 : ℝ) / 2 < 1)

Goal state after:
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
x : ℝ
hx : x ∈ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
e : ℕ
this : 0 < (1 / 2) ^ e
R : ℝ
R_pos : R > 0
hR : ∀ r ∈ Ioo 0 R, x ∈ A f (derivWithin f (Ici x) x) r ((1 / 2) ^ e)
n : ℕ
hn : (1 / 2) ^ n < R
⊢ x ∈ ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
Module: Mathlib.Topology.ContinuousMap.ContinuousMapZero

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
s : Set X
inst✝ : Zero ↑s
f : X → R
g : C(↑s, R)₀
hf : ¬ContinuousOn f s
⊢ mkD (s.domRestrict f) g = g

Tactic:
rw [continuousOn_iff_continuous_domRestrict] at hf

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
s : Set X
inst✝ : Zero ↑s
f : X → R
g : C(↑s, R)₀
hf : ¬Continuous[instTopologicalSpaceSubtype, inst✝¹] (s.domRestrict f)
⊢ mkD (s.domRestrict f) g = g
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
𝕜 : Type u_8
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : X → 𝕜
c : E
hf : ¬Integrable f μ
⊢ ∫ (x : X), f x • c ∂μ = (∫ (x : X), f x ∂μ) • c

Tactic:
by_cases hc : c = 0
    · simp [hc, integral_zero, smul_zero]
    rw [integral_undef hf, integral_undef, zero_smul]
    rw [integrable_smul_const hc]
    simp_rw [hf, not_false_eq_true]

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : TopologicalSpace X
μ : Measure ℝ
inst✝ : FirstCountableTopology X
F : X → ℝ → E
bound : ℝ → ℝ
a b a₀ b₀ : ℝ
x₀ : X
hF_meas : ∀ (x : X), AEStronglyMeasurable (F x) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
bound_integrable : IntervalIntegrable bound μ a b
h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ContinuousAt (fun x ↦ F x t) x₀
ha₀ : a₀ ∈ Ioo a b
hb₀ : b₀ ∈ Ioo a b
hμb₀ : μ {b₀} = 0
hsub : ∀ {a₀ b₀ : ℝ}, a₀ ∈ Ioo a b → b₀ ∈ Ioo a b → Ι a₀ b₀ ⊆ Ι a b
Ioo_nhds : Ioo a b ∈ 𝓝 b₀
Icc_nhds : Icc a b ∈ 𝓝 b₀
hx₀ : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x₀ t‖ ≤ bound t
x : X
t : ℝ
hx : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t
ht : t ∈ Ioo a b
s : ℝ
hs₁ : ‖F x s‖ ≤ bound s
hs₂ : ‖F x₀ s‖ ≤ bound s
⊢ ‖F x s - F x₀ s‖ ≤ 2 * bound s

Tactic:
calc
          ‖F x s - F x₀ s‖ ≤ ‖F x s‖ + ‖F x₀ s‖ := norm_sub_le _ _
          _ ≤ 2 * bound s := by linarith only [hs₁, hs₂]

Goal state after: