mathlib-initiative/mathlib-tactics huggingface dataset:
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
h_norm : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
x : E
this : ∀ (x : ↥e.range), ((f.compLeftInverse e).extend e.range.subtypeL) (e.range.subtypeL x) = (f.compLeftInverse e) x
⊢ (f.extendOfNorm e) (e x) = f x

Tactic:
convert! this ⟨e x, LinearMap.mem_range_self e x⟩

Goal state after:
case e'_3
𝕜 : 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
h_norm : ∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
x : E
this : ∀ (x : ↥e.range), ((f.compLeftInverse e).extend e.range.subtypeL) (e.range.subtypeL x) = (f.compLeftInverse e) x
⊢ f x = (f.compLeftInverse e) ⟨e x, ⋯⟩
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case neg.h_disj
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
h_left_eq' :
  (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) =
    (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a))
⊢ ∀ i ∈ {b ∈ f.range | g b = g (f a)}, ∀ j ∈ {b ∈ f.range | g b = g (f a)}, i ≠ j → Disjoint (⇑f ⁻¹' {i}) (⇑f ⁻¹' {j})

Tactic:
· grind [Set.disjoint_iff]

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

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

Tactic:
forall_mem_range

Goal state after:
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
f : α →ₛ F
hf : 0 ≤ᵐ[μ] ⇑f
⊢ ∀ (x : α), 0 ≤ μ.real (⇑f ⁻¹' {f x}) • f x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

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''
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α →ₛ G'
hf : 0 ≤ f
hfi : Integrable (⇑f) μ
⊢ 0 ≤ setToSimpleFunc T f

Tactic:
refine sum_nonneg fun i hi => ?_
  by_cases h0 : i = 0
  · simp [h0]
  refine
    hT_nonneg _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hfi h0) i ?_
  rw [mem_range] at hi
  obtain ⟨y, hy⟩ := Set.mem_range.mp hi
  rw [← hy]
  convert! hf y

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

Goal state before:
pp: case refine_1
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
s : Set α
⊢ ∀ᶠ (i : ι) in l, Integrable (F i) (μ.restrict s)

pp: case refine_2
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
s : Set α
⊢ Tendsto (fun i ↦ ∫⁻ (x : α) in s, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)

Tactic:
· filter_upwards [hFi] with i hi using hi.restrict

Goal state after:
case refine_2
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
f : α → G
hfi : AEStronglyMeasurable f μ
F : ι → α → G
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, Integrable (F i) μ
hF : Tendsto (fun i ↦ ∫⁻ (x : α), ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
s : Set α
⊢ Tendsto (fun i ↦ ∫⁻ (x : α) in s, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

Tactic:
by
  simp +unfoldPartialApp only [IsEquivalent, const, isLittleO_const_iff h]
  constructor <;> intro h
  · have := h.sub (tendsto_const_nhds (x := -c))
    simp only [Pi.sub_apply, sub_neg_eq_add, sub_add_cancel, zero_add] at this
    exact this
  · have := h.sub (tendsto_const_nhds (x := c))
    rwa [sub_self] at this

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

Tactic:
apply dist_vsub_vsub_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
hpq : p + q = 1
⊢ ∫ (x : α), p • f x a + q • f x b ∂μ = ∫ (x : α), p • f x a ∂μ + ∫ (x : α), q • f x b ∂μ

Tactic:
by
                  apply integral_add
                  all_goals fun_prop (disch := aesop)

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᵐ[μ] f
this : f =ᵐ[μ] fun x ↦ ‖f x‖
⊢ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
exact lintegral_congr_ae (this.symm.fun_comp ENNReal.ofReal)

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

Goal state before:
pp: α : 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 : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
this : Tendsto (fun n ↦ ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
by
    simp_rw [f', integral_sub (hf _) (hf _), integral_sub' hF (hf 0),
      tendsto_sub_const_iff] at this
    exact this

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

Goal state before:
pp: case e_f
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
x : G
⊢ (‖x‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal = (μ (⇑(toSimpleFunc f) ⁻¹' {x})).toReal * ‖x‖

Tactic:
rw [ENNReal.toReal_mul, mul_comm, ← ofReal_norm,
      ENNReal.toReal_ofReal (norm_nonneg _)]

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
h_eq : ∀ (a : α), (SimpleFunc.map (fun x ↦ ‖x‖ₑ) (toSimpleFunc f)) a = ‖(toSimpleFunc f) a‖ₑ
⊢ ∀ a ∈ (toSimpleFunc f).range, ‖a‖ₑ * μ (⇑(toSimpleFunc f) ⁻¹' {a}) ≠ ∞

Tactic:
· intro x _
    by_cases hx0 : x = 0
    · rw [hx0]; simp
    · finiteness [SimpleFunc.measure_preimage_lt_top_of_integrable _ (SimpleFunc.integrable f) hx0]

Goal state after:
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ C, ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ C, ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
⊢ ∀ ⦃x : R⦄, x ∈ s * t → ∀ ⦃y : R⦄, y ∈ s * t → dist x y ≤ 2 * Af * Ag

Tactic:
intro z

Goal state after:
case h
R : Type u_1
inst✝ : NonUnitalSeminormedRing R
s t : Set R
hs : ∃ C, ∀ ⦃x : R⦄, x ∈ s → ∀ ⦃y : R⦄, y ∈ s → dist x y ≤ C
ht : ∃ C, ∀ ⦃x : R⦄, x ∈ t → ∀ ⦃y : R⦄, y ∈ t → dist x y ≤ C
Af : ℝ
hAf : s ⊆ Metric.closedBall 0 Af
Ag : ℝ
hAg : t ⊆ Metric.closedBall 0 Ag
z : R
⊢ z ∈ s * t → ∀ ⦃y : R⦄, y ∈ s * t → dist z y ≤ 2 * Af * Ag
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
hf : Integrable f μ
⊢ ‖Integrable.toL1 f hf‖ = ∫ (a : α), ‖f a‖ ∂μ

Tactic:
rw [L1.norm_eq_integral_norm]
  exact integral_congr_ae <| hf.coeFn_toL1.fun_comp _

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

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
⊢ LipschitzWith ‖↑A‖₊ ⇑A

Tactic:
apply A.lipschitz

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

Goal state before:
pp: α : Type u
γ : Type w
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : TopologicalSpace α
inst✝¹ : NormedRing γ
inst✝ : NormedAlgebra 𝕜 γ
k : 𝕜
a : α
⊢ ((algebraMap 𝕜 (α →ᵇ γ)) k) a = k • 1

Tactic:
by
  simp only [Algebra.algebraMap_eq_smul_one, coe_smul, coe_one, Pi.one_apply]

Goal state after:
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
hf : Summable f
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x ↦ ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := v.equivFunL
⊢ Summable fun x ↦ ‖f x‖

Tactic:
have H : Summable fun x => ‖e (f x)‖ := this (e.summable.2 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
this : ∀ {N : ℕ} {g : α → Fin N → ℝ}, Summable g → Summable fun x ↦ ‖g x‖
v : Basis (Fin (finrank ℝ E)) ℝ E
e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := v.equivFunL
H : Summable fun x ↦ ‖e (f x)‖
⊢ Summable fun x ↦ ‖f x‖
Module: Mathlib.Topology.ContinuousMap.Bounded.Star

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
inst✝³ : StarAddMonoid β
inst✝² : NormedStarGroup β
inst✝¹ : NormedSpace 𝕜 β
inst✝ : StarModule 𝕜 β
f : α →ᵇ β
⊢ ‖star f‖ ≤ ‖f‖

Tactic:
simp only [norm_eq, star_apply, norm_star, le_of_eq]

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

Goal state before:
pp: G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
hf_seq_int : ∀ (n : ℕ), Integrable (⇑(f_seq n)) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable (⇑(f_seq n)) (μ.trim hm)
hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), (f_seq n) x ∂μ = ∫ (x : β), (f_seq n) x ∂μ.trim hm
h_lim_1 : Tendsto (fun n ↦ ∫ (x : β), (f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : β), (f_seq n) x ∂μ.trim hm) atTop (𝓝 (∫ (x : β), f x ∂μ.trim hm))

Tactic:
refine @tendsto_integral_of_L1 β G _ _ m (μ.trim hm) _ f (hf_int.trim hm hf).1 _ _
      (Eventually.of_forall hf_seq_int_m) ?_

Goal state after:
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
f_seq : ℕ → β →ₛ G := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
hf_seq_meas : ∀ (n : ℕ), StronglyMeasurable ⇑(f_seq n)
hf_seq_int : ∀ (n : ℕ), Integrable (⇑(f_seq n)) μ
hf_seq_int_m : ∀ (n : ℕ), Integrable (⇑(f_seq n)) (μ.trim hm)
hf_seq_eq : ∀ (n : ℕ), ∫ (x : β), (f_seq n) x ∂μ = ∫ (x : β), (f_seq n) x ∂μ.trim hm
h_lim_1 : Tendsto (fun n ↦ ∫ (x : β), (f_seq n) x ∂μ) atTop (𝓝 (∫ (x : β), f x ∂μ))
⊢ Tendsto (fun i ↦ ∫⁻ (x : β), ‖(f_seq i) x - f x‖ₑ ∂μ.trim hm) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.h_add
α : 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 α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
⊢ ∀ ⦃f g : α → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          setToFun μ T hT f = setToFun μ' T hT' f →
            setToFun μ T hT g = setToFun μ' T hT' g → setToFun μ T hT (f + g) = setToFun μ' T hT' (f + g)

Tactic:
intro f₂ g₂ _ hf₂ hg₂ h_eq_f h_eq_g

Goal state after:
case pos.h_add
α : 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 α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
f₂ g₂ : α → E
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂ μ
hg₂ : Integrable g₂ μ
h_eq_f : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
h_eq_g : setToFun μ T hT g₂ = setToFun μ' T hT' g₂
⊢ setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)
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
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero : Tendsto (fun n ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
x : α
hx : ↑↑(Integrable.toL1 (fs n - f) ⋯) x = (fs n - f) x
⊢ ‖↑↑(Integrable.toL1 (fs n - f) ⋯) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖

Tactic:
rw [hx, ofReal_norm, Pi.sub_apply]

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ ∀ a < x, f a ≤ f y

Tactic:
intro z

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
z : α
⊢ z < x → f z ≤ f y
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
⊢ ∀ a < y, f a ≤ f y

Tactic:
intro z

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
z : α
⊢ z < y → f z ≤ f y
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
⊢ ∫ (x : X) in ∅, f x ∂μ = 0

Tactic:
Measure.restrict_empty,

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
⊢ ∫ (x : X), f x ∂0 = 0
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 : Set α → E →L[ℝ] F
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : ¬CompleteSpace F
⊢ StronglyMeasurable fun x ↦ setToFun μ T hT (f x)

Tactic:
simp [setToFun, hF, stronglyMeasurable_const]

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : Countable G
inst✝ : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : μ s = 0
⊢ 0 ≤ 0

Tactic:
le_refl

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁴ : OrderTopology R
inst✝³ : CompactIccSpace R
inst✝² : MeasurableSpace R
inst✝¹ : BorelSpace R
inst✝ : DenselyOrdered R
s : Set R
⊢ f.outer.trim s ≤ f.outer s

Tactic:
OuterMeasure.trim_eq_iInf

Goal state after:
R : Type u_1
inst✝⁶ : LinearOrder R
inst✝⁵ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁴ : OrderTopology R
inst✝³ : CompactIccSpace R
inst✝² : MeasurableSpace R
inst✝¹ : BorelSpace R
inst✝ : DenselyOrdered R
s : Set R
⊢ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), f.outer t ≤ f.outer s
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
⊢ (sum fun g ↦ ν.restrict (g • s)) = ν

Tactic:
← restrict_iUnion_ae (h.aedisjoint.mono fun i j h => hν h) fun g =>
      (h.nullMeasurableSet_smul g).mono_ac hν,

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s μ
hν : ν ≪ μ
⊢ ν.restrict (⋃ i, i • s) = ν
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'
this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L'
M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }
hM' : ↑M' ⊆ ↑U' \ ↑L'
⊢ μ L' + μ M' ≤ μ.outerMeasure ↑U'

Tactic:
have : (↑(L' ⊔ M') : Set G) ⊆ U' := by
    simp only [Compacts.coe_sup, union_subset_iff, hL'U', true_and]
    exact hM'.trans sdiff_subset

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝² : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L'
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L'
M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }
hM' : ↑M' ⊆ ↑U' \ ↑L'
this : ↑(L' ⊔ M') ⊆ ↑U'
⊢ μ L' + μ M' ≤ μ.outerMeasure ↑U'
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: case neg
G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s μ
⊢ ¬Integrable f (μ.restrict t)

Tactic:
rwa [hs.integrableOn_iff ht hf] at hfs

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ essSup f μ ≤ sInf {a | (μ.restrict s) {x | a < f x} = 0}

Tactic:
essSup_eq_sInf μ f

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ sInf {a | μ {x | a < f x} = 0} ≤ sInf {a | (μ.restrict s) {x | a < f x} = 0}