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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ Integrable (fun x ↦ (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞

Tactic:
rw [Integrable, hasFiniteIntegral_toReal_iff hf_ne_top]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ AEStronglyMeasurable (fun x ↦ (f x).toReal) μ ∧ ∫⁻ (x : α), f x ∂μ ≠ ∞ ↔ ∫⁻ (x : α), f x ∂μ ≠ ∞
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ∂μ) * ‖c‖ₑ < ∞ ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
ENNReal.mul_lt_top_iff

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
E : Type u_9
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
c : E
hc : c ≠ 0
a✝ : AEStronglyMeasurable f μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞ ∧ ‖c‖ₑ < ∞ ∨ ∫⁻ (a : α), ‖f a‖ₑ ∂μ = 0 ∨ ‖c‖ₑ = 0 ↔ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

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

Tactic:
by
  apply le_antisymm
  · apply opNorm_le_bound <;> simp
  · convert! ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1
    simp

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

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

Tactic:
· refine le_antisymm norm_mkPiAlgebra_le ?_
    convert! ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1
    simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ dist f g = (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ).toReal

Tactic:
by
  simp_rw [dist_edist, edist_def]

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

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
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✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i
⊢ ‖g.compContinuousLinearMap fun i ↦ (f i).toContinuousLinearMap‖ ≤ ‖g‖

Tactic:
refine opNorm_le_bound (norm_nonneg _) fun m => ?_

Goal state after:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
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✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i
m : (i : ι) → E i
⊢ ‖(g.compContinuousLinearMap fun i ↦ (f i).toContinuousLinearMap) m‖ ≤ ‖g‖ * ∏ i, ‖m i‖
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
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✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i
⊢ ‖g.compContinuousLinearMap fun i ↦ (f i).toContinuousLinearMap‖ ≤ ‖g‖

Tactic:
by
  refine opNorm_le_bound (norm_nonneg _) fun m => ?_
  apply (g.le_opNorm _).trans _
  simp only [ContinuousLinearMap.coe_coe, LinearIsometry.coe_toContinuousLinearMap,
    LinearIsometry.norm_map, le_rfl]

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

Goal state before:
pp: α : Type u_1
F : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
h_map : (fun x ↦ ‖f x‖ₑ ^ p) = ⇑(map (fun x ↦ ‖x‖ₑ ^ p) f)
⊢ eLpNorm' (⇑f) p μ = (∑ y ∈ f.range, ‖y‖ₑ ^ p * μ (⇑f ⁻¹' {y})) ^ (1 / p)

Tactic:
eLpNorm'_eq_lintegral_enorm,

Goal state after:
α : Type u_1
F : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
p : ℝ
f : α →ₛ F
μ : Measure α
h_map : (fun x ↦ ‖f x‖ₑ ^ p) = ⇑(map (fun x ↦ ‖x‖ₑ ^ p) f)
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) = (∑ y ∈ f.range, ‖y‖ₑ ^ p * μ (⇑f ⁻¹' {y})) ^ (1 / p)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
⊢ (map (fun x ↦ ‖x‖ₑ ^ p.toReal) f).lintegral μ ≠ ∞

Tactic:
← (f.map fun x ↦ ‖x‖ₑ ^ p.toReal).lintegral_eq_lintegral μ

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
⊢ ∫⁻ (a : α), (map (fun x ↦ ‖x‖ₑ ^ p.toReal) f) a ∂μ ≠ ∞
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁷ : AddCommGroup E
inst✝¹⁶ : UniformSpace E
inst✝¹⁵ : IsUniformAddGroup E
inst✝¹⁴ : AddCommGroup F
inst✝¹³ : UniformSpace F
inst✝¹² : IsUniformAddGroup F
inst✝¹¹ : T0Space F
inst✝¹⁰ : AddCommMonoid Eₗ
inst✝⁹ : UniformSpace Eₗ
inst✝⁸ : ContinuousAdd Eₗ
inst✝⁷ : Semiring 𝕜
inst✝⁶ : Semiring 𝕜₂
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : Module 𝕜 Eₗ
inst✝² : ContinuousConstSMul 𝕜 Eₗ
inst✝¹ : ContinuousConstSMul 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
f g : E →SL[σ₁₂] F
inst✝ : CompleteSpace F
e : E →L[𝕜] Eₗ
h : DenseRange ⇑e ∧ IsUniformInducing ⇑e
cont : Continuous (⋯.extend ⇑f)
eq : ∀ (b : E), ⋯.extend (⇑f) (e b) = f b
⊢ ∀ (a₁ a₂ : E), ⋯.extend (⇑f) (e a₁ + e a₂) = ⋯.extend (⇑f) (e a₁) + ⋯.extend (⇑f) (e a₂)

Tactic:
· intro x y
        simp only [eq, ← e.map_add]
        exact f.map_add _ _

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

Goal state before:
pp: α : 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)
hSp : ∀ i ∈ sι, μ (S i) ≠ ∞
h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)
⊢ T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)

Tactic:
revert hSp h_disj
  refine Finset.induction_on sι ?_ ?_
  · simp only [Finset.notMem_empty, IsEmpty.forall_iff, iUnion_false, iUnion_empty, sum_empty,
      imp_true_iff, T_empty]
  intro a s has h hps h_disj
  rw [Finset.sum_insert has, ← h]
  swap; · exact fun i hi => hps i (Finset.mem_insert_of_mem hi)
  swap
  · exact fun i hi j hj hij =>
      h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij
  rw [←
    h_add (S a) (⋃ i ∈ s, S i) (hS_meas a) (measurableSet_biUnion _ fun i _ => hS_meas i)
      (hps a (Finset.mem_insert_self a s))]
  · congr; convert! Finset.iSup_insert a s S
  · exact (measure_biUnion_lt_top s.finite_toSet fun i hi ↦
      (hps i <| Finset.mem_insert_of_mem hi).lt_top).ne
  · simp_rw [Set.disjoint_iUnion_right]
    intro i hi
    refine h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_
    rw [← hai] at hi
    exact has hi

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ∞ → μ' s = ∞
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ∞
hμs : μ s < ∞
⊢ C * μ.real s ≤ C * μ'.real s

Tactic:
simp only [measureReal_def]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' : ∀ (s : Set α), μ s = ∞ → μ' s = ∞
s : Set α
hs : MeasurableSet s
hμ's : μ' s < ∞
hμs : μ s < ∞
⊢ C * (μ s).toReal ≤ C * (μ' s).toReal
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 α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
x : F
⊢ (μ.real s + ν.real s) • x = μ.real s • x + ν.real s • x

Tactic:
add_smul

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
x : F
⊢ μ.real s • x + ν.real s • x = μ.real s • x + ν.real s • x
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 α
s t : Set α
ht : MeasurableSet t
hs_finite : μ s ≠ ∞
ht_finite : μ t ≠ ∞
hdisj : Disjoint s t
x : F
⊢ (μ.real s + μ.real t) • x = μ.real s • x + μ.real t • x

Tactic:
add_smul

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
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
⊢ integral (μ + ν) f = integral μ f + integral ν f

Tactic:
simp_rw [integral_def]

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
⊢ setToSimpleFunc (weightedSMul (μ + ν)) f = setToSimpleFunc (weightedSMul μ) f + setToSimpleFunc (weightedSMul ν) f
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: case pos.inr
α : 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
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx✝ : 0 ≤ f x
hx : 0 < f x
⊢ μ.real (⇑f ⁻¹' {f x}) • f x ≤ ν.real (⇑f ⁻¹' {f x}) • f x

Tactic:
simp only [measureReal_def]

Goal state after:
case pos.inr
α : 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
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx✝ : 0 ≤ f x
hx : 0 < f x
⊢ (μ (⇑f ⁻¹' {f x})).toReal • f x ≤ (ν (⇑f ⁻¹' {f x})).toReal • f x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ Continuous integral

Tactic:
simp_rw [integral_def]

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ Continuous ⇑integralCLM
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 α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[ν] g a
⊢ (fun a ↦ ∫ (b : β), f a b ∂ν) =ᵐ[μ] fun a ↦ ∫ (b : β), g a b ∂ν

Tactic:
filter_upwards [h] with _ ha

Goal state after:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x✝ : MeasurableSpace β
ν : Measure β
f g : α → β → G
h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[ν] g a
a✝ : α
ha : f a✝ =ᵐ[ν] g a✝
⊢ ∫ (b : β), f a✝ b ∂ν = ∫ (b : β), g a✝ b ∂ν
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 α
ι : 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)
⊢ Tendsto (fun i ↦ setToFun μ (weightedSMul μ) ⋯ (F i)) l (𝓝 (setToFun μ (weightedSMul μ) ⋯ f))

Tactic:
exact tendsto_setToFun_of_L1 (dominatedFinMeasAdditive_weightedSMul μ) f hfi hFi hF

Goal state after:
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 α
X : Type u_6
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → G
x₀ : X
bound : α → ℝ
s : Set X
hF_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x ↦ F x a) s x₀
⊢ ContinuousWithinAt (fun x ↦ ∫ (a : α), F x a ∂μ) s x₀

Tactic:
by
  simp only [integral_eq_setToFun]
  exact continuousWithinAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
    hF_meas h_bound bound_integrable h_cont

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

Goal state before:
pp: α : 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✝
⊢ ENNReal.ofReal (f a✝) = ‖↑↑(Lp.posPart f₁) a✝‖ₑ

Tactic:
rw [h₁, h₂, ENNReal.ofReal]

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 = ‖max (f a✝) 0‖ₑ
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart f₁) a✝ = -min (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ENNReal.ofReal (-f a✝) = ‖↑↑(Lp.negPart f₁) a✝‖ₑ

Tactic:
rw [h₁, h₂, ENNReal.ofReal]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart f₁) a✝ = -min (↑↑f₁ a✝) 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(-f a✝).toNNReal = ‖-min (f a✝) 0‖ₑ
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case zero
α : Type u_1
β : Type u_3
inst✝ : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
⊢ t ^ 0 ~[l] u ^ 0

Tactic:
simpa using IsEquivalent.refl

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

Goal state before:
pp: 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
f g : P →ᴬ[R] Q
h : ↑f = ↑g
⊢ f = g

Tactic:
by
  cases f
  cases g
  congr

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous ((↑e₁).prodCongr ↑e₂).toFun

Tactic:
eta_expand; dsimp; fun_prop

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
e₁ : P₁ ≃ᴬ[k] P₂
e₂ : P₃ ≃ᴬ[k] P₄
⊢ Continuous ((↑e₁).prodCongr ↑e₂).invFun

Tactic:
eta_expand; dsimp; fun_prop

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous (AffineEquiv.prodAssoc k P₁ P₂ P₃).toFun

Tactic:
eta_expand; dsimp; fun_prop

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

Goal state before:
pp: k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
⊢ Continuous (AffineEquiv.prodAssoc k P₁ P₂ P₃).invFun

Tactic:
eta_expand; dsimp; fun_prop

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

Goal state before:
pp: 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
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝²⁰ : AddCommGroup W₂
inst✝¹⁹ : Module R W₂
inst✝¹⁸ : TopologicalSpace Q₂
inst✝¹⁷ : AddTorsor W₂ Q₂
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₁ →ᴬ[k] P₃
⊢ Continuous ((↑f).prod ↑g).toFun

Tactic:
eta_expand; dsimp; fun_prop

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

Goal state before:
pp: 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
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst✝²⁰ : AddCommGroup W₂
inst✝¹⁹ : Module R W₂
inst✝¹⁸ : TopologicalSpace Q₂
inst✝¹⁷ : AddTorsor W₂ Q₂
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst✝¹⁶ : Ring k
inst✝¹⁵ : AddCommGroup V₁
inst✝¹⁴ : Module k V₁
inst✝¹³ : AddTorsor V₁ P₁
inst✝¹² : TopologicalSpace P₁
inst✝¹¹ : AddCommGroup V₂
inst✝¹⁰ : Module k V₂
inst✝⁹ : AddTorsor V₂ P₂
inst✝⁸ : TopologicalSpace P₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AddTorsor V₃ P₃
inst✝⁴ : TopologicalSpace P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AddTorsor V₄ P₄
inst✝ : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₃ →ᴬ[k] P₄
⊢ Continuous ((↑f).prodMap ↑g).toFun

Tactic:
eta_expand; dsimp; fun_prop

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
a : α
⊢ (∀ (i : ℕ), f i a ≤ F a) → ∀ (i : ℕ), f' i a ≤ F' a

Tactic:
ha_bound

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
a : α
ha_bound : ∀ (i : ℕ), f i a ≤ F a
⊢ ∀ (i : ℕ), f' i a ≤ F' a