mathlib-initiative/mathlib-tactics huggingface dataset:
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
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 [hi, ↓reduceDIte, pred_lt_pred_iff, Nat.succ_eq_add_one]
      exact (c.emb_strictMono _).comp (cast_strictMono _) hab

Goal state after:
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
n : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔
    (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ f', ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x

Tactic:
contDiffOn_succ_iff_fderivWithin hs

Goal state after:
𝕜 : 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f s) s ↔
    (n = ω → AnalyticOn 𝕜 f s) ∧ ∃ f', ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s 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
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (∞ + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (fderivWithin 𝕜 f s) s

Tactic:
contDiffOn_succ_iff_fderivWithin hs

Goal state after:
𝕜 : 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
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (fderivWithin 𝕜 f s) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (fderivWithin 𝕜 f s) s
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}
i : Fin c.length
x✝¹ : i ∈ univ
h : i ≠ c.index 0
x✝ : c.index 0 ∈ univ
hij : i ≠ c.index 0
⊢ (Disjoint on fun m ↦
      range 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 ⋯)
    i (c.index 0)

Tactic:
simp only [onFun, hij, ↓reduceDIte]

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✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
x✝¹ : i ∈ univ
h : i ≠ c.index 0
x✝ : c.index 0 ∈ univ
hij : i ≠ c.index 0
⊢ Disjoint (range fun j ↦ (c.emb i (Fin.cast ⋯ j)).pred ⋯)
    (range fun j ↦ (c.emb (c.index 0) (Fin.cast ⋯ j.succ)).pred ⋯)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case emb.inl.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
o : Option (Fin c.length)
a : Fin c.length
⊢ c.partSize a =
    update (c.extendMiddle a).partSize ((c.extendMiddle a).index 0)
      ((c.extendMiddle a).partSize ((c.extendMiddle a).index 0) - 1) a

pp: case emb.inl.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
o : Option (Fin c.length)
a : Fin c.length
⊢ ∀ (i : Fin (c.partSize a)),
    c.emb a i =
      if h : a = a then ((c.extendMiddle a).emb a (Fin.cast ⋯ ⟨↑i, ⋯⟩.succ)).pred ⋯
      else ((c.extendMiddle a).emb a (Fin.cast ⋯ ⟨↑i, ⋯⟩)).pred ⋯

Tactic:
· rw [index_extendMiddle_zero]
            simp [extendMiddle]

Goal state after:
case emb.inl.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
o : Option (Fin c.length)
a : Fin c.length
⊢ ∀ (i : Fin (c.partSize a)),
    c.emb a i =
      if h : a = a then ((c.extendMiddle a).emb a (Fin.cast ⋯ ⟨↑i, ⋯⟩.succ)).pred ⋯
      else ((c.extendMiddle a).emb a (Fin.cast ⋯ ⟨↑i, ⋯⟩)).pred ⋯
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case emb.inr.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
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
⊢ c.partSize a =
    update (c.extendMiddle i).partSize ((c.extendMiddle i).index 0)
      ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1) a

pp: case emb.inr.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
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
⊢ ∀ (i_1 : Fin (c.partSize a)),
    c.emb a i_1 =
      if h : a = i then ((c.extendMiddle i).emb a (Fin.cast ⋯ ⟨↑i_1, ⋯⟩.succ)).pred ⋯
      else ((c.extendMiddle i).emb a (Fin.cast ⋯ ⟨↑i_1, ⋯⟩)).pred ⋯

Tactic:
· rw [index_extendMiddle_zero]
            simp [extendMiddle]

Goal state after:
case emb.inr.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
o : Option (Fin c.length)
i a : Fin c.length
hij : a ≠ i
⊢ ∀ (i_1 : Fin (c.partSize a)),
    c.emb a i_1 =
      if h : a = i then ((c.extendMiddle i).emb a (Fin.cast ⋯ ⟨↑i_1, ⋯⟩.succ)).pred ⋯
      else ((c.extendMiddle i).emb a (Fin.cast ⋯ ⟨↑i_1, ⋯⟩)).pred ⋯
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝔸 : Type u_2
inst✝¹⁰ : Ring 𝔸
inst✝⁹ : TopologicalSpace 𝔸
inst✝⁸ : IsTopologicalRing 𝔸
R : Type u_3
S : Type u_4
inst✝⁷ : Monoid R
inst✝⁶ : SMul ℚ R
inst✝⁵ : MulAction R 𝔸
inst✝⁴ : Algebra ℚ 𝔸
inst✝³ : IsScalarTower ℚ R 𝔸
inst✝² : SetLike S 𝔸
inst✝¹ : SubsemiringClass S 𝔸
inst✝ : SMulMemClass S R 𝔸
s : S
h_closed : IsClosed[inst✝⁹] ↑s
x : 𝔸
h : x ∈ s
⊢ exp x ∈ s

Tactic:
have := SMulMemClass.ofIsScalarTower S ℚ R 𝔸
  rw [exp_eq_tsum ℚ]
  exact tsum_mem h_closed fun i => SMulMemClass.smul_mem _ <| pow_mem h _

Goal state after:
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 : ℕ
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
⊢ iteratedDerivWithin n (fun z ↦ c + f z) s x = iteratedDerivWithin n f s x

Tactic:
obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn.ne'

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
⊢ iteratedDerivWithin n.succ (fun z ↦ c + f z) s x = iteratedDerivWithin n.succ f 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 : ℕ
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
⊢ iteratedDerivWithin n (fun z ↦ c - f z) s x = iteratedDerivWithin n (fun z ↦ -f z) s x

Tactic:
obtain ⟨n, rfl⟩ := n.exists_eq_succ_of_ne_zero hn.ne'

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
f : 𝕜 → F
c : F
n : ℕ
hn : 0 < n.succ
⊢ iteratedDerivWithin n.succ (fun z ↦ c - f z) s x = iteratedDerivWithin n.succ (fun z ↦ -f z) s x
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 s x + iteratedFDerivWithin 𝕜 i (-g) s x =
    iteratedFDerivWithin 𝕜 i f s x - iteratedFDerivWithin 𝕜 i g s x

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
⊢ ContDiffWithinAt 𝕜 (↑i) (-g) s x

Tactic:
iteratedFDerivWithin_neg_apply hu hx,

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
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 s x + -iteratedFDerivWithin 𝕜 i g s x =
    iteratedFDerivWithin 𝕜 i f s x - iteratedFDerivWithin 𝕜 i g s x

𝕜 : 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
⊢ ContDiffWithinAt 𝕜 (↑i) (-g) s x
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✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : E → 𝔸
hf : ContDiff 𝕜 n f
m : ℕ
⊢ ContDiff 𝕜 n fun x ↦ f x ^ (m + 1)

Tactic:
simpa [pow_succ] using (hf.pow m).mul hf

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
n✝ : ℕ∞ω
inst✝ : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f) (↑f₀') (↑f.symm a)
n : ℕ
IH : ContDiffAt 𝕜 (↑↑n) (↑f) (↑f.symm a) → ContDiffAt 𝕜 (↑↑n) (↑f.symm) a
hf : ContDiffAt 𝕜 (↑↑n.succ) (↑f) (↑f.symm a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n) f' (↑f.symm a)
u : Set E
hu : u ∈ 𝓝 (↑f.symm a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f) (f' x) x
eq_f₀' : f' (↑f.symm a) = ↑f₀'
⊢ ContDiffAt 𝕜 (↑n) inverse ↑f₀'

Tactic:
exact contDiffAt_map_inverse _

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

Goal state before:
pp: f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

Tactic:
by
  let h x := (g b - g a) * f x - (f b - f a) * g x
  have hI : h a = h b := by simp only [h]; ring
  let h' x := (g b - g a) * f' x - (f b - f a) * g' x
  have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := fun x hx =>
    ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a))
  have hhc : ContinuousOn h (Icc a b) :=
    (continuousOn_const.mul hfc).sub (continuousOn_const.mul hgc)
  rcases exists_hasDerivAt_eq_zero hab hhc hI hhh' with ⟨c, cmem, hc⟩
  exact ⟨c, cmem, sub_eq_zero.1 hc⟩

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

Goal state before:
pp: X : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure X
l : Filter X
inst✝ : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s✝ : ι → Set X
li : Filter ι
hs : Tendsto s✝ li l.smallSets
m : ι → ℝ
hsμ : (fun i ↦ μ.real (s✝ i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
s : Set X
hμs : μ s < ⊤
h_integrable : IntegrableOn f s μ
⊢ AEStronglyMeasurable f (μ.restrict s) →
    (∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε) → ‖∫ (x : X) in s, f x ∂μ - μ.real s • b‖ ≤ ε * ‖μ.real s‖

Tactic:
hfm

Goal state after:
X : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure X
l : Filter X
inst✝ : l.IsMeasurablyGenerated
f : X → E
b : E
h : Tendsto f (l ⊓ ae μ) (𝓝 b)
hfm✝ : StronglyMeasurableAtFilter f l μ
hμ : μ.FiniteAtFilter l
s✝ : ι → Set X
li : Filter ι
hs : Tendsto s✝ li l.smallSets
m : ι → ℝ
hsμ : (fun i ↦ μ.real (s✝ i)) =ᶠ[li] m
ε : ℝ
ε₀ : 0 < ε
this : ∀ᶠ (s : Set X) in l.smallSets, ∀ᵐ (x : X) ∂μ, x ∈ s → f x ∈ closedBall b ε
s : Set X
hμs : μ s < ⊤
h_integrable : IntegrableOn f s μ
hfm : AEStronglyMeasurable f (μ.restrict s)
⊢ (∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x - b‖ ≤ ε) → ‖∫ (x : X) in s, f x ∂μ - μ.real s • b‖ ≤ ε * ‖μ.real s‖
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: case neg.refine_2
α : 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 : α), ↑(u.indicator (fun x ↦ c) x) ∂μ ≤ ∫⁻ (x : α), ↑((piecewise s hs (const α c) (const α 0)) x) ∂μ + ε

Tactic:
suffices (c : ℝ≥0∞) * μ u ≤ c * μ s + ε by
        simpa only [ENNReal.coe_indicator, u_open.measurableSet, lintegral_indicator,
          lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, const_zero,
          coe_piecewise, coe_const, coe_zero, Set.piecewise_eq_indicator, Function.const_apply, hs]
      calc
        (c : ℝ≥0∞) * μ u ≤ c * (μ s + ε / c) := by grw [μu]
        _ = c * μ s + ε := by
          simp_rw [mul_add]
          rw [ENNReal.mul_div_cancel _ ENNReal.coe_ne_top]
          simpa using hc

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 : α → ℝ≥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 ∂μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (g a).toReal ∂μ < ∞

Tactic:
convert! gint_ne.lt_top using 1

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

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

Tactic:
by_cases h : (0 : E) ∈ s

Goal state after:
case pos
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : 0 ∈ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : 0 ∉ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
ha : 0 ≤ a
hx : x ∈ a • s
ha' : 0 < a
⊢ gauge s x ≤ a

Tactic:
exact csInf_le bddBelow_gauge_set ⟨ha', hx⟩

Goal state after:
Module: Mathlib.Analysis.RCLike.Extend

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : Dual ℝ F
x : F
⊢ ‖fr.extendRCLike x‖ ^ 2 = re ((starRingEnd 𝕜) (fr.extendRCLike x) * fr.extendRCLike x)

Tactic:
by
    rw [RCLike.conj_mul, ← ofReal_pow, ofReal_re]

Goal state after:
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
θ : ℝ
hθ : 0 < θ
⊢ ‖↑‖r‖‖ = ‖r‖

Tactic:
RCLike.norm_ofReal,

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
θ : ℝ
hθ : 0 < θ
⊢ |‖r‖| = ‖r‖
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
this : ε⁻¹ • x ∈ s
h_gauge_lt : ε⁻¹ * gauge s x < 1
⊢ gauge s x < ε

Tactic:
inv_mul_lt_iff₀ hε,

Goal state after:
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
this : ε⁻¹ • x ∈ s
h_gauge_lt : gauge s x < ε * 1
⊢ gauge s x < ε
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T2Space R
⊢ T2Space V

Tactic:
apply (t2Space_iff _).2 (fun {x} {y} hxy ↦ ?_)

Goal state after:
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T2Space R
x y : V
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
Module: Mathlib.Analysis.LocallyConvex.SeparatingDual

Goal state before:
pp: R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
⊢ (∀ (x : V →L[R] V), x ∘SL ↑(f.trans g.symm) = ↑(f.trans g.symm) ∘SL x) ↔ ∃ α, f = α • g

Tactic:
← mul_def,

Goal state after:
R : Type u_4
V : Type u_5
W : Type u_6
inst✝¹³ : NormedField R
inst✝¹² : AddCommGroup V
inst✝¹¹ : AddCommGroup W
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : TopologicalSpace V
inst✝⁸ : TopologicalSpace W
inst✝⁷ : IsTopologicalRing R
inst✝⁶ : Module R V
inst✝⁵ : Module R W
inst✝⁴ : SeparatingDual R V
inst✝³ : IsTopologicalAddGroup V
inst✝² : IsTopologicalAddGroup W
inst✝¹ : ContinuousSMul R V
inst✝ : ContinuousSMul R W
f g : V ≃L[R] W
⊢ (∀ (x : V →L[R] V), x * ↑(f.trans g.symm) = ↑(f.trans g.symm) * x) ↔ ∃ α, f = α • g
Module: Mathlib.Topology.Algebra.IsUniformGroup.Order

Goal state before:
pp: α : Type u_1
ι : Type u_2
β : Type u_3
inst✝⁶ : UniformSpace β
inst✝⁵ : AddGroup β
inst✝⁴ : IsUniformAddGroup β
inst✝³ : PartialOrder β
inst✝² : OrderTopology β
inst✝¹ : AddLeftMono β
inst✝ : AddRightMono β
f : ι → α → β
g : α → β
K : Set α
p : Filter ι
u v : β
huv : u < v
hf : TendstoUniformlyOn f g p K
hg : ∀ x ∈ K, g x ≤ u
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ K, f i x < v

Tactic:
by
  simp only [tendstoUniformlyOn_iff_tendsto, uniformity_eq_comap_neg_add_nhds_zero,
    tendsto_iff_eventually, eventually_comap, Prod.forall] at *
  conv at hf => enter [2]; rw [eventually_iff_exists_mem]
  have hf2 := hf (fun x ↦ -x.1 + x.2 < -u + v) ⟨_, (isOpen_gt' (-u + v)).mem_nhds (by simp [huv]),
    fun y hy a b hab ↦ (hab.symm ▸ hy :)⟩
  filter_upwards [eventually_prod_principal_iff.mp hf2] with i hi x hx
  simpa using add_lt_add_of_le_of_lt (hg x hx) (hi x hx)

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

Goal state before:
pp: 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))) μ

Tactic:
exact hf.im.ofReal.smul (𝕜 := 𝕜) (β := 𝕜) RCLike.I

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

Goal state before:
pp: case refine_3
α : Type u_1
E : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : ℕ → Set α
f : α → E
hsm : ∀ (i : ℕ), MeasurableSet (s i)
h_anti : Antitone s
hfi : IntegrableOn f (s 0) μ
bound : α → ℝ := (s 0).indicator fun a ↦ ‖f a‖
h_int_eq : (fun i ↦ ∫ (a : α) in s i, f a ∂μ) = fun i ↦ ∫ (a : α), (s i).indicator f a ∂μ
n : ℕ
x : α
⊢ (s n).indicator (fun a ↦ ‖f a‖) x ≤ bound x

Tactic:
grw [h_anti zero_le]

Goal state after: