mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
⊢ Absorbs 𝕜 V (⇑f '' s)

Tactic:
let _ : NontriviallyNormedField 𝕜 := ⟨by simpa using h₁⟩

Goal state after:
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
⊢ Absorbs 𝕜 V (⇑f '' s)
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ 1 ∈ I

Tactic:
simpa only [show u.inv * x = 1 by simp [u]] using I.mul_mem_left u.inv hxI

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_5
inst✝² : NormedAddCommGroup E
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
x : E
h : x ≠ 0
hx : 0 < ‖x‖
this : Nontrivial ↥(𝕜 ∙ x)
⊢ ‖coord 𝕜 x h‖ = ‖x‖⁻¹

Tactic:
exact ContinuousLinearMap.homothety_norm _ fun y =>
    homothety_inverse _ hx _ (LinearEquiv.toSpanNonzeroSingleton_homothety 𝕜 x h) _

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : Semiring 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : Module 𝕜 F
⊢ IsBoundedLinearMap 𝕜 fun x ↦ x.1

Tactic:
by
  refine (LinearMap.fst 𝕜 E F).isLinear.with_bound 1 fun x => ?_
  rw [one_mul]
  exact le_max_left _ _

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
f_quot : IsQuotientMap f
⊢ IsStrictMap g ↔ IsStrictMap (g ∘ f)

Tactic:
set Φ : range (g ∘ f) ≃ₜ range g := .setCongr <| f_quot.surjective.range_comp g
  have key : rangeFactorization g ∘ f = Φ ∘ rangeFactorization (g ∘ f) := rfl
  simp_rw [isStrictMap_iff_isQuotientMap_rangeFactorization, ← f_quot.of_comp_iff, key]
  exact ⟨fun H ↦ by simpa using! Φ.symm.isQuotientMap.comp H, fun H ↦ Φ.isQuotientMap.comp H⟩

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsQuotientMap f ↔ IsStrictMap f ∧ Surjective f

Tactic:
by
  refine ⟨fun H ↦ ⟨H.isStrictMap, H.surjective⟩, fun ⟨f_strict, f_surj⟩ ↦ ?_⟩
  rw [isStrictMap_iff_isQuotientMap_rangeFactorization] at f_strict
  set Φ : range f ≃ₜ Y := .trans (.setCongr f_surj.range_eq) (Homeomorph.Set.univ Y)
  exact Φ.isQuotientMap.comp f_strict

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsEmbedding f ↔ IsStrictMap f ∧ Injective f

Tactic:
refine ⟨fun H ↦ ⟨H.isStrictMap, H.injective⟩, fun ⟨f_strict, f_inj⟩ ↦ ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : IsStrictMap f ∧ Injective f
f_strict : IsStrictMap f
f_inj : Injective f
⊢ IsEmbedding f
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: case inr
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ t ≠ ∞
hs : μ s < ∞
⊢ μ.real s ≤ μ.real (s ∪ t)

Tactic:
exact measureReal_mono subset_union_left (measure_union_lt_top hs h.lt_top).ne

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ ‖indicatorConstLp p hs hμs c‖ ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
rw [indicatorConstLp, Lp.norm_toLp]
  refine ENNReal.toReal_le_of_le_ofReal (by positivity) ?_
  refine (eLpNorm_indicator_const_le _ _).trans_eq ?_
  rw [ENNReal.ofReal_mul (norm_nonneg _), ofReal_norm, measureReal_def,
    ENNReal.toReal_rpow, ENNReal.ofReal_toReal]
  finiteness

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᵐ[μ.restrict {x}] fun x_1 ↦ f x
⊢ ‖f x‖ₑ ≠ ∞

Tactic:
exact hfx

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable g (μ.withDensity f) ↔ Integrable (fun x ↦ (f x).toReal • g x) μ

Tactic:
by
  rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
    integrable_withDensity_iff_integrable_smul]
  · simp_rw [NNReal.smul_def, ENNReal.toReal]
  · exact hf.ennreal_toNNReal

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
refine
    aestronglyMeasurable_iff_aemeasurable_separable.2
      ⟨hf.aemeasurable hs, f '' s, ?_,
        mem_of_superset (self_mem_ae_restrict hs) (subset_preimage_image _ _)⟩

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
h : SecondCountableTopologyEither α β
inst✝¹ : OpensMeasurableSpace α
inst✝ : PseudoMetrizableSpace β
f : α → β
s : Set α
μ : Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
⊢ IsSeparable (f '' s)
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
inst✝ : RCLike 𝕜
f : α → 𝕜
⊢ Integrable (fun x ↦ RCLike.re (f x)) μ ∧ Integrable (fun x ↦ RCLike.im (f x)) μ ↔ Integrable f μ

Tactic:
by
  simp_rw [← memLp_one_iff_integrable]
  exact memLp_re_im_iff

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ'.trim hm < ∞

Tactic:
lintegral_trim hm _

Goal state after:
α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ' < ∞

α : Type u_1
m : MeasurableSpace α
H : Type u_8
inst✝ : NormedAddCommGroup H
m0 : MeasurableSpace α
μ' : Measure α
f : α → H
hm : m ≤ m0
hf_int : Integrable f μ'
hf : StronglyMeasurable f
⊢ Measurable fun a ↦ ‖f a‖ₑ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case refine_2
𝕜 : 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 ι
A : ∀ (f : ContinuousMultilinearMap 𝕜 E G × ContinuousMultilinearMap 𝕜 E G), ‖-f.1 + f.2‖ = ‖f.1 - f.2‖
x✝¹ : Set ((i : ι) → E i) × ℝ
s : Set ((i : ι) → E i)
r : ℝ
x✝ : Bornology.IsVonNBounded 𝕜 (s, r).1 ∧ 0 < (s, r).2
hs : Bornology.IsVonNBounded 𝕜 (s, r).1
hr : 0 < (s, r).2
⊢ ∃ r_1 > 0, (ContinuousMultilinearMap.seminorm 𝕜 E G).ball 0 r_1 ⊆ {f | Set.MapsTo ⇑f (s, r).1 (closedBall 0 (s, r).2)}

Tactic:
· rcases (NormedSpace.isVonNBounded_iff' _).1 hs with ⟨ε, hε⟩
    rcases exists_pos_mul_lt hr (ε ^ Fintype.card ι) with ⟨δ, hδ₀, hδ⟩
    refine ⟨δ, hδ₀, fun f hf x hx ↦ ?_⟩
    simp only [Seminorm.mem_ball_zero, mem_closedBall_zero_iff] at hf ⊢
    replace hf : ‖f‖ ≤ δ := hf.le
    replace hx : ‖x‖ ≤ ε := hε x hx
    calc
      ‖f x‖ ≤ ‖f‖ * ε ^ Fintype.card ι := le_opNorm_mul_pow_card_of_le f hx
      _ ≤ δ * ε ^ Fintype.card ι := by have := (norm_nonneg x).trans hx; gcongr
      _ ≤ r := (mul_comm _ _).trans_le hδ.le

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:
dist_edist,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ (edist f g).toReal = (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ).toReal
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case hbc
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
x : E
⊢ ‖x‖ ≤ ↑N * ‖e x‖

Tactic:
exact h_e x

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
h : ∃ᶠ (x : α) in l, v x = 0 ∧ u x ≠ 0
x : α
x✝ : v x = 0 ∧ u x ≠ 0
hv : v x = 0
hu : u x ≠ 0
⊢ (u / v) x = 0

Tactic:
simp [hv]

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖f z‖ ≤ c / r * ‖z‖

Tactic:
rw [z_zero]

Goal state after:
case pos
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : z = 0
⊢ ‖f 0‖ ≤ c / r * ‖0‖
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Fintype n
inst✝³ : Mul R
inst✝² : AddCommMonoid R
inst✝¹ : ContinuousAdd R
inst✝ : ContinuousMul R
A B : X → n → R
hA : Continuous A
hB : Continuous B
⊢ Continuous fun x ↦ A x ⬝ᵥ B x

Tactic:
dsimp only [dotProduct]
  fun_prop

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: case inl.inl
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : l
⊢ Continuous fun a ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inl i) (Sum.inl j)

Tactic:
refine Continuous.matrix_elem ?_ i j

Goal state after:
case inl.inl
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : l
⊢ Continuous A
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: case inl.inr
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : m
⊢ Continuous fun a ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inl i) (Sum.inr j)

Tactic:
refine Continuous.matrix_elem ?_ i j

Goal state after:
case inl.inr
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : n
j : m
⊢ Continuous B
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: case inr.inl
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : l
⊢ Continuous fun a ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inr i) (Sum.inl j)

Tactic:
refine Continuous.matrix_elem ?_ i j

Goal state after:
case inr.inl
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : l
⊢ Continuous C
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: case inr.inr
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : m
⊢ Continuous fun a ↦ fromBlocks (A a) (B a) (C a) (D a) (Sum.inr i) (Sum.inr j)

Tactic:
refine Continuous.matrix_elem ?_ i j

Goal state after:
case inr.inr
X : Type u_1
l : Type u_3
m : Type u_4
n : Type u_5
p : Type u_6
R : Type u_8
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace R
A : X → Matrix n l R
B : X → Matrix n m R
C : X → Matrix p l R
D : X → Matrix p m R
hA : Continuous A
hB : Continuous B
hC : Continuous C
hD : Continuous D
i : p
j : m
⊢ Continuous D
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 α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
x : ↥(α →₁ₛ[μ] E)
⊢ ‖x‖ = ‖(coeToLp α E ℝ) x‖

Tactic:
simp [coeToLp]

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

Goal state before:
pp: 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 }
⊢ Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)

pp: case hs
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 (μ.restrict s)
hi : Countable { x // x ∈ s }
⊢ MeasurableSet s

Tactic:
integrable_map_measure

Goal state after:
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 ∘ Subtype.val) (Measure.comap Subtype.val μ)
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)

case hg
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 }
⊢ AEStronglyMeasurable f (Measure.map Subtype.val (Measure.comap Subtype.val μ))

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 μ)

case hs
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 (μ.restrict s)
hi : Countable { x // x ∈ s }
⊢ MeasurableSet 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 : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
h : μ = 0
⊢ f =ᵐ[μ] 0

Tactic:
simp [h, EventuallyEq]

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

Goal state before:
pp: case inl
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ setToFun (∞ • μ) (weightedSMul (∞ • μ)) ⋯ f = 0

Tactic:
setToFun_top_smul_measure

Goal state after:
case inl
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ).toReal ^ (1 / p) *
      (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ).toReal ^ (1 / q)

Tactic:
rw [ENNReal.toReal_rpow, ENNReal.toReal_rpow, ← ENNReal.toReal_mul]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
⊢ (∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ).toReal ≤
    ((∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ) ^ (1 / p) *
        (∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ) ^ (1 / q)).toReal
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
⊢ ⇑f = toReal ∘ ⇑f.nnrealPart - toReal ∘ ⇑(-f).nnrealPart

Tactic:
by
  funext x
  dsimp
  simp only [max_zero_sub_max_neg_zero_eq_self]

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 α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
⊢ Continuous fun f ↦ Integrable.toL1 ↑↑f ⋯

Tactic:
by_cases hc'0 : c' = 0

Goal state after:
case pos
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : c' = 0
⊢ Continuous fun f ↦ Integrable.toL1 ↑↑f ⋯

case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
⊢ Continuous fun f ↦ Integrable.toL1 ↑↑f ⋯
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 δ E x = 1

Tactic:
← thickenedIndicatorAux_closure_eq,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ thickenedIndicatorAux δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) x = 1
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 α
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 μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ μ' s ≠ ∞

Tactic:
refine ((hμ'_le s).trans_lt ?_).ne

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 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 μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ (c' • μ) s < ∞
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ (thickenedIndicator δ_pos E) y ≤ (thickenedIndicator δ_pos E) x

Tactic:
by
  simp only [thickenedIndicator_apply]
  gcongr
  · finiteness
  · exact thickenedIndicatorAux_mono_infEDist δ h

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

Goal state before:
pp: case pos.h_closed
α : 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 μ'
⊢ IsClosed {f | setToFun μ T hT ↑↑f = setToFun μ' T hT' ↑↑f}

Tactic:
refine isClosed_eq (continuous_setToFun hT) ?_

Goal state after:
case pos.h_closed
α : 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 μ'
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ setToFun μ' T hT' ↑↑f