mathlib-initiative/mathlib-tactics huggingface dataset:
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
hi : Function.Injective ⇑(l.ker.liftQ l ⋯)
⊢ l.range = ⊤

Tactic:
exact Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝ : NormedDivisionRing 𝕜
f : α → 𝕜
h : Integrable f μ
c : 𝕜
⊢ Integrable (fun x ↦ f x / c) μ

Tactic:
div_eq_mul_inv,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝ : NormedDivisionRing 𝕜
f : α → 𝕜
h : Integrable f μ
c : 𝕜
⊢ Integrable (fun x ↦ f x * c⁻¹) μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: case pos
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntegrableOn f (Ico a b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
eq_true (integrableOn_singleton hb'),

Goal state after:
case pos
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntegrableOn f (Ico a b) μ ∧ True ↔ IntegrableOn f (Ico a b) μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: case pos
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
hab : a < b
⊢ IntegrableOn f (Ioo a b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
eq_true (integrableOn_singleton hb'),

Goal state after:
case pos
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
hab : a < b
⊢ IntegrableOn f (Ioo a b) μ ∧ True ↔ IntegrableOn f (Ioo a b) μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
⊢ IntegrableOn f (Ioi b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Ioi b) μ

Tactic:
eq_true (integrableOn_singleton hb'),

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
⊢ IntegrableOn f (Ioi b) μ ∧ True ↔ IntegrableOn f (Ioi b) μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
⊢ IntegrableOn f (Iio b) μ ∧ IntegrableOn f {b} μ ↔ IntegrableOn f (Iio b) μ

Tactic:
eq_true (integrableOn_singleton hb'),

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
⊢ IntegrableOn f (Iio b) μ ∧ True ↔ IntegrableOn f (Iio b) μ
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‖₊ ≤ ‖f.smulRight z‖₊ / ‖z‖₊ * ∏ i, ‖m i‖₊

Tactic:
rw [div_mul_eq_mul_div, le_div_iff₀ hz]

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.smulRight z‖₊ * ∏ i, ‖m i‖₊
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 μ
⊢ ∃ u, (∀ (n : ℕ), IsOpen[inst✝³] (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), IntegrableOn f (u n ∩ s) μ

Tactic:
rcases hf.exists_countable_integrableOn with ⟨T, T_count, T_open, sT, hT⟩
  let T' : Set (Set X) := insert ∅ T
  have T'_count : T'.Countable := Countable.insert ∅ T_count
  have T'_ne : T'.Nonempty := by simp only [T', insert_nonempty]
  rcases T'_count.exists_eq_range T'_ne with ⟨u, hu⟩
  refine ⟨u, ?_, ?_, ?_⟩
  · intro n
    have : u n ∈ T' := by rw [hu]; exact mem_range_self n
    rcases mem_insert_iff.1 this with h | h
    · rw [h]
      exact isOpen_empty
    · exact T_open _ h
  · intro x hx
    obtain ⟨v, hv, h'v⟩ : ∃ v, v ∈ T ∧ x ∈ v := by simpa only [mem_iUnion, exists_prop] using sT hx
    have : v ∈ range u := by rw [← hu]; exact subset_insert ∅ T hv
    obtain ⟨n, rfl⟩ : ∃ n, u n = v := by simpa only [mem_range] using this
    exact mem_iUnion_of_mem _ h'v
  · intro n
    have : u n ∈ T' := by rw [hu]; exact mem_range_self n
    rcases mem_insert_iff.1 this with h | h
    · simp only [h, empty_inter, integrableOn_empty]
    · exact hT _ h

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝³ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst✝² : SeminormedAddGroup 𝕜
inst✝¹ : DistribSMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
⊢ DominatedFinMeasAdditive μ (fun s ↦ c • T s) (‖c‖ * C)

Tactic:
refine ⟨hT.1.smul c, fun s hs hμs => (norm_smul_le _ _).trans ?_⟩
  rw [mul_assoc]
  exact mul_le_mul le_rfl (hT.2 s hs hμs) (norm_nonneg _) (norm_nonneg _)

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
⊢ Continuous fun x ↦ ‖(f.extend e) x‖

pp: case refine_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖(f.extend e) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖

Tactic:
· exact (cont _).norm

Goal state after:
case refine_3
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖(f.extend e) (e x)‖ ≤ ↑N * ‖f‖ * ‖e x‖
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
f : ↥(simpleFunc G p μ)
hf : 0 ≤ f
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑f =ᵐ[μ] ⇑f'

Tactic:
rcases f with ⟨⟨f, hp⟩, g, (rfl : _ = f)⟩

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ ⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩
⊢ ∃ f', 0 ≤ f' ∧ ↑↑↑⟨⟨AEEqFun.mk ⇑g ⋯, hp⟩, ⋯⟩ =ᵐ[μ] ⇑f'
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

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

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
⊢ Tendsto u l (𝓝 c)

Tactic:
rcases em <| c = 0 with rfl | h
  · exact (tendsto_congr' <| isEquivalent_zero_iff_eventually_zero.mp hu).mpr tendsto_const_nhds
  · exact (isEquivalent_const_iff_tendsto h).mp hu

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
| 𝓝 0

Tactic:
rw [← sub_self (1 : β)]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
| 𝓝 (1 - 1)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
this : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
hfi,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ = ∞
this : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ
⊢ 0 = ∞.toReal
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) μ
⊢ ConvexOn ℝ s fun b ↦ ∫ (x : α), f x b ∂μ

Tactic:
by
  refine ⟨hs, ?_⟩
  intro a ha b hb p q hp hq hpq
  calc ∫ x, f x (p • a + q • b) ∂μ ≤ ∫ x, p • f x a + q • f x b ∂μ := by
                  refine integral_mono_ae ?lhs ?rhs ?ae_le
                  case lhs =>
                    refine hf_int _ ?_
                    rw [convex_iff_add_mem] at hs
                    exact hs ha hb hp hq hpq
                  case rhs => fun_prop (disch := aesop)
                  case ae_le =>
                    filter_upwards [hf_conv] with x hx
                    exact hx.2 ha hb hp hq hpq
            _ = ∫ x, p • f x a ∂μ + ∫ x, q • f x b ∂μ := by
                  apply integral_add
                  all_goals fun_prop (disch := aesop)
            _ = p • ∫ x, f x a ∂μ + q • ∫ x, f x b ∂μ := by simp [integral_smul]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f μ
⊢ ¬μ {a | ¬f a = 0} = 0 ↔ ¬μ (Function.support f) = 0

Tactic:
Function.support

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

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ ENNReal.ofReal (f' n x)

pp: case refine_2.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))

Tactic:
· filter_upwards [h_mono] with x hx n m hnm
    refine ENNReal.ofReal_le_ofReal ?_
    simp only [f', tsub_le_iff_right, sub_add_cancel]
    exact hx hnm

Goal state after:
case refine_2.refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal (f' n x)) atTop (𝓝 (ENNReal.ofReal ((F - f 0) x)))
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖f z‖ ≤ c / r * ‖z‖

pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
⊢ ‖f z‖ ≤ c / r * ‖z‖

Tactic:
· rw [z_zero]
    simp only [map_zero, norm_zero, mul_zero]
    exact le_rfl

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
⊢ ‖f z‖ ≤ c / r * ‖z‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case refine_3
α : 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 : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
filter_upwards [h, hf_mono, hf_bound] with a ha ha_mono ha_bound

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
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
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'
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ (T + T') ⋯ f = setToFun μ T hT f + setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_add_left hT hT']

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ
hM : 0 ≤ M
hu : ∀ (i : ι), ‖u (v i)‖ ≤ M
⊢ ‖u‖ ≤ Fintype.card ι • ‖↑v.equivFunL‖ * M

Tactic:
by
  simpa using! NNReal.coe_le_coe.mpr (v.opNNNorm_le ⟨M, hM⟩ hu)

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : SeminormedAddCommGroup β
f g : α →ᵇ β
x : α
C : ℝ
inst✝² : Nonempty α
inst✝¹ : One β
inst✝ : NormOneClass β
⊢ ‖1‖ = 1

Tactic:
simp only [norm_eq_iSup_norm, coe_one, Pi.one_apply, norm_one, ciSup_const]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f‖ₑ = ⨆ x, ‖f x‖ₑ

Tactic:
by
  simpa only [← edist_zero_right] using! edist_eq_iSup

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : CompleteSpace 𝕜
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : Module 𝕜 V
inst✝ : ContinuousSMul 𝕜 V
r : ℝ
rpos : 0 < r
c : V
h : IsCompact (closedBall c r)
⊢ IsCompact (closedBall 0 r)

Tactic:
simpa using h.vadd (-c)

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
x : X
h : ∀ (y : E), ContinuousWithinAt (fun q ↦ (f q) y) s x
e : (E →L[𝕜] F) ≃L[𝕜] Fin (finrank 𝕜 E) → F :=
  ((ContinuousLinearEquiv.ofFinrankEq ⋯).arrowCongr 1).trans (ContinuousLinearEquiv.piRing (Fin (finrank 𝕜 E)))
⊢ ContinuousWithinAt (⇑e.toHomeomorph ∘ f) s x

Tactic:
exact continuousWithinAt_pi.mpr fun i ↦ h _

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) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
⊢ ∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)

Tactic:
have h_right_f : ∫ a, f a ^ p ∂μ = ∫ a, ‖f a‖ ^ p ∂μ := by
    refine integral_congr_ae ?_
    filter_upwards [hf_nonneg] with x hxf
    rw [Real.norm_of_nonneg hxf]

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 ∂μ
⊢ ∫ (a : α), f a * g a ∂μ ≤ (∫ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫ (a : α), g a ^ q ∂μ) ^ (1 / q)