mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x ↦ ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := v.equivFunL
H : Summable fun x ↦ ‖e (f x)‖
i : α
⊢ ‖‖f i‖‖ ≤ ↑‖↑e.symm‖₊ * ‖e (f i)‖

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x ↦ ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := v.equivFunL
H : Summable fun x ↦ ‖e (f x)‖
i : α
⊢ ‖f i‖ ≤ ‖↑e.symm‖ * ‖e (f i)‖
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
E✝ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CompactSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : SeminormedAddCommGroup E✝
inst✝² : Nonempty α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : Nontrivial E
⊢ NontrivialTopology C(α, E)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
E✝ : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CompactSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : SeminormedAddCommGroup E✝
inst✝² : Nonempty α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : Nontrivial E
⊢ ∃ x, ¬x = 0
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : u =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ (fun n ↦ ‖u n‖ * ‖r‖ ^ n) =O[atTop] fun n ↦ ‖↑n ^ k‖ * ‖r‖ ^ n

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
k : ℕ
r : F
hr : ‖r‖ < 1
u : ℕ → F
hu : u =O[atTop] fun n ↦ ↑(n ^ k)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ (fun n ↦ ‖u n‖ * ‖r‖ ^ n) =O[atTop] fun n ↦ ‖↑n‖ ^ k * ‖r‖ ^ n
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
R : Type u_4
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : C(α, R)
h : f * g = 0
⊢ ‖f - g‖ = max ‖f‖ ‖g‖

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
R : Type u_4
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : C(α, R)
h : f * g = 0
⊢ ‖f + -g‖ = max ‖f‖ ‖g‖
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
R : Type u_4
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
h : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
this : f j * ∑ i ∈ s, f i = 0
⊢ ‖∑ i ∈ insert j s, f i‖₊ = (insert j s).sup fun x ↦ ‖f x‖₊

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
R : Type u_4
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
h : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
this : f j * ∑ i ∈ s, f i = 0
⊢ ‖f j + ∑ i ∈ s, f i‖₊ = max ‖f j‖₊ ‖∑ i ∈ s, f i‖₊
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : ℕ → E
g : ℕ → F
h : f =Θ[atTop] g
⊢ f =Θ[cofinite] g

Tactic:
simpa using

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : ℕ → E
g : ℕ → F
h : f =Θ[atTop] g
⊢ f =Θ[cofinite] g
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: case insert
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
R : Type u_4
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
h : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
⊢ f j * ∑ i ∈ s, f i = 0

Tactic:
simpa using

Goal state after:
case insert
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
R : Type u_4
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
h : Pairwise ((fun x1 x2 ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : ‖∑ i ∈ s, f i‖₊ = s.sup fun x ↦ ‖f x‖₊
⊢ ∑ i ∈ s, f j * f i = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
by
  have hf : StronglyMeasurable[m] f := @SimpleFunc.stronglyMeasurable β F m _ f
  have hf_int_m := hf_int.trim hm hf
  rw [integral_simpleFunc_larger_space (le_refl m) f hf_int_m,
    integral_simpleFunc_larger_space hm f hf_int]
  congr with x
  simp only [measureReal_def]
  congr 2
  exact (trim_measurableSet_eq hm (@SimpleFunc.measurableSet_fiber β F m f x)).symm

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
key : 1 - infEDist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEDist x E / ENNReal.ofReal δ ≤ ⊥

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
key : 1 - infEDist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEDist x E / ENNReal.ofReal δ = 0
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
⊢ x ∉ thickening ε E

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → |δseq b| < ε
n : ℕ
n_large : n ≥ N
⊢ ENNReal.ofReal ε ≤ infEDist x E
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (ENNReal.toNNReal ∘ thickenedIndicatorAux δ E) x ≤ 1

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (thickenedIndicatorAux δ E x).toNNReal ≤ 1
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ' T C
f : α → E
hf : Integrable f (μ + μ')
⊢ setToFun (μ + μ') T hT_add f = setToFun μ' T hT f

Tactic:
refine setToFun_congr_measure_of_integrable 1 one_ne_top ?_ hT_add hT f hf
  rw [one_smul]
  exact Measure.le_add_left le_rfl

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T' C'
hT'' : DominatedFinMeasAdditive μ'' T'' C''
h : ∀ (s : Set α), MeasurableSet s → (μ + μ') s < ∞ → T'' s = T s + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
⊢ μ'' ≤ 1 • (μ + μ')

Tactic:
simpa using

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ μ' μ'' : Measure α
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T' C'
hT'' : DominatedFinMeasAdditive μ'' T'' C''
h : ∀ (s : Set α), MeasurableSet s → (μ + μ') s < ∞ → T'' s = T s + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
I : DominatedFinMeasAdditive (μ + μ') T C
A : setToFun (μ + μ') T I f = setToFun μ T hT f
I' : DominatedFinMeasAdditive (μ + μ') T' C'
A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f
I'' : DominatedFinMeasAdditive (μ + μ') T'' C''
⊢ μ'' ≤ μ + μ'
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∈ s
x : (i : δ) → X i
⊢ (∫⋯∫⁻_s, f ∂μ) x = ∫⁻ (xᵢ : X i), (∫⋯∫⁻_s.erase i, f ∂μ) (update x i xᵢ) ∂μ i

Tactic:
simpa using

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∈ s
x : (i : δ) → X i
⊢ (∫⋯∫⁻_s, f ∂μ) x = ∫⁻ (xᵢ : X i), (∫⋯∫⁻_s.erase i, f ∂μ) (update x i xᵢ) ∂μ i
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∈ s
⊢ ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s.erase i, fun x ↦ ∫⁻ (xᵢ : X i), f (update x i xᵢ) ∂μ i ∂μ

Tactic:
simpa using

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∈ s
⊢ ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s.erase i, fun x ↦ ∫⁻ (xᵢ : X i), f (update x i xᵢ) ∂μ i ∂μ
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this✝ : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
this : ∀ᶠ (x : α) in 𝓝[<] a, f x ∈ id s
⊢ ∃ u < a, Ioo u a ⊆ {x | f x ∈ s}

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this✝ : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
this : ∀ᶠ (x : α) in 𝓝[<] a, f x ∈ id s
⊢ ∃ u < a, Ioo u a ⊆ {x | f x ∈ s}
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : 𝓝[<] c = ⊥
⊢ leftLim f c ∈ id s

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : 𝓝[<] c = ⊥
⊢ f c ∈ s
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ¬∃ y, Tendsto f (𝓝[<] c) (𝓝 y)
⊢ leftLim f c ∈ id s

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ¬∃ y, Tendsto f (𝓝[<] c) (𝓝 y)
⊢ f c ∈ s
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
this : ∀ᶠ (x : α) in 𝓝[<] a, f x ∈ id s
⊢ ∃ u < a, Ioo u a ⊆ {x | f x ∈ s}

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
this : ∀ᶠ (x : α) in 𝓝[<] a, f x ∈ id s
⊢ ∃ u < a, Ioo u a ⊆ {x | f x ∈ s}
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : 𝓝[>] c = ⊥
⊢ rightLim f c ∈ id s

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : 𝓝[>] c = ⊥
⊢ f c ∈ s
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
⊢ rightLim f c ∈ id s

Tactic:
by_cases! h''c : ¬ ∃ y, Tendsto f (𝓝[>] c) (𝓝 y)

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
h''c : ¬∃ y, Tendsto f (𝓝[>] c) (𝓝 y)
⊢ rightLim f c ∈ id s

case neg
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
h''c : ∃ y, Tendsto f (𝓝[>] c) (𝓝 y)
⊢ rightLim f c ∈ id s
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
h''c : ¬∃ y, Tendsto f (𝓝[>] c) (𝓝 y)
⊢ rightLim f c ∈ id s

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[>] c).NeBot
h''c : ¬∃ y, Tendsto f (𝓝[>] c) (𝓝 y)
⊢ f c ∈ s
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst✝⁴] s
⊢ ∃ a, ∀ (b : α), a ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst✝⁴] s
⊢ ∃ a, ∀ (b : α), a ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x = ⊥
⊢ leftLim f x ≤ f y

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] x = ⊥
⊢ f x ≤ f y
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y = ⊥
⊢ rightLim f x ≤ leftLim f y

Tactic:
simpa using

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y = ⊥
⊢ rightLim f x ≤ f y
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
f✝ : StieltjesFunction R
inst✝ : OrderTopology R
f : R → ℝ
hf : Monotone f
⊢ ∀ (x : R), ContinuousWithinAt (rightLim f) (Ici x) x

Tactic:
intro x s hs

Goal state after:
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
f✝ : StieltjesFunction R
inst✝ : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
⊢ s ∈ map (rightLim f) (𝓝[≥] x)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure X
mY : MeasurableSpace Y
ν : Measure Y
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), ∫ (y : Y), s.indicator (fun x ↦ f x y) x ∂ν ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂ν ∂μ

Tactic:
by
  simp_rw [← integral_indicator hs, integral_indicator₂]

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, μ (s i) ≠ ∞
i : ι
hi : i ∈ t
⊢ IntegrableOn (fun x ↦ 1) (s i) μ

Tactic:
simpa using

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, μ (s i) ≠ ∞
i : ι
hi : i ∈ t
⊢ μ (s i) < ∞
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
⊢ Icc ?m.78 ?m.79 ⊆ ⋃ i ∈ univ, Iotop (c i) (d i)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
⊢ Icc ?m.78 ?m.79 ⊆ ⋃ i, Iotop (c i) (d i)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i)
ab : a ≤ b
⊢ ∃ i ∈ s, b ∈ Iotop (c i) (d i)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i)
ab : a ≤ b
⊢ ∃ i ∈ s, b ∈ Iotop (c i) (d i)