mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s : Finset ι
hf : ∀ i ∈ ∅, MemLp (f i) (p i) μ
hμ : ¬μ = 0
⊢ MemLp (∏ i ∈ ∅, f i) (∑ i ∈ ∅, (p i)⁻¹)⁻¹ μ

Tactic:
simp [MemLp, eLpNormEssSup_const, hμ, aestronglyMeasurable_const, Pi.one_def]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h : ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (fun i ↦ μ {x | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
intro ε hε
  by_cases hε_top : ε = ∞
  · have h1 : Tendsto (fun n ↦ μ {ω | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0) := h 1 (by simp) (by simp)
    refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h1 (fun _ ↦ zero_le) ?_
    intro n
    simp only [hε_top]
    gcongr
    simp
  · exact h ε hε hε_top

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
ι : Type u_6
s : Finset ι
f : ι → ↥(Lp E p μ)
⊢ ↑↑(∑ i ∈ s, f i) =ᵐ[μ] fun x ↦ ∑ i ∈ s, ↑↑(f i) x

Tactic:
by
  grw [coeFn_finsetSum]
  filter_upwards with x using by simp

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, ↑(w x * f x).toNNReal ≤ ↑((∑ i ∈ s, (w i).toNNReal) ^ (1 - p⁻¹)) * (∑ x ∈ s, ↑(w x * f x ^ p).toNNReal) ^ p⁻¹
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
sum_congr rfl fun i hi ↦ coe_toNNReal (H'.2 i hi)

Goal state after:
case neg
ι : Type u
s : Finset ι
p : ℝ
hp✝ : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) ≠ 0 ∧ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this : ∑ x ∈ s, ↑(w x * f x).toNNReal ≤ ↑((∑ i ∈ s, (w i).toNNReal) ^ (1 - p⁻¹)) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
Module: Mathlib.MeasureTheory.Function.LpOrder

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup E
inst✝ : PartialOrder E
f g : ↥(Lp E p μ)
⊢ ↑↑f ≤ᵐ[μ] ↑↑g ↔ f ≤ g

Tactic:
by
  rw [← Subtype.coe_le_coe, ← AEEqFun.coeFn_le]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : NormedAlgebra 𝕜 R
inst✝³ : Module R E
inst✝² : NormSMulClass R E
inst✝¹ : IsScalarTower 𝕜 R E
inst✝ : Nontrivial E
a : R
⊢ ‖(lsmul 𝕜 R) a‖ = ‖a‖

Tactic:
refine ContinuousLinearMap.opNorm_eq_of_bounds (norm_nonneg _) (fun x => ?_) fun N _ h => ?_
  · simp [norm_smul]
  obtain ⟨y, hy⟩ := exists_ne (0 : E)
  refine le_of_mul_le_mul_right ?_ (norm_pos_iff.mpr hy)
  simpa [norm_smul] using h y

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
⊢ ∃ K, AntilipschitzWith K ⇑f

Tactic:
rcases ((nhds_basis_ball.comap _).le_basis_iff nhds_basis_ball).1 hf 1 one_pos with ⟨ε, ε0, hε⟩

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ
ε0 : 0 < ε
hε : ⇑f ⁻¹' ball 0 ε ⊆ ball 0 1
⊢ ∃ K, AntilipschitzWith K ⇑f
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕜₂
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomIsometric σ₂₁
inst✝ : RingHomIsometric σ₁₂
e : E ≃SL[σ₁₂] F
_i : Nontrivial E
⊢ Subsingleton E ∨ 0 < ‖↑e.symm‖

Tactic:
· right
    exact e.norm_symm_pos

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁸ : NormedField 𝕜
inst✝⁷ : (i : ι) → TopologicalSpace (E i)
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
⊢ IsVonNBounded 𝕜 (image2 (fun f x ↦ f x) S s)

Tactic:
by
  intro U hU
  filter_upwards [hS (eventually_nhds_zero_mapsTo hs hU)] with c hc
  rw [image2_subset_iff]
  intro f hf x hx
  rcases hc hf with ⟨g, hg, rfl⟩
  exact smul_mem_smul_set (hg hx)

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
g_emb : IsEmbedding g
Φ : Quotient (ker (g ∘ f)) ≃ₜ Quotient (ker f) := Homeomorph.Quotient.congrRight ⋯
key : g ∘ kerLift f ∘ ⇑Φ = kerLift (g ∘ f)
H : IsEmbedding (g ∘ kerLift f ∘ ⇑Φ)
⊢ IsEmbedding (g ∘ kerLift f)

Tactic:
simpa [comp_assoc] using H.comp Φ.symm.isEmbedding

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
s : Set α
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : μ s ≠ ∞
x : E
h_compLp :
  ↑↑((ContinuousLinearMap.toSpanSingleton ℝ x).compLp (indicatorConstLp 2 hs hμs 1)) =ᵐ[μ] fun a ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = s.indicator (fun x ↦ 1) y
⊢ s.indicator (fun x_1 ↦ x) y = s.indicator (fun x ↦ 1) y • x

Tactic:
by_cases hy_mem : y ∈ s <;> simp [hy_mem]

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

Goal state before:
pp: case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : finrank 𝕜 ↥l.range = 0
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑l

Tactic:
rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H

Goal state after:
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
hl : IsClosed[inst✝²] ↑l.ker
H : l = 0
⊢ Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑l
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case inr
𝕜 : 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 : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m - 0‖ < ε → ‖f m - f 0‖ < 1
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖

Tactic:
simp only [sub_zero, f.map_zero] at hε

Goal state after:
case inr
𝕜 : 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 : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
⊢ ∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
⊢ μ.restrict (toMeasurable μ s) = μ.restrict s

Tactic:
rcases exists_seq_strictAnti_tendsto' ENNReal.zero_lt_top with ⟨u, _, u_pos, u_lim⟩
  let v n := toMeasurable (μ.restrict s) { x | u n ≤ ‖f x‖ₑ }
  have A : ∀ n, μ (s ∩ v n) ≠ ∞ := by
    intro n
    rw [inter_comm, ← Measure.restrict_apply (measurableSet_toMeasurable _ _),
      measure_toMeasurable]
    exact (hf.measure_enorm_ge_lt_top (u_pos n).1 (u_pos n).2.ne).ne
  apply Measure.restrict_toMeasurable_of_cover _ A
  intro x hx
  obtain ⟨n, hn⟩ : ∃ n, u n < ‖f x‖ₑ :=
    ((tendsto_order.1 u_lim).2 _ (pos_of_ne_zero (h's x hx))).exists
  exact mem_iUnion.2 ⟨n, subset_toMeasurable _ _ hn.le⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSingletonClass α
f : α → β
⊢ Integrable f Measure.count ↔ Summable fun x ↦ ‖f x‖

Tactic:
rw [Integrable, hasFiniteIntegral_count_iff, and_iff_right_iff_imp]
  intro hs
  have hs' : (Function.support f).Countable := by
    simpa only [Ne, Pi.zero_apply, eq_comm, Function.support, norm_eq_zero]
      using hs.countable_support
  let : MeasurableSpace β := borel β
  have : BorelSpace β := ⟨rfl⟩
  refine aestronglyMeasurable_iff_aemeasurable_separable.mpr ⟨?_, ?_⟩
  · refine (measurable_zero.measurable_of_countable_ne ?_).aemeasurable
    simpa only [Ne, Pi.zero_apply, eq_comm, Function.support] using hs'
  · refine ⟨f '' univ, ?_, ae_of_all _ fun a ↦ ⟨a, ⟨mem_univ _, rfl⟩⟩⟩
    suffices f '' univ ⊆ (f '' f.support) ∪ {0} from
      (((hs'.image f).union (countable_singleton 0)).mono this).isSeparable
    grind [Function.mem_support]

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 : AEMeasurable f μ
g : α → E
⊢ (fun x ↦ ↑(f x)) =ᵐ[μ] fun x ↦ ↑(AEMeasurable.mk f hf x)

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(f x) = ↑(AEMeasurable.mk f hf x)
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 : AEMeasurable f μ
g : α → E
⊢ (fun x ↦ ↑(AEMeasurable.mk f hf x) • g x) =ᵐ[μ] fun x ↦ ↑(f x) • g x

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(AEMeasurable.mk f hf x) • g x = ↑(f x) • g x
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝² : Fintype ι
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed[inst✝⁴] ↑s
f : E →ₗ[𝕜] 𝕜
H : finrank 𝕜 ↥f.range = 0
⊢ Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f

Tactic:
rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H

Goal state after:
case pos
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace 𝕜
n : ℕ
IH :
  ∀ {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E] [inst_2 : TopologicalSpace E]
    [inst_3 : IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {ι : Type v} [inst_6 : Finite ι]
    (ξ : Basis ι 𝕜 E) (this : Fintype ι),
    let this_1 := IsTopologicalAddGroup.rightUniformSpace E;
    let this_2 := ⋯;
    Fintype.card ι = n → Continuous[_, Pi.topologicalSpace] ⇑ξ.equivFun
E : Type v
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝² : Fintype ι
this✝¹ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this✝ : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
hn : Fintype.card ι = n + 1
this : FiniteDimensional 𝕜 E
H₁ : ∀ (s : Submodule 𝕜 E), finrank 𝕜 ↥s = n → IsClosed[inst✝⁴] ↑s
f : E →ₗ[𝕜] 𝕜
H : f = 0
⊢ Continuous[inst✝⁴, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
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: 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)
⊢ StronglyMeasurable (∏'[L] (i : ι), f i)

Tactic:
rw [tprod_def, finprod_def']

Goal state after:
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)
⊢ StronglyMeasurable
    (if h : Multipliable (fun i ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite then
        if h : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down) then
          ∏ i ∈ Finite.toFinset h, L.support.mulIndicator (fun i ↦ f i) i.down
        else 1
      else if HasProd (fun i ↦ f i) 1 L then 1 else Exists.choose h
    else 1)
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
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ AEStronglyMeasurable (∏'[L] (i : ι), f i) μ

Tactic:
rw [tprod_def, finprod_def']

Goal state after:
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) μ
⊢ AEStronglyMeasurable
    (if h : Multipliable (fun i ↦ f i) L then
      if L.HasSupport ∧ ((Function.mulSupport fun i ↦ f i) ∩ L.support).Finite then
        if h : Function.HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down) then
          ∏ i ∈ Finite.toFinset h, L.support.mulIndicator (fun i ↦ f i) i.down
        else 1
      else if HasProd (fun i ↦ f i) 1 L then 1 else Exists.choose h
    else 1)
    μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst✝⁸ : Fintype ι'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
inst✝¹ : (i : ι') → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι') → NormedSpace 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
⊢ ‖f.mkContinuousMultilinear C H‖ ≤ max C 0

Tactic:
dsimp only [mkContinuousMultilinear]

Goal state after:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E' : ι' → Type wE'
G : Type wG
inst✝⁸ : Fintype ι'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : Fintype ι
inst✝¹ : (i : ι') → SeminormedAddCommGroup (E' i)
inst✝ : (i : ι') → NormedSpace 𝕜 (E' i)
f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)
C : ℝ
H : ∀ (m₁ : (i : ι) → E i) (m₂ : (i : ι') → E' i), ‖(f m₁) m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖
⊢ ‖{ toFun := fun m ↦ (f m).mkContinuous (C * ∏ i, ‖m i‖) ⋯, map_update_add' := ⋯, map_update_smul' := ⋯ }.mkContinuous
        (max C 0) ⋯‖ ≤
    max C 0
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hf : LocallyIntegrable f (μ.restrict s)
⊢ LocallyIntegrableOn f s μ

Tactic:
by
  intro x _
  obtain ⟨t, ht_mem, ht_int⟩ := hf x
  obtain ⟨u, hu_sub, hu_o, hu_mem⟩ := mem_nhds_iff.mp ht_mem
  refine ⟨_, inter_mem_nhdsWithin s (hu_o.mem_nhds hu_mem), ?_⟩
  simpa only [IntegrableOn, Measure.restrict_restrict hu_o.measurableSet, inter_comm] using
    ht_int.mono_set hu_sub

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 = (g.compContinuousLinearMap fun i ↦ ↑↑(f i)).compContinuousLinearMap fun i ↦ ↑↑(f i).symm

Tactic:
ext1 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 m = ((g.compContinuousLinearMap fun i ↦ ↑↑(f i)).compContinuousLinearMap fun i ↦ ↑↑(f i).symm) m
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
⊢ ‖(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊

Tactic:
by
  have := edist_approxOn_le hf h₀ x n
  rw [edist_comm y₀] at this
  simp only [edist_nndist, nndist_eq_nnnorm] at this
  exact mod_cast this

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

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → E
hf : LocallyIntegrable f μ
g : X → 𝕜
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
x : X
hx : x ∉ K
⊢ g x • f x = 0

Tactic:
simp [image_eq_zero_of_notMem_tsupport hx]

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

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : NormedAddCommGroup E
μ : Measure X
𝕜 : Type u_9
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → 𝕜
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous[inst✝⁶, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
x : X
hx : x ∉ K
⊢ f x • g x = 0

Tactic:
simp [image_eq_zero_of_notMem_tsupport hx]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ ‖(T + T') s‖ ≤ max C C' * (μ + ν).real s

Tactic:
rw [Pi.add_apply, measureReal_add_apply hμs.ne hνs.ne, mul_add]

Goal state after:
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst✝ : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ ‖T s + T' s‖ ≤ max C C' * μ.real s + max C C' * ν.real s
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: 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, ⋯⟩

Tactic:
exact (compLeftInverse_apply_of_bdd _ _ h_norm _ _ rfl).symm

Goal state after: