mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.ExtendFrom

Goal state before:
pp: case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ a ∈ closure[inst✝⁵] (Ioo a b)

Tactic:
rw [closure_Ioo hab.ne]

Goal state after:
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
la : β
inst✝ : T2Space β
hab : a < b
ha : Tendsto f (𝓝[>] a) (𝓝 la)
⊢ a ∈ Icc a b
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 : ℕ∞ω
A : Type u_4
inst✝⁴ : NormedRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : Module A F
inst✝¹ : IsScalarTower 𝕜 A F
inst✝ : IsBoundedSMul A F
f : E → A
x : E
hf : ContDiffAt 𝕜 n f x
v : F
⊢ ContDiffAt 𝕜 n (fun y ↦ f y • v) x

Tactic:
rw [← contDiffWithinAt_univ] at *; exact hf.smul_const v

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

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑0) f
x✝¹ : E
x✝ : Fin 0 → E
⊢ (iteratedFDeriv 𝕜 0 (fun z ↦ f (a • z)) x✝¹) x✝ = (a ^ 0 • iteratedFDeriv 𝕜 0 f (a • x✝¹)) x✝

Tactic:
simp

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

Goal state before:
pp: case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
lb : β
inst✝ : T2Space β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ b ∈ closure[inst✝⁵] (Ioo a b)

Tactic:
rw [closure_Ioo hab.ne]

Goal state after:
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
f : α → β
a b : α
lb : β
inst✝ : T2Space β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ b ∈ Icc a b
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case empty
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ ∅, ContDiffWithinAt 𝕜 (↑n) (f i) s x
⊢ iteratedDerivWithin n (∑ i ∈ ∅, f i) s x = ∑ i ∈ ∅, iteratedDerivWithin n (f i) s x

Tactic:
simp

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

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i✝ : ℕ
a : 𝕜
i : ℕ
hi : ContDiff 𝕜 (↑i) f → (iteratedFDeriv 𝕜 i fun z ↦ f (a • z)) = fun x ↦ a ^ i • iteratedFDeriv 𝕜 i f (a • x)
hf : ContDiff 𝕜 (↑(i + 1)) f
v : E
x✝ : Fin (i + 1) → E
⊢ ((a ^ (i + 1) • fderiv 𝕜 (iteratedFDeriv 𝕜 i f) (a • v)) (x✝ 0)) (tail x✝) =
    a ^ (i + 1) • ((fderiv 𝕜 (iteratedFDeriv 𝕜 i f) (a • v)) (x✝ 0)) (tail x✝)

Tactic:
simp

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

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff :
  ∀ (i : ℝ × ℝ),
    i.1 < derivWithin f (Ioi a) a ∧ derivWithin f (Ioi a) a < i.2 → ∀ᶠ (x : ℝ) in 𝓝[>] a, slope f a x ∈ Ioo i.1 i.2
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
⊢ (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).1 < derivWithin f (Ioi a) a ∧
    derivWithin f (Ioi a) a < (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).2

Tactic:
simp

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

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x✝ : ℝ
hx✝ : x✝ ∈ D
y : ℝ
hy : y ∈ D
hxy : x✝ < y
x : ℝ
hx : x ∈ interior D
⊢ -C < deriv (fun y ↦ -f y) x

Tactic:
by
    rw [deriv.fun_neg, neg_lt_neg_iff]
    exact lt_hf' x hx

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t ↦ (AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t
⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : SMul R M
x : M
ι : Sort u_7
f : ι → ConvexCone R M
⊢ (∀ i ∈ Set.range f, x ∈ ↑i) ↔ ∀ (i : ι), x ∈ f i

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
x : M
x✝¹ : R
x✝ : 0 < x✝¹
⊢ ∀ ⦃x : M⦄, x ∈ 0 → x✝¹ • x ∈ 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
x x✝ : M
⊢ x✝ ∈ 0 → ∀ ⦃y : M⦄, y ∈ 0 → x✝ + y ∈ 0

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
c : 𝕜
hc : 1 < ‖c‖
r ε : ℝ
hε : 0 < ε
hr : 0 < r
x : E
L₁ L₂ : E →L[𝕜] F
h₁ : x ∈ A f L₁ r ε
h₂ : x ∈ A f L₂ r ε
y : E
ley : r ≤ 2 * ‖c‖ * ‖y‖
ylt : ‖y‖ < r / 2
⊢ ‖(L₁ - L₂) y‖ = ‖f (x + y) - f x - L₂ (x + y - x) - (f (x + y) - f x - L₁ (x + y - x))‖

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
x : M
x✝¹ : ConvexCone R M
x✝ : M
⊢ x✝ ∈ 0 + x✝¹ ↔ x✝ ∈ x✝¹

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C₁ C₂ : ConvexCone R M
x : M
x✝¹ : ConvexCone R M
x✝ : M
⊢ x✝ ∈ x✝¹ + 0 ↔ x✝ ∈ x✝¹

Tactic:
simp

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ⊤.IsGenerating

Tactic:
simp

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

Goal state before:
pp: n : ℕ∞ω
x✝ : ℝ
hx✝ : x✝ ≠ 0
A : ∀ (y : ℝ), 0 < y → ContDiffAt ℝ n log y
hx : x✝ < 0
this : ContDiffAt ℝ n (log ∘ fun y ↦ -y) x✝
x : ℝ
⊢ log x = (log ∘ fun y ↦ -y) x

Tactic:
simp

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

Goal state before:
pp: case refine_2
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)
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ 0 ∈ Set.Icc (-|x|) |x|

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
s : Set E
c : E →₀ R
hc : ↑c.support ⊆ s
hc₀ : ∀ (y : E), 0 ≤ c y
⊢ ∀ (a : E), a ∈ c.support ↔ ⟨c a, ⋯⟩ ≠ 0

Tactic:
simp

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
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 : α), ↑(f a) ∂μ).toReal + ↑ε = (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ).toReal + ↑ε

Tactic:
simp

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
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 ∂μ
⊢ ∀ (x : α), 0 x ≤ (fun x ↦ ↑(f x)) x

Tactic:
simp

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

Goal state before:
pp: x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)
F' : ℝ → ℝ := fun y ↦ (y ^ 2) ^ n / (1 - y ^ 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - x ^ 2)
⊢ 0 ∈ Set.Icc (-|x|) |x|

Tactic:
simp

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
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 ∂μ
⊢ ∀ (x : α), 0 x ≤ (fun x ↦ (g x).toReal) x

Tactic:
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₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
⊢ x ∈ {x | gauge s x ≤ a} ↔ x ∈ ⋂ r, ⋂ (_ : a < r), r • s

Tactic:
simp_rw [Set.mem_iInter, Set.mem_ofPred_eq]

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
a : ℝ
hs₁ : Convex ℝ s
hs₀ : 0 ∈ s
hs₂ : Absorbent ℝ s
ha : 0 ≤ a
x : E
⊢ gauge s x ≤ a ↔ ∀ (i : ℝ), a < i → x ∈ i • s
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0
int_f : ∫⁻ (x : α), ↑(f x) ∂μ ≠ ∞
ε : ℝ≥0∞
ε0 : ε ≠ 0
this :
  ∫⁻ (x : α), ↑(f x) ∂μ <
    (⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ ↑(f x)), (SimpleFunc.map ENNReal.ofNNReal φ).lintegral μ) + ε / 2
x : α
⊢ ↑(0 x) ≤ ↑(f x)

Tactic:
simp

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

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

Tactic:
simp

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
fc : F → 𝕜 := fun x ↦ ↑(fr x) - I * ↑(fr (I • x))
add : ∀ (x y : F), fc (x + y) = fc x + fc y
c : ℝ
x : F
⊢ ↑(fr (↑c • x)) = ↑c * ↑(fr x)

Tactic:
simp

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

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

Tactic:
simp

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
g : Dual ℝ F
x : F
⊢ im (g.extendRCLike x) = -g (I • x)

Tactic:
by
  obtain (h | h) := RCLike.I_eq_zero_or_im_I_eq_one (K := 𝕜)
  all_goals simp [h, extendRCLike_apply]

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

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

Tactic:
simp

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
f : Dual ℝ F
x✝ : F
⊢ ((fun f ↦ reLm ∘ₗ ↑ℝ f) f.extendRCLike) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: case hre
𝕜 : 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
⊢ re ((extendRCLike ((fun f ↦ reLm ∘ₗ ↑ℝ f) f)) x✝) = re (f x✝)

Tactic:
simp

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

Goal state before:
pp: case him
𝕜 : 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
⊢ im ((extendRCLike ((fun f ↦ reLm ∘ₗ ↑ℝ f) f)) x✝) = im (f x✝)

Tactic:
simp

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

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

Tactic:
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
g : StrongDual ℝ F
x : F
⊢ im (g.extendRCLike x) = -g (I • x)

Tactic:
by
  obtain (h | h) := RCLike.I_eq_zero_or_im_I_eq_one (K := 𝕜)
  all_goals simp [h, extendRCLike_apply]

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
f : StrongDual ℝ F
x✝ : F
⊢ ((fun f ↦ reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f) f.extendRCLike) x✝ = f x✝

Tactic:
simp

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
ht : Convex ℝ t
hs₁ : Convex ℝ ∅
hs₂ : IsOpen ∅
disj : Disjoint ∅ t
⊢ ∀ a ∈ ∅, 0 a < 0

Tactic:
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
x : E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : ε • s ∩ -(ε • s) ∈ 𝓝 0
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s x = gauge s (x + y + -y)

Tactic:
simp

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht : Convex ℝ ∅
disj : Disjoint s ∅
⊢ ∀ b ∈ ∅, 1 ≤ 0 b

Tactic:
simp

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
inst✝ : SigmaFinite μ
f : α → ℝ
hf : Integrable f μ
ε : ℝ
εpos : 0 < ε
δ : ℝ≥0 := NNReal.mk (ε / 2) ⋯
δpos : 0 < δ
fp : α → ℝ≥0 := fun x ↦ (f x).toNNReal
int_fp : Integrable (fun x ↦ ↑(fp x)) μ
gp : α → ℝ≥0∞
fp_lt_gp : ∀ (x : α), ↑(fp x) < gp x
gpcont : LowerSemicontinuous gp
gp_lt_top : ∀ᵐ (x : α) ∂μ, gp x < ∞
gp_integrable : Integrable (fun x ↦ (gp x).toReal) μ
gpint : ∫ (x : α), (gp x).toReal ∂μ < ∫ (x : α), ↑(fp x) ∂μ + ↑δ
fm : α → ℝ≥0 := fun x ↦ (-f x).toNNReal
int_fm : Integrable (fun x ↦ ↑(fm x)) μ
gm : α → ℝ≥0
gm_le_fm : ∀ (x : α), gm x ≤ fm x
gmcont : UpperSemicontinuous gm
gm_integrable : Integrable (fun x ↦ ↑(gm x)) μ
gmint : ∫ (x : α), ↑(fm x) ∂μ - ↑δ ≤ ∫ (x : α), ↑(gm x) ∂μ
g : α → EReal := fun x ↦ ↑(gp x) - ↑↑(gm x)
ae_g : ∀ᵐ (x : α) ∂μ, (g x).toReal = (↑(gp x)).toReal - (↑↑(gm x)).toReal
x✝ : α
⊢ (↑(gp x✝)).toReal - (↑↑(gm x✝)).toReal = ((fun x ↦ (gp x).toReal) - fun x ↦ ↑(gm x)) x✝

Tactic:
simp

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
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 : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : ‖y‖ ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < ‖y‖
m_ge : n e ≤ m
km : k = m + 1
J1 : ‖f (x + y) - f x - (L e (n e) m) (x + y - x)‖ ≤ (1 / 2) ^ e * (1 / 2) ^ m
J2 : ‖f (x + y) - f x - (L e (n e) m) y‖ ≤ 4 * (1 / 2) ^ e * ‖y‖
⊢ f (x + y) - f x - f' y = f (x + y) - f x - (L e (n e) m) y + (L e (n e) m - f') y

Tactic:
simp

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
ht₁ : Convex ℝ t
ht₃ : IsOpen t
hs₁ : Convex ℝ ∅
hs₂ : IsOpen ∅
disj : Disjoint ∅ t
⊢ ∀ a ∈ ∅, 0 a < -1

Tactic:
simp

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
ht₁ : Convex ℝ t
ht₃ : IsOpen t
hs₁ : Convex ℝ ∅
hs₂ : IsOpen ∅
disj : Disjoint ∅ t
b : E
_hb : b ∈ t
⊢ -1 < 0 b

Tactic:
simp

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

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hr : 0 ≤ 0
⊢ gauge (ball 0 0) x = ‖x‖ / 0

Tactic:
simp

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht₁ : Convex ℝ ∅
ht₃ : IsOpen ∅
disj : Disjoint s ∅
a : E
_ha : a ∈ s
⊢ 0 a < 1

Tactic:
simp

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht₁ : Convex ℝ ∅
ht₃ : IsOpen ∅
disj : Disjoint s ∅
⊢ ∀ b ∈ ∅, 1 < 0 b

Tactic:
simp

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

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ≥0
hc : Convex ℝ s
hr : 0 < r
hs : ball 0 ↑r ⊆ s
this : Absorbent ℝ (ball 0 ↑r)
x y : E
⊢ gauge s x = gauge s (y + (x - y))

Tactic:
simp

Goal state after:
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✝ : T1Space R
x y : V
hxy : x ≠ y
f : StrongDual R V
hf : f x ≠ f y
⊢ y ∉ ⇑f ⁻¹' {f y}ᶜ

Tactic:
simp

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

Goal state before:
pp: E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s t : Set E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hs : Convex ℝ s
ht : Convex ℝ t
hst : Disjoint (interior s) t
hsint : (interior s).Nonempty
htne : ¬t.Nonempty
⊢ (∀ a ∈ s, 0 a ≤ 0) ∧ ∀ b ∈ t, 0 ≤ 0 b

Tactic:
simp

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

Goal state before:
pp: E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
t : Set E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
hs₁ : Convex ℝ ∅
hs₂ : IsCompact ∅
disj : Disjoint ∅ t
⊢ (∀ a ∈ ∅, 0 a < -2) ∧ -2 < -1 ∧ ∀ b ∈ t, -1 < 0 b

Tactic:
simp

Goal state after: