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

Goal state before:
pp: case refine_3
𝕜 : 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 : ℕ∞ω
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) → ((i : ι) → E [×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E [×m]→L[𝕜] (i : ι) → F' i :=
  fun m ↦ ContinuousMultilinearMap.piₗᵢ 𝕜 fun _i ↦ E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ContinuousMultilinearMap.pi fun i ↦ p' i x m)
    (ContinuousMultilinearMap.pi fun i ↦ p' i x m.succ).curryLeft s x

Tactic:
exact (L m).hasFDerivAt.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.2 fun i => (h i).fderivWithin m hm x hx

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
⊢ ContDiffWithinAt 𝕜 (↑(k + 1)) (fun x ↦ x ^ i) s x

Tactic:
fun_prop

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
i : ℕ
f : E → F
⊢ iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x

Tactic:
simp_rw [← iteratedFDerivWithin_univ]
  exact iteratedFDerivWithin_neg_apply uniqueDiffOn_univ (Set.mem_univ _)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
⊢ ContDiffWithinAt 𝕜 (↑(k + 1)) (fun x ↦ x) s x

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
f : 𝕜 → 𝕜
h : ContDiff 𝕜 (↑n) f
c : 𝕜
⊢ (iteratedDeriv n fun x ↦ f (c * x)) = fun x ↦ c ^ n * iteratedDeriv n f (c * x)

Tactic:
simpa only [smul_eq_mul] using iteratedDeriv_comp_const_smul h c

Goal state after:
Module: Mathlib.Topology.Order.Rolle

Goal state before:
pp: case neg.refine_1
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ a = C → f C = f a

pp: case neg.refine_2
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ C = b → f C = f a

Tactic:
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]

Goal state after:
Module: Mathlib.Topology.Order.Rolle

Goal state before:
pp: case neg.refine_1
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
⊢ a = c → f c = f a

pp: case neg.refine_2
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
⊢ c = b → f c = f a

Tactic:
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]

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

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
f' : ℝ → ℝ := f ∘ Neg.neg
b : ℝ
hb₁ : b < a
hb₂ : ∀ ⦃x : ℝ⦄, x ∈ Ioo b a → deriv f x ∈ Iic (-1)
x : ℝ
hx : x ∈ Ioo (-a) (-b)
⊢ DifferentiableAt ℝ Neg.neg x

Tactic:
fun_prop

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

Goal state before:
pp: case refine_2
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[<] a) atBot
f' : ℝ → ℝ := f ∘ Neg.neg
hderiv : deriv f' =ᶠ[𝓝[>] (-a)] -deriv f ∘ Neg.neg
hmain : ¬DifferentiableWithinAt ℝ f' (Ioi (-a)) (-a)
h : DifferentiableWithinAt ℝ f (Iio a) a
⊢ DifferentiableWithinAt ℝ Neg.neg (Ioi (-a)) (-a)

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
⊢ (∀ ⦃a : M⦄, a ∈ s → a ∉ C) → ∀ ⦃a : M⦄, (∃ r, 0 < r ∧ a ∈ r • s) → a ∉ C

Tactic:
rintro hsC _ ⟨r, hr, y, hy, rfl⟩

Goal state after:
𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
C : ConvexCone 𝕜 M
s : Set M
hs : Convex 𝕜 s
hsC : ∀ ⦃a : M⦄, a ∈ s → a ∉ C
r : 𝕜
hr : 0 < r
y : M
hy : y ∈ s
⊢ (fun x ↦ r • x) y ∉ C
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
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 ∂μ).toReal < (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ).toReal + ↑ε

Tactic:
calc
        ENNReal.toReal (∫⁻ a : α, ENNReal.ofReal (g a).toReal ∂μ) =
            ENNReal.toReal (∫⁻ a : α, g a ∂μ) := by congr 1
        _ ≤ ENNReal.toReal ((∫⁻ a : α, f a ∂μ) + δ) := by
          apply ENNReal.toReal_mono _ gint
          simpa using int_f_ne_top
        _ = ENNReal.toReal (∫⁻ a : α, f a ∂μ) + δ := by
          rw [ENNReal.toReal_add int_f_ne_top ENNReal.coe_ne_top, ENNReal.coe_toReal]
        _ < ENNReal.toReal (∫⁻ a : α, f a ∂μ) + ε := by gcongr
        _ = (∫⁻ a : α, ENNReal.ofReal ↑(f a) ∂μ).toReal + ε := by simp

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
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun x ↦ b • x) x}
hx : (fun x ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x ↦ b • x) x} ⊆ c • s
⊢ a ≤ b

Tactic:
refine not_lt.1 fun hba => hx ?_

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₀ : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : ℝ⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
r : ℝ
hr : r > 0
b : ℝ
hb : 0 < b
x : E
hx' : x ∈ s
hs₂ : Absorbs ℝ s {(fun x ↦ b • x) x}
hx : (fun x ↦ b • x) x ∉ a • s
h : ∀ (c : ℝ), r ≤ ‖c‖ → {(fun x ↦ b • x) x} ⊆ c • s
hba : b < a
⊢ (fun x ↦ b • x) x ∈ a • s
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
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this✝ : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
hk : (1 / 2) ^ (k + 1) < ‖y‖
h'k : ‖y‖ ≤ (1 / 2) ^ k
this : (1 / 2) ^ (k + 1) < (1 / 2) ^ (n e + 1)
⊢ n e < k

Tactic:
pow_lt_pow_iff_right_of_lt_one₀ (by norm_num : (0 : ℝ) < 1 / 2) (by norm_num)

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
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this✝ : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
hk : (1 / 2) ^ (k + 1) < ‖y‖
h'k : ‖y‖ ≤ (1 / 2) ^ k
this : n e + 1 < k + 1
⊢ n e < k
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

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
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
hk : (1 / 2) ^ (k + 1) < ‖y‖
h'k : ‖y‖ ≤ (1 / 2) ^ k
k_gt : n e < k
m : ℕ := k - 1
⊢ ‖f (x + y) - f x - f' y‖ ≤ ε * ‖y‖

Tactic:
have m_ge : n e ≤ m := Nat.le_sub_one_of_lt k_gt

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
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : ℕ → ℕ
L : ℕ → ℕ → ℕ → E →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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun e ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : y ∈ ball 0 ((1 / 2) ^ (n e + 1))
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
hk : (1 / 2) ^ (k + 1) < ‖y‖
h'k : ‖y‖ ≤ (1 / 2) ^ k
k_gt : n e < k
m : ℕ := k - 1
m_ge : n e ≤ m
⊢ ‖f (x + y) - f x - f' y‖ ≤ ε * ‖y‖
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
f : Dual 𝕜 F
x✝ : F
⊢ (extendRCLike ((fun f ↦ reLm ∘ₗ ↑ℝ f) f)) x✝ = f x✝

Tactic:
apply RCLike.ext <;> simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
F : Type u_2
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : Module ℝ F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
⊢ Continuous fun x ↦ ↑(fr x) - I * ↑(fr (I • x))

Tactic:
fun_prop

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
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ Continuous[_, inst✝¹] fun x_1 ↦ x_1 • x

Tactic:
fun_prop

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x ≠ 0
⊢ (v x)⁻¹ * v y ≠ 0

Tactic:
simp [vx, vy]

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

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalRing R
inst✝¹ : Module R V
inst✝ : SeparatingDual R V
x y : V
hx : x ≠ 0
hy : y ≠ 0
u : StrongDual R V
ux : u x = 1
uy : u y = 0
v : StrongDual R V
vy : v y = 1
vx : v x = 0
⊢ (u + v) x = 1

Tactic:
simp [ux, vx]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.CompleteCodomain

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeparatingDual 𝕜 E
inst✝¹ : Nontrivial E
inst✝ : CompleteSpace (E →L[𝕜] F)
f : ℕ → F
hf : CauchySeq f
v : E
hv : v ≠ 0
φ : StrongDual 𝕜 E
hφ : φ v = 1
g : ℕ → E →L[𝕜] F := fun n ↦ ((ContinuousLinearMap.smulRightL 𝕜 E F) φ) (f n)
this : CauchySeq g
a : E →L[𝕜] F
ha : Tendsto g atTop (𝓝 a)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun i ↦ i v

Tactic:
fun_prop

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

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

Tactic:
simp_rw [integral_neg, lt_neg_add_iff_add_lt] at gint

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁵ : Zero X
inst✝⁴ : Zero Y
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace R
f : C(X, Y)₀
⊢ Continuous fun g ↦ (↑g).comp ↑f

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
K : Set F
⊢ {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} ⊆ D f K

Tactic:
by
  intro x hx
  rw [D, mem_iInter]
  intro e
  have : (0 : ℝ) < (1 / 2) ^ e := pow_pos (by norm_num) _
  rcases mem_A_of_differentiable this hx.1 with ⟨R, R_pos, hR⟩
  obtain ⟨n, hn⟩ : ∃ n : ℕ, (1 / 2) ^ n < R :=
    exists_pow_lt_of_lt_one R_pos (by norm_num : (1 : ℝ) / 2 < 1)
  simp only [mem_iUnion, mem_iInter, B, mem_inter_iff]
  refine ⟨n, fun p hp q hq => ⟨derivWithin f (Ici x) x, hx.2, ⟨?_, ?_⟩⟩⟩ <;>
    · refine hR _ ⟨pow_pos (by norm_num) _, lt_of_le_of_lt ?_ hn⟩
      exact pow_le_pow_of_le_one (by norm_num) (by norm_num) (by assumption)

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ENNReal.ofReal (∫ (a : α), ↑‖F i a‖₊ ∂μ) = ENNReal.ofReal ↑‖∫ (a : α), ‖F i a‖ ∂μ‖₊

Tactic:
coe_nnnorm,

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i ↦ ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ENNReal.ofReal (∫ (a : α), ↑‖F i a‖₊ ∂μ) = ENNReal.ofReal ‖∫ (a : α), ‖F i a‖ ∂μ‖
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 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 := fun e ↦ L e (n e) (n e)
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 : ℕ
hk : (1 / 2) ^ (k + 1) < y - x
h'k : y - x ≤ (1 / 2) ^ k
this : (1 / 2) ^ (k + 1) < (1 / 2) ^ (n e + 1)
⊢ n e < k

Tactic:
pow_lt_pow_iff_right_of_lt_one₀ (by norm_num : (0 : ℝ) < 1 / 2) (by norm_num)

Goal state after:
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 := fun e ↦ L e (n e) (n e)
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 : ℕ
hk : (1 / 2) ^ (k + 1) < y - x
h'k : y - x ≤ (1 / 2) ^ k
this : n e + 1 < k + 1
⊢ n e < k
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: case inr
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 := fun e ↦ L e (n e) (n e)
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 : ℕ
hk : (1 / 2) ^ (k + 1) < y - x
h'k : y - x ≤ (1 / 2) ^ k
k_gt : n e < k
m : ℕ := k - 1
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖

Tactic:
have m_ge : n e ≤ m := Nat.le_sub_one_of_lt k_gt

Goal state after:
case inr
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 := fun e ↦ L e (n e) (n e)
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 : ℕ
hk : (1 / 2) ^ (k + 1) < y - x
h'k : y - x ≤ (1 / 2) ^ k
k_gt : n e < k
m : ℕ := k - 1
m_ge : n e ≤ m
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
inst✝ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
g : ℝ → ε
h : f =ᵐ[μ.restrict (Ι a b)] g
⊢ IntegrableOn g (Ι a b) μ ↔ IntervalIntegrable g μ a b

Tactic:
intervalIntegrable_iff

Goal state after:
ε : Type u_3
inst✝² : TopologicalSpace ε
inst✝¹ : ENormedAddMonoid ε
inst✝ : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
g : ℝ → ε
h : f =ᵐ[μ.restrict (Ι a b)] g
⊢ IntegrableOn g (Ι a b) μ ↔ IntegrableOn g (Ι a b) μ
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Goal state before:
pp: A : Type u_7
inst✝ : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntervalIntegrable f μ a b
hg : ContinuousOn g [[a, b]]
⊢ IntervalIntegrable (fun x ↦ f x * g x) μ a b

Tactic:
intervalIntegrable_iff

Goal state after:
A : Type u_7
inst✝ : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn (fun x ↦ f x * g x) (Ι a b) μ