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
n : ℕ∞ω
g : G →L[𝕜] E
f : E → F
hf : ContDiff 𝕜 n f
x : G
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDeriv 𝕜 i (f ∘ ⇑g) x = (iteratedFDeriv 𝕜 i f (g x)).compContinuousLinearMap fun x ↦ g

Tactic:
simp only [← iteratedFDerivWithin_univ]
  exact g.iteratedFDerivWithin_comp_right hf.contDiffOn uniqueDiffOn_univ uniqueDiffOn_univ
      (mem_univ _) hi

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

Goal state before:
pp: case mpr.refine_1
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
hn : n ≠ ∞
h'n : n + 1 ≠ ∞
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : n = ω → AnalyticOn 𝕜 f u
f' : E → E →L[𝕜] F
f'_eq_deriv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
Hf' : ContDiffWithinAt 𝕜 n f' u x
v : Set E
hv : v ∈ 𝓝[insert x u] x
p' : E → FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
Hp' : HasFTaylorSeriesUpToOn n f' p' v
p'_an : n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p' x i) v
⊢ v ∩ u ∈ 𝓝[insert x s] x

Tactic:
apply Filter.inter_mem _ hu
      apply nhdsWithin_le_of_mem hu
      exact nhdsWithin_mono _ (subset_insert x u) hv

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

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
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ univ ⊆ g ⁻¹' univ

Tactic:
preimage_univ

Goal state after:
𝕜 : 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
m n : ℕ∞ω
f : E → F → G
g : E → F
hf : ContDiffAt 𝕜 n (uncurry f) (x₀, g x₀)
hg : ContDiffAt 𝕜 m g x₀
hmn : m + 1 ≤ n
⊢ univ ⊆ univ
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedFDerivWithin 𝕜 n f s = id ∘ iteratedFDerivWithin 𝕜 n f s

Tactic:
Function.id_comp

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
⊢ iteratedFDerivWithin 𝕜 n f s = iteratedFDerivWithin 𝕜 n f s
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedFDeriv 𝕜 n f = id ∘ iteratedFDeriv 𝕜 n f

Tactic:
Function.id_comp

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedFDeriv 𝕜 n f = iteratedFDeriv 𝕜 n f
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv (n + 1) f = deriv (iteratedDeriv n f)

Tactic:
rw [← iteratedDerivWithin_univ, ← iteratedDerivWithin_univ, ← derivWithin_univ]
  exact iteratedDerivWithin_succ

Goal state after:
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
      intro a' b' h'
      induction b' using Fin.induction with
      | zero => simp at h'
      | succ b =>
        induction a' using Fin.induction with
        | zero => simp
        | succ a' =>
          simp only [cases_succ, comp_apply, succ_lt_succ_iff]
          exact c.emb_strictMono m (by simpa using h')

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

Goal state before:
pp: case refine_2.inr
𝕜 : 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
k : Fin c.length
i : Fin n
hi : c.index i ≠ k
⊢ ∃ m y,
    (if h : m = k then (fun i ↦ cases 0 (succ ∘ c.emb k) i) ∘ Fin.cast ⋯ else succ ∘ c.emb m ∘ Fin.cast ⋯) y = i.succ

Tactic:
· have A : update c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i) := by
          simp [hi]
        exact ⟨c.index i, (c.invEmbedding i).cast A.symm, by simp [hi]⟩

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

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x ↦ c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) f s → iteratedDerivWithin n (fun x ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
x : 𝕜
hx : x ∈ s
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
⊢ iteratedDerivWithin (n + 1) (fun x ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)

Tactic:
have hcx : c * x ∈ s := hs hx

Goal state after:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x ↦ c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) f s → iteratedDerivWithin n (fun x ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
x : 𝕜
hx : x ∈ s
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hcx : c * x ∈ s
⊢ iteratedDerivWithin (n + 1) (fun x ↦ f (c * x)) s x = c ^ (n + 1) • iteratedDerivWithin (n + 1) f s (c * x)
Module: Mathlib.Topology.Order.Rolle

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
have ne : (Icc a b).Nonempty := nonempty_Icc.2 (le_of_lt hab)
  -- Consider absolute min and max points
  obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x :=
    isCompact_Icc.exists_isMinOn ne hfc
  obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C :=
    isCompact_Icc.exists_isMaxOn ne hfc
  by_cases hc : f c = f a
  · by_cases hC : f C = f a
    · have : ∀ x ∈ Icc a b, f x = f a := fun x hx => le_antisymm (hC ▸ Cge x hx) (hc ▸ cle x hx)
      -- `f` is a constant, so we can take any point in `Ioo a b`
      rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩
      refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩
      simp only [mem_ofPred_eq, this x hx, this c' (Ioo_subset_Icc_self hc'), le_rfl]
    · refine ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt ?_ hC, lt_of_le_of_ne Cmem.2 <| mt ?_ hC⟩, Or.inr Cge⟩
      exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
  · refine ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt ?_ hc, lt_of_le_of_ne cmem.2 <| mt ?_ hc⟩, Or.inl cle⟩
    exacts [fun h => by rw [h], fun h => by rw [h, hfI]]

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
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
⊢ False

Tactic:
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

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
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
hcont_Ioc : ∀ z ∈ Ioc a b, ContinuousWithinAt f (Icc a b) z
⊢ False
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : ℕ → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), (eapproxDiff f n) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg : ∀ (n : ℕ), ∫⁻ (x : α), ↑(g n x) ∂μ ≤ ∫⁻ (x : α), ↑((eapproxDiff f n) x) ∂μ + δ n
⊢ ∫⁻ (x : α), ∑' (n : ℕ), ↑(g n x) ∂μ = ∑' (n : ℕ), ∫⁻ (x : α), ↑(g n x) ∂μ

Tactic:
rw [lintegral_tsum fun n => (gcont n).measurable.coe_nnreal_ennreal.aemeasurable]

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

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

Tactic:
let F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)

Goal state after:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
⊢ |∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)| ≤ |x| ^ (n + 1) / (1 - |x|)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case hx
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 + 1 / (2 * a + 1) ≠ 0

pp: case hy
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 - 1 / (2 * a + 1) ≠ 0

Tactic:
· field_simp
    positivity

Goal state after:
case hy
a : ℝ
h : 0 < a
h₁ : |1 / (2 * a + 1)| < 1
h₂ : 2 * a + 1 ≠ 0
h₃ : a ≠ 0
⊢ 1 - 1 / (2 * a + 1) ≠ 0
Module: Mathlib.Analysis.Convex.Gauge

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

Tactic:
congrm sInf {r | ?_}
  exact and_congr_right fun hr => mem_smul_set_iff_inv_smul_mem₀ hr.ne' _ _

Goal state after:
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
this : 0 < a • r
⊢ a • x ∈ (a • r) • s

Tactic:
smul_assoc

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
⊢ a • x ∈ a • r • s
Module: Mathlib.Analysis.LocallyConvex.Separation

Goal state before:
pp: case refine_2
𝕜 : 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
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
u : ℝ
hfne : f ≠ 0
hA' : ∀ a ∈ s, f a ≤ u
hB' : ∀ b ∈ t, u ≤ f b
⊢ ∀ a ∈ s, re ((StrongDual.extendRCLikeₗ f) a) ≤ u

Tactic:
simpa [f.extendRCLikeₗ_apply] using hA'

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
x : E
inst✝⁴ : RCLike 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
A : Set E
hA : Convex ℝ A
hxA : x ∉ interior A
hAint : (interior A).Nonempty
this : ContinuousSMul ℝ E
f : StrongDual ℝ E
hfne : f ≠ 0
hA' : ∀ a ∈ A, f a ≤ f x
⊢ ∀ a ∈ A, re ((StrongDual.extendRCLikeₗ f) a) ≤ re ((StrongDual.extendRCLikeₗ f) x)

Tactic:
simpa [f.extendRCLikeₗ_apply] using hA'

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
g : α → EReal
g_lt_f : ∀ (x : α), ↑(-f x) < g x
gcont : LowerSemicontinuous g
g_integrable : Integrable (fun x ↦ (g x).toReal) μ
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ⊤
gint : ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), -f x ∂μ + ε
⊢ ∀ (x : α), (fun x ↦ -g x) x < ↑(f x)

Tactic:
exact fun x => EReal.neg_lt_comm.1 (by simpa only [EReal.coe_neg] using g_lt_f x)

Goal state after:
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
inst✝ : Zero X
f : X → R
g : C(X, R)₀
x : X
hf : Continuous[inst✝², inst✝¹] f
hf₀ : f 0 = 0
⊢ { toFun := f, continuous_toFun := hf, map_zero' := hf₀ } x = f x

Tactic:
coe_mk,

Goal state after:
X : Type u_1
R : Type u_2
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
inst✝ : Zero X
f : X → R
g : C(X, R)₀
x : X
hf : Continuous[inst✝², inst✝¹] f
hf₀ : f 0 = 0
⊢ { toFun := f, continuous_toFun := hf } x = f x
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)₀
x : ↑s
hf : ContinuousOn f s
hf₀ : f ↑0 = 0
⊢ { toFun := s.domRestrict f, continuous_toFun := ⋯, map_zero' := hf₀ } x = f ↑x

Tactic:
coe_mk,

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)₀
x : ↑s
hf : ContinuousOn f s
hf₀ : f ↑0 = 0
⊢ { toFun := s.domRestrict f, continuous_toFun := ⋯ } x = f ↑x
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ∫ (x : X), ↑(re (f x)) ∂μ + (∫ (x : X), ↑(im (f x)) ∂μ) * I = ∫ (x : X), f x ∂μ

Tactic:
rw [mul_comm, ← smul_eq_mul, ← integral_smul, ← integral_add]

Goal state after:
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ∫ (a : X), ↑(re (f a)) + I • ↑(im (f a)) ∂μ = ∫ (x : X), f x ∂μ

case hf
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Integrable (fun x ↦ ↑(re (f x))) μ

case hg
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ Integrable (fun a ↦ I • ↑(im (f a))) μ
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)‖ₑ ≠ ∞
⊢ ‖f (min a b - 0)‖ₑ ≠ ∞

Tactic:
sub_zero

Goal state after:
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst✝ : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ ‖f (min a b)‖ₑ ≠ ∞
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
⊢ Icc a b ⊆ {t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal}

Tactic:
refine s_closed.Icc_subset_of_forall_exists_gt
      (by simp only [integral_same, mem_ofPred_eq, sub_self, le_rfl]) fun t ht v t_lt_v => ?_

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
⊢ ({t | g t - g a ≤ ∫ (u : ℝ) in a..t, (G' u).toReal} ∩ Ioc t v).Nonempty
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case h₂
𝕜 : 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 : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this✝ : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst✝] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ ‖f a y - f a' y‖ ≤ ε

Tactic:
rw [← dist_eq_norm']

Goal state after:
case h₂
𝕜 : 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 : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this✝ : ProperSpace E
a : α
x : E
r' : ℝ
hr :
  ∀ (y : E),
    dist y (a, x).2 < r' → ∀ (z : E), dist z (a, x).2 < r' → ‖f (a, x).1 z - f (a, x).1 y - (L z - L y)‖ < s * r
Irr' : r / 2 < r'
Ir'r : r' ≤ r
t : ℝ
hrt : r / 2 < t
htr' : t < r'
t' : ℝ
hrt' : r / 2 < t'
ht't : t' < t
b : ℝ
b_lt : b < s * r
hb : ∀ y ∈ closedBall x t, ∀ z ∈ closedBall x t, ‖f a z - f a y - (L z - L y)‖ ≤ b
ε : ℝ
εpos : 0 < ε
hε : b + 2 * ε < s * r
u : Set α
u_open : IsOpen[inst✝] u
au : a ∈ u
hu : ∀ (p : α × E), p.1 ∈ u → p.2 ∈ closedBall x t → dist (Function.uncurry f p) (Function.uncurry f (a, p.2)) < ε
this : u ×ˢ ball x (t - t') ∈ 𝓝 (a, x)
a' : α
x' : E
ha'x' : a' ∈ u ∧ dist x' x < t - t'
y : E
hy : dist y (a', x').2 < t'
z : E
hz : dist z (a', x').2 < t'
dyx : dist y x ≤ t
dzx : dist z x ≤ t
⊢ dist (f a' y) (f a y) ≤ ε
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Goal state before:
pp: case pos
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
⊢ IntegrableOn g' (Ioc a b) volume

Tactic:
integrableOn_Ioc_iff_integrableOn_Ioo

Goal state after:
case pos
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
⊢ IntegrableOn g' (Ioo a b) volume
Module: Mathlib.Order.Filter.AtTopBot.Floor

Goal state before:
pp: case calc_2
K : Type u_1
inst✝³ : Ring K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorSemiring K
a c : K
d n : ℕ
h : ⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n < (n - d)!
⊢ ↑⌈|a|⌉₊ * ↑⌈|c|⌉₊ ^ n = ↑(⌈|a|⌉₊ * ⌈|c|⌉₊ ^ n)

Tactic:
simp_rw [Nat.cast_mul, Nat.cast_pow]

Goal state after: