mathlib-initiative/mathlib-tactics huggingface dataset:
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
x✝ : (i : Fin c.length) × Fin (c.partSize i)
⊢ (fun i ↦ ⟨c.index i, c.invEmbedding i⟩) ((fun p ↦ c.emb p.fst p.snd) x✝) = x✝

Tactic:
apply c.emb_injective

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
x✝ : (i : Fin c.length) × Fin (c.partSize i)
⊢ (fun p ↦ c.emb p.fst p.snd) ((fun i ↦ ⟨c.index i, c.invEmbedding i⟩) ((fun p ↦ c.emb p.fst p.snd) x✝)) =
    (fun p ↦ c.emb p.fst p.snd) x✝
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case succ
𝕜 : 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 + 1)
j : Fin c.length
a✝ :
  i < j.castSucc →
    (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        i <
      (fun m ↦
          cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
            ⟨cons 1 c.partSize m - 1, ⋯⟩)
        j.castSucc
hij : i < j.succ
⊢ (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      i <
    (fun m ↦
        cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m
          ⟨cons 1 c.partSize m - 1, ⋯⟩)
      j.succ

Tactic:
induction i using Fin.induction with

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
i : Fin (c.length + 1)
hi : i ∈ univ
j : Fin (c.length + 1)
hj : j ∈ univ
hij : i ≠ j
h : j < i
⊢ (Disjoint on fun m ↦
      range (cases (motive := fun x ↦ Fin (cons 1 c.partSize x) → Fin (n + 1)) (fun x ↦ 0) (fun m ↦ succ ∘ c.emb m) m))
    i j

Tactic:
induction i using Fin.induction with

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
⊢ ∀ (a' b' : Fin (c.partSize m + 1)), a' < b' → cases 0 (succ ∘ c.emb m) a' < cases 0 (succ ∘ c.emb m) b'

Tactic:
intro a'

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' : Fin (c.partSize m + 1)
⊢ ∀ (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: 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
i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
⊢ ∀ (a' : Fin (c.partSize i)) (b' : Fin (c.partSize j + 1)), (c.emb i a').succ ≠ cases 0 (succ ∘ c.emb j) b'

Tactic:
intro a'

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
i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj : j ∈ univ
hij h : i ≠ j
a' : Fin (c.partSize i)
⊢ ∀ (b' : Fin (c.partSize j + 1)), (c.emb i a').succ ≠ cases 0 (succ ∘ c.emb j) b'
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case 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✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
hi : i ≠ c.index 0
⊢ 0 < update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i

Tactic:
· simp only [ne_eq, hi, not_false_eq_true, update_of_ne]
      exact c.partSize_pos i

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

Goal state before:
pp: case pos.partSize
𝕜 : 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}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
⊢ { length := c.length - 1 + 1, partSize := cons 1 fun i ↦ c.partSize (Fin.cast ⋯ i.succ), partSize_pos := ⋯,
          emb := fun i ↦
            cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
              (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i,
          emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.partSize
      i =
    c.partSize ⟨↑i, ⋯⟩

Tactic:
induction i using Fin.induction with

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝³ : DivisionRing 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : CharZero 𝔸
⊢ exp = fun x ↦ ∑' (n : ℕ), x ^ n / ↑n !

Tactic:
rw [exp_eq_expSeries_sum ℚ]
  ext x
  exact expSeries_sum_eq_div x

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

Goal state before:
pp: case pos.emb.refine_1
𝕜 : 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}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
⊢ cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i = c.partSize (Fin.cast A i)

Tactic:
induction i using Fin.induction with

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

Goal state before:
pp: case pos.emb.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✝ : OrderedFinpartition n✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : range (c.emb 0) = {0}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
h' : i ≍ Fin.cast A i
j : Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) i)
⊢ cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
      (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i j =
    c.emb (Fin.cast A i) ⟨↑j, ⋯⟩

Tactic:
induction i using Fin.induction with

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : CompleteSpace 𝔸
inst✝¹ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
inst✝ : Invertible (exp x)
⊢ ⅟(exp x) = exp (-x)

Tactic:
by
  let := invertibleExpOfMemBall hx; convert! (rfl : ⅟(exp x) = _)

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : CharZero 𝕂
inst✝² : ContinuousSMul ℚ 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
⊢ 0 < ∞

Tactic:
exact WithTop.top_pos

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

Goal state before:
pp: case pos.e_6.hf
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ Injective (c.emb (c.index j))

Tactic:
exact (c.emb_strictMono (c.index j)).injective

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
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
⊢ ‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i, ‖p i‖

Tactic:
refine ContinuousMultilinearMap.opNorm_le_bound (by positivity) fun v ↦ ?_

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
n : ℕ
c : OrderedFinpartition n
f : F [×c.length]→L[𝕜] G
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
v : Fin n → E
⊢ ‖(c.compAlongOrderedFinpartition f p) v‖ ≤ (‖f‖ * ∏ i, ‖p i‖) * ∏ i, ‖v i‖
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
s : Set 𝕜
𝕜' : Type u_6
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
d : 𝕜'
n : ℕ
IH : ∀ {x : 𝕜} (f : 𝕜 → 𝕜'), iteratedDerivWithin n (fun z ↦ f z * d) s x = iteratedDerivWithin n f s x * d
x : 𝕜
f : 𝕜 → 𝕜'
⊢ iteratedDerivWithin (n + 1) (fun z ↦ f z * d) s x = iteratedDerivWithin (n + 1) f s x * d

Tactic:
simp_rw [iteratedDerivWithin_succ, funext (@IH · f), derivWithin_mul_const_field]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
s : Set 𝕜
𝕜' : Type u_6
inst✝¹ : NormedDivisionRing 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
d : 𝕜'
⊢ iteratedDerivWithin n (fun z ↦ f z * d) s x = iteratedDerivWithin n f s x * d

Tactic:
induction n generalizing f x with
  | zero => simp
  | succ n IH =>
    simp_rw [iteratedDerivWithin_succ, funext (@IH · f), derivWithin_mul_const_field]

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

Goal state before:
pp: n : ℕ
c : ℂ
⊢ (fun x ↦ c ^ n * deriv^[n] cexp (c * x)) = fun s ↦ c ^ n * cexp (c * s)

Tactic:
iter_deriv_exp

Goal state after:
n : ℕ
c : ℂ
⊢ (fun x ↦ c ^ n * cexp (c * x)) = fun s ↦ c ^ n * cexp (c * s)
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: n : ℕ
c : ℝ
⊢ (fun x ↦ c ^ n * deriv^[n] rexp (c * x)) = fun s ↦ c ^ n * rexp (c * s)

Tactic:
iter_deriv_exp

Goal state after:
n : ℕ
c : ℝ
⊢ (fun x ↦ c ^ n * rexp (c * x)) = fun s ↦ c ^ n * rexp (c * 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
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i) f s x
hg : ContDiffWithinAt 𝕜 (↑i) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x

Tactic:
by
  have := (hf.eventually (by simp)).and (hg.eventually (by simp))
  obtain ⟨t, ht, hxt, h⟩ := mem_nhdsWithin.mp this
  have hft : ContDiffOn 𝕜 i f (s ∩ t) := fun a ha ↦ (h (by simp_all)).1.mono inter_subset_left
  have hgt : ContDiffOn 𝕜 i g (s ∩ t) := fun a ha ↦ (h (by simp_all)).2.mono inter_subset_left
  have hut : UniqueDiffOn 𝕜 (s ∩ t) := hu.inter ht
  have H : ↑(s ∩ t) =ᶠ[𝓝 x] s :=
    inter_eventuallyEq_left.mpr (eventually_of_mem (ht.mem_nhds hxt) (fun _ h _ ↦ h))
  rw [← iteratedFDerivWithin_congr_set H, ← iteratedFDerivWithin_congr_set H,
    ← iteratedFDerivWithin_congr_set H]
  exact .symm (((hft.ftaylorSeriesWithin hut).add
      (hgt.ftaylorSeriesWithin hut)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hut ⟨hx, hxt⟩)

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
x : E
n : ℕ∞ω
f : E → F
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt 𝕜 n (fun x ↦ -f x) x

Tactic:
by rw [← contDiffWithinAt_univ] at *; exact hf.neg

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

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

Tactic:
have ne_top : μ s ≠ ⊤ := by
      simpa [f, hs, hc, lt_top_iff_ne_top, SimpleFunc.coe_const,
        Function.const_apply, lintegral_const, ENNReal.coe_indicator, Set.univ_inter,
        ENNReal.coe_ne_top, MeasurableSet.univ, ENNReal.mul_eq_top, SimpleFunc.const_zero,
        lintegral_indicator, ENNReal.coe_eq_zero, Ne, not_false_iff,
        SimpleFunc.coe_zero, Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise,
        restrict_apply] using h

Goal state after:
case neg
α : 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) ∂μ = ∞
hc : ¬c = 0
ne_top : μ s ≠ ∞
⊢ ∃ g,
    (∀ (x : α), (piecewise s hs (const α c) (const α 0)) x ≤ g x) ∧
      LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case neg.refine_1
α : 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) ∂μ = ∞
hc : ¬c = 0
ne_top : μ s ≠ ∞
this : μ s < μ s + ε / ↑c
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : μ u < μ s + ε / ↑c
x : α
⊢ (piecewise s hs (const α c) (const α 0)) x ≤ u.indicator (fun x ↦ c) x

Tactic:
simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, ← Function.const_def]

Goal state after:
case neg.refine_1
α : 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) ∂μ = ∞
hc : ¬c = 0
ne_top : μ s ≠ ∞
this : μ s < μ s + ε / ↑c
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : μ u < μ s + ε / ↑c
x : α
⊢ s.indicator (fun x ↦ c) x ≤ u.indicator (fun x ↦ c) x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
⊢ StrictMonoOn f D

Tactic:
intro x hx y hy

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x < y → f x < f y
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: n : ℕ∞ω
x : ℝ
⊢ ContDiffAt ℝ n log x ↔ x ≠ 0

Tactic:
refine ⟨fun h ↦ continuousAt_log_iff.1 h.continuousAt, fun hx ↦ ?_⟩
  have A y (hy : 0 < y) : ContDiffAt ℝ n log y := by
    apply expPartialHomeomorph.contDiffAt_symm_deriv (f₀' := y) hy.ne' (by simpa)
    · convert! hasDerivAt_exp (log y)
      rw [exp_log hy]
    · exact analyticAt_rexp.contDiffAt
  rcases hx.lt_or_gt with hx | hx
  · have : ContDiffAt ℝ n (log ∘ (fun y ↦ -y)) x := by
      apply ContDiffAt.comp
      · apply A _ (Left.neg_pos_iff.mpr hx)
      apply contDiffAt_id.neg
    convert! this
    ext x
    simp
  · exact A x hx

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

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
⊢ ⟨c, hc⟩ • x ∈ ↑C

Tactic:
SetLike.mem_coe

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
C✝ C₁ C₂ : PointedCone R E
x✝¹ : E
r : R
C : ConvexCone R E
hC : C.Pointed
x✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
x : E
hx : x ∈ ↑C
c : R
hc : 0 ≤ c
⊢ ⟨c, hc⟩ • x ∈ C
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

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

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

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

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
x : α
⊢ F.indicator (fun x ↦ c) x ≤ (piecewise s hs (const α c) (const α 0)) x

Tactic:
simp only [SimpleFunc.coe_const, SimpleFunc.const_zero, SimpleFunc.coe_zero,
        Set.piecewise_eq_indicator, SimpleFunc.coe_piecewise, ← Function.const_def]

Goal state after:
case neg.refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
c : ℝ≥0
s : Set α
hs : MeasurableSet s
int_f : ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
hc : ¬c = 0
μs_lt_top : μ s < ∞
this : 0 < ε / ↑c
F : Set α
Fs : F ⊆ s
F_closed : IsClosed F
μF : μ s < μ F + ε / ↑c
x : α
⊢ F.indicator (fun x ↦ c) x ≤ s.indicator (fun x ↦ c) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: case inr
a : ℝ
h : 0 ≤ a
ha0 : a ≠ 0
⊢ HasSum (fun k ↦ 2 * (1 / (2 * ↑k + 1)) * (a / (a + 2)) ^ (2 * k + 1)) (log (1 + a))

Tactic:
· convert! hasSum_log_one_add_inv (inv_pos.mpr (lt_of_le_of_ne h ha0.symm)) using 4
    all_goals simp [field, add_comm]

Goal state after:
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
⊢ ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s

Tactic:
rintro ⟨x, y⟩

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
x : E
y : ℝ
⊢ ∃ x_1, ↑x_1 + (x, y) ∈ s
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case hy
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := ⋯
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := ⋯
h'k : y - x ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < y - x
m_ge : n e ≤ m
km : k = m + 1
⊢ x ∈ Icc x (x + (1 / 2) ^ m / 2)

Tactic:
simp only [one_div, inv_pow, left_mem_Icc, le_add_iff_nonneg_right]
            positivity

Goal state after: