mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Semiring 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedAddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : SeminormedAddCommGroup G
inst✝ : Module 𝕜 G
f : E × F → G
h : IsBoundedBilinearMap 𝕜 f
e₁ : E
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, instTopologicalSpaceProd] (Prod.mk e₁)

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
x : X
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt (fun x ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) s x

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
x : X
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt (fun x ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) x

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
s : Set X
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn (fun x ↦ f x ∘SL ContinuousLinearMap.fst 𝕜 E F + g x ∘SL ContinuousLinearMap.snd 𝕜 E F) s

Tactic:
fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_4
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
X : Type u_5
inst✝ : TopologicalSpace X
f : X → E →L[𝕜] G
g : X → F →L[𝕜] G
hf : Continuous[inst✝, _] f
hg : Continuous[inst✝, _] g
⊢ ContinuousOn (fun x ↦ (f x).coprod (g x)) Set.univ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ

Tactic:
have A : MeasurableSet { x : α | f x ≠ 0 } := (hf (measurableSet_singleton 0)).compl

Goal state after:
case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
this : ↑(f a) ≠ 0
⊢ ↑(f a) • g a = ↑(f a) • g' a

Tactic:
ha this

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a ≠ 0
this : ↑(f a) ≠ 0
⊢ ↑(f a) • g' a = ↑(f a) • g' a
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsCompl p q
⊢ IsTopCompl p q ↔ IsHomeomorph ⇑(p.prodEquivOfIsCompl q h)

Tactic:
by
  rw [(p.prodEquivOfIsCompl q h).isHomeomorph_iff,
    isTopCompl_iff_continuous_symm_prodEquivOfIsCompl, and_iff_right]
  exact continuous_prodEquivOfIsCompl h

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

Goal state before:
pp: E : Type u_2
p : ℝ≥0∞
inst✝³ : NormedAddCommGroup E
X : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasureOnCompacts μ
f : X → E
hf : HasCompactSupport f
h2f : AEStronglyMeasurable f μ
C : ℝ≥0∞
hfC : ∀ᵐ (x : X) ∂μ, ‖f x‖ₑ ≤ C
hC : C ≠ ∞
this : MemLp f ∞ μ
⊢ MemLp f p μ

Tactic:
exact this.mono_exponent_of_measure_support_ne_top
    (fun x ↦ image_eq_zero_of_notMem_tsupport) hf.measure_ne_top le_top

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

Goal state before:
pp: case pos
α : 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
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : p = ∞
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)

Tactic:
rw [hp_top, ENNReal.toReal_top, _root_.div_zero, Real.rpow_zero, mul_one]
    exact norm_indicatorConstLp_top hμs_pos

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : Finite ι
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : TopologicalSpace F
inst✝⁶ : AddCommGroup F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : Module 𝕜 F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : Module 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
⊢ Continuous[instTopologicalSpaceProd, inst✝⁷] fun p ↦ (f p.1) p.2

Tactic:
fun_prop

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

Goal state before:
pp: case left
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ AEStronglyMeasurable f 0

Tactic:
fun_prop

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

Goal state before:
pp: case right
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ HasFiniteIntegral f 0

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝² : TopologicalSpace ε
inst✝¹ : ESeminormedAddMonoid ε
inst✝ : IsFiniteMeasure μ
f : α → ε
⊢ Integrable f ((μ univ)⁻¹ • μ) ↔ Integrable f μ

Tactic:
classical
  exact (eq_or_ne μ 0).by_cases (fun h => by simp [h]) fun h =>
    integrable_smul_measure (ENNReal.inv_ne_zero.2 <| by finiteness)
      (ENNReal.inv_ne_top.2 <| mt Measure.measure_univ_eq_zero.1 h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ HasFiniteIntegral (-f) μ

Tactic:
fun_prop

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

Goal state before:
pp: case left
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ AEStronglyMeasurable (fun x ↦ ‖f x‖ₑ) μ

Tactic:
fun_prop

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

Goal state before:
pp: case right
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : Integrable f μ
⊢ HasFiniteIntegral (fun x ↦ ‖f x‖ₑ) μ

Tactic:
fun_prop

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ AEStronglyMeasurable (fun a ↦ ‖f a‖) μ

Tactic:
fun_prop

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ HasFiniteIntegral (fun a ↦ ‖f a‖) μ

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᵐ[μ] f
h_le₂ : f ≤ᵐ[μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
h_le_add : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ Integrable (fun a ↦ ‖g₁ a‖ + ‖g₂ a‖) μ

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
g : α → γ
hf : Integrable f μ
hg : Integrable g μ
⊢ AEStronglyMeasurable (fun x ↦ (f x, g x)) μ

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
x : α
⊢ ε ≤ ‖f x‖ ↔ ‖ε‖ₑ ≤ ‖f x‖ₑ

Tactic:
enorm_le_iff_norm_le,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
x : α
⊢ ε ≤ ‖f x‖ ↔ ‖ε‖ ≤ ‖f x‖
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x).toNNReal) μ

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
f : ↥(Lp E p μ)
hp : 1 ≤ p
hμs : μ s ≠ ∞
⊢ IntegrableOn (↑↑f) s μ

Tactic:
refine memLp_one_iff_integrable.mp ?_
  have hμ_restrict_univ : (μ.restrict s) Set.univ < ∞ := by
    simpa only [Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply, lt_top_iff_ne_top]
  have hμ_finite : IsFiniteMeasure (μ.restrict s) := ⟨hμ_restrict_univ⟩
  exact ((Lp.memLp _).restrict s).mono_exponent hp

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
s : Set α
hs : s ∈ l ∧ IntegrableOn (f ∘ e) s μ
⊢ ∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ

Tactic:
exact ⟨e '' s, by rwa [mem_map, he.injective.preimage_image]⟩

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

Goal state before:
pp: case e'_4
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SeminormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap 𝕜 (fun x ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i, ‖m i‖
v : Fin k → G
⊢ (∏ i, ‖v i‖) * ‖z‖ ^ (n - k) = ∏ i, ‖if h : i ∈ s then v ((s.orderIsoOfFin hk).symm ⟨i, h⟩) else z‖

Tactic:
simp only [apply_dite norm, Fintype.prod_dite, prod_const ‖z‖, Finset.card_univ,
    Fintype.card_of_subtype sᶜ fun _ => mem_compl, card_compl, Fintype.card_fin, hk, ←
    (s.orderIsoOfFin hk).symm.bijective.prod_comp fun x => ‖v x‖]

Goal state after:
case e'_4
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SeminormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k n : ℕ
f : MultilinearMap 𝕜 (fun x ↦ G) G'
s : Finset (Fin n)
hk : #s = k
z : G
C : ℝ
H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i, ‖m i‖
v : Fin k → G
⊢ (∏ i, ‖v ((s.orderIsoOfFin hk).symm i)‖) * ‖z‖ ^ (n - k) =
    (∏ a, ‖v ((s.orderIsoOfFin hk).symm ⟨↑a, ⋯⟩)‖) * ‖z‖ ^ (n - k)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ Continuous fun x ↦ x * ∏ i, ‖m i‖

Tactic:
fun_prop

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

Goal state before:
pp: case left
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ AEStronglyMeasurable (fun a ↦ max (f a) 0) μ

Tactic:
fun_prop

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

Goal state before:
pp: case right
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ HasFiniteIntegral (fun a ↦ max (f a) 0) μ

Tactic:
fun_prop

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_8
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : Integrable f μ
⊢ AEStronglyMeasurable (c • f) μ

Tactic:
fun_prop

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_8
inst✝² : NormedAddCommGroup 𝕜
inst✝¹ : SMulZeroClass 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α → β
hf : Integrable f μ
⊢ HasFiniteIntegral (c • f) μ

Tactic:
fun_prop

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

Goal state before:
pp: case left
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
ε : Type u_9
inst✝⁵ : TopologicalSpace ε
inst✝⁴ : ESeminormedAddMonoid ε
inst✝³ : NormedAddCommGroup 𝕜
inst✝² : SMul 𝕜 ε
inst✝¹ : ContinuousConstSMul 𝕜 ε
inst✝ : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
hf : Integrable f μ
⊢ AEStronglyMeasurable (c • f) μ

Tactic:
fun_prop

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

Goal state before:
pp: case right
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_8
ε : Type u_9
inst✝⁵ : TopologicalSpace ε
inst✝⁴ : ESeminormedAddMonoid ε
inst✝³ : NormedAddCommGroup 𝕜
inst✝² : SMul 𝕜 ε
inst✝¹ : ContinuousConstSMul 𝕜 ε
inst✝ : ENormSMulClass 𝕜 ε
c : 𝕜
f : α → ε
hf : Integrable f μ
⊢ HasFiniteIntegral (c • f) μ

Tactic:
fun_prop

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
⊢ Measurable fun a ↦ ‖f a‖ₑ

Tactic:
fun_prop

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
H : Type u_9
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup H
𝕜 : Type u_10
𝕜' : Type u_11
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜' E
inst✝¹ : NormedSpace 𝕜 H
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
φ : α → H
L : H →SL[σ] E
φ_int : Integrable φ μ
⊢ AEStronglyMeasurable (fun a ↦ L (φ a)) μ

Tactic:
fun_prop

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

Goal state before:
pp: case pos
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
hab : a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

pp: case neg
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
· rw [← Ico_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]

Goal state after:
case neg
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
hab : ¬a ≤ b
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case succ
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_1
inst✝² : SeminormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : NormOneClass A
n✝ : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (n✝ + 1) A‖ = 1

Tactic:
· refine le_antisymm norm_mkPiAlgebraFin_succ_le ?_
    refine le_of_eq_of_le ?_ <|
      ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 (Nat.succ _) A) fun _ => 1
    simp

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case pos
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst✝ : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x | ∃ c, Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x
x : X
hx : x ∈ conv
⊢ (l.limUnder fun x_1 ↦ f x_1 x) = Function.extend Subtype.val (fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x) (fun x ↦ e) x

Tactic:
rw [Function.extend_val_apply hx]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : ContinuousMul E
L : SummationFilter ι
inst✝² : L.NeBot
inst✝¹ : L.filter.IsCountablyGenerated
inst✝ : PseudoMetrizableSpace E
f : ι → X → E
g : X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
h' : ∀ (x : X), HasProd (fun i ↦ f i x) (g x) L
⊢ ∀ (i : Finset ι), StronglyMeasurable fun x ↦ ∏ b ∈ i, (fun i ↦ f i x) b

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: X : Type u_4
E✝ : Type u_5
ι : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : CommMonoid E✝
inst✝⁵ : TopologicalSpace E✝
inst✝⁴ : ContinuousMul E✝
L : SummationFilter ι
inst✝³ : L.NeBot
inst✝² : L.filter.IsCountablyGenerated
inst✝¹ : IsCompletelyPseudoMetrizableSpace E✝
inst✝ : Countable ι
f : ι → X → E✝
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x | Multipliable (fun x_1 ↦ f x_1 x) L}
⊢ ∀ (i : Finset ι), StronglyMeasurable fun x ↦ ∏ b ∈ i, (fun x_1 ↦ f x_1 x) b

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: X : Type u_4
E✝ : Type u_5
ι : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : CommMonoid E✝
inst✝⁵ : TopologicalSpace E✝
inst✝⁴ : ContinuousMul E✝
L : SummationFilter ι
inst✝³ : L.NeBot
inst✝² : L.filter.IsCountablyGenerated
inst✝¹ : IsCompletelyPseudoMetrizableSpace E✝
inst✝ : Countable ι
f : ι → X → E✝
h : ∀ (i : ι), StronglyMeasurable (f i)
E : Set X := {x | Multipliable (fun x_1 ↦ f x_1 x) L}
hE : MeasurableSet E
h0 : (Eᶜ.domRestrict fun x ↦ ∏'[L] (i : ι), f i x) = fun x ↦ 1
⊢ ∀ (i : Finset ι), StronglyMeasurable fun e ↦ ∏ b ∈ i, (fun x ↦ f x ↑e) b

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∈ L.support
⊢ StronglyMeasurable (f x✝¹.down)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝¹ : ¬(L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite)
h✝ : ¬HasProd (fun i ↦ f i) 1 L
⊢ ∀ (i : Finset ι), StronglyMeasurable (∏ b ∈ i, (fun i ↦ f i) b)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case pos
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∈ L.support
⊢ AEStronglyMeasurable (f x✝¹.down) μ

Tactic:
fun_prop

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case neg
X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁶ : MeasurableSpace X
inst✝⁵ : CommMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : PseudoMetrizableSpace E
inst✝² : ContinuousMul E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∉ L.support
⊢ AEStronglyMeasurable 1 μ

Tactic:
fun_prop

Goal state after: