mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case inr.const
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε : ε✝ ≠ 0
hp_pos : p ≠ 0
c : E
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
⊢ ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Goal state after:
case inr.const.inl
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε : ε✝ ≠ 0
hp_pos : p ≠ 0
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0))) p μ
⊢ ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α 0) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g

case inr.const.inr
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε : ε✝ ≠ 0
hp_pos : p ≠ 0
c : E
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
hc : c ≠ 0
⊢ ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g
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
⊢ (fun x ↦ f x (p • a + q • b)) ≤ᵐ[μ] fun x ↦ p • f x a + q • f x b

Tactic:
filter_upwards [hf_conv] with x hx

Goal state after:
α : 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 : α
hx : ConvexOn ℝ s (f x)
⊢ f x (p • a + q • b) ≤ p • f x a + q • f x b
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : ¬Integrable (fun a ↦ ↑(f a)) μ
⊢ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

Tactic:
integral_undef hf

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : ¬Integrable (fun a ↦ ↑(f a)) μ
⊢ 0 ≤ ↑b
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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f : ↥(α →₁ₛ[μ] E)
⊢ setToL1S T (-f) = -setToL1S T f

Tactic:
by
  simp_rw [setToL1S]
  have : simpleFunc.toSimpleFunc (-f) =ᵐ[μ] ⇑(-simpleFunc.toSimpleFunc f) :=
    neg_toSimpleFunc f
  rw [SimpleFunc.setToSimpleFunc_congr T h_zero h_add (SimpleFunc.integrable _) this]
  exact SimpleFunc.setToSimpleFunc_neg T h_add (SimpleFunc.integrable f)

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

Goal state before:
pp: case pos
α : 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' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT) (Integrable.toL1 f hf) = (L1.setToL1 hT') (Integrable.toL1 f hf)

Tactic:
L1.setToL1_congr_left' T T' hT hT' h

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
h1 : (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a
⊢ 0 ≤ F a - f 0 a

Tactic:
· simp [ha_bound 0]

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
inst✝ : NormedSpace ℝ E
hf : Integrable f (Measure.sum μ)
hfi : ∀ (i : ι), Integrable f (μ i)
ε : ℝ≥0
ε0 : 0 < ↑ε
hf_lt : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∞
hmem : ∀ᶠ (y : ℝ≥0∞) in 𝓝 (∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ), ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < y + ↑ε
s : Finset ι
hs : ∫⁻ (x : X), ‖f x‖ₑ ∂Measure.sum μ < ∑ b ∈ s, (fun i ↦ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i) b + ↑ε
⊢ ∃ ν, ∑ i ∈ s, μ i + ν = Measure.sum μ

Tactic:
by
    refine ⟨Measure.sum fun i : ↥(sᶜ : Set ι) ↦ μ i, ?_⟩
    simpa only [← Measure.sum_coe_finset] using! Measure.sum_add_sum_compl (s : Set ι) μ

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
h1 : (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
⊢ Tendsto (fun i ↦ (f' i a).toReal + f 0 a) atTop (𝓝 (F a))

Tactic:
h2

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
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
h1 : (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
⊢ Tendsto (fun i ↦ (f' i a).toReal + f 0 a) atTop (𝓝 ((F' a).toReal + f 0 a))
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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
⊢ setToFun μ T hT f = 0

Tactic:
have : f =ᵐ[μ] 0 := by simp [h, EventuallyEq]
  rw [setToFun_congr_ae hT this, setToFun_zero]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal

Tactic:
h_left,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
by
  simp_rw [norm_def, ← dist_zero_right]
  exact dist_lt_iff_of_nonempty_compact

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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
hF : CompleteSpace F
hfi' : Integrable f μ'
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
⊢ ∑ x ∈ (SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range,
      (T' (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ⁻¹' {x})) x =
    setToFun μ T hT ⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i)

Tactic:
setToFun_simpleFunc,

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
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
hF : CompleteSpace F
hfi' : Integrable f μ'
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
⊢ ∑ x ∈ (SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i).range,
      (T' (⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) ⁻¹' {x})) x =
    ∑ x ∈ (SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i).range,
      (T (⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i) ⁻¹' {x})) x

case hf
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : StronglyMeasurable f
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
hF : CompleteSpace F
hfi' : Integrable f μ'
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range f ∪ {0})
i : ℕ
⊢ Integrable (⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i)) μ
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
⊢ Injective fun f ↦ f.toFun

Tactic:
simp [Injective]

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ (fun f ↦ f.toFun) 0 x ≤ (fun f ↦ f.toFun) (f + const α ‖f‖) x

Tactic:
simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, coe_zero, Pi.zero_apply, coe_add,
    const_apply, Pi.add_apply]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ 0 ≤ f x + ‖f‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
h_right_g : ∫ (a : α), g a ^ q ∂μ = ∫ (a : α), ‖g a‖ ^ q ∂μ
⊢ ∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
h_left,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
h_right_g : ∫ (a : α), g a ^ q ∂μ = ∫ (a : α), ‖g a‖ ^ q ∂μ
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
⊢ f =ᵐ[μ] 0

Tactic:
have := (integral_eq_zero_iff_of_nonneg_ae ?_ hfint.neg).1 hnegf

Goal state after:
case pos.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
this : -f =ᵐ[μ] 0
⊢ f =ᵐ[μ] 0

case pos.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : ∫ (x : α), -f x ∂μ = 0
⊢ 0 ≤ᵐ[μ] -f
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f g : StieltjesFunction R
h : ∀ (x : R), ↑f x = ↑g x
⊢ f = g

Tactic:
exact (StieltjesFunction.mk.injEq ..).mpr (funext h)

Goal state after:
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
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
by
  let k := f ⁻¹' {0}
  have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
  have h's : IntegrableOn f s μ := H.mono subset_union_left le_rfl
  have A : ∀ u : Set X, ∫ x in u ∩ k, f x ∂μ = 0 := fun u =>
    setIntegral_eq_zero_of_forall_eq_zero fun x hx => hx.2
  rw [← integral_inter_add_sdiff hk h's, ← integral_inter_add_sdiff hk H, A, A, zero_add, zero_add,
    union_sdiff_distrib, union_comm]
  apply setIntegral_congr_set
  rw [union_ae_eq_right]
  apply measure_mono_null sdiff_subset
  rw [measure_eq_zero_iff_ae_notMem]
  filter_upwards [ae_imp_of_ae_restrict ht_eq] with x hx h'x using h'x.2 (hx h'x.1)

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

Goal state before:
pp: case msU
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
⊢ ∀ ⦃f : ℕ → Set G⦄ (hm : ∀ (i : ℕ), IsOpen (f i)),
    μ.innerContent { carrier := ⋃ i, f i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := f i, is_open' := ⋯ }

Tactic:
apply innerContent_iUnion_nat

Goal state after:
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
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : AEStronglyMeasurable f (μ.restrict s)
a✝ : X
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
⊢ (a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝) → a✝ ∈ s → ‖AEStronglyMeasurable.mk f hfm a✝‖ ≤ C

Tactic:
h2

Goal state after:
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)
a✝ : X
h1 : a✝ ∈ s → ‖f a✝‖ ≤ C
h2 : a✝ ∈ s → f a✝ = AEStronglyMeasurable.mk f hfm a✝
⊢ a✝ ∈ s → ‖AEStronglyMeasurable.mk f hfm a✝‖ ≤ C
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: case h.right.left
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n ↦ ‖u - ↑(w n)‖) atTop (𝓝 δ)
b : ℕ → ℝ := fun n ↦ 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
⊢ dist ↑(w p) ↑(w q) ≤ √(b N)

Tactic:
let wq := (w q : F)

Goal state after:
case h.right.left
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n ↦ ‖u - ↑(w n)‖) atTop (𝓝 δ)
b : ℕ → ℝ := fun n ↦ 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
wq : F := ↑(w q)
⊢ dist ↑(w p) ↑(w q) ≤ √(b N)
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : SecondCountableTopology G
K₀ : PositiveCompacts G
⊢ SigmaFinite (haarMeasure K₀)

Tactic:
by
  have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group; infer_instance

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
hx : x ≠ 0
r : ℝ
hr : 0 < r
⊢ ⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1

Tactic:
exact real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx hr

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
x : E
y : E'
| ⟪f x, y⟫

Tactic:
← f.apply_symm_apply y,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
x : E
y : E'
| ⟪f x, f (f.symm y)⟫
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
⊢ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0

Tactic:
have A : ∀ w ∈ K, re ⟪u - v, w⟫ = 0 := (K'.norm_eq_iInf_iff_real_inner_eq_zero hv).1 H

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
⊢ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
Module: Mathlib.Topology.Baire.CompleteMetrizable

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyPseudoMetrizableSpace X
x✝ : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun n ↦ 1 / 2 ^ n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
r : ℝ≥0∞
rpos : r > 0
hr : closedEBall y r ⊆ f n
⊢ 0 < min (min (δ / 2) r) (B (n + 1))

Tactic:
show 0 < min (min (δ / 2) r) (B (n + 1))
      exact lt_min (lt_min (ENNReal.half_pos δpos) rpos) (Bpos (n + 1))

Goal state after: