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

Goal state before:
pp: case fderivWithin
𝕜 : 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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) → (E [×m]→L[𝕜] F) → G [×m]→L[𝕜] F := ⋯
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ x ∈ ⇑g ⁻¹' s,
        HasFDerivWithinAt (fun x ↦ (p (g x) m).compContinuousLinearMap fun x ↦ g.contLinear)
          ((p (g x) m.succ).compContinuousLinearMap fun x ↦ g.contLinear).curryLeft (⇑g ⁻¹' s) x

Tactic:
intro m hm x hx
    convert!
      (hA m).hasFDerivAt.comp_hasFDerivWithinAt x
        ((hf.fderivWithin m hm (g x) hx).comp x g.hasFDerivWithinAt (Subset.refl _))
    ext y v
    change p (g x) (Nat.succ m) (g.contLinear ∘ cons y v)
      = p (g x) m.succ (cons (g.contLinear y) (g.contLinear ∘ v))
    rw [comp_cons]

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ ContDiff 𝕜 ∞ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ∞ (deriv f)

Tactic:
rw [show (∞ : ℕ∞ω) = ∞ + 1 from rfl, contDiff_succ_iff_deriv]

Goal state after:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ Differentiable 𝕜 f ∧ (∞ = ω → AnalyticOn 𝕜 f univ) ∧ ContDiff 𝕜 ∞ (deriv f) ↔
    Differentiable 𝕜 f ∧ ContDiff 𝕜 (∞ + 1) (deriv f)
Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
⊢ e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s) = e.target ∩ t

Tactic:
rw [iff_symm_preimage_eq, ← image_source_inter_eq, ← image_source_inter_eq']

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

Goal state before:
pp: case refine_2
𝕜 : 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
i : Fin c.length
⊢ StrictMono
    (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) i.succ)

Tactic:
· exact strictMono_succ.comp (c.emb_strictMono i)

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✝ c : OrderedFinpartition n
⊢ ∀ (m : Fin (c.length + 1)),
    StrictMono
      (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m)

Tactic:
by
    refine Fin.cases ?_ (fun i ↦ ?_)
    · exact @Subsingleton.strictMono _ _ _ _ (by simp; infer_instance) _
    · exact strictMono_succ.comp (c.emb_strictMono i)

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

Goal state before:
pp: case none
𝕜 : 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
H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s
⊢ ContDiffOn 𝕜 (↑none) f s

pp: case some
𝕜 : 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
H : ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s
n : ℕ
⊢ ContDiffOn 𝕜 (↑(some n)) f s

Tactic:
exacts [contDiffOn_infty.2 H, H n]

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
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i j : Fin c.length
hij : i < j
⊢ ↑(if h : i = c.index 0 then
        (c.emb i (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1, ⋯⟩.succ)).pred ⋯
      else (c.emb i (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1, ⋯⟩)).pred ⋯) <
    ↑(if h : j = c.index 0 then
        (c.emb j (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1, ⋯⟩.succ)).pred ⋯
      else (c.emb j (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1, ⋯⟩)).pred ⋯)

Tactic:
rw [← Nat.add_lt_add_iff_right (k := 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
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
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i j : Fin c.length
hij : i < j
⊢ ↑(if h : i = c.index 0 then
          (c.emb i (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1, ⋯⟩.succ)).pred ⋯
        else (c.emb i (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i - 1, ⋯⟩)).pred ⋯) +
      1 <
    ↑(if h : j = c.index 0 then
          (c.emb j (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1, ⋯⟩.succ)).pred ⋯
        else (c.emb j (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1, ⋯⟩)).pred ⋯) +
      1
Module: Mathlib.Analysis.Complex.RealDeriv

Goal state before:
pp: z : ℝ
f : ℝ → ℝ
s : Set ℝ
u : ℝ
hf : HasDerivWithinAt f u s z
⊢ HasDerivWithinAt (fun y ↦ ↑(f y)) (↑u) s z

Tactic:
simpa only [Function.comp_apply, ofRealCLM_apply] using!
    ofRealCLM.hasFDerivAt.comp_hasDerivWithinAt z hf

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

Goal state before:
pp: case neg.emb
𝕜 : 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✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (c.emb 0) = {0}
B : c.partSize (c.index 0) - 1 + 1 = c.partSize (c.index 0)
⊢ { length := c.length,
        partSize :=
          update (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1)) (c.index 0)
            (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) + 1),
        partSize_pos := ⋯,
        emb := fun m ↦
          if h_1 : m = c.index 0 then
            (fun i ↦ cases 0 (succ ∘ fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯) i) ∘ Fin.cast ⋯
          else
            succ ∘
              (fun j ↦
                  if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯) ∘
                Fin.cast ⋯,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.emb ≍
    c.emb

Tactic:
· refine hfunext rfl ?_
        simp only [heq_eq_eq, forall_eq']
        intro i
        refine ((Fin.heq_fun_iff ?_).mpr ?_).symm
        · simp only [update_self, B, update_idem, update_eq_self]
        · intro j
          rcases eq_or_ne i (c.index 0) with rfl | hi
          · simp only [↓reduceDIte, comp_apply]
            rcases eq_or_ne j 0 with rfl | hj
            · simpa using c.emb_zero
            · let j' := Fin.pred (j.cast B.symm) (by simpa using hj)
              have : j = (succ j').cast B := by simp [j']
              simp only [this, val_cast, val_succ, cast_mk, cases_succ', comp_apply, succ_mk,
                succ_pred]
              rfl
          · simp [hi]

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
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : ℕ∞ω
⊢ HasFTaylorSeriesUpToOn n (fun x i ↦ φ i x) (fun x m ↦ ContinuousMultilinearMap.pi fun i ↦ p' i x m) s ↔
    ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s

Tactic:
set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _
  set L : ∀ m : ℕ, (∀ i, E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] ∀ i, F' i := fun m =>
    ContinuousMultilinearMap.piₗᵢ _ _
  refine ⟨fun h i => ?_, fun h => ⟨fun x hx => ?_, ?_, ?_⟩⟩
  · exact h.continuousLinearMap_comp (pr i)
  · ext1 i
    exact (h i).zero_eq x hx
  · intro m hm x hx
    exact (L m).hasFDerivAt.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.2 fun i => (h i).fderivWithin m hm x hx
  · intro m hm
    exact (L m).continuous.comp_continuousOn <| continuousOn_pi.2 fun i => (h i).cont m hm

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
s : Set E
x : E
n : ℕ∞ω
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
⊢ ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x ↦ Φ x i) s x

Tactic:
by
  set pr := @ContinuousLinearMap.proj 𝕜 _ ι F' _ _ _
  refine ⟨fun h i => h.continuousLinearMap_comp (pr i), fun h ↦ ?_⟩
  match n with
  | ω =>
    choose u hux p hp h'p using h
    refine ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _, fun m ↦ ?_⟩
    set L : (∀ i, E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] ∀ i, F' i :=
      ContinuousMultilinearMap.piₗᵢ _ _
    change AnalyticOn 𝕜 (fun x ↦ L (fun i ↦ p i x m)) (⋂ i, u i)
    apply (L.analyticOnNhd univ).comp_analyticOn ?_ (mapsTo_univ _ _)
    exact AnalyticOn.pi (fun i ↦ (h'p i m).mono (iInter_subset _ _))
  | (n : ℕ∞) =>
    intro m hm
    choose u hux p hp using fun i => h i m hm
    exact ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
      hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩

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
n : ℕ∞ω
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
⊢ ContDiff 𝕜 n Φ ↔ ∀ (i : ι), ContDiff 𝕜 n fun x ↦ Φ x i

Tactic:
by
  simp only [← contDiffOn_univ, contDiffOn_pi]

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s
⊢ y ∈ posTangentConeAt s x

Tactic:
by
  rw [← NNReal.coe_zero, ← NNReal.map_coe_nhdsGT, frequently_map, frequently_iff_neBot] at h
  apply mem_tangentConeAt_of_add_smul_mem (l := 𝓝[>] (0 : ℝ≥0) ⊓ 𝓟 {t | x + (t : ℝ) • y ∈ s})
  · exact tendsto_id'.mpr <| inf_le_left.trans <| nhdsGT_le_nhdsNE _
  · simp [eventually_inf_principal, NNReal.smul_def]

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
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:
rw [(by aesop : (∑ j ∈ u, f j) = (fun x ↦ ∑ j ∈ u, f j x))]

Goal state after:
𝕜 : 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 (fun x ↦ ∑ j ∈ u, f j x) s x = ∑ j ∈ u, 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 : ℕ
f : 𝕜 → F
a : 𝕜
⊢ iteratedDeriv n (-f) a = -iteratedDeriv n f a

Tactic:
simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_neg f

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

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

Tactic:
show Tendsto (fun n : ℕ => ∑ i ∈ range n, x ^ (i + 1) / (i + 1)) atTop (𝓝 (-log (1 - x)))

Goal state after:
x : ℝ
h : |x| < 1
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1)) atTop (𝓝 (-log (1 - x)))
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ gauge s (r • x) = gauge s (‖r‖ • x)

Tactic:
gauge_norm_smul hs

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
inst✝² : RCLike 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsScalarTower ℝ 𝕜 E
hs : Balanced 𝕜 s
r : 𝕜
x : E
⊢ gauge s (r • x) = gauge s (r • x)
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case refine_2.hf
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
If : ∫⁻ (x : α), ↑(f x) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε
Ig : ∫⁻ (x : α), ↑(g x) ∂μ < ∞
⊢ 0 ≤ᵐ[μ] fun x ↦ ↑(f x)

pp: case refine_2.hfm
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
If : ∫⁻ (x : α), ↑(f x) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε
Ig : ∫⁻ (x : α), ↑(g x) ∂μ < ∞
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x)) μ

Tactic:
· apply Filter.Eventually.of_forall; simp

Goal state after:
case refine_2.hfm
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
ε : ℝ≥0
εpos : 0 < ↑ε
If : ∫⁻ (x : α), ↑(f x) ∂μ < ∞
g : α → ℝ≥0
gf : ∀ (x : α), g x ≤ f x
gcont : UpperSemicontinuous g
gint : ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ↑ε
Ig : ∫⁻ (x : α), ↑(g x) ∂μ < ∞
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x)) μ
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
x : E
ε : ℝ
hε : 0 < ε
hs₂ : IsOpen[inst✝¹] s
hx : x ∈ ε • s
⊢ gauge s x < ε

Tactic:
have : ε⁻¹ • x ∈ s := by rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne']
  have h_gauge_lt := gauge_lt_one_of_mem_of_isOpen hs₂ this
  rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff₀ hε, mul_one]
    at h_gauge_lt

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

Goal state before:
pp: case inl
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
ht₁ : Convex ℝ t
ht₃ : IsOpen t
hs₁ : Convex ℝ ∅
hs₂ : IsOpen ∅
disj : Disjoint ∅ t
⊢ ∃ f u, (∀ a ∈ ∅, f a < u) ∧ ∀ b ∈ t, u < f b

pp: case inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u < f b

Tactic:
· exact ⟨0, -1, by simp, fun b _hb => by simp⟩

Goal state after:
case inr
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
⊢ ∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u < f b
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

Goal state after:
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
s_meas : MeasurableSet s
hs : (μ.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 ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap

Goal state before:
pp: case inr
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))
u v : X → E
huv : u =ᵐ[μ.withDensity fun x ↦ ↑(f x)] v
a✝ : Integrable u (μ.withDensity fun x ↦ ↑(f x))
hu : (∫ (x : X), u x ∂μ.withDensity fun x ↦ ↑(f x)) = ∫ (x : X), f x • u x ∂μ
x : X
hx : ↑(f x) ≠ 0 → u x = v x
h'x : f x ≠ 0
⊢ f x • u x = f x • v x

Tactic:
· rw [hx _]
      simpa only [Ne, ENNReal.coe_eq_zero] using h'x

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ℝ
⊢ FTCFilter a (𝓝[{a}] a) ⊥

Tactic:
by
  rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]; infer_instance

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
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
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun p ↦ f a p.2
b : α
y : E
hb : (b, y).1 ∈ {a}
⊢ Function.uncurry f (b, y) = (fun p ↦ f a p.2) (b, y)

Tactic:
simp only [mem_singleton_iff] at hb

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : LocallyCompactSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
α : Type u_4
inst✝ : TopologicalSpace α
f : α → E → F
r s : ℝ
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
C : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun p ↦ f a p.2
b : α
y : E
hb : b = a
⊢ Function.uncurry f (b, y) = (fun p ↦ f a p.2) (b, y)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: E : Type u_5
inst✝⁴ : NormedAddCommGroup E
μ : Measure ℝ
inst✝³ : IsLocallyFiniteMeasure μ
inst✝² : ConditionallyCompleteLinearOrder E
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
u : ℝ → E
a b : ℝ
hu : MonotoneOn u [[a, b]]
⊢ IntegrableOn u (Ι a b) μ

Tactic:
exact (hu.integrableOn_isCompact isCompact_uIcc).mono_set Ioc_subset_Icc_self

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 ∂μ

Tactic:
rw [← add_neg_eq_zero, ← integral_symm, integral_add_adjacent_intervals_cancel hab hbc]

Goal state after: