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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • (ENNReal.toReal ∘ g) x = (∑ x ∈ f.range, g x * μ (⇑f ⁻¹' {x})).toReal

pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ (ENNReal.toReal ∘ g) 0 = 0

Tactic:
ENNReal.toReal_sum

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • (ENNReal.toReal ∘ g) x = ∑ a ∈ f.range, (g a * μ (⇑f ⁻¹' {a})).toReal

α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ ∀ a ∈ f.range, g a * μ (⇑f ⁻¹' {a}) ≠ ∞

α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
⊢ (ENNReal.toReal ∘ g) 0 = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
b : E
x✝ : b ∈ f.range
⊢ (g b).toReal * μ.real (⇑f ⁻¹' {b}) = (g b).toReal * (μ (⇑f ⁻¹' {b})).toReal

Tactic:
measureReal_def

Goal state after:
α : Type u_1
E : Type u_2
inst✝ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
f : α →ₛ E
g : E → ℝ≥0∞
hf : Integrable (⇑f) μ
hg0 : g 0 = 0
ht : ∀ (b : E), g b ≠ ∞
hf' : f.FinMeasSupp μ
b : E
x✝ : b ∈ f.range
⊢ (g b).toReal * (μ (⇑f ⁻¹' {b})).toReal = (g b).toReal * (μ (⇑f ⁻¹' {b})).toReal
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_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
h : ⇑f =ᵐ[μ] ⇑g
⊢ setToSimpleFunc T f = setToSimpleFunc T g

Tactic:
by
  refine setToSimpleFunc_congr' T h_add hf ((integrable_congr h).mp hf) ?_
  refine fun x y hxy => h_zero _ ((measurableSet_fiber f x).inter (measurableSet_fiber g y)) ?_
  rw [EventuallyEq, ae_iff] at h
  refine measure_mono_null (fun z => ?_) h
  simp_rw [Set.mem_inter_iff, Set.mem_ofPred_eq, Set.mem_preimage, Set.mem_singleton_iff]
  intro h
  rwa [h.1, h.2]

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
⊢ g ∈ closure[instTopologicalSpaceSubtype] (Set.range (coeSimpleFuncNonnegToLpNonneg p μ G))

Tactic:
borelize G
  rw [mem_closure_iff_seq_limit]
  have hg_memLp : MemLp (g : α → G) p μ := Lp.memLp (g : Lp G p μ)
  have zero_mem : (0 : G) ∈ (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y } := by
    simp only [union_singleton, mem_inter_iff, mem_insert_iff, true_or,
      mem_ofPred_eq, le_refl, and_self_iff]
  have : SeparableSpace ((range (g : α → G) ∪ {0}) ∩ { y | 0 ≤ y } : Set G) := by
    apply IsSeparable.separableSpace
    apply IsSeparable.mono _ Set.inter_subset_left
    exact
      (Lp.stronglyMeasurable (g : Lp G p μ)).isSeparable_range.union
        (finite_singleton _).isSeparable
  have g_meas : Measurable (g : α → G) := (Lp.stronglyMeasurable (g : Lp G p μ)).measurable
  let x n := SimpleFunc.approxOn (g : α → G) g_meas
    ((range (g : α → G) ∪ {0}) ∩ { y | 0 ≤ y }) 0 zero_mem n
  have hx_nonneg : ∀ n, 0 ≤ x n := by
    intro n a
    change x n a ∈ { y : G | 0 ≤ y }
    have A : (range (g : α → G) ∪ {0} : Set G) ∩ { y | 0 ≤ y } ⊆ { y | 0 ≤ y } :=
      inter_subset_right
    apply A
    exact SimpleFunc.approxOn_mem g_meas _ n a
  have hx_memLp : ∀ n, MemLp (x n) p μ :=
    SimpleFunc.memLp_approxOn _ hg_memLp _ ⟨aestronglyMeasurable_const, by simp⟩
  have h_toLp := fun n => MemLp.coeFn_toLp (hx_memLp n)
  have hx_nonneg_Lp : ∀ n, 0 ≤ toLp (x n) (hx_memLp n) := by
    intro n
    rw [← Lp.simpleFunc.coeFn_le, Lp.simpleFunc.toLp_eq_toLp]
    filter_upwards [Lp.simpleFunc.coeFn_zero p μ G, h_toLp n] with a ha0 ha_toLp
    rw [ha0, ha_toLp]
    exact hx_nonneg n a
  have hx_tendsto :
      Tendsto (fun n : ℕ => eLpNorm ((x n : α → G) - (g : α → G)) p μ) atTop (𝓝 0) := by
    apply SimpleFunc.tendsto_approxOn_Lp_eLpNorm g_meas zero_mem hp_ne_top
    · have hg_nonneg : (0 : α → G) ≤ᵐ[μ] g := (Lp.coeFn_nonneg _).mpr g.2
      refine hg_nonneg.mono fun a ha => subset_closure ?_
      simpa using ha
    · simp_rw [sub_zero]; finiteness
  refine
    ⟨fun n =>
      (coeSimpleFuncNonnegToLpNonneg p μ G) ⟨toLp (x n) (hx_memLp n), hx_nonneg_Lp n⟩,
      fun n => mem_range_self _, ?_⟩
  suffices Tendsto (fun n : ℕ => (toLp (x n) (hx_memLp n) : Lp G p μ)) atTop (𝓝 (g : Lp G p μ)) by
    rw [tendsto_iff_dist_tendsto_zero] at this ⊢
    simp_rw [Subtype.dist_eq]
    exact this
  rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']
  refine Filter.Tendsto.congr (fun n => eLpNorm_congr_ae (EventuallyEq.sub ?_ ?_)) hx_tendsto
  · symm
    rw [Lp.simpleFunc.toLp_eq_toLp]
    exact h_toLp n
  · rfl

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

Goal state before:
pp: case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
f : β → α → G
s : Set β
b : β
hb : b ∈ s
⊢ ∫ (y : α), s.indicator (fun x ↦ f x y) b ∂μ = s.indicator (fun x ↦ ∫ (y : α), f x y ∂μ) b

Tactic:
simp [hb]

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

Goal state before:
pp: case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
f : β → α → G
s : Set β
b : β
hb : b ∉ s
⊢ ∫ (y : α), s.indicator (fun x ↦ f x y) b ∂μ = s.indicator (fun x ↦ ∫ (y : α), f x y ∂μ) b

Tactic:
simp [hb]

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : OrderClosedTopology E
f : α → E
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᵐ[ν] f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := ⋯
this✝ : BorelSpace E
g : α → E
hfi : Integrable g ν
hg : StronglyMeasurable g
hg_nonneg : ∀ (x : α), g x ∈ Ici 0
hfg : f =ᵐ[ν] g
x✝ : SeparableSpace ↑(range g ∪ {0})
h₁ : Tendsto (fun n ↦ SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop (𝓝 (∫ (x : α), g x ∂ν))
h₂ : Tendsto (fun n ↦ SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
⊢ ∀ (x : ℕ),
    SimpleFunc.integral μ (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ x) ≤
      SimpleFunc.integral ν (approxOn g ⋯ (range g ∪ {0}) 0 ⋯ x)

Tactic:
exact fun n ↦ SimpleFunc.integral_mono_measure
    (Eventually.of_forall <| SimpleFunc.approxOn_range_nonneg hg_nonneg n) hle
    (SimpleFunc.integrable_approxOn_range _ hfi n)

Goal state after:
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✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ ∫ (x : α), f x (p • a + q • b) ∂μ ≤ ∫ (x : α), p • f x a + q • f x b ∂μ

Tactic:
refine integral_mono_ae ?lhs ?rhs ?ae_le

Goal state after:
case lhs
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ Integrable (fun x ↦ f x (p • a + q • b)) μ

case rhs
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ Integrable (fun x ↦ p • f x a + q • f x b) μ

case ae_le
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : PartialOrder E
inst✝⁴ : IsOrderedAddMonoid E
inst✝³ : IsOrderedModule ℝ E
inst✝² : ClosedIciTopology E
β : Type u_6
inst✝¹ : AddCommMonoid β
inst✝ : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ (fun x ↦ f x (p • a + q • b)) ≤ᵐ[μ] fun x ↦ p • f x a + q • f x b
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ (∫⁻ (x : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) x ∂μ).toReal =
    ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖

Tactic:
measureReal_def

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ (∫⁻ (x : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) x ∂μ).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ (∑ x ∈ (toSimpleFunc f).range, ‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
ENNReal.toReal_sum

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∑ a ∈ (toSimpleFunc f).range, (‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a})).toReal =
    ∑ x ∈ (toSimpleFunc f).range, (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∀ a ∈ (toSimpleFunc f).range, ‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a}) ≠ ∞
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
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a

Tactic:
filter_upwards [hf_bound] with a ha_bound i

Goal state after:
α : 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
a : α
ha_bound : ∀ (i : ℕ), f i a ≤ F a
i : ℕ
⊢ f' i a ≤ F' a
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: case hbc
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := ⋯
yy' : y = d • y'
⊢ ‖c‖ / R * ‖x‖ ≤ ‖x - y'‖

Tactic:
exact hx y' (by simp [y', Submodule.smul_mem _ _ hy])

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
x y : P
⊢ edist (f x) (f y) = edist x y

Tactic:
simp [edist_dist]

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

Goal state before:
pp: case e_f
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f (Measure.sum fun a ↦ μ {a} • Measure.dirac a)
a : X
⊢ (μ {a}).toReal • f a = μ.real {a} • f a

Tactic:
measureReal_def

Goal state after:
case e_f
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f (Measure.sum fun a ↦ μ {a} • Measure.dirac a)
a : X
⊢ (μ {a}).toReal • f a = (μ {a}).toReal • f a
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
Ag : ℝ
hAg : t ⊆ closedBall 0 Ag
key : IsCompact (closedBall 0 Af ×ˢ closedBall 0 Ag)
⊢ s * t ⊆ (fun p ↦ p.1 * p.2) '' closedBall 0 Af ×ˢ closedBall 0 Ag

Tactic:
intro _ ⟨x, x_in_s, y, y_in_t, xy_eq⟩

Goal state after:
s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
Ag : ℝ
hAg : t ⊆ closedBall 0 Ag
key : IsCompact (closedBall 0 Af ×ˢ closedBall 0 Ag)
a✝ x : ℝ≥0
x_in_s : x ∈ s
y : ℝ≥0
y_in_t : y ∈ t
xy_eq : (fun x1 x2 ↦ x1 * x2) x y = a✝
⊢ a✝ ∈ (fun p ↦ p.1 * p.2) '' closedBall 0 Af ×ˢ closedBall 0 Ag
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
⊢ (∀ (x : α), dist (f x) (g x) < C) → dist f g < C

Tactic:
by_cases h : Nonempty α
    · exact dist_lt_of_nonempty_compact
    · rintro -
      convert! C0
      apply le_antisymm _ dist_nonneg'
      rw [dist_eq]
      exact csInf_le ⟨0, fun C => And.left⟩ ⟨le_rfl, fun x => False.elim (h (Nonempty.intro x))⟩

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f g : α →ᵇ β
x : α
⊢ ↑C * dist (f x) (g x) ≤ ↑C * dist f g

Tactic:
gcongr; apply dist_coe_le_dist

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
x : α
⊢ ‖f x‖ = dist (f x) (0 x)

Tactic:
simp [dist_zero_right]

Goal state after:
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:
intros; ext; simp

Goal state after:
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:
intros; ext; simp

Goal state after:
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‖
⊢ Summable fun x ↦ ‖f x‖

Tactic:
by
    obtain v := Module.finBasis ℝ E
    set e := v.equivFunL
    have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 hf)
    refine .of_norm_bounded (H.mul_left ↑‖(e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E)‖₊) fun i ↦ ?_
    simpa using (e.symm : (Fin (finrank ℝ E) → ℝ) →L[ℝ] E).le_opNorm (e <| f i)

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

Goal state before:
pp: case e_f
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
hE : CompleteSpace E
inst✝ : Unique α
f : α → E
x : α
⊢ x = default

Tactic:
exact Unique.uniq _ x

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
inst✝² : StarAddMonoid β
inst✝¹ : NormedStarGroup β
inst✝ : CompactSpace α
f : C(α, β)
⊢ ‖mkOfCompact (star f)‖ ≤ ‖f‖

Tactic:
BoundedContinuousFunction.mkOfCompact_star,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
inst✝² : StarAddMonoid β
inst✝¹ : NormedStarGroup β
inst✝ : CompactSpace α
f : C(α, β)
⊢ ‖star (mkOfCompact f)‖ ≤ ‖f‖
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
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
⊢ s ∈ map (rightLim f) (𝓝[≥] x)

Tactic:
change ∀ᶠ y in 𝓝[≥] x, rightLim f y ∈ s

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)
⊢ ∀ᶠ (y : R) in 𝓝[≥] x, rightLim f y ∈ s
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case hf
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
this :
  ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
⊢ Integrable ((⋂ i ∈ u, s i).indicator fun a ↦ (-1) ^ (#u + 1) • f a) μ

Tactic:
integrable_indicator_iff (A u hu)

Goal state after:
case hf
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
this :
  ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
⊢ IntegrableOn (fun a ↦ (-1) ^ (#u + 1) • f a) (⋂ i ∈ u, s i) μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ =
    ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) • ∫ (x : X) in ⋂ i ∈ u, s i, f x ∂μ

Tactic:
simp_rw [← integral_smul, ← integral_indicator (Finset.measurableSet_biUnion _ hs)]
  have A (u) (hu : u ∈ t.powerset.filter (·.Nonempty)) : MeasurableSet (⋂ i ∈ u, s i) := by
    refine u.measurableSet_biInter fun i hi ↦ hs i ?_
    grind
  have : ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1 : ℝ) ^ (#x + 1) • f a ∂μ
      = ∑ x ∈ t.powerset with x.Nonempty, ∫ a, indicator (⋂ i ∈ x, s i)
        (fun a ↦ (-1 : ℝ) ^ (#x + 1) • f a) a ∂μ := by
    apply Finset.sum_congr rfl (fun x hx ↦ ?_)
    rw [← integral_indicator (A x hx)]
  rw [this, ← integral_finsetSum]; swap
  · intro u hu
    rw [integrable_indicator_iff (A u hu)]
    apply Integrable.smul
    simp only [Finset.mem_filter, Finset.mem_powerset] at hu
    rcases hu.2 with ⟨i, hi⟩
    exact (hf i (hu.1 hi)).mono (biInter_subset_of_mem hi) le_rfl
  congr with x
  convert! Finset.indicator_biUnion_eq_sum_powerset t s f x with u hu
  rw [indicator_smul_apply]
  norm_cast

Goal state after: