mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
a : α
ha : Antitone fun i ↦ f i a
i j : ℕ
hij : i ≤ j
⊢ (fun i ↦ f' i a) i ≤ (fun i ↦ f' i a) j

Tactic:
simp [f', ha hij]

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

Goal state before:
pp: R : Type u_1
inst✝² : PseudoMetricSpace R
inst✝¹ : Monoid R
inst✝ : LipschitzMul R
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith C fun p ↦ p.1 * p.2
p : R
⊢ p ∈ s * t ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a * b = p

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : PseudoMetricSpace R
inst✝¹ : Monoid R
inst✝ : LipschitzMul R
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith C fun p ↦ p.1 * p.2
p : R
⊢ p ∈ s * t → ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a * b = p

case mpr
R : Type u_1
inst✝² : PseudoMetricSpace R
inst✝¹ : Monoid R
inst✝ : LipschitzMul R
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith C fun p ↦ p.1 * p.2
p : R
⊢ (∃ a b, (a ∈ s ∧ b ∈ t) ∧ a * b = p) → p ∈ s * t
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
⊢ Tendsto (fun x_1 ↦ x - x_1) (cobounded R) (cobounded R)

Tactic:
simpa only [sub_eq_add_neg] using! (tendsto_const_add_cobounded x).comp tendsto_neg_cobounded

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

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s

Tactic:
obtain ⟨g, hg, gs⟩ :
    ∃ g : α → ι → ℝ, LipschitzWith (‖A.toContinuousLinearMap‖₊ * K) g ∧ EqOn (A ∘ f) g s :=
    L.extend_pi

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (⇑A ∘ f) g s
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (⇑A ∘ f) g s
⊢ LipschitzWith ‖↑A.symm‖₊ ⇑A.symm

Tactic:
apply A.symm.lipschitz

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
⊢ setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f + setToFun ν (weightedSMul ν) ⋯ f

Tactic:
apply setToFun_add_left'' (fun s hs h's ↦ ?_) hμ hν le_rfl zero_le_one zero_le_one zero_le_one

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
s : Set α
hs : MeasurableSet s
h's : (μ + ν) s < ∞
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
⊢ Injective ⇑f ↔ ∃ K > 0, AntilipschitzWith K ⇑f

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
⊢ Injective ⇑f → ∃ K > 0, AntilipschitzWith K ⇑f

case mpr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
⊢ (∃ K > 0, AntilipschitzWith K ⇑f) → Injective ⇑f
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
⊢ Injective ⇑f ↔ ∃ K > 0, AntilipschitzWith K ⇑f

Tactic:
by
  constructor
  · rw [← LinearMap.ker_eq_bot]
    exact f.exists_antilipschitzWith
  · rintro ⟨K, -, H⟩
    exact H.injective

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ TendstoUniformly (fun i ↦ ⇑(id i)) (⇑f) l ↔
    Tendsto (⇑UniformFun.ofFun ∘ DFunLike.coe) l (𝓝 ((⇑UniformFun.ofFun ∘ DFunLike.coe) f))

Tactic:
UniformFun.tendsto_iff_tendstoUniformly

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ TendstoUniformly (fun i ↦ ⇑(id i)) (⇑f) l ↔
    TendstoUniformly (⇑UniformFun.toFun ∘ ⇑UniformFun.ofFun ∘ DFunLike.coe)
      (UniformFun.toFun ((⇑UniformFun.ofFun ∘ DFunLike.coe) f)) l
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace R
inst✝² : Monoid R
inst✝¹ : BoundedMul R
inst✝ : ContinuousMul R
x✝ y✝ : α →ᵇ R
⊢ (x✝ * y✝).toContinuousMap = x✝.toContinuousMap * y✝.toContinuousMap

Tactic:
ext

Goal state after:
F : Type u_1
α : Type u
β : Type v
γ : Type w
R : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace R
inst✝² : Monoid R
inst✝¹ : BoundedMul R
inst✝ : ContinuousMul R
x✝ y✝ : α →ᵇ R
a✝ : α
⊢ (x✝ * y✝).toContinuousMap a✝ = (x✝.toContinuousMap * y✝.toContinuousMap) a✝
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
⊢ (fun C ↦ 0 ≤ C ∧ ∀ (x : α), ‖f x‖ ≤ C) = fun C ↦ ∀ (x : α), ‖f x‖ ≤ C

Tactic:
ext

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
a : α
x✝ : ℝ
⊢ (0 ≤ x✝ ∧ ∀ (x : α), ‖f x‖ ≤ x✝) ↔ ∀ (x : α), ‖f x‖ ≤ x✝
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
c : 𝕜
f : α →ᵇ β
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
refine norm_ofNormedAddCommGroup_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) ?_

Goal state after:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
c : 𝕜
f : α →ᵇ β
⊢ ∀ (x : α), ‖(c • ⇑f.toContinuousMap) x‖ ≤ ‖c‖ * ‖f‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝¹ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g✝ : β →L[𝕜] γ
f g : α →ᵇ β
⊢ ofNormedAddCommGroup (⇑g✝ ∘ ⇑(f + g)) ⋯ (‖g✝‖ * ‖f + g‖) ⋯ =
    ofNormedAddCommGroup (⇑g✝ ∘ ⇑f) ⋯ (‖g✝‖ * ‖f‖) ⋯ + ofNormedAddCommGroup (⇑g✝ ∘ ⇑g) ⋯ (‖g✝‖ * ‖g‖) ⋯

Tactic:
ext

Goal state after:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝¹ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g✝ : β →L[𝕜] γ
f g : α →ᵇ β
x✝ : α
⊢ (ofNormedAddCommGroup (⇑g✝ ∘ ⇑(f + g)) ⋯ (‖g✝‖ * ‖f + g‖) ⋯) x✝ =
    (ofNormedAddCommGroup (⇑g✝ ∘ ⇑f) ⋯ (‖g✝‖ * ‖f‖) ⋯ + ofNormedAddCommGroup (⇑g✝ ∘ ⇑g) ⋯ (‖g✝‖ * ‖g‖) ⋯) x✝
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
c : 𝕜
f : α →ᵇ β
⊢ ofNormedAddCommGroup (⇑g ∘ ⇑(c • f)) ⋯ (‖g‖ * ‖c • f‖) ⋯ =
    (RingHom.id 𝕜) c • ofNormedAddCommGroup (⇑g ∘ ⇑f) ⋯ (‖g‖ * ‖f‖) ⋯

Tactic:
ext

Goal state after:
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
c : 𝕜
f : α →ᵇ β
x✝ : α
⊢ (ofNormedAddCommGroup (⇑g ∘ ⇑(c • f)) ⋯ (‖g‖ * ‖c • f‖) ⋯) x✝ =
    ((RingHom.id 𝕜) c • ofNormedAddCommGroup (⇑g ∘ ⇑f) ⋯ (‖g‖ * ‖f‖) ⋯) x✝
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜✝ : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SeminormedAddCommGroup β
f g✝ : α →ᵇ β
x : α
C : ℝ
inst✝⁴ : NontriviallyNormedField 𝕜✝
inst✝³ : NormedSpace 𝕜✝ β
𝕜 : Type u_2
inst✝² : TopologicalSpace γ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
g : C(γ, α)
x✝ y✝ : α →ᵇ β
⊢ (x✝ + y✝).compContinuous g = x✝.compContinuous g + y✝.compContinuous g

Tactic:
ext

Goal state after:
α : Type u
β : Type v
γ : Type w
𝕜✝ : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SeminormedAddCommGroup β
f g✝ : α →ᵇ β
x : α
C : ℝ
inst✝⁴ : NontriviallyNormedField 𝕜✝
inst✝³ : NormedSpace 𝕜✝ β
𝕜 : Type u_2
inst✝² : TopologicalSpace γ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
g : C(γ, α)
x✝¹ y✝ : α →ᵇ β
x✝ : γ
⊢ ((x✝¹ + y✝).compContinuous g) x✝ = (x✝¹.compContinuous g + y✝.compContinuous g) x✝
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
⊢ Std.Symm fun x y ↦ 1 ≤ ‖x - y‖

Tactic:
constructor

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
⊢ ∀ (a b : E), 1 ≤ ‖a - b‖ → 1 ≤ ‖b - a‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜✝ : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SeminormedAddCommGroup β
f g✝ : α →ᵇ β
x : α
C : ℝ
inst✝⁴ : NontriviallyNormedField 𝕜✝
inst✝³ : NormedSpace 𝕜✝ β
𝕜 : Type u_2
inst✝² : TopologicalSpace γ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
g : C(γ, α)
m✝ : 𝕜
x✝ : α →ᵇ β
⊢ (m✝ • x✝).compContinuous g = (RingHom.id 𝕜) m✝ • x✝.compContinuous g

Tactic:
ext

Goal state after:
α : Type u
β : Type v
γ : Type w
𝕜✝ : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SeminormedAddCommGroup β
f g✝ : α →ᵇ β
x : α
C : ℝ
inst✝⁴ : NontriviallyNormedField 𝕜✝
inst✝³ : NormedSpace 𝕜✝ β
𝕜 : Type u_2
inst✝² : TopologicalSpace γ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
g : C(γ, α)
m✝ : 𝕜
x✝¹ : α →ᵇ β
x✝ : γ
⊢ ((m✝ • x✝¹).compContinuous g) x✝ = ((RingHom.id 𝕜) m✝ • x✝¹.compContinuous g) x✝
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
f : C(α, β)
⊢ (mkOfCompact f).toContinuousMap = f

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : SeminormedAddCommGroup E
f : C(α, β)
a✝ : α
⊢ (mkOfCompact f).toContinuousMap a✝ = f a✝
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
f : α →ᵇ β
⊢ mkOfCompact f.toContinuousMap = f

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : SeminormedAddCommGroup E
f : α →ᵇ β
x✝ : α
⊢ (mkOfCompact f.toContinuousMap) x✝ = f x✝
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
𝕜 : Type u_4
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
f : C(α, E)
⊢ (addEquivBoundedOfCompact α E).toFun (c • f) = (RingHom.id 𝕜) c • (addEquivBoundedOfCompact α E).toFun f

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CompactSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : SeminormedAddCommGroup E
𝕜 : Type u_4
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
c : 𝕜
f : C(α, E)
x✝ : α
⊢ ((addEquivBoundedOfCompact α E).toFun (c • f)) x✝ = ((RingHom.id 𝕜) c • (addEquivBoundedOfCompact α E).toFun f) x✝
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ ¬(c' = 0 ∨ c' = ∞)

Tactic:
simp [hc', hc'0]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
hμ' : ¬μ univ = ∞
⊢ False

Tactic:
exact hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ S ≤ μ.outerMeasure.caratheodory

Tactic:
BorelSpace.measurable_eq (α := G)

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
⊢ borel G ≤ μ.outerMeasure.caratheodory
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ μ.outerMeasure (↑U' ∩ U) + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'

Tactic:
μ.outerMeasure_of_isOpen ((U' : Set G) ∩ U) (U'.isOpen.inter hU)

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
⊢ μ.innerContent { carrier := ↑U' ∩ U, is_open' := ⋯ } + μ.outerMeasure (↑U' \ U) ≤ μ.outerMeasure ↑U'
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : g₂ • y = g₁ • x
⊢ (g₂⁻¹ * g₁) • x = y

Tactic:
rw [mul_smul, ← hxy, inv_smul_smul]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ ∃ (_ : g₀ ∈ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}), g ∈ (fun h ↦ g₀ * h) ⁻¹' V

Tactic:
constructor

Goal state after:
case h.h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g ∈ (fun h ↦ g₀ * h) ⁻¹' V

case h.w
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ g₀ ∈ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this✝ : ∃ᵐ (x : X) ∂μ, x ∈ s
x : X
hx : x ∈ s
h'x : x ∈ s → ‖f x‖ ≤ C
this : 0 ≤ C
⊢ ‖0‖ ≤ C * μ.real s

Tactic:
simp only [norm_zero, ge_iff_le]

Goal state after:
case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
this✝ : ∃ᵐ (x : X) ∂μ, x ∈ s
x : X
hx : x ∈ s
h'x : x ∈ s → ‖f x‖ ≤ C
this : 0 ≤ C
⊢ 0 ≤ C * μ.real s
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₁⁻¹ ∈ K₁.carrier * V⁻¹ ⊓ K₂.carrier * V⁻¹

Tactic:
constructor

Goal state after:
case left
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₁⁻¹ ∈ K₁.carrier * V⁻¹

case right
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ g₁⁻¹ ∈ K₂.carrier * V⁻¹
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ ↑(index (↑K₁) U) ≤ ↑(index (↑K₂) U)

pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ 0 < ↑(index (↑K₀) U)

Tactic:
· exact mod_cast index_mono K₂.2 h hU

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ 0 < ↑(index (↑K₀) U)
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
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ IsFiniteMeasure f.measure

Tactic:
constructor

Goal state after:
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ f.measure univ < ∞