mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥0∞
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
obtain rfl | hp := hp.eq_or_lt
  · simp
  have hp₀ : 0 < p := by positivity
  have hp₁ : p⁻¹ < 1 := inv_lt_one_of_one_lt₀ hp
  by_cases! H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = 0 ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = 0
  · replace H : (∀ i ∈ s, w i = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0 := by
      simpa [hp₀, hp₁, hp₀.not_gt, hp₁.not_gt, sum_eq_zero_iff_of_nonneg] using H
    have (i) (hi : i ∈ s) : w i * f i = 0 := by rcases H with H | H <;> simp [H i hi]
    simp [sum_eq_zero this]
  by_cases H' : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = ⊤ ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ⊤
  · rcases H' with H' | H' <;> simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]
  replace H' : (∀ i ∈ s, w i ≠ ⊤) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ⊤ := by
    simpa [rpow_eq_top_iff, hp₀, hp₁, hp₀.not_gt, hp₁.not_gt, sum_eq_top, not_or] using H'
  have := coe_le_coe.2 <| NNReal.inner_le_weight_mul_Lp s hp.le (fun i ↦ ENNReal.toNNReal (w i))
    fun i ↦ ENNReal.toNNReal (f i)
  rw [coe_mul] at this
  simp_rw [coe_rpow_of_nonneg _ <| inv_nonneg.2 hp₀.le, ofNNReal_finsetSum, ← ENNReal.toNNReal_rpow,
    ← ENNReal.toNNReal_mul, sum_congr rfl fun i hi ↦ coe_toNNReal (H'.2 i hi)] at this
  simp only [toNNReal_mul, coe_mul, sub_nonneg, hp₁.le, coe_rpow_of_nonneg, ofNNReal_finsetSum]
    at this
  convert! this using 2 with i hi
  · obtain hw | hw := eq_or_ne (w i) 0
    · simp [hw]
    rw [coe_toNNReal (H'.1 _ hi), coe_toNNReal]
    simpa [mul_eq_top, hw, hp₀, hp₀.not_gt, H'.1 _ hi] using H'.2 _ hi
  · convert! rfl with i hi
    exact coe_toNNReal (H'.1 _ hi)

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
ω : α
hg1 : Tendsto (fun i ↦ f (ns i) ω) atTop (𝓝 (g ω))
⊢ Tendsto (fun i ↦ (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω)) → g ω = h ω

Tactic:
hh1

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
ω : α
hg1 : Tendsto (fun i ↦ f (ns i) ω) atTop (𝓝 (g ω))
hh1 : Tendsto (fun i ↦ (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω))
⊢ g ω = h ω
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
⊢ Subsingleton E ∨ 0 < ‖↑e.symm‖

Tactic:
rcases subsingleton_or_nontrivial E with (_i | _i)
  · left
    infer_instance
  · right
    exact e.norm_symm_pos

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
ι : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
⊢ (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)

Tactic:
bddAbove_iff_exists_ge (0 : ℝ),

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
ι : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
⊢ (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ ∃ x, 0 ≤ x ∧ ∀ y ∈ Set.range fun x ↦ ‖f x‖, y ≤ x
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
f T : M →L[R] M
hT : IsUnit T
hf : IsIdempotentElem f
⊢ Commute f T ↔ Submodule.map (↑T) (↑f).range = (↑f).range ∧ Submodule.map (↑T) (↑f).ker = (↑f).ker

Tactic:
have := hT.map ContinuousLinearMap.toLinearMapRingHom
  lift T to (M →L[R] M)ˣ using hT
  simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← toLinearMap_comp] using!
    LinearMap.IsIdempotentElem.commute_iff_of_isUnit this hf.toLinearMap

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ ⇑Φ = kerLift (g ∘ f)
⊢ IsEmbedding (g ∘ kerLift f) ↔ IsEmbedding (g ∘ kerLift f ∘ ⇑Φ)

Tactic:
exact ⟨fun H ↦ H.comp Φ.isEmbedding,
    fun H ↦ by simpa [comp_assoc] using H.comp Φ.symm.isEmbedding⟩

Goal state after:
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
⊢ IsTopCompl ⊥ ⊤

Tactic:
by
  have : IsIdempotentElem (0 : M →L[R] M) := .zero
  simpa using this.isTopCompl

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : IsFiniteMeasure μ
f : α → ε
p : ℝ≥0∞
hf : MemLp f p μ
⊢ Integrable (fun x ↦ ‖f x‖ₑ ^ p.toReal) μ

Tactic:
by_cases h_zero : p = 0
  · simp [h_zero]
  by_cases h_top : p = ∞
  · simp [h_top]
  exact hf.integrable_enorm_rpow h_zero h_top

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

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
p : ℕ
hf : MemLp f (↑p) μ
hp : p ≠ 0
⊢ Integrable (fun x ↦ ‖f x‖ₑ ^ p) μ

Tactic:
by
  simpa using hf.integrable_enorm_rpow (mod_cast hp) (by simp)

Goal state after:
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
⊢ Function.Injective ⇑(l.ker.liftQ l ⋯)

Tactic:
rw [← LinearMap.ker_eq_bot]

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : ¬finrank 𝕜 ↥l.range = 0
this : finrank 𝕜 ↥l.range = 1
⊢ (l.ker.liftQ l ⋯).ker = ⊥
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hu : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x = f x • ↑↑v x
huv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(u + v) x) ⋯) x = f x • ↑↑(u + v) x
h' :
  ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x =
    (↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) + ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯)) x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x ≠ 0
⊢ f x • ↑↑(u + v) x = f x • ↑↑u x + f x • ↑↑v x

Tactic:
h'' _,

Goal state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hu : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x = f x • ↑↑v x
huv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(u + v) x) ⋯) x = f x • ↑↑(u + v) x
h' :
  ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x =
    (↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) + ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯)) x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x ≠ 0
⊢ f x • (↑↑u + ↑↑v) x = f x • ↑↑u x + f x • ↑↑v x

α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u v : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hu : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x = f x • ↑↑v x
huv : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(u + v) x) ⋯) x = f x • ↑↑(u + v) x
h' :
  ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯ + MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯) x =
    (↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) + ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑v x) ⋯)) x
h'' : ↑(f x) ≠ 0 → ↑↑(u + v) x = (↑↑u + ↑↑v) x
hx : f x ≠ 0
⊢ ↑(f x) ≠ 0
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : UniformSpace E
inst✝⁴ : T2Space E
inst✝³ : IsUniformAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 := ContinuousLinearEquiv.ofFinrankEq ⋯
this : IsUniformEmbedding ⇑(↑e).toEquiv.symm
⊢ CompleteSpace E

Tactic:
exact (completeSpace_congr this).1 inferInstance

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case refine_2.inr
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E 𝕜
z : G
hz : 0 < ‖z‖₊
m : (i : ι) → E i
⊢ ‖f m‖₊ * ‖z‖₊ ≤ ‖(f.smulRight z) m‖₊

Tactic:
smulRight_apply,

Goal state after:
case refine_2.inr
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E 𝕜
z : G
hz : 0 < ‖z‖₊
m : (i : ι) → E i
⊢ ‖f m‖₊ * ‖z‖₊ ≤ ‖f m • z‖₊
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case neg
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∉ L.support
⊢ StronglyMeasurable 1

Tactic:
· exact stronglyMeasurable_one

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E₁ : ι → Type wE₁
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E₁ G
k : ℕ
x : (i : ι) → E₁ i
⊢ ‖f.iteratedFDeriv k x‖ ≤ ↑((Fintype.card ι).descFactorial k) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)

Tactic:
calc ‖f.iteratedFDeriv k x‖
  _ ≤ ∑ e : Fin k ↪ ι, ‖iteratedFDerivComponent f e.toEquivRange (fun i ↦ x i)‖ := norm_sum_le _ _
  _ ≤ ∑ _ : Fin k ↪ ι, ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
    gcongr with e _
    simpa using norm_iteratedFDerivComponent_le f e.toEquivRange x
  _ = Nat.descFactorial (Fintype.card ι) k * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k) := by
    simp [card_univ, mul_assoc]

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

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
⊢ MemLp f ∞ (μ.restrict s)

Tactic:
borelize E
  have hbelow : BddBelow (f '' s) := ⟨f a, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono ha.1 hy (ha.2 hy)⟩
  have habove : BddAbove (f '' s) := ⟨f b, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono hy hb.1 (hb.2 hy)⟩
  have : IsBounded (f '' s) := Metric.isBounded_of_bddAbove_of_bddBelow habove hbelow
  rcases isBounded_iff_forall_norm_le.mp this with ⟨C, hC⟩
  have A : MemLp (fun _ => C) ⊤ (μ.restrict s) := memLp_top_const _
  apply MemLp.mono A (aemeasurable_restrict_of_monotoneOn h's hmono).aestronglyMeasurable
  apply (ae_restrict_iff' h's).mpr
  apply ae_of_all _ fun y hy ↦ ?_
  exact (hC _ (mem_image_of_mem f hy)).trans (le_abs_self _)

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

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
f : α →ₛ F
hf : 0 ≤ᵐ[μ] ⇑f
y : α
hy : ¬0 ≤ f y
⊢ 0 ≤ μ.real (⇑f ⁻¹' {f y}) • f y

Tactic:
suffices μ (f ⁻¹' {f y}) = 0 by simp [this, measureReal_def]

Goal state after:
case neg
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
f : α →ₛ F
hf : 0 ≤ᵐ[μ] ⇑f
y : α
hy : ¬0 ≤ f y
⊢ μ (⇑f ⁻¹' {f y}) = 0
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_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2 =
    setToSimpleFunc T (map Prod.fst (f.pair g)) + setToSimpleFunc T (map Prod.snd (f.pair g))

Tactic:
by
      rw [map_setToSimpleFunc T h_add hp_pair Prod.snd_zero,
        map_setToSimpleFunc T h_add hp_pair Prod.fst_zero]

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[ν] g a
a✝¹ : α
ha : f a✝¹ =ᵐ[ν] g a✝¹
a✝ : β
⊢ f a✝¹ a✝ = g a✝¹ a✝ → f a✝¹ a✝ = g a✝¹ a✝

Tactic:
hb

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[ν] g a
a✝¹ : α
ha : f a✝¹ =ᵐ[ν] g a✝¹
a✝ : β
hb : f a✝¹ a✝ = g a✝¹ a✝
⊢ f a✝¹ a✝ = g a✝¹ a✝
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ 0 ∉ {x}

pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.ite Set.univ ∅ = s

Tactic:
· rw [Set.mem_singleton_iff]; exact Ne.symm hx0

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.ite Set.univ ∅ = s
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ ∀ (x : α), 0 ≤ f x → ENNReal.ofReal (-f x) = 0

Tactic:
intro a h

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : Integrable f μ
a : α
h : 0 ≤ f a
⊢ ENNReal.ofReal (-f a) = 0
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✝ : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
⊢ b ∈ s → a ≤ b → (fun b ↦ ∫ (x : α), f x b ∂μ) a ≤ (fun b ↦ ∫ (x : α), f x b ∂μ) b

Tactic:
hb

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✝ : Preorder β
f : α → β → E
s : Set β
hf_mono : ∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
⊢ a ≤ b → (fun b ↦ ∫ (x : α), f x b ∂μ) a ≤ (fun b ↦ ∫ (x : α), f x b ∂μ) b
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✝ : Preorder β
f : α → β → E
s : Set β
hf_anti : ∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
⊢ b ∈ s → a ≤ b → (fun b ↦ ∫ (x : α), f x b ∂μ) b ≤ (fun b ↦ ∫ (x : α), f x b ∂μ) a

Tactic:
hb

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✝ : Preorder β
f : α → β → E
s : Set β
hf_anti : ∀ᵐ (x : α) ∂μ, AntitoneOn (f x) s
hf_int : ∀ a ∈ s, Integrable (fun x ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
⊢ a ≤ b → (fun b ↦ ∫ (x : α), f x b ∂μ) b ≤ (fun b ↦ ∫ (x : α), f x b ∂μ) a
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 : β
⊢ b ∈ s →
    ∀ ⦃a_2 b_1 : ℝ⦄,
      0 ≤ a_2 →
        0 ≤ b_1 →
          a_2 + b_1 = 1 →
            (fun b ↦ ∫ (x : α), f x b ∂μ) (a_2 • a + b_1 • b) ≤
              a_2 • (fun b ↦ ∫ (x : α), f x b ∂μ) a + b_1 • (fun b ↦ ∫ (x : α), f x b ∂μ) b

Tactic:
hb

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
⊢ ∀ ⦃a_1 b_1 : ℝ⦄,
    0 ≤ a_1 →
      0 ≤ b_1 →
        a_1 + b_1 = 1 →
          (fun b ↦ ∫ (x : α), f x b ∂μ) (a_1 • a + b_1 • b) ≤
            a_1 • (fun b ↦ ∫ (x : α), f x b ∂μ) a + b_1 • (fun b ↦ ∫ (x : α), f x b ∂μ) b
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : AddCommGroup W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup V
inst✝ : IsTopologicalAddGroup W
f : V →ᴬ[R] W
⊢ ⇑f = ⇑f.contLinear + Function.const V (f 0)

Tactic:
rcases f with ⟨f, h⟩
  rw [ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousAffineMap.coe_mk, f.decomp,
    Pi.add_apply, LinearMap.map_zero, zero_add, ← Function.const_def]

Goal state after: