mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun ⊆
    Function.support f₁.toFun ∪ Function.support f₂.toFun

Tactic:
intro x

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
x : α
⊢ x ∈ Function.support (f₂.toContinuousMap - f₁.toContinuousMap).toFun →
    x ∈ Function.support f₁.toFun ∪ Function.support f₂.toFun
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
f g : α →C_c ℝ
⊢ (f + g).nnrealPart ≤ f.nnrealPart + g.nnrealPart

Tactic:
intro x

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
f g : α →C_c ℝ
x : α
⊢ (f + g).nnrealPart x ≤ (f.nnrealPart + g.nnrealPart) x
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
⊢ ↑(Λ (a • f).nnrealPart) - ↑(Λ (-(a • f)).nnrealPart) = (RingHom.id ℝ) a • (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))

Tactic:
rcases le_total 0 a with ha | ha
        · rw [RingHom.id_apply, smul_eq_mul, ← (smul_neg a f), nnrealPart_smul_pos f ha,
            nnrealPart_smul_pos (-f) ha]
          simp [sup_of_le_left ha, mul_sub]
        · simp only [RingHom.id_apply, smul_eq_mul, ← (smul_neg a f),
            nnrealPart_smul_neg f ha, nnrealPart_smul_neg (-f) ha, map_smul,
            NNReal.coe_mul, Real.coe_toNNReal', neg_neg, sup_of_le_left (neg_nonneg.mpr ha)]
          ring

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := ⋯
ν : Measure α := ⋯
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
⊢ ∀ (x : α), 0 ≤ g x → (fun x ↦ (ρ x).toReal) x = g x

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
x : α
⊢ 0 ≤ g x → (fun x ↦ (ρ x).toReal) x = g x
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := ⋯
ν : Measure α := ⋯
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
⊢ ∀ (x : α), (fun x ↦ (ρ x).toReal) x = g x → (fun a ↦ f a * g a) x = (fun a ↦ (ρ a).toReal * f a) x

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
x : α
⊢ (fun x ↦ (ρ x).toReal) x = g x → (fun a ↦ f a * g a) x = (fun a ↦ (ρ a).toReal * f a) x
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
ω : E → E →L[𝕜] F
a b : E
⊢ ∫ᶜ (x : E) in Path.segment a b, ω x = ∫ (t : ℝ) in 0..1, (ω ((lineMap a b) t)) (b - a)

Tactic:
by
  rw [curveIntegral_def]
  refine intervalIntegral.integral_congr fun t ht ↦ ?_
  rw [uIcc_of_le zero_le_one] at ht
  exact curveIntegralFun_segment ω a b ht

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := ⋯
ν : Measure α := ⋯
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : g =ᵐ[μ.restrict s] 0
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
⊢ ∀ (x : α), g x = 0 x → (fun x ↦ f x * g x) x = 0 x

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : g =ᵐ[μ.restrict s] 0
hν0 : ∫ (x : α) in s, 1 ∂ν = 0
c : α
hc : c ∈ s
x : α
⊢ g x = 0 x → (fun x ↦ f x * g x) x = 0 x
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] a, ‖∫ᶜ (x : E) in Path.segment a x, ω x - (ω a) (x - a)‖ ≤ c * ‖x - a‖

Tactic:
intro ε hε

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝[s] a, ‖∫ᶜ (x : E) in Path.segment a x, ω x - (ω a) (x - a)‖ ≤ ε * ‖x - a‖
Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
⊢ {a | ContinuousWithinAt ω s a} ∩ {a_1 | dist (ω a_1) (ω a) ≤ ε} ∈ 𝓝[s] a

Tactic:
inter_mem_iff

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
⊢ {a | ContinuousWithinAt ω s a} ∈ 𝓝[s] a ∧ {a_1 | dist (ω a_1) (ω a) ≤ ε} ∈ 𝓝[s] a
Module: Mathlib.MeasureTheory.Integral.MeanValue

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := ⋯
ν : Measure α := ⋯
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
⊢ ∀ (x : α), (fun x ↦ (ρ x).toReal) x = g x → (fun x ↦ (ρ x).toReal * f x) x = (fun x ↦ f x * g x) x

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
s : Set α
f g : α → ℝ
μ : Measure α
hs_conn : IsConnected s
hs_meas : MeasurableSet s
hf : ContinuousOn f s
hg : IntegrableOn g s μ
hfg : IntegrableOn (fun x ↦ f x * g x) s μ
hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x
ρ : α → ENNReal := fun x ↦ ENNReal.ofReal (g x)
ν : Measure α := μ.withDensity ρ
hρ_ae : AEMeasurable ρ (μ.restrict s)
hρ_top : ∀ᵐ (x : α) ∂μ.restrict s, ρ x < ⊤
h_toReal_ae : (fun x ↦ (ρ x).toReal) =ᵐ[μ.restrict s] g
heq : ∫ (x : α) in s, f x * g x ∂μ = ∫ (x : α) in s, f x ∂ν
hg1 : ∫ (x : α) in s, g x ∂μ = ∫ (x : α) in s, 1 ∂ν
hν0 : ¬∫ (x : α) in s, 1 ∂ν = 0
hν0' : (ν s).toReal ≠ 0
hνfin : ν s ≠ ⊤
hν0'' : ν s ≠ 0
x : α
⊢ (fun x ↦ (ρ x).toReal) x = g x → (fun x ↦ (ρ x).toReal * f x) x = (fun x ↦ f x * g x) x
Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ ∀ a ∈ {x | f x ≠ 0}ᶜ, ↑(f a) • g a = ↑(f a) • g' a

Tactic:
intro x

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
⊢ x ∈ {x | f x ≠ 0}ᶜ → ↑(f x) • g x = ↑(f x) • g' x
Module: Mathlib.MeasureTheory.Integral.LebesgueNormedSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
⊢ ∀ (a : α), ↑(f a) • g a = g' a → ↑(f a) ≠ 0 → g a = (↑(f a))⁻¹ • g' a

Tactic:
intro x

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : SecondCountableTopology E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
⊢ ↑(f x) • g x = g' x → ↑(f x) ≠ 0 → g x = (↑(f x))⁻¹ • g' x
Module: Mathlib.MeasureTheory.Integral.Regular

Goal state before:
pp: case hs
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : NormalSpace X
r : ENNReal
hr : r < μ U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < μ K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
fK : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 K
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
⊢ ∀ x ∈ K, 1 ≤ f x

Tactic:
intro x

Goal state after:
case hs
X : Type u_1
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace X
inst✝⁴ : BorelSpace X
inst✝³ : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : NormalSpace X
r : ENNReal
hr : r < μ U
K : Set X
KU : K ⊆ U
K_comp : IsCompact K
hK : r < μ K
f : X → ℝ
f_cont : Continuous f
fU : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 0 Uᶜ
fK : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 K
f_range : ∀ (x : X), { toFun := f, continuous_toFun := f_cont } x ∈ Icc 0 1
x : X
⊢ x ∈ K → 1 ≤ f x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ trapezoidal_integral f N a b = -trapezoidal_integral f N b a

Tactic:
unfold trapezoidal_integral

Goal state after:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ (b - a) / ↑N * ((f a + f b) / 2 + ∑ k ∈ Finset.range (N - 1), f (a + (↑k + 1) * (b - a) / ↑N)) =
    -((a - b) / ↑N * ((f b + f a) / 2 + ∑ k ∈ Finset.range (N - 1), f (b + (↑k + 1) * (a - b) / ↑N)))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ -trapezoidal_integral f N b a - ∫ (x : ℝ) in a..b, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)

Tactic:
integral_symm,

Goal state after:
f : ℝ → ℝ
N : ℕ
N_nonzero : 0 < N
a b : ℝ
⊢ -trapezoidal_integral f N b a - -∫ (x : ℝ) in b..a, f x = -(trapezoidal_integral f N b a - ∫ (x : ℝ) in b..a, f x)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case h
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
⊢ { toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport }.nnrealPart ∈ {f | ∀ x ∈ K, 1 ≤ f x}

Tactic:
intro x

Goal state after:
case h
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K : Compacts X
V : Set X
hVcp : IsCompact V
hKsubintV : K.carrier ⊆ interior V
hIsCompact_closure_interior : IsCompact (closure (interior V))
f : C(X, ℝ)
hsuppfsubV : tsupport ⇑f ⊆ interior V
hfeq1onK : EqOn (⇑f) 1 K.carrier
hfinicc : ∀ (x : X), f x ∈ Icc 0 1
hfHasCompactSupport : HasCompactSupport ⇑f
x : X
⊢ x ∈ K → 1 ≤ { toContinuousMap := f, hasCompactSupport' := hfHasCompactSupport }.nnrealPart x
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
⊢ t ⊆ ⋃ j, if j = 0 then s₀ᶜ else s₁ᶜ

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
⊢ x ∈ t → x ∈ ⋃ j, if j = 0 then s₀ᶜ else s₁ᶜ
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ

Tactic:
rw [← subset_compl_iff_disjoint_right, ← compl_compl s₀, compl_subset_iff_union] at disj

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : s₀ᶜ ∪ s₁ᶜ = univ
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
x : X
hx : x ∈ t
⊢ ∃ i, x ∈ if i = 0 then s₀ᶜ else s₁ᶜ
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case h.refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
⊢ EqOn (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ }.nnrealPart) 1 s₀

Tactic:
intro x

Goal state after:
case h.refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
⊢ x ∈ s₀ → { toContinuousMap := f 1, hasCompactSupport' := ⋯ }.nnrealPart x = 1 x
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
⊢ EqOn (⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ }.nnrealPart) 1 s₁

Tactic:
intro x

Goal state after:
case h.refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
⊢ x ∈ s₁ → { toContinuousMap := f 0, hasCompactSupport' := ⋯ }.nnrealPart x = 1 x
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: case h.refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
⊢ EqOn
    (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ }.nnrealPart +
      ⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ }.nnrealPart)
    1 t

Tactic:
intro x

Goal state after:
case h.refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
s₀ s₁ t : Set X
s₀_compact : IsCompact s₀
s₁_compact : IsCompact s₁
t_compact : IsCompact t
disj : Disjoint s₀ s₁
hst : s₀ ∪ s₁ ⊆ t
so : Fin 2 → Set X := fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
hso : so = fun j ↦ if j = 0 then s₀ᶜ else s₁ᶜ
soopen : ∀ (j : Fin 2), IsOpen (so j)
hsot : t ⊆ ⋃ j, so j
f : Fin 2 → C(X, ℝ)
f_supp_in_so : ∀ (i : Fin 2), tsupport ⇑(f i) ⊆ so i
sum_f_one_on_t : EqOn (∑ i, ⇑(f i)) 1 t
f_in_icc : ∀ (i : Fin 2) (x : X), (f i) x ∈ Icc 0 1
f_hcs : ∀ (i : Fin 2), HasCompactSupport ⇑(f i)
sum_one_x : ∀ x ∈ t, (f 0) x + (f 1) x = 1
x : X
⊢ x ∈ t →
    (⇑{ toContinuousMap := f 1, hasCompactSupport' := ⋯ }.nnrealPart +
          ⇑{ toContinuousMap := f 0, hasCompactSupport' := ⋯ }.nnrealPart)
        x =
      1 x
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
⊢ ∀ x ∈ K₁ ⊔ K₂, x ∈ support ⇑f

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K₁ K₂ : Compacts X
disj : Disjoint ↑K₁ ↑K₂
b : ℝ≥0
f : X →C_c ℝ≥0
hf : f ∈ {f | ∀ x ∈ K₁ ⊔ K₂, 1 ≤ f x}
Λf_eq_b : Λ f = b
x : X
⊢ x ∈ K₁ ⊔ K₂ → x ∈ support ⇑f
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule

Goal state before:
pp: f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
⊢ EqOn (_root_.derivWithin f (Set.Icc a b)) (_root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))))
    (Set.Icc (ak k) (ak (k + 1)))

Tactic:
intro x

Goal state after:
f : ℝ → ℝ
ζ a b : ℝ
a_lt_b : a < b
h_df : DifferentiableOn ℝ f (Set.Icc a b)
h_ddf : DifferentiableOn ℝ (_root_.derivWithin f (Set.Icc a b)) (Set.Icc a b)
fpp_bound : ∀ (x : ℝ), |iteratedDerivWithin 2 f (Set.Icc a b) x| ≤ ζ
N : ℕ
N_nonzero : 0 < N
h : ℝ := (b - a) / ↑N
ak : ℕ → ℝ := fun k ↦ a + ↑k * h
h0 : ∀ (k : ℕ), ak (k + 1) - ak k = h
hab : 0 < b - a
hpos : 0 < h
hb : b = a + ↑N * h
k : ℕ
hk : k < N
h1 : a ≤ ak k
h2 : ak (k + 1) ≤ b
h3 : Set.Icc (ak k) (ak (k + 1)) ⊆ Set.Icc a b
h4 : ak k < ak (k + 1)
x : ℝ
⊢ x ∈ Set.Icc (ak k) (ak (k + 1)) →
    _root_.derivWithin f (Set.Icc a b) x = _root_.derivWithin f (Set.Icc (ak k) (ak (k + 1))) x