mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
s : Finset ι
⊢ ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
by
    induction s using Finset.induction with
    | empty => simp
    | insert i s his Hrec =>
      have I :
        ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
          C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
        have A : (insert i s).piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₂ i) :=
          s.piecewise_insert _ _ _
        have B : s.piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₁ i) := by
          simp [his]
        rw [B, A, ← f.map_update_sub]
        apply le_trans (H _)
        gcongr with j
        by_cases h : j = i
        · rw [h]
          simp
        · by_cases h' : j ∈ s <;> simp [h', h]
      calc
        ‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
            ‖f m₁ - f (s.piecewise m₂ m₁)‖ +
              ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ := by
          rw [← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm]
          exact dist_triangle _ _ _
        _ ≤ (C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
              C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
          (add_le_add Hrec I)
        _ = C * ∑ i ∈ insert i s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
          simp [his, add_comm, left_distrib]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_9
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : SigmaFinite μ
C : ℝ≥0∞
hC : C < ∞
f : α → ε
hf_meas : AEStronglyMeasurable f μ
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
@trim_eq_self _ m

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_9
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : SigmaFinite μ
C : ℝ≥0∞
hC : C < ∞
f : α → ε
hf_meas : AEStronglyMeasurable f μ
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ∞ → ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ ≤ C
⊢ SigmaFinite μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
ε' : Type u_4
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : X → ε
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → ε'
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ₑ ≤ ‖f x‖ₑ
⊢ LocallyIntegrableOn g s μ

Tactic:
intro x hx
  rcases hf x hx with ⟨t, t_mem, ht⟩
  exact ⟨t, t_mem, ht.mono_enorm hg.restrict (ae_restrict_of_ae h)⟩

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

Goal state before:
pp: case zero
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ max 1 ‖1‖

pp: case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
n✝ : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n✝ + 1) A‖ ≤ max 1 ‖1‖

Tactic:
· exact norm_mkPiAlgebraFin_zero.le.trans (le_max_right _ _)

Goal state after:
case succ
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
n✝ : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n✝ + 1) A‖ ≤ max 1 ‖1‖
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 α
a b : α
inst✝ : NullSingletonClass μ
ha : ‖f a‖ₑ ≠ ∞
hb : ‖f b‖ₑ ≠ ∞
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [integrableOn_Icc_iff_integrableOn_Ioc ha, integrableOn_Ioc_iff_integrableOn_Ioo hb]

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 0
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional 𝕜 ↥M := Finite.span_of_finite 𝕜 hF_finite
h_cover : U ⊆ ↑M + c • U
h_ind : ∀ (n : ℕ), U ⊆ ↑M + c ^ n • U
h_small : Tendsto (fun n ↦ c ^ n • U) atTop (𝓝 0).smallSets
x : Eᵤ
hx : x ∈ U
m : ℕ → Eᵤ
hm : ∀ (n : ℕ), m n ∈ ↑M
u : ℕ → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun x1 x2 ↦ x1 + x2) (m n) (u n) = x
hu_tendsto : Tendsto u atTop (𝓝 0)
⊢ x ∈ ↑M

Tactic:
have hm_tendsto : Tendsto m atTop (𝓝 x) := by
      simpa [show m = fun n ↦ x - u n by grind] using! tendsto_const_nhds.sub hu_tendsto

Goal state after:
𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 0
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional 𝕜 ↥M := Finite.span_of_finite 𝕜 hF_finite
h_cover : U ⊆ ↑M + c • U
h_ind : ∀ (n : ℕ), U ⊆ ↑M + c ^ n • U
h_small : Tendsto (fun n ↦ c ^ n • U) atTop (𝓝 0).smallSets
x : Eᵤ
hx : x ∈ U
m : ℕ → Eᵤ
hm : ∀ (n : ℕ), m n ∈ ↑M
u : ℕ → Eᵤ
hu : ∀ (n : ℕ), u n ∈ c ^ n • U
h_eq : ∀ (n : ℕ), (fun x1 x2 ↦ x1 + x2) (m n) (u n) = x
hu_tendsto : Tendsto u atTop (𝓝 0)
hm_tendsto : Tendsto m atTop (𝓝 x)
⊢ x ∈ ↑M
Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ eLpNorm f 1 μ = ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
apply eLpNorm_one_eq_lintegral_enorm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
⊢ ∀ {x : ↥(Lp E p μ)}, x ∈ {f | ∃ s, AEEqFun.mk ⇑s ⋯ = ↑f} → -x ∈ {f | ∃ s, AEEqFun.mk ⇑s ⋯ = ↑f}

Tactic:
rintro f ⟨s, hs⟩

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
E : Type u_4
F : Type u_5
𝕜 : Type u_6
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f : ↥(Lp E p μ)
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hs : AEEqFun.mk ⇑s ⋯ = ↑f
⊢ -f ∈ {f | ∃ s, AEEqFun.mk ⇑s ⋯ = ↑f}
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (f - g)) a✝ = ↑↑↑(f - g) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
        ↑↑(↑f - ↑g) a✝ = (↑↑↑f - ↑↑↑g) a✝ → (toSimpleFunc (f - g)) a✝ = (⇑(toSimpleFunc f) - ⇑(toSimpleFunc g)) a✝

Tactic:
simp only [AddSubgroup.coe_sub, Pi.sub_apply]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f g : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (f - g)) a✝ = ↑(↑↑f - ↑↑g) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ →
      (toSimpleFunc g) a✝ = ↑↑↑g a✝ →
        ↑(↑↑f - ↑↑g) a✝ = ↑↑↑f a✝ - ↑↑↑g a✝ → (toSimpleFunc (f - g)) a✝ = (toSimpleFunc f) a✝ - (toSimpleFunc g) a✝
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
ae_eq : ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
a : α
h : (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
⊢ (toSimpleFunc (posPart f)) a = (toSimpleFunc f).posPart a

Tactic:
h,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
eq : ∀ (a : α), (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0
ae_eq : ∀ᵐ (a : α) ∂μ, (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
a : α
h : (toSimpleFunc (posPart f)) a = max ((toSimpleFunc f) a) 0
⊢ max ((toSimpleFunc f) a) 0 = (toSimpleFunc f).posPart 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
c : ℝ
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x)

Tactic:
rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]; rw [smul_zero]

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

Goal state before:
pp: α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : SMulZeroClass 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : DistribSMul 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x)

Tactic:
rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]; rw [smul_zero]

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
inst✝ : CompleteSpace E
⊢ Continuous fun f ↦ integral f

Tactic:
simp only [integral]
  exact L1.integralCLM.continuous

Goal state after:
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, ‖T (⇑f ⁻¹' {x})‖ * ‖x‖ ≤ ∑ x ∈ f.range, C * μ.real (⇑f ⁻¹' {x}) * ‖x‖

Tactic:
by
      refine Finset.sum_le_sum fun b hb => ?_
      obtain rfl | hb := eq_or_ne b 0
      · simp
      gcongr
      exact hT_norm _ (SimpleFunc.measurableSet_fiber _ _) <|
        SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hb

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ φ, Tendsto φ l (𝓝 0) ∧ u - v =ᶠ[l] φ * v

Tactic:
refine ⟨φ - 1, ?_, ?_⟩

Goal state after:
case mpr.refine_1
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Tendsto (φ - 1) l (𝓝 0)

case mpr.refine_2
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u - v =ᶠ[l] (φ - 1) * v
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
⊢ u ~[l] v ↔ ∃ φ, ∃ (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v

Tactic:
by
  rw [IsEquivalent, isLittleO_iff_exists_eq_mul]
  constructor <;> rintro ⟨φ, hφ, h⟩ <;> [refine ⟨φ + 1, ?_, ?_⟩; refine ⟨φ - 1, ?_, ?_⟩]
  · conv in 𝓝 _ => rw [← zero_add (1 : β)]
    exact hφ.add tendsto_const_nhds
  · convert! h.fun_add (EventuallyEq.refl l v) <;> simp [add_mul]
  · conv in 𝓝 _ => rw [← sub_self (1 : β)]
    exact hφ.sub tendsto_const_nhds
  · convert! h.fun_sub (EventuallyEq.refl l v); simp [sub_mul]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x ↦ ↑(f x)) μ
b : ℝ≥0
⊢ ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b ↔ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

Tactic:
rw [lintegral_coe_eq_integral f hfi, ENNReal.ofReal, ENNReal.coe_le_coe,
    Real.toNNReal_le_iff_le_coe]

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

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ ↑f x✝ = (const R P q) x✝

Tactic:
h,

Goal state after:
case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ (AffineMap.const R P q) x✝ = (const R P q) x✝
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_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : ↥(α →₁ₛ[μ] E)
⊢ ‖setToL1S T f‖ ≤ C * ‖f‖

Tactic:
setToL1S,

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ‖T s‖ ≤ C * μ.real s
f : ↥(α →₁ₛ[μ] E)
⊢ ‖SimpleFunc.setToSimpleFunc T (toSimpleFunc f)‖ ≤ C * ‖f‖
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : 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'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x
f : ↥(α →₁ₛ[μ] G'')
hf : 0 ≤ f
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)

Tactic:
obtain ⟨f', hf', hff'⟩ := exists_simpleFunc_nonneg_ae_eq hf

Goal state after:
α : 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'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x
f : ↥(α →₁ₛ[μ] G'')
hf : 0 ≤ f
f' : SimpleFunc α G''
hf' : 0 ≤ f'
hff' : ↑↑↑f =ᵐ[μ] ⇑f'
⊢ 0 ≤ SimpleFunc.setToSimpleFunc T (toSimpleFunc f)
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'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ (L1.setToL1 hT') (Integrable.toL1 f hf) = c • (L1.setToL1 hT) (Integrable.toL1 f hf)

Tactic:
L1.setToL1_smul_left' hT hT' c h_smul

Goal state after:
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 : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a

Tactic:
· filter_upwards [hf_bound] with a ha i
    simp [f', F', ha i]

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

Tactic:
· rw [setToFun_eq hT hf, setToFun_eq hT (hf.smul c), Integrable.toL1_smul' f hf,
      L1.setToL1_smul hT h_smul c]

Goal state after:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
f g : α →ᵇ β
⊢ dist f g = dist g f

Tactic:
by simp [dist_eq, dist_comm]

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
⊢ ‖f + g‖ = max ‖f‖ ‖g‖

Tactic:
have hfg' x : ‖(f + g) x‖ = max ‖f x‖ ‖g x‖ := by obtain (h | h) := hfg x <;> simp [h]

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
R : Type u_1
inst✝¹ : NonUnitalSeminormedRing R
inst✝ : IsCancelMulZero R
f g : α →ᵇ R
h : f * g = 0
hfg : ∀ (x : α), f x = 0 ∨ g x = 0
hfg' : ∀ (x : α), ‖(f + g) x‖ = max ‖f x‖ ‖g x‖
⊢ ‖f + g‖ = max ‖f‖ ‖g‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (f x) (f y) ≤ C₁
⊢ ∃ C, ∀ (x y : α), dist ((⇑f ⊔ ⇑g) x) ((⇑f ⊔ ⇑g) y) ≤ C

Tactic:
obtain ⟨C₂, hg⟩ := g.bounded

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (f x) (f y) ≤ C₁
C₂ : ℝ
hg : ∀ (x y : α), dist (g x) (g y) ≤ C₂
⊢ ∃ C, ∀ (x y : α), dist ((⇑f ⊔ ⇑g) x) ((⇑f ⊔ ⇑g) y) ≤ C
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (f x) (f y) ≤ C₁
⊢ ∃ C, ∀ (x y : α), dist ((⇑f ⊓ ⇑g) x) ((⇑f ⊓ ⇑g) y) ≤ C

Tactic:
obtain ⟨C₂, hg⟩ := g.bounded

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup β
inst✝² : Lattice β
inst✝¹ : HasSolidNorm β
inst✝ : IsOrderedAddMonoid β
f g : α →ᵇ β
C₁ : ℝ
hf : ∀ (x y : α), dist (f x) (f y) ≤ C₁
C₂ : ℝ
hg : ∀ (x y : α), dist (g x) (g y) ≤ C₂
⊢ ∃ C, ∀ (x y : α), dist ((⇑f ⊓ ⇑g) x) ((⇑f ⊓ ⇑g) y) ≤ C
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
⊢ (Summable fun x ↦ ‖f x‖) ↔ Summable f

Tactic:
refine ⟨Summable.of_norm, fun hf ↦ ?_⟩

Goal state after:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
f : α → E
hf : Summable f
⊢ Summable fun x ↦ ‖f x‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
⊢ 0 ≤ f + const α ‖f‖

Tactic:
intro x
  simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, coe_zero, Pi.zero_apply, coe_add,
    const_apply, Pi.add_apply]
  linarith [(abs_le.mp (norm_coe_le_norm f x)).1]

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CompactSpace α
inst✝² : NonUnitalNormedRing β
inst✝¹ : StarRing β
inst✝ : CStarRing β
f : C(α, β)
x : α
⊢ ‖star (f x) * f x‖ ≤ ‖star f * f‖

Tactic:
exact ContinuousMap.norm_coe_le_norm (star f * f) x

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ thickenedIndicatorAux δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) x = 1

Tactic:
thickenedIndicatorAux_one δ (closure E) x_mem

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ 1 = 1