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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖ ^ (n + 1)‖

Tactic:
simp_rw [norm_pow, pow_succ, ← mul_assoc, norm_norm]

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖x - x₀‖ ^ n * ‖x - x₀‖
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : 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 ≠ ∞
⊢ ContDiffWithinAt 𝕜 n f s x ↔
    ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn n f p u ∧ (n = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u)

Tactic:
by
  match n with
  | ω => simp [ContDiffWithinAt]
  | ∞ => simp at hn
  | (n : ℕ) => simp [contDiffWithinAt_nat]

Goal state after:
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
h : e.IsImage s t
⊢ e.IsImage (interior s) (interior t)

Tactic:
simpa only [closure_compl, compl_compl] using h.compl.closure.compl

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
⊢ cases 0 (succ ∘ c.emb m) ⟨c.partSize m, ⋯⟩ = (c.emb m ⟨c.partSize m - 1, ⋯⟩).succ

Tactic:
let a : Fin (c.partSize m + 1) := ⟨c.partSize m, lt_add_one (c.partSize m)⟩

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) := ⟨c.partSize m, ⋯⟩
⊢ cases 0 (succ ∘ c.emb m) ⟨c.partSize m, ⋯⟩ = (c.emb m ⟨c.partSize m - 1, ⋯⟩).succ
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case refine_1.zero_eq
𝕜 : 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
n : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
⊢ ∀ x ∈ s, (ftaylorSeriesWithin 𝕜 f s x 0).curry0 = f x

Tactic:
intro y _
      simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply,
        iteratedFDerivWithin_zero_apply]

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}
x : Fin n
⊢ ∃ m,
    x ∈
      range fun j ↦
        have this := ⋯;
        (c.emb (Fin.cast this m.succ) j).pred ⋯

Tactic:
by
    simp only [mem_range]
    obtain ⟨i, j, hij⟩ : ∃ (i : Fin c.length), ∃ (j : Fin (c.partSize i)), c.emb i j = succ x :=
      ⟨c.index (succ x), c.invEmbedding (succ x), by simp⟩
    have A : c.length = c.length - 1 + 1 :=
      (Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))).symm
    have i_ne : i ≠ 0 := by
      intro h
      have : succ x ∈ range (c.emb i) := by rw [← hij]; apply mem_range_self
      rw [h, hc, mem_singleton_iff] at this
      exact Fin.succ_ne_zero _ this
    refine ⟨pred (Fin.cast A i) (by simpa using i_ne), Fin.cast (by simp) j, ?_⟩
    have : x = pred (succ x) (succ_ne_zero x) := rfl
    rw [this]
    congr
    rw [← hij]
    congr 1
    · simp
    · simp [Fin.heq_ext_iff]

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✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
a b : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0))
hab : a < b
⊢ (fun j ↦
        if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
        else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯)
      a <
    (fun j ↦
        if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
        else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯)
      b

Tactic:
simp only [↓reduceDIte, Nat.succ_eq_add_one, pred_lt_pred_iff]
      exact (c.emb_strictMono _).comp (cast_strictMono _) (by simpa using hab)

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✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
a b : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0))
hab : a < b
⊢ (fun j ↦
        if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
        else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯)
      a <
    (fun j ↦
        if h : c.index 0 = c.index 0 then (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯
        else (c.emb (c.index 0) (Fin.cast ⋯ j)).pred ⋯)
      b

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
a b : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
hab : a < b
hi : i ≠ c.index 0
⊢ (fun j ↦ if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) a <
    (fun j ↦ if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) b

Tactic:
· simp only [↓reduceDIte, Nat.succ_eq_add_one, pred_lt_pred_iff]
      exact (c.emb_strictMono _).comp (cast_strictMono _) (by simpa using hab)

Goal state after:
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
a b : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
hab : a < b
hi : i ≠ c.index 0
⊢ (fun j ↦ if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) a <
    (fun j ↦ if h : i = c.index 0 then (c.emb i (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb i (Fin.cast ⋯ j)).pred ⋯) b
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
A : 1 < c.partSize (c.index 0)
⊢ 0 = ↑(c.emb (c.index 0) 0)

Tactic:
simp [emb_zero]

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 : Fin c.length
hij : i < c.index 0
A : 1 < c.partSize (c.index 0)
⊢ 0 = ↑(c.emb (c.index 0) 0)

Tactic:
simp [emb_zero]

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

Goal state before:
pp: case neg
𝕜 : 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}
⊢ (if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩).fst.extend
      (if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩).snd =
    c

Tactic:
dif_neg h

Goal state after:
case neg
𝕜 : 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}
⊢ ⟨c.eraseMiddle h, some (c.index 0)⟩.fst.extend ⟨c.eraseMiddle h, some (c.index 0)⟩.snd = c
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 y : 𝔸
hxy : Commute x y
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hy : y ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
n : ℕ
kl : ℕ × ℕ
hkl : kl ∈ Finset.antidiagonal n
⊢ ((↑n !)⁻¹ * (↑n ! / (↑kl.1! * ↑kl.2!))) • (x ^ kl.1 * y ^ kl.2) = ((↑kl.1!)⁻¹ * (↑kl.2!)⁻¹) • (x ^ kl.1 * y ^ kl.2)

Tactic:
field_simp [n.factorial_ne_zero]

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

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

Tactic:
← exp_add_of_commute_of_mem_ball (Commute.neg_left <| Commute.refl x) hnx hx,

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : CompleteSpace 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
hx : x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
hnx : -x ∈ Metric.eball 0 (expSeries 𝕂 𝔸).radius
⊢ exp (-x + x) = 1
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
  rw [sub_eq_add_neg, iteratedFDerivWithin_add_apply hf _ hu hx,
    iteratedFDerivWithin_neg_apply hu hx, sub_eq_add_neg]
  exact hg.neg

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
A :
  ∀ (c : OrderedFinpartition m),
    HasFDerivWithinAt (fun x ↦ (q (f x)).compAlongOrderedFinpartition (p x) c)
      (∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
B :
  HasFDerivWithinAt (fun x ↦ (q (f x)).taylorComp (p x) m)
    (∑ c, ∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x
this : ∑ c, ∑ i, (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i) = (q (f x)).taylorComp (p x) (m + 1)
v : E
x✝ : Fin m → E
⊢ ((∑ c, ∑ i, (q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft v) x✝ =
    ((∑ c, ∑ i, ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) v) x✝

Tactic:
simp only [Nat.succ_eq_add_one, Fintype.sum_option, ContinuousMultilinearMap.curryLeft_apply,
        FormalMultilinearSeries.compAlongOrderedFinpartition_apply, sum_apply, add_apply]

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

Goal state before:
pp: case right
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ f' c = (f b - f a) / (b - a)

Tactic:
rwa [mul_one, mul_comm, ← eq_div_iff (sub_ne_zero.2 hab.ne')] at hc

Goal state after:
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) ∂μ = ∞
hc : ¬c = 0
ne_top : μ s ≠ ∞
this : μ s < μ s + ε / ↑c
u : Set α
su : u ⊇ s
u_open : IsOpen u
μu : μ u < μ s + ε / ↑c
⊢ ↑c * μ s + ↑c * (ε / ↑c) = ↑c * μ s + ε

Tactic:
ENNReal.mul_div_cancel _ ENNReal.coe_ne_top

Goal state after:
α : 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
⊢ ↑c * μ s + ε = ↑c * μ s + ε

α : 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
⊢ ↑c ≠ 0
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case refine_2
α : 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
⊢ LowerSemicontinuous fun x ↦ ∑' (n : ℕ), ↑(g n x)

Tactic:
refine lowerSemicontinuous_tsum fun n => ?_
    exact
      ENNReal.continuous_coe.comp_lowerSemicontinuous (gcont n) fun x y hxy =>
        ENNReal.coe_le_coe.2 hxy

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

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this✝ : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : {x | (fun x ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∈ s
this : s.indicator (fun _x ↦ ∞) x ≤ g1 x
⊢ ↑(f x) < (fun x ↦ g0 x + g1 x) x

Tactic:
simp only [h, Set.indicator_of_mem, top_le_iff] at this

Goal state after:
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fmeas : AEMeasurable f μ
ε : ℝ≥0∞
ε0 : ε ≠ 0
this✝ : ε / 2 ≠ 0
g0 : α → ℝ≥0∞
f_lt_g0 : ∀ (x : α), ↑(AEMeasurable.mk f fmeas x) < g0 x
g0_cont : LowerSemicontinuous g0
g0_int : ∫⁻ (x : α), g0 x ∂μ ≤ ∫⁻ (x : α), ↑(AEMeasurable.mk f fmeas x) ∂μ + ε / 2
s : Set α
hs : {x | (fun x ↦ f x = AEMeasurable.mk f fmeas x) x}ᶜ ⊆ s
smeas : MeasurableSet s
μs : μ s = 0
g1 : α → ℝ≥0∞
le_g1 : ∀ (x : α), s.indicator (fun _x ↦ ∞) x ≤ g1 x
g1_cont : LowerSemicontinuous g1
g1_int : ∫⁻ (x : α), g1 x ∂μ ≤ ∫⁻ (x : α), s.indicator (fun _x ↦ ∞) x ∂μ + ε / 2
x : α
h : x ∈ s
this : g1 x = ∞
⊢ ↑(f x) < (fun x ↦ g0 x + g1 x) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
hx : 0 < x
this : HasStrictDerivAt log (rexp (log x))⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x

Tactic:
exp_log hx

Goal state after:
x : ℝ
hx : 0 < x
this : HasStrictDerivAt log x⁻¹ x
⊢ HasStrictDerivAt log x⁻¹ x
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 : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ Integrable (fun x ↦ (g x).toReal) μ

Tactic:
refine ⟨gcont.measurable.ennreal_toReal.aemeasurable.aestronglyMeasurable, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ∞
g : α → ℝ≥0∞
f_lt_g : ∀ (x : α), ↑(f x) < g x
gcont : LowerSemicontinuous g
gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ↑δ
gint_ne : ∫⁻ (x : α), g x ∂μ ≠ ∞
g_lt_top : ∀ᵐ (x : α) ∂μ, g x < ∞
Ig : ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ HasFiniteIntegral (fun x ↦ (g x).toReal) μ
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)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
⊢ HasDerivAt F (F' y) y

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

Goal state after:
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
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
⊢ ↑c * μ F + ↑c * (ε / ↑c) = ↑c * μ F + ε

Tactic:
ENNReal.mul_div_cancel _ ENNReal.coe_ne_top

Goal state after:
α : 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
⊢ ↑c * μ F + ε = ↑c * μ F + ε

α : 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
⊢ ↑c ≠ 0