mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
i : ι
⊢ ∃ c, c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i

Tactic:
isVonNBounded_pi_iff

Goal state after:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : ∀ (i : ι), IsVonNBounded 𝕜 (eval i '' s)
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
i : ι
⊢ ∃ c, c ≠ 0 ∧ ∀ (c' : 𝕜), ‖c'‖ ≤ ‖c‖ → ∀ x ∈ s, c' • x i ∈ t i
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case h.calc_2
𝕜 : Type u_1
E : Type u_5
Fₗ : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r

Tactic:
div_le_iff₀ (zero_lt_one.trans hk)

Goal state after:
case h.calc_2
𝕜 : Type u_1
E : Type u_5
Fₗ : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r ≤ ‖x‖ * ‖k‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : ContinuousSub M
h : IsTopCompl p q
x : M
⊢ (q.projectionL p ⋯) x + (p.projectionL q h) x = x

Tactic:
projectionL_add_projectionL_eq_self

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : ContinuousSub M
h : IsTopCompl p q
x : M
⊢ x = x
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : μ s₂ ≠ ∞
h₂ : μ t₂ ≠ ∞
⊢ (μ (s₁ ∪ t₁)).toReal = (μ (s₂ ∪ t₂)).toReal

Tactic:
measure_union_congr_of_subset hs _ ht

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : μ s₂ ≠ ∞
h₂ : μ t₂ ≠ ∞
⊢ (μ (s₂ ∪ t₂)).toReal = (μ (s₂ ∪ t₂)).toReal

α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : μ s₂ ≠ ∞
h₂ : μ t₂ ≠ ∞
⊢ μ t₂ ≤ μ t₁

α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : μ s₂ ≠ ∞
h₂ : μ t₂ ≠ ∞
⊢ μ s₂ ≤ μ s₁
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : NullMeasurableSet s μ
⊢ AEMeasurable f (μ.restrict s)

Tactic:
rcases hs.exists_measurable_subset_ae_eq with ⟨t, ts, ht, t_eq_s⟩
  rw [← Measure.restrict_congr_set t_eq_s]
  exact ContinuousOn.aemeasurable (hf.mono ts) ht

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_8
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
f : α → β
φ : α → 𝕜
hf : Integrable f μ
hφ : MemLp φ ∞ μ
⊢ Integrable (φ • f) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢
  exact MemLp.smul hf hφ

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ Integrable (fun x ↦ f x • c) μ ↔ Integrable f μ

Tactic:
simp_rw [Integrable, aestronglyMeasurable_smul_const_iff (f := f) hc, and_congr_right_iff,
    hasFiniteIntegral_iff_enorm, enorm_smul]
  intro _; rw [lintegral_mul_const' _ _ enorm_ne_top, ENNReal.mul_lt_top_iff]
  have : ∀ x : ℝ≥0∞, x = 0 → x < ∞ := by simp
  simp [hc, or_iff_left_of_imp (this _)]

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
x : X
hx : x ∈ s
⊢ ∃ v ∈ T, x ∈ v

Tactic:
simpa only [mem_iUnion, exists_prop] using sT hx

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

Goal state before:
pp: case e'_5
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm (fun x ↦ f x - y₀) p μ < ∞
hp_zero : ¬p = 0
hp : 0 < p.toReal
this : Tendsto (fun n ↦ ∫⁻ (x : β), ‖(approxOn f hf s y₀ h₀ n) x - f x‖ₑ ^ p.toReal ∂μ) atTop (𝓝 0)
⊢ 0 = 0 ^ (1 / p.toReal)

Tactic:
simp [zero_rpow_of_pos (_root_.inv_pos.mpr hp)]

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) μ
⊢ ∀ ⦃x : β⦄,
    x ∈ s →
      ∀ ⦃y : β⦄,
        y ∈ s →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b →
                a + b = 1 →
                  (fun b ↦ ∫ (x : α), f x b ∂μ) (a • x + b • y) ≤
                    a • (fun b ↦ ∫ (x : α), f x b ∂μ) x + b • (fun b ↦ ∫ (x : α), f x b ∂μ) y

Tactic:
intro a ha b hb p q hp hq hpq

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
⊢ (fun b ↦ ∫ (x : α), f x b ∂μ) (p • a + q • b) ≤
    p • (fun b ↦ ∫ (x : α), f x b ∂μ) a + q • (fun b ↦ ∫ (x : α), f x b ∂μ) b
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f μ
⊢ (fun a ↦ ENNReal.ofReal (f a)) =ᵐ[μ] 0 ↔ f =ᵐ[μ] 0

Tactic:
rw [← hf.ge_iff_eq', Filter.EventuallyEq, Filter.EventuallyLE]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f μ
⊢ (∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x) = 0 x) ↔ ∀ᵐ (x : α) ∂μ, f x ≤ 0 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)
⊢ (∫⁻ (x : α), ‖(toSimpleFunc f) x‖ₑ ∂μ).toReal = ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖

Tactic:
have h_eq := SimpleFunc.map_apply (‖·‖ₑ) (toSimpleFunc f)

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 : α), ‖(toSimpleFunc f) x‖ₑ ∂μ).toReal = ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
rcases eq_or_ne (infDist x sᶜ) 0 with h₀ | h₀

Goal state after:
case inl
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

case inr
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ ≠ 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case indicatorConst
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝⁵ : NormedAddCommGroup G''
inst✝⁴ : PartialOrder G''
inst✝³ : IsOrderedAddMonoid G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : CompleteSpace G''
inst✝ : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ (setToL1 hT) ↑(indicatorConst 1 hs ⋯ c) ≤ (setToL1 hT') ↑(indicatorConst 1 hs ⋯ c)

Tactic:
| @indicatorConst c s hs hμs =>

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 : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : ¬Integrable f μ
hF : CompleteSpace F
⊢ setToFun μ T hT f = 0

pp: case neg
α : 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
hf : ¬Integrable f μ
hF : ¬CompleteSpace F
⊢ setToFun μ T hT f = 0

Tactic:
· simp [setToFun, hF, hf]

Goal state after:
case neg
α : 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
hf : ¬Integrable f μ
hF : ¬CompleteSpace F
⊢ setToFun μ T hT f = 0
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 α
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ 0 C
⊢ setToFun μ 0 hT f = 0

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  by_cases hf : Integrable f μ
  · rw [setToFun_eq hT hf]; exact L1.setToL1_zero_left hT _
  · exact setToFun_undef hT hf

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

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

Tactic:
rw [← Set.preimage_compl]

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

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

Tactic:
rw [← Set.preimage_compl]

Goal state after:
R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
⊢ Bornology.IsBounded ((fun x_1 ↦ x + x_1) ⁻¹' sᶜ)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case refine_1
α : 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
LAsymm : LipschitzWith ‖↑A.symm‖₊ ⇑A.symm
⊢ ‖↑A.symm‖₊ * ‖↑A‖₊ * K ≤
    (have A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
      max (‖↑A.symm‖₊ * ‖↑A‖₊) 1) *
      K

Tactic:
exact mul_le_mul' (le_max_left _ _) le_rfl

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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᵐ[μ] g
hF : CompleteSpace F
hfi : ¬Integrable f μ
⊢ ¬Integrable g μ

Tactic:
integrable_congr h

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 : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
h : f =ᵐ[μ] g
hF : CompleteSpace F
hfi : ¬Integrable g μ
⊢ ¬Integrable g μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} < ∞
⊢ ε * μ.real {x | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ

Tactic:
have := Fact.mk hμ

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} < ∞
this : Fact (μ {x | ε ≤ f x} < ∞)
⊢ ε * μ.real {x | ε ≤ f x} ≤ ∫ (x : α), f x ∂μ
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
h✝ : Nonempty α
⊢ BddAbove (range fun x ↦ dist (f x) (g x))

Tactic:
exact dist_set_exists.imp fun C hC => forall_mem_range.2 hC.2

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

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

Tactic:
have fF_bdd : ∀ x N, dist (f N x) (F x) ≤ b N :=
      fun x N => le_of_tendsto (tendsto_const_nhds.dist (hF x))
        (Filter.eventually_atTop.2 ⟨N, fun n hn => f_bdd x N n N (le_refl N) hn⟩)

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

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

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

Tactic:
· -- Check that `F` is bounded
      rcases (f 0).bounded with ⟨C, hC⟩
      refine ⟨C + (b 0 + b 0), fun x y => ?_⟩
      calc
        dist (F x) (F y) ≤ dist (f 0 x) (f 0 y) + (dist (f 0 x) (F x) + dist (f 0 y) (F y)) :=
          dist_triangle4_left _ _ _ _
        _ ≤ C + (b 0 + b 0) := add_le_add (hC x y) (add_le_add (fF_bdd x 0) (fF_bdd y 0))

Goal state after:
case refine_3
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist ((f n) x) ((f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n ↦ (f n) x
F : α → β
hF : ∀ (x : α), Tendsto (fun n ↦ (f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N) x) (F x) ≤ b N
⊢ Tendsto f atTop (𝓝 { toFun := F, continuous_toFun := ⋯, map_bounded' := ⋯ })
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 : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) = eLpNorm f (ENNReal.ofReal p) μ

Tactic:
eLpNorm_eq_lintegral_rpow_enorm_toReal

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 : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) =
    (∫⁻ (x : α), ‖f x‖ₑ ^ (ENNReal.ofReal p).toReal ∂μ) ^ (1 / (ENNReal.ofReal p).toReal)

case hp_ne_zero
α : 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 ∂μ
⊢ ENNReal.ofReal p ≠ 0

case hp_ne_top
α : 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 ∂μ
⊢ ENNReal.ofReal p ≠ ∞
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})
⊢ (fun n ↦ setToFun μ' T' hT' ⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ n)) = fun n ↦
    setToFun μ T hT ⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ n)

Tactic:
ext i : 1

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 : ℕ
⊢ setToFun μ' T' hT' ⇑(SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯ i) =
    setToFun μ T hT ⇑(SimpleFunc.approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ i)