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

Goal state before:
pp: α : 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

Tactic:
simpa only [Ne, ENNReal.coe_eq_zero] using hx

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 : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
⊢ ‖f m₁ - f m₂‖ ≤ C * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖

Tactic:
classical
  have A :
    ∀ i : ι,
      ∏ j, (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
        ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by
    intro i
    calc
      ∏ j, (if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
          ∏ j : ι, Function.update (fun _ => max ‖m₁‖ ‖m₂‖) i ‖m₁ - m₂‖ j := by
        gcongr with j
        rcases eq_or_ne j i with rfl | h
        · simp only [ite_true, Function.update_self]
          exact norm_le_pi_norm (m₁ - m₂) _
        · simp [h, -le_sup_iff, -sup_le_iff, sup_le_sup, norm_le_pi_norm]
      _ = ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by
        rw [prod_update_of_mem (Finset.mem_univ _)]
        simp [card_univ_sdiff]
  calc
    ‖f m₁ - f m₂‖ ≤ C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
      f.norm_image_sub_le_of_bound' hC H m₁ m₂
    _ ≤ C * ∑ _i, ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) := by gcongr; apply A
    _ = C * Fintype.card ι * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖ := by
      rw [sum_const, card_univ, nsmul_eq_mul]
      ring

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

Goal state before:
pp: α : 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
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) x = f x • ↑↑(r • u) x
h'' : ↑↑(r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = (r • ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯)) x
h''' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
hx : f x ≠ 0
⊢ ↑(f x) ≠ 0

Tactic:
simpa only [Ne, ENNReal.coe_eq_zero] using hx

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

Goal state before:
pp: case neg
α : 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 (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
rw [Icc_eq_empty hab, Ico_eq_empty]

Goal state after:
case neg
α : 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
⊢ ¬a < b
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case inl
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
h✝ : IsEmpty ι
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = 1

Tactic:
simp [norm_mkPiAlgebra_of_empty]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case pos
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)
⊢ StronglyMeasurable (∏ i ∈ Finite.toFinset h✝, L.support.mulIndicator (fun i ↦ f i) i.down)

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✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ StronglyMeasurable (Exists.choose hm)

Tactic:
· refine Finset.stronglyMeasurable_prod _ (fun _ _ ↦ ?_)
    rw [Set.mulIndicator]
    split_ifs
    · fun_prop
    · exact stronglyMeasurable_one

Goal state after:
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✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ StronglyMeasurable (Exists.choose hm)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : 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'
inst✝ : DecidableEq ι
m : (i : ι) → E i
i : ι
x y : E i
⊢ { toFun := fun x_1 ↦ (f x_1) (update m i (x + y)), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous
      (‖f‖ * ∏ i_1, ‖update m i (x + y) i_1‖) ⋯ =
    { toFun := fun x_1 ↦ (f x_1) (update m i x), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous
        (‖f‖ * ∏ i_1, ‖update m i x i_1‖) ⋯ +
      { toFun := fun x ↦ (f x) (update m i y), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous
        (‖f‖ * ∏ i_1, ‖update m i y i_1‖) ⋯

Tactic:
ext1
        simp only [add_apply, ContinuousMultilinearMap.map_update_add, LinearMap.coe_mk,
          LinearMap.mkContinuous_apply, AddHom.coe_mk]

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

Goal state before:
pp: case refine_2
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ ⦃s t : Set X⦄,
    s ⊆ t → (∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen[inst✝³] u ∧ s ⊆ u ∧ IntegrableOn f u μ

pp: case refine_3
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ ⦃s t : Set X⦄,
    (∃ u, IsOpen[inst✝³] u ∧ s ⊆ u ∧ IntegrableOn f u μ) →
      (∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen[inst✝³] u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

pp: case refine_4
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ

Tactic:
· rintro s t hst ⟨u, u_open, tu, hu⟩
    exact ⟨u, u_open, hst.trans tu, hu⟩

Goal state after:
case refine_3
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ ⦃s t : Set X⦄,
    (∃ u, IsOpen[inst✝³] u ∧ s ⊆ u ∧ IntegrableOn f u μ) →
      (∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ) → ∃ u, IsOpen[inst✝³] u ∧ s ∪ t ⊆ u ∧ IntegrableOn f u μ

case refine_4
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
hf : LocallyIntegrable f μ
k : Set X
hk : IsCompact k
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ u, IsOpen[inst✝³] u ∧ t ⊆ u ∧ IntegrableOn f u μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
G : Type wG
inst✝⁵ : Fintype ι
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Subsingleton ι
inst✝ : Nontrivial G
i : ι
⊢ ‖(ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖ = 1

Tactic:
by
  simp [ContinuousLinearMap.norm_id]

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

Goal state before:
pp: case refine_2.h_disj
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h : (∀ i ∈ s, μ (S i) ≠ ∞) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, μ (S i) ≠ ∞
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
⊢ ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h : (∀ i ∈ s, μ (S i) ≠ ∞) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, μ (S i) ≠ ∞
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)

Tactic:
· exact fun i hi j hj hij =>
      h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
a : ι
s : Finset ι
has : a ∉ s
h : (∀ i ∈ s, μ (S i) ≠ ∞) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)
hps : ∀ i ∈ insert a s, μ (S i) ≠ ∞
h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
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 : 𝕜
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ ‖c‖ * ‖T s‖ ≤ ‖c‖ * (C * μ.real s)

Tactic:
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: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
x : Eₗ
⊢ ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖

Tactic:
have h_mem : ∀ (x : Eₗ) (hy : x ∈ (LinearMap.range e)), ‖extendOfNorm f e x‖ ≤ C * ‖x‖ := by
    intro x ⟨y, hxy⟩
    simpa only [← hxy, extendOfNorm_eq h_dense ⟨C, h_norm⟩ y] using h_norm y

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
x : Eₗ
h_mem : ∀ x ∈ e.range, ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖
⊢ ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖
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_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
h : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
z : α
⊢ z ∈ ⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y} → z ∈ {a | ¬f a = g a}

Tactic:
Set.mem_inter_iff,

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
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
h : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
z : α
⊢ z ∈ ⇑f ⁻¹' {x} ∧ z ∈ ⇑g ⁻¹' {y} → z ∈ {a | ¬f a = g a}
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)) μ
⊢ setToSimpleFunc T (f + g) = ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) (x.1 + x.2)

Tactic:
add_eq_map₂,

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ setToSimpleFunc T (map (fun p ↦ p.1 + p.2) (f.pair g)) = ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) (x.1 + x.2)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case pos
α : 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''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α →ₛ E
hf : Integrable (⇑f) μ
i : E
a✝ : i ∈ f.range
h0 : i = 0
⊢ (T (⇑f ⁻¹' {i})) i ≤ (T' (⇑f ⁻¹' {i})) i

Tactic:
simp [h0]

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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁶ : NormedAddCommGroup G''
inst✝⁵ : PartialOrder G''
inst✝⁴ : IsOrderedAddMonoid G''
inst✝³ : NormedSpace ℝ G''
inst✝² : NormedAddCommGroup G'
inst✝¹ : PartialOrder G'
inst✝ : NormedSpace ℝ G'
T : Set α → G' →L[ℝ] G''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable (⇑f) μ
i : G'
hi : i ∈ f.range
h0 : i = 0
⊢ 0 ≤ (T (⇑f ⁻¹' {i})) i

Tactic:
simp [h0]

Goal state after:
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 α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s
f : α →ₛ F
⊢ ∑ x ∈ f.range, C * μ.real (⇑f ⁻¹' {x}) * ‖x‖ ≤ ∑ i ∈ f.range, C * (μ.real (⇑f ⁻¹' {i}) * ‖i‖)

Tactic:
← mul_assoc

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 α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s
f : α →ₛ F
⊢ ∑ x ∈ f.range, C * μ.real (⇑f ⁻¹' {x}) * ‖x‖ ≤ ∑ x ∈ f.range, C * μ.real (⇑f ⁻¹' {x}) * ‖x‖
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, C * μ.real (⇑f ⁻¹' {x}) * ‖x‖ ≤ ∑ i ∈ f.range, C * (μ.real (⇑f ⁻¹' {i}) * ‖i‖)

Tactic:
← mul_assoc

Goal state after:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, C * μ.real (⇑f ⁻¹' {x}) * ‖x‖ ≤ ∑ x ∈ f.range, C * μ.real (⇑f ⁻¹' {x}) * ‖x‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := ⋯
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = max (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(f a✝).toNNReal = ↑‖max (f a✝) 0‖₊

Tactic:
rw [Real.nnnorm_of_nonneg (le_max_right _ _)]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = max (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(f a✝).toNNReal = ↑(NNReal.mk (max (f a✝) 0) ⋯)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case succ
α : Type u_1
β : Type u_3
inst✝ : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
n✝ : ℕ
ih : t ^ n✝ ~[l] u ^ n✝
⊢ t ^ (n✝ + 1) ~[l] u ^ (n✝ + 1)

Tactic:
| succ _ ih =>

Goal state after:
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v : V
x : P
⊢ dist (v +ᵥ x) x = ‖v‖

Tactic:
dist_vadd_left

Goal state after:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v : V
x : P
⊢ ‖v‖ = ‖v‖
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfi : Integrable f μ
⊢ 0 < ∫ (x : α), f x ∂μ ↔ 0 < μ (Function.support f)

Tactic:
by
  simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
    integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
    Function.support]

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

Goal state before:
pp: case 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) ∂μ)
⊢ Tendsto (fun n ↦ (∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ).toReal) atTop
    (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ).toReal)

Tactic:
refine h_cont.tendsto.comp ?_

Goal state after:
case 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) ∂μ)
⊢ Tendsto (fun n ↦ ∫⁻ (a : α), ENNReal.ofReal (f' n a) ∂μ) atTop (𝓝 (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ))