mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ setToFun μ (weightedSMul μ) ⋯ ↑↑f

Tactic:
exact continuous_setToFun (dominatedFinMeasAdditive_weightedSMul μ)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h : c ≠ 0
⊢ Tendsto (u - fun x ↦ c) l (𝓝 0) ↔ Tendsto u l (𝓝 c)

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto (u - fun x ↦ c) l (𝓝 0)
⊢ Tendsto u l (𝓝 c)

case mpr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
h✝ : c ≠ 0
h : Tendsto u l (𝓝 c)
⊢ Tendsto (u - fun x ↦ c) l (𝓝 0)
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

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)

case inr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
inst✝ : SeparableSpace ↑(range f ∪ {0})
⊢ Tendsto (fun n ↦ ∫ (x : α), ‖(approxOn f fmeas (range f ∪ {0}) 0 ⋯ n) x - f x‖ ∂μ) atTop (𝓝 0)

Tactic:
convert! (tendsto_toReal zero_ne_top).comp (tendsto_approxOn_range_L1_enorm fmeas hf) with n
  rw [integral_norm_eq_lintegral_enorm]
  · simp
  · apply (SimpleFunc.aestronglyMeasurable _).sub
    apply (stronglyMeasurable_iff_measurable_separable.2 ⟨fmeas, ?_⟩).aestronglyMeasurable
    exact .mono (.of_subtype (range f ∪ {0})) subset_union_left

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
p₁ p₂ p₃ p₄ : P
⊢ dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄

Tactic:
rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V]
  exact norm_sub_le _ _

Goal state after:
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 : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ p + q = 1 →
    (fun b ↦ ∫ (x : α), f x b ∂μ) (p • a + q • b) ≤
      p • (fun b ↦ ∫ (x : α), f x b ∂μ) a + q • (fun b ↦ ∫ (x : α), f x b ∂μ) b

Tactic:
hpq

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
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ (fun b ↦ ∫ (x : α), f x b ∂μ) (p • a + q • b) ≤
    p • (fun b ↦ ∫ (x : α), f x b ∂μ) a + q • (fun b ↦ ∫ (x : α), f x b ∂μ) b
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case inr.const.inr
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f : α → E
hf : MemLp f p μ
ε✝ : ℝ≥0∞
hε : ε✝ ≠ 0
hp_pos : p ≠ 0
c : E
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
εpos : ε ≠ 0
Hs : MemLp (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))) p μ
hc : c ≠ 0
⊢ ∃ g, eLpNorm (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) - g) p μ ≤ ε ∧ P g

Tactic:
· have : μ s < ∞ := SimpleFunc.measure_lt_top_of_memLp_indicator hp_pos hp_ne_top hc hs Hs
      rcases h0P c hs this εpos with ⟨g, hg, Pg⟩
      rw [← eLpNorm_neg, neg_sub] at hg
      exact ⟨g, hg, Pg⟩

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

Goal state before:
pp: case inr.add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f✝ : α → E
hf✝ : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g
⊢ (∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g) →
    ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑(f + f')) p μ → ∃ g, eLpNorm (⇑(f + f') - g) p μ ≤ δ ∧ P g

Tactic:
hf'

Goal state after:
case inr.add
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_ne_top : p ≠ ∞
P : (α → E) → Prop
h0P :
  ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → μ s < ∞ → ∀ {ε : ℝ≥0∞}, ε ≠ 0 → ∃ g, eLpNorm (g - s.indicator fun x ↦ c) p μ ≤ ε ∧ P g
h1P : ∀ (f g : α → E), P f → P g → P (f + g)
h2P : ∀ (f : α → E), P f → AEStronglyMeasurable f μ
f✝ : α → E
hf✝ : MemLp f✝ p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp_pos : p ≠ 0
f f' : α →ₛ E
hff' : Disjoint (support ⇑f) (support ⇑f')
hf : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f) p μ → ∃ g, eLpNorm (⇑f - g) p μ ≤ δ ∧ P g
hf' : ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑f') p μ → ∃ g, eLpNorm (⇑f' - g) p μ ≤ δ ∧ P g
⊢ ∀ (δ : ℝ≥0∞), δ ≠ 0 → MemLp (⇑(f + f')) p μ → ∃ g, eLpNorm (⇑(f + f') - g) p μ ≤ δ ∧ P g
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Ring S
inst✝¹¹ : Ring R
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : AddCommGroup W
inst✝⁵ : Module R W
inst✝⁴ : TopologicalSpace W
inst✝³ : Module S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : IsTopologicalAddGroup W
p : W × (V →L[R] W)
⊢ ((decompLinearEquiv R S V W).symm p).contLinear = p.2

Tactic:
by
  ext; simp [decompLinearEquiv]

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

Goal state before:
pp: α : 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 α
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 F
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
f : ↥(α →₁ₛ[μ] E)
⊢ (setToL1' 𝕜 hT h_smul) ↑f = (setToL1SCLM α E μ hT) f

Tactic:
apply ContinuousLinearMap.extend_eq _ _ simpleFunc.isUniformInducing
  · exact simpleFunc.denseRange one_ne_top

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

Goal state before:
pp: case h_e
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = A ↑f
f : ↥(Lp E 1 μ)
⊢ IsUniformInducing ⇑(coeToLp α E ℝ)

pp: case H
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = A ↑f
f : ↥(Lp E 1 μ)
⊢ A ∘SL coeToLp α E ℝ = setToL1SCLM α E μ hT

Tactic:
· exact simpleFunc.isUniformInducing

Goal state after:
case H
α : 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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
A : ↥(Lp E 1 μ) →L[ℝ] F
hA : ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ hT) f = A ↑f
f : ↥(Lp E 1 μ)
⊢ A ∘SL coeToLp α E ℝ = setToL1SCLM α E μ hT
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x ↑F
hFn : (↑F).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖

Tactic:
gcongr; apply le_max_left

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x ↑F
hFn : (↑F).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r' * ‖x - y₀‖ < d

Tactic:
← dist_eq_norm

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
r : ℝ
hr : r < 1
x : E
hx : x ∉ F
d : ℝ := infDist x ↑F
hFn : (↑F).Nonempty
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : x - y₀ ∉ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r' * dist x y₀ < d
Module: Mathlib.Analysis.Normed.Module.RieszLemma

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

Tactic:
hy

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

Goal state before:
pp: case neg
α : 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'
h : T = T'
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
setToFun_undef _ hf

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

Goal state before:
pp: case neg
α : 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'
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
setToFun_undef _ hf

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

Goal state before:
pp: case hf
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))
hi : Countable { x // x ∈ s }
⊢ AEMeasurable Subtype.val (Measure.comap Subtype.val μ)

Tactic:
exact Measurable.aemeasurable measurable_subtype_coe

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
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
hF : CompleteSpace F
⊢ setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g

Tactic:
setToFun_eq hT (hf.add hg),

Goal state after:
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 : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
hF : CompleteSpace F
⊢ (L1.setToL1 hT) (Integrable.toL1 (f + g) ⋯) = setToFun μ T hT f + setToFun μ T hT g
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

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 : α) ∂μ, 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 : α
ha : ∀ (i : ℕ), F a ≤ f i a
i : ℕ
⊢ f' i a ≤ F' a
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 : ℝ
β : Type ?u.21
inst✝ : MetricSpace β
x✝ y✝ : α →ᵇ β
hfg : dist x✝ y✝ = 0
x : α
⊢ x✝ x = y✝ x

Tactic:
exact eq_of_dist_eq_zero (le_antisymm (hfg ▸ dist_coe_le_dist _) dist_nonneg)

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

Goal state before:
pp: case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (g i)).ker = ⊥

Tactic:
rcases LinearMap.exists_antilipschitzWith _ hf with ⟨K, K0, hK⟩

Goal state after:
case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (g i)).ker = ⊥
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✝ : ℝ
G : β → γ
C : ℝ≥0
H : LipschitzWith C G
f : α →ᵇ β
D : ℝ
hD : ∀ (x y : α), dist (f x) (f y) ≤ D
x y : α
⊢ ↑C * dist (f x) (f y) ≤ ↑(max C 0) * dist (f x) (f y)

Tactic:
gcongr; apply le_max_left

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

Goal state before:
pp: case inr
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
⊢ Tendsto (fun i ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

Tactic:
let f_lp := hfi.toL1 f

Goal state after:
case inr
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
⊢ Tendsto (fun i ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this✝ : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
this : ∃ x, x ∉ F
x : E
xR : ‖x‖ ≤ R
hx : ∀ y ∈ F, 1 ≤ ‖x - y‖
y : E
⊢ y ∈ F → 1 ≤ ‖y - x‖

Tactic:
hy

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this✝ : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
this : ∃ x, x ∉ F
x : E
xR : ‖x‖ ≤ R
hx : ∀ y ∈ F, 1 ≤ ‖x - y‖
y : E
hy : y ∈ F
⊢ 1 ≤ ‖y - x‖
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
⊢ infDist x Kᶜ = dist x x

Tactic:
rw [frontier_eq_closure_inter_closure] at hx'

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' :
  x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] Kᶜ
⊢ infDist x Kᶜ = dist x x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r

Tactic:
have : μ Set.univ = ∞ := by
      by_contra hμ'
      exact hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')
    rw [this, ENNReal.mul_top', if_neg, ENNReal.top_mul', if_neg]
    · exact le_top
    · simp [hr]
    · simp

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
hT_add : DominatedFinMeasAdditive (μ + μ') T C'
hT : DominatedFinMeasAdditive μ T C
f : α → E
hf : Integrable f (μ + μ')
⊢ μ + 0 ≤ μ + μ'

Tactic:
exact add_le_add le_rfl bot_le

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

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

Tactic:
filter_upwards [univ_mem] with δ _
    have obs : x ∈ cthickening δ E := closure_subset_cthickening δ E x_mem_closure
    rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst✝⁴] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
y : α
⊢ y ∈ Ici u → f y ∈ s

Tactic:
hy

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst✝⁴] s
u : α
hu : ∀ (b : α), u ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s
a : α
ha : u < a
y : α
hy : y ∈ Ici u
⊢ f y ∈ s
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F✝ : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F✝
inst✝¹ : NormedSpace ℝ F✝
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F✝
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ bound n a
bound_integrable : Integrable (fun a ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a ↦ ∑' (n : ι), bound n a
n : ι
⊢ ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ ∑' (n : ι), bound n a

Tactic:
exact EventuallyLE.trans (h_bound n) (hb_le_tsum n)

Goal state after: