mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T'' (⇑f ⁻¹' {x})) x =
    ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range with x ≠ 0, (T' (⇑f ⁻¹' {x})) x

Tactic:
rw [← sum_add_distrib]

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
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
this : ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (⇑f ⁻¹' {x}) = T (⇑f ⁻¹' {x}) + T' (⇑f ⁻¹' {x})
⊢ ∑ x ∈ f.range with x ≠ 0, (T'' (⇑f ⁻¹' {x})) x = ∑ x ∈ f.range with x ≠ 0, ((T (⇑f ⁻¹' {x})) x + (T' (⇑f ⁻¹' {x})) x)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T (map (fun x ↦ c • x) f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x)

Tactic:
map_setToSimpleFunc T h_add hf

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 : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x)

α : 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
h_add : FinMeasAdditive μ T
c : ℝ
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ c • 0 = 0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : SMulZeroClass 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T (map (fun x ↦ c • x) f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x)

Tactic:
map_setToSimpleFunc T h_add hf

Goal state after:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : SMulZeroClass 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x)

α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : SMulZeroClass 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ c • 0 = 0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : i ∈ Set.range ⇑f
⊢ 0 ≤ i

Tactic:
obtain ⟨y, hy⟩ := Set.mem_range.mp hi

Goal state after:
α : Type u_1
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
m : MeasurableSpace α
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α) (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
i : G'
hi : i ∈ Set.range ⇑f
y : α
hy : f y = i
⊢ 0 ≤ i
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable (⇑f) μ
i : G'
hi : i ∈ Set.range ⇑f
h0 : ¬i = 0
⊢ 0 ≤ i

Tactic:
obtain ⟨y, hy⟩ := Set.mem_range.mp hi

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable (⇑f) μ
i : G'
hi : i ∈ Set.range ⇑f
h0 : ¬i = 0
y : α
hy : f y = i
⊢ 0 ≤ i
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
this : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
⊢ 0 = ∞.toReal

Tactic:
toReal_top

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
this : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : CompleteSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
⊢ Tendsto (fun n ↦ SimpleFunc.integral μ (approxOn f fmeas s 0 ⋯ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
apply tendsto_integral_approxOn_of_measurable hf fmeas _ _ (integrable_zero _ _ _)

Goal state after:
α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : CompleteSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v v' : V
p p' : P
⊢ dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'

Tactic:
by
  simpa using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f μ
⊢ (¬∀ᵐ (x : α) ∂μ, f x = 0 x) ↔ ¬μ (Function.support f) = 0

Tactic:
ae_iff,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f μ
⊢ ¬μ {a | ¬f a = 0 a} = 0 ↔ ¬μ (Function.support f) = 0
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : AddCommGroup W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup V
inst✝ : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
⊢ ⇑{ toAffineMap := f, cont := h } =
    ⇑{ toAffineMap := f, cont := h }.contLinear + Function.const V ({ toAffineMap := f, cont := h } 0)

Tactic:
ContinuousAffineMap.coe_mk_contLinear_eq_linear,

Goal state after:
R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : AddCommGroup W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup V
inst✝ : IsTopologicalAddGroup W
f : V →ᵃ[R] W
h : Continuous f.toFun
⊢ ⇑{ toAffineMap := f, cont := h } = ⇑f.linear + Function.const V ({ toAffineMap := f, cont := h } 0)
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ f z = ↑‖z‖ / ↑r * f z₁

Tactic:
hz₁,

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
⊢ f z = ↑‖z‖ / ↑r * f ((↑r * (↑‖z‖)⁻¹) • z)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case H
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = A ↑f
f : ↥(Lp E 1 μ)
⊢ A ∘SL coeToLp α E ℝ = setToL1SCLM α E μ hT

Tactic:
ext f

Goal state after:
case H
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = A ↑f
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (A ∘SL coeToLp α E ℝ) f = (setToL1SCLM α E μ hT) f
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case H
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = A ↑f
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (A ∘SL coeToLp α E ℝ) f = (setToL1SCLM α E μ hT) f

Tactic:
rw [hA f]

Goal state after:
case H
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = A ↑f
f✝ : ↥(Lp E 1 μ)
f : ↥(α →₁ₛ[μ] E)
⊢ (A ∘SL coeToLp α E ℝ) f = A ↑f
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: case neg
X : Type u_1
l : Type u_3
R : Type u_8
m' : l → Type u_9
n' : l → Type u_10
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace R
inst✝¹ : Zero R
inst✝ : DecidableEq l
A : X → (i : l) → Matrix (m' i) (n' i) R
hA : Continuous A
x✝¹ : (i : l) × m' i
x✝ : (i : l) × n' i
i₁ : l
i₂ : m' i₁
j₁ : l
j₂ : n' j₁
h : ¬i₁ = j₁
⊢ Continuous fun a ↦ 0

Tactic:
exact continuous_const

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone fun i ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
i : ℕ
⊢ 0 ≤ f i a - f 0 a

Tactic:
· simp [ha_mono zero_le]

Goal state after:
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ (fun x_1 ↦ x_1 + x) ⁻¹' sᶜ = sᶜ - {x}

Tactic:
ext y

Goal state after:
R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
y : R
⊢ y ∈ (fun x_1 ↦ x_1 + x) ⁻¹' sᶜ ↔ y ∈ sᶜ - {x}
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ (fun x_1 ↦ x + x_1) ⁻¹' sᶜ = {-x} + sᶜ

Tactic:
ext y

Goal state after:
R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
y : R
⊢ y ∈ (fun x_1 ↦ x + x_1) ⁻¹' sᶜ ↔ y ∈ {-x} + sᶜ
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
⊢ ∃ a, Tendsto f atTop (𝓝 a)

Tactic:
have f_bdd := fun x n m N hn hm => le_trans (dist_coe_le_dist x) (b_bound n m N hn hm)

Goal state after:
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist ((f n) x) ((f m) x) ≤ b N
⊢ ∃ a, Tendsto f atTop (𝓝 a)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁸ : NormedAddCommGroup G''
inst✝⁷ : PartialOrder G''
inst✝⁶ : IsOrderedAddMonoid G''
inst✝⁵ : NormedSpace ℝ G''
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : PartialOrder G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : ClosedIciTopology G''
inst✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
⊢ 0 ≤ setToFun μ T hT (g - f)

Tactic:
refine setToFun_nonneg hT hT_nonneg (hfg.mono fun a ha => ?_)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁸ : NormedAddCommGroup G''
inst✝⁷ : PartialOrder G''
inst✝⁶ : IsOrderedAddMonoid G''
inst✝⁵ : NormedSpace ℝ G''
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : PartialOrder G'
inst✝² : NormedSpace ℝ G'
inst✝¹ : ClosedIciTopology G''
inst✝ : IsOrderedAddMonoid G'
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f g : α → G'
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᵐ[μ] g
a : α
ha : f a ≤ g a
⊢ 0 a ≤ (g - f) a
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case refine_3
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist ((f n) x) ((f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n ↦ (f n) x
F : α → β
hF : ∀ (x : α), Tendsto (fun n ↦ (f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N) x) (F x) ≤ b N
⊢ Tendsto f atTop (𝓝 { toFun := F, continuous_toFun := ⋯, map_bounded' := ⋯ })

Tactic:
refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero (fun _ => dist_nonneg) ?_ b_lim)
      exact fun N => (dist_le (b0 _)).2 fun x => fF_bdd x N

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 : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ setToFun μ T hT ↑↑f

Tactic:
by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF, continuous_const]
  simp_rw [L1.setToFun_eq_setToL1 hT]; exact ContinuousLinearMap.continuous _

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
by_cases hy : y ∈ s

Goal state after:
case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∈ s
hy : y ∉ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

Tactic:
by_cases hy : y ∈ s

Goal state after:
case pos
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
hy : y ∈ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1

case neg
F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f g : α →ᵇ β
x✝ : α
C : ℝ
s : Set α
hs : IsClopen s
x y : α
hx : x ∉ s
hy : y ∉ s
⊢ dist (s.indicator 1 x) (s.indicator 1 y) ≤ 1
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
⊢ ∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖

Tactic:
have hF : F.FG := ⟨s, rfl⟩

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
⊢ ∃ x, ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
⊢ dist f g = ‖-f + g‖

Tactic:
by simp only [norm_eq, dist_eq, dist_eq_norm_neg_add, add_apply, neg_apply]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
hC : ∀ (n : ℕ), IsCompact (closedBall 0 (‖c‖ ^ n * r))
hTop : Tendsto (fun n ↦ ‖c‖ ^ n * r) atTop atTop
⊢ ProperSpace E

Tactic:
exact .of_seq_closedBall hTop (Eventually.of_forall hC)

Goal state after:
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) μ
hf : StronglyMeasurable ⇑f
hf_int_m : Integrable (⇑f) (μ.trim hm)
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
integral_simpleFunc_larger_space (le_refl m) f hf_int_m,

Goal state after:
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) μ
hf : StronglyMeasurable ⇑f
hf_int_m : Integrable (⇑f) (μ.trim hm)
⊢ ∫ (x : β), f x ∂μ = ∑ x ∈ f.range, (μ.trim hm).real (⇑f ⁻¹' {x}) • x
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ ↑(thickenedIndicatorAux δ E x).toNNReal + ↑(thickenedIndicatorAux δ E y).toNNReal ≤ 2

Tactic:
← one_add_one_eq_two

Goal state after:
case h
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ ↑(thickenedIndicatorAux δ E x).toNNReal + ↑(thickenedIndicatorAux δ E y).toNNReal ≤ 1 + 1
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

pp: case inr
α : 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).NeBot
⊢ rightLim f x ≤ leftLim f y

Tactic:
· simpa [leftLim, h'] using rightLim_le hf h

Goal state after:
case inr
α : 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).NeBot
⊢ rightLim f x ≤ leftLim f y