mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case refine_1
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ ‖(flipMultilinearEquivₗ 𝕜 E G G') f‖ ≤ 1 * ‖f‖

Tactic:
suffices ‖f.flipMultilinear‖ ≤ ‖f‖ by simpa

Goal state after:
case refine_1
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ ‖f.flipMultilinear‖ ≤ ‖f‖
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T T' : Set α → β
inst✝ : AddCommMonoid β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
⊢ FinMeasAdditive μ (T + T')

Tactic:
intro s t hs ht hμs hμt hst

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T T' : Set α → β
inst✝ : AddCommMonoid β
hT : FinMeasAdditive μ T
hT' : FinMeasAdditive μ T'
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
⊢ (T + T') (s ∪ t) = (T + T') s + (T + T') t
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst✝ : AddGroup β
hT : FinMeasAdditive μ T
⊢ FinMeasAdditive μ (-T)

Tactic:
intro s t hs ht hμs hμt hst

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
T : Set α → β
inst✝ : AddGroup β
hT : FinMeasAdditive μ T
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
⊢ (-T) (s ∪ t) = (-T) s + (-T) t
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : ¬(x ∈ f.range ∧ x ≠ 0)
⊢ (T (⇑f ⁻¹' {x})) x = 0

Tactic:
not_and_or,

Goal state after:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ ¬x ≠ 0
⊢ (T (⇑f ⁻¹' {x})) x = 0
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : ∀ (hf : MemLp (⇑f) p μ), P (f.toLp hf)
⊢ (∀ (hf : MemLp (⇑g) p μ), P (g.toLp hf)) → ∀ (hf : MemLp (⇑(f + g)) p μ), P ((f + g).toLp hf)

Tactic:
hg

Goal state after:
case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : ∀ (hf : MemLp (⇑f) p μ), P (f.toLp hf)
hg : ∀ (hf : MemLp (⇑g) p μ), P (g.toLp hf)
⊢ ∀ (hf : MemLp (⇑(f + g)) p μ), P ((f + g).toLp hf)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
𝕜 : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : SMul 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
c : 𝕜
s : Set α
x : F
⊢ (weightedSMul μ s) (c • x) = c • (weightedSMul μ s) x

Tactic:
by
  simp_rw [weightedSMul_apply, smul_comm]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : ¬(x ∈ f.range ∧ x ≠ 0)
⊢ μ.real (⇑f ⁻¹' {x}) • x = 0

Tactic:
not_and_or,

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : DecidablePred fun x ↦ x ≠ 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx : x ∉ f.range ∨ ¬x ≠ 0
⊢ μ.real (⇑f ⁻¹' {x}) • x = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
y : F
⊢ ∑ z ∈ {y}, μ.real (⇑(const α y) ⁻¹' {z}) • z = μ.real Set.univ • y

Tactic:
by simp [Set.preimage]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
⊢ integral (μ + ν) f = integral μ f + integral ν f

Tactic:
by
  simp_rw [integral_def]
  refine setToSimpleFunc_add_left'
    (weightedSMul μ) (weightedSMul ν) (weightedSMul (μ + ν)) (fun s _ hμνs => ?_) hf
  rw [lt_top_iff_ne_top, Measure.coe_add, Pi.add_apply, ENNReal.add_ne_top] at hμνs
  rw [weightedSMul_add_measure _ _ hμνs.1 hμνs.2]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : (toSimpleFunc f).negPart a✝ = (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
⊢ (toSimpleFunc f) a✝ = (toSimpleFunc f).posPart a✝ - (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝

Tactic:
← h₂

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
a✝ : α
h₁ : (toSimpleFunc f).posPart a✝ = (SimpleFunc.map norm (toSimpleFunc (posPart f))) a✝
h₂ : (toSimpleFunc f).negPart a✝ = (SimpleFunc.map norm (toSimpleFunc (negPart f))) a✝
⊢ (toSimpleFunc f) a✝ = (toSimpleFunc f).posPart a✝ - (toSimpleFunc f).negPart a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : MemLp (⇑f) p μ → motive ⇑f
⊢ (MemLp (⇑g) p μ → motive ⇑g) → MemLp (⇑(f + g)) p μ → motive ⇑(f + g)

Tactic:
hg

Goal state after:
case add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
_i : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
motive : (α → E) → Prop
indicator : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → motive (s.indicator fun x ↦ c)
add :
  ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f p μ → MemLp g p μ → motive f → motive g → motive (f + g)
closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {f | motive ↑↑f}
ae : ∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MemLp f p μ → motive f → motive g
f g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : MemLp (⇑f) p μ → motive ⇑f
hg : MemLp (⇑g) p μ → motive ⇑g
⊢ MemLp (⇑(f + g)) p μ → motive ⇑(f + g)
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: case refine_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
h₂ : ‖(↑‖x₀‖)⁻¹ • (x₀ - ↑‖x₀‖ • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - ↑‖x₀‖ • y‖
h₁ : r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - (↑‖x₀‖)⁻¹ • ↑‖x₀‖ • y‖
⊢ r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - y‖

Tactic:
inv_smul_smul₀

Goal state after:
case refine_2
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
h₂ : ‖(↑‖x₀‖)⁻¹ • (x₀ - ↑‖x₀‖ • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - ↑‖x₀‖ • y‖
h₁ : r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - y‖
⊢ r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - y‖

case refine_2.ha
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
hx₀' : x₀ ≠ 0
y : E
hy : y ∈ F
h₂ : ‖(↑‖x₀‖)⁻¹ • (x₀ - ↑‖x₀‖ • y)‖ = ‖x₀‖⁻¹ * ‖x₀ - ↑‖x₀‖ • y‖
h₁ : r ≤ ‖(↑‖x₀‖)⁻¹ • x₀ - (↑‖x₀‖)⁻¹ • ↑‖x₀‖ • y‖
⊢ ↑‖x₀‖ ≠ 0
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
⊢ dist ((pointReflection 𝕜 x) y) y = ‖2‖ * dist x y

Tactic:
dist_pointReflection_self',

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
⊢ ‖2 • (x -ᵥ y)‖ = ‖2‖ * dist x y
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂Measure.sum μ < ∞

Tactic:
lintegral_sum_measure

Goal state after:
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
⊢ ∑' (i : ι), ∫⁻ (a : X), ‖f a‖ₑ ∂μ i < ∞
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 : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ setToFun μ T hT 0 = 0

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  rw [setToFun_eq hT (integrable_zero _ _ _), Integrable.toL1_zero, map_zero]

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

Goal state before:
pp: case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
i₀ : ι
⊢ IsOpen[Pi.topologicalSpace] {p | AffineIndependent 𝕜 p}

Tactic:
· simp_rw [affineIndependent_iff_linearIndependent_vsub 𝕜 _ i₀]
    let ι' := { x // x ≠ i₀ }
    cases nonempty_fintype ι
    have : Fintype ι' := Subtype.fintype _
    convert_to!
      IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})
    exact isOpen_setOfPred_linearIndependent.preimage (by fun_prop)

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

Goal state before:
pp: case refine_1
α : 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) * (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q) ≠ ∞

Tactic:
refine ENNReal.mul_ne_top ?_ ?_
    · convert! hf.eLpNorm_ne_top
      rw [eLpNorm_eq_lintegral_rpow_enorm_toReal]
      · rw [ENNReal.toReal_ofReal hpq.nonneg]
      · rw [Ne, ENNReal.ofReal_eq_zero, not_le]
        exact hpq.pos
      · finiteness
    · convert! hg.eLpNorm_ne_top
      rw [eLpNorm_eq_lintegral_rpow_enorm_toReal]
      · rw [ENNReal.toReal_ofReal hpq.symm.nonneg]
      · rw [Ne, ENNReal.ofReal_eq_zero, not_le]
        exact hpq.symm.pos
      · finiteness

Goal state after:
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) μ
⊢ ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ

Tactic:
refine integral_congr_ae ?_

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) μ
⊢ (fun a ↦ f a * g a) =ᵐ[μ] fun a ↦ ‖f a‖ * ‖g a‖
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‖ ∂μ
⊢ ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ

Tactic:
refine integral_congr_ae ?_

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‖ ∂μ
⊢ (fun a ↦ f a ^ p) =ᵐ[μ] fun a ↦ ‖f a‖ ^ p
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: α : Type u_1
N : ℕ
g : α → Fin N → ℝ
⊢ Summable g → Summable fun x ↦ ‖g x‖

Tactic:
hg

Goal state after:
α : Type u_1
N : ℕ
g : α → Fin N → ℝ
hg : Summable g
⊢ Summable fun x ↦ ‖g x‖
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 ∂μ
⊢ ∫ (a : α), g a ^ q ∂μ = ∫ (a : α), ‖g a‖ ^ q ∂μ

Tactic:
refine integral_congr_ae ?_

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 ∂μ
⊢ (fun a ↦ g a ^ q) =ᵐ[μ] fun a ↦ ‖g a‖ ^ q
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LocallyCompactSpace X
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable fun i ↦ ‖restrict (↑K) (F i)‖
⊢ Summable F

Tactic:
by
  refine (ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => ?_
  lift K to Compacts X using hK
  have A : ∀ s : Finset ι, restrict K (∑ i ∈ s, F i) = ∑ i ∈ s, restrict K (F i) := by
    intro s
    ext1 x
    -- TODO: there is a non-confluence problem in the lemmas here,
    -- and `SetLike.coe_sort_coe` prevents `restrict_apply` from being used.
    simp [-SetLike.coe_sort_coe]
  simpa only [HasSum, A] using! (hF K).of_norm

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
⊢ thickenedIndicatorAux δ E x ≤ 1

Tactic:
by
  apply tsub_le_self (α := ℝ≥0∞)

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x

Tactic:
simp only [thickenedIndicatorAux]
  rcases le_total (infEDist x E / ENNReal.ofReal δ) 1 with hle | hle
  · rw [ENNReal.sub_le_sub_iff_left hle (by simp)]
    gcongr
  · rw [tsub_eq_zero_of_le hle, tsub_eq_zero_of_le]
    exact hle.trans (by gcongr)

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 T' : Set α → E →L[ℝ] F
C C' : ℝ
f : α → E
ν : Measure α
hTμ : DominatedFinMeasAdditive μ T C
hTν : DominatedFinMeasAdditive ν T' C'
hμ : Integrable f μ
hν : Integrable f ν
hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0)
hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0)
⊢ setToFun μ T hTμ f + setToFun (μ + ν) T' hTν_add f = setToFun μ T hTμ f + setToFun ν T' hTν f

Tactic:
setToFun_congr_measure_of_add_left hTν_add hTν f (hμ.add_measure 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
f : α → E
ν : Measure α
hTμ : DominatedFinMeasAdditive μ T C
hTν : DominatedFinMeasAdditive ν T' C'
hμ : Integrable f μ
hν : Integrable f ν
hTμ_add : DominatedFinMeasAdditive (μ + ν) T (max C 0)
hTν_add : DominatedFinMeasAdditive (μ + ν) T' (max C' 0)
⊢ setToFun μ T hTμ f + setToFun ν T' hTν f = setToFun μ T hTμ f + setToFun ν T' hTν f
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
by_cases x_mem_closure : x ∈ closure E
  · filter_upwards [univ_mem] with δ _
    have obs : x ∈ cthickening δ E := closure_subset_cthickening δ E x_mem_closure
    rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]
  · filter_upwards [eventually_notMem_cthickening_of_infEDist_pos x_mem_closure] with δ hδ
    simp only [hδ, not_false_eq_true, mulIndicator_of_notMem, x_mem_closure]

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 : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hC : 0 ≤ C
⊢ ‖setToFun μ T hT f‖ ≤ C * ‖Integrable.toL1 f hf‖

Tactic:
by_cases hF : CompleteSpace F; swap
  · simp only [setToFun, hF, ↓reduceDIte, norm_zero]
    positivity
  rw [setToFun_eq hT hf]
  exact L1.norm_setToL1_le_mul_norm hT hC _

Goal state after:
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 ∂μ
⊢ ∀ i ∈ {x ∈ t.powerset | x.Nonempty}, Integrable ((⋂ i_1 ∈ i, s i_1).indicator fun a ↦ (-1) ^ (#i + 1) • f a) μ

Tactic:
intro 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}
⊢ Integrable ((⋂ i ∈ u, s i).indicator fun a ↦ (-1) ^ (#u + 1) • f a) μ
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ∑ x ∈ s.erase i, ofReal (↑f (d x) - ↑f (c x))

Tactic:
← IH _ (Finset.erase_ssubset is) (c i),

Goal state after:
case inr
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ofReal (↑f (c i) - ↑f a)

case a
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ Icc a (c i) ⊆ ⋃ i_1 ∈ ↑(s.erase i), Iotop (c i_1) (d i_1)